--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/CTL.thy Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,31 @@
+(* Title: HOL/Modelcheck/CTL.thy
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+CTL = MuCalculus +
+
+
+types
+ 'a trans = "('a * 'a) set"
+
+
+consts
+
+ CEX ::"['a trans,'a pred, 'a]=>bool"
+ EG ::"['a trans,'a pred]=> 'a pred"
+
+
+
+defs
+
+CEX_def "CEX N f u == (? v. (f v & (u,v):N))"
+EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
+
+
+
+
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/Example.ML Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,23 @@
+(* Title: HOL/Modelcheck/Example.ML
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+val reach_rws = [reach_def,INIT_def,N_def];
+
+
+goal thy "reach (True,True,True)";
+by (simp_tac (MC_ss addsimps reach_rws) 1);
+
+(*show the current proof state using the model checker syntax*)
+setmp print_mode ["Eindhoven"] pr ();
+
+(*actually invoke the model checker*)
+by (mc_tac 1);
+
+qed "reach_ex_thm1";
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/Example.thy Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,33 @@
+(* Title: HOL/Modelcheck/Example.thy
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+Example = MCSyn +
+
+
+types
+ state = "bool * bool * bool"
+
+consts
+
+ INIT :: "state pred"
+ N :: "[state,state] => bool"
+ reach:: "state pred"
+
+defs
+
+ INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+
+ N_def "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
+ y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
+ in (~x1&~x2&~x3 & y1&~y2&~y3) |
+ (x1&~x2&~x3 & ~y1&~y2&~y3) |
+ (x1&~x2&~x3 & y1&y2&y3) "
+
+ reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
+
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MCSyn.ML Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,46 @@
+(* Title: HOL/Modelcheck/MCSyn.ML
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+fun mc_tac i state =
+let val sign = #sign (rep_thm state)
+in
+case drop(i-1,prems_of state) of
+ [] => Sequence.null |
+ subgoal::_ =>
+ let val concl = Logic.strip_imp_concl subgoal;
+ val OraAss = invoke_oracle(MCSyn.thy,sign,MCOracleExn concl);
+ in
+ ((cut_facts_tac [OraAss] i) THEN (atac i)) state
+ end
+end;
+
+
+goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
+auto();
+by (split_all_tac 1);
+auto();
+qed "split_paired_Ex";
+
+
+goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+ br ext 1;
+ by (stac (surjective_pairing RS sym) 1);
+ br refl 1;
+qed "pair_eta_expand";
+
+local
+ val lhss = [cterm_of (sign_of thy) (read "f::'a*'b=>'c")];
+ val rew = mk_meta_eq pair_eta_expand;
+
+ fun proc _ (Abs _) = Some rew
+ | proc _ _ = None;
+in
+ val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
+end;
+
+
+val MC_ss = (!simpset addsimprocs [pair_eta_expand_proc])
+ addsimps [split_paired_Ex,Let_def];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MCSyn.thy Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,33 @@
+(* Title: HOL/Modelcheck/MCSyn.thy
+ ID: $Id$
+ Author: Olaf M"uller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+MCSyn = MuCalculus +
+
+syntax (Eindhoven output)
+
+ True :: bool ("TRUE")
+ False :: bool ("FALSE")
+
+ Not :: bool => bool ("NOT _" [40] 40)
+ "op &" :: [bool, bool] => bool (infixr "AND" 35)
+ "op |" :: [bool, bool] => bool (infixr "OR" 30)
+
+ "! " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
+ "? " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
+ "ALL " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
+ "EX " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
+ "_lambda" :: [idts, 'a::logic] => 'b::logic ("(3L _./ _)" 10)
+
+ "_idts" :: [pttrn, idts] => idts ("_,/_" [1, 0] 0)
+ "_pttrn" :: [pttrn, pttrns] => pttrn ("_,/_" [1, 0] 0)
+
+ "Mu " :: [idts, 'a pred] => 'a pred ("(3[mu _./ _])" 1000)
+ "Nu " :: [idts, 'a pred] => 'a pred ("(3[nu _./ _])" 1000)
+
+oracle
+ mk_mc_oracle
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuCalculus.ML Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,35 @@
+(* Title: HOL/Modelcheck/MuCalculus.ML
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+exception MCOracleExn of term;
+exception MCFailureExn of string;
+
+
+val trace_mc = ref false;
+
+
+fun termtext sign term =
+ setmp print_mode ["Eindhoven"]
+ (Sign.string_of_term sign) term;
+
+fun call_mc s =
+ execute ( "echo \"" ^ s ^ "\" | pmu -w" );
+
+
+fun mk_mc_oracle (sign, MCOracleExn trm) =
+ let
+ val tmtext = termtext sign trm;
+ val debug = writeln ("MC debugger: " ^ tmtext);
+ val result = call_mc tmtext;
+ in
+ if ! trace_mc then
+ (writeln tmtext; writeln("----"); writeln result)
+ else ();
+ (case result of
+ "TRUE\n" => trm |
+ "FALSE\n" => (error "MC oracle yields FALSE") |
+ _ => (error ("MC syntax error: " ^ result)))
+ end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuCalculus.thy Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,28 @@
+(* Title: HOL/Modelcheck/MuCalculus.thy
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+MuCalculus = HOL + Inductive +
+
+types
+ 'a pred = "'a=>bool"
+
+consts
+
+ Charfun :: "'a set => 'a pred"
+ mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
+ nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
+ monoP :: "('a pred => 'a pred) => bool"
+
+defs
+
+Charfun_def "Charfun == (% A.% x.x:A)"
+monoP_def "monoP f == mono(Collect o f o Charfun)"
+mu_def "mu f == Charfun(lfp(Collect o f o Charfun))"
+nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/README.html Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,28 @@
+<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>
+
+<H3>Invoking Model Checkers in Isabelle/HOL </H3>
+
+Authors: Olaf Mueller, Jan Philipps, Robert Sandner<BR>
+Copyright 1997 Technische Universität München<P>
+
+
+This directory contains four theories:
+
+<UL>
+ <li>MuCalculus: A formalization of the relational mu calculus using the fixed point
+ theory Lfp and Gfp of HOL.<P>
+ <li>CTL: A formulation of some CTL operators in the mu calculus.<P>
+ <li>MCSyn: The definition of the output syntax "Eindhoven" tailored for the the model checker due to G. Janssen from Eindhoven using
+ the print_mode facilities provided by Isabelle. <P>
+ <li>Example: A simple reachability property is formulated in the mu calculus and checked
+ by the model checker simply by invoking the tactic mc_tac.
+</UL>
+
+Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">Eindhoven Model Checker</A>). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x.
+
+
+
+</BODY></HTML>
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/ROOT.ML Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,10 @@
+(* Title: HOL/Modelcheck/ROOT.ML
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+
+This is the ROOT file for the Eindhoven Modelchecker example
+*)
+
+
+use_thy"Example";