src/HOL/Modelcheck/ROOT.ML
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 28263 69eaa97e7e96
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
mueller@3210
     1
(*  Title:      HOL/Modelcheck/ROOT.ML
mueller@3210
     2
    ID:         $Id$
wenzelm@7295
     3
    Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
mueller@3210
     4
wenzelm@7295
     5
Basic Modelchecker examples.
mueller@3210
     6
*)
mueller@3210
     7
wenzelm@17272
     8
time_use_thy "CTL";
wenzelm@17272
     9
wenzelm@17272
    10
wenzelm@17272
    11
(* Einhoven model checker *)
wenzelm@17272
    12
wenzelm@28263
    13
(*check if user has pmu installed*)
wenzelm@28263
    14
fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
wenzelm@28263
    15
fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
wenzelm@28263
    16
wenzelm@17272
    17
time_use_thy "EindhovenSyn";
wenzelm@17272
    18
if_eindhoven_enabled time_use_thy "EindhovenExample";
wenzelm@17272
    19
wenzelm@7295
    20
wenzelm@7295
    21
(* Mucke -- mu-calculus model checker from Karlsruhe *)
wenzelm@7295
    22
wenzelm@9000
    23
time_use_thy "MuckeSyn";
mueller@3210
    24
wenzelm@28263
    25
(*check if user has mucke installed*)
wenzelm@28263
    26
fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
wenzelm@28263
    27
fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
wenzelm@28263
    28
wenzelm@9000
    29
if_mucke_enabled time_use_thy "MuckeExample1";
wenzelm@9000
    30
if_mucke_enabled time_use_thy "MuckeExample2";