src/HOL/Modelcheck/ROOT.ML
author wenzelm
Thu, 30 Nov 2000 20:04:16 +0100
changeset 10548 e8c774c12105
parent 9000 c20d58286a51
child 17272 c63e5220ed77
permissions -rw-r--r--
'consumes' att;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/Modelcheck/ROOT.ML
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     2
    ID:         $Id$
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
     3
    Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     4
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
     5
Basic Modelchecker examples.
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     6
*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     7
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
     8
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
     9
(* Mucke -- mu-calculus model checker from Karlsruhe *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    10
9000
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    11
time_use "mucke_oracle.ML";
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    12
time_use_thy "MuckeSyn";
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    13
9000
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    14
if_mucke_enabled time_use_thy "MuckeExample1";
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    15
if_mucke_enabled time_use_thy "MuckeExample2";
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    16
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    17
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    18
(* Einhoven model checker *)
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    19
9000
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    20
time_use_thy "CTL";
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    21
time_use_thy "EindhovenSyn";
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 6465
diff changeset
    22
9000
c20d58286a51 cleaned up;
wenzelm
parents: 7295
diff changeset
    23
if_eindhoven_enabled time_use_thy "EindhovenExample";