author | wenzelm |
Thu, 19 Aug 1999 21:49:10 +0200 | |
changeset 7299 | 743b22579a2f |
parent 6488 | 271969bb7f95 |
child 9000 | c20d58286a51 |
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$ |
7299 | 3 |
Author: Olaf Mueller 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"; |
11 |
use_thy "../../../HOL/Modelcheck/MuckeSyn"; |
|
12 |
use_thy "MuIOAOracle"; |
|
7299 | 13 |
|
14 |
(*examples*) |
|
15 |
if_mucke_enabled use_thy "Cockpit"; |
|
16 |
if_mucke_enabled use_thy "Ring3"; |