| author | haftmann |
| Wed, 18 Jan 2006 11:55:50 +0100 | |
| changeset 18704 | 2c86ced392a8 |
| parent 14981 | e73f8140af78 |
| child 19360 | f47412f922ab |
| permissions | -rw-r--r-- |
| 6488 | 1 |
(* Title: HOLCF/IOA/Modelcheck/ROOT.ML |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
| 12218 | 3 |
Author: Olaf Müller and Tobias Hamberger, TU Muenchen |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
4 |
|
| 7299 | 5 |
Modelchecker setup for I/O automata. |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
6 |
*) |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
7 |
|
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
8 |
goals_limit := 1; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
9 |
|
| 6488 | 10 |
use "../../../HOL/Modelcheck/mucke_oracle.ML"; |
| 9000 | 11 |
with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle"; |
| 7299 | 12 |
|
13 |
(*examples*) |
|
| 9000 | 14 |
if_mucke_enabled time_use_thy "Cockpit"; |
15 |
if_mucke_enabled time_use_thy "Ring3"; |