# HG changeset patch
# User mueller
# Date 863789381 -7200
# Node ID e80db1660614296f70921f2737e1a9b2bf03f208
# Parent ccb55f3121d14522fe498b2ccdb75d988b8306ec
Invoking Model Checkers in Isabelle/HOL;
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/CTL.thy
--- /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
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/Example.ML
--- /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";
+
+
+
+
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/Example.thy
--- /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
+
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/MCSyn.ML
--- /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];
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/MCSyn.thy
--- /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
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/MuCalculus.ML
--- /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;
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/MuCalculus.thy
--- /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
+
+
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/README.html
--- /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 @@
+HOL/Modelcheck/Readme
+
+Invoking Model Checkers in Isabelle/HOL
+
+Authors: Olaf Mueller, Jan Philipps, Robert Sandner
+Copyright 1997 Technische Universität München
+
+
+This directory contains four theories:
+
+
+ - MuCalculus: A formalization of the relational mu calculus using the fixed point
+ theory Lfp and Gfp of HOL.
+
- CTL: A formulation of some CTL operators in the mu calculus.
+
- 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.
+
- Example: A simple reachability property is formulated in the mu calculus and checked
+ by the model checker simply by invoking the tactic mc_tac.
+
+
+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 (Eindhoven Model Checker). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x.
+
+
+
+
+
+
+
diff -r ccb55f3121d1 -r e80db1660614 src/HOL/Modelcheck/ROOT.ML
--- /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";