equal
deleted
inserted
replaced
1 (* Title: HOL/Modelcheck/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen |
|
4 |
|
5 Basic Modelchecker examples. |
|
6 *) |
|
7 |
|
8 time_use_thy "CTL"; |
|
9 |
|
10 |
|
11 (* Einhoven model checker *) |
|
12 |
|
13 (*check if user has pmu installed*) |
|
14 fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> ""; |
|
15 fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else (); |
|
16 |
|
17 time_use_thy "EindhovenSyn"; |
|
18 if_eindhoven_enabled time_use_thy "EindhovenExample"; |
|
19 |
|
20 |
|
21 (* Mucke -- mu-calculus model checker from Karlsruhe *) |
|
22 |
|
23 time_use_thy "MuckeSyn"; |
|
24 |
|
25 (*check if user has mucke installed*) |
|
26 fun mucke_enabled () = getenv "MUCKE_HOME" <> ""; |
|
27 fun if_mucke_enabled f x = if mucke_enabled () then f x else (); |
|
28 |
|
29 if_mucke_enabled time_use_thy "MuckeExample1"; |
|
30 if_mucke_enabled time_use_thy "MuckeExample2"; |
|