Invoking Model Checkers in Isabelle/HOL;
authormueller
Fri May 16 15:29:41 1997 +0200 (1997-05-16)
changeset 3210e80db1660614
parent 3209 ccb55f3121d1
child 3211 57a9b613036e
Invoking Model Checkers in Isabelle/HOL;
src/HOL/Modelcheck/CTL.thy
src/HOL/Modelcheck/Example.ML
src/HOL/Modelcheck/Example.thy
src/HOL/Modelcheck/MCSyn.ML
src/HOL/Modelcheck/MCSyn.thy
src/HOL/Modelcheck/MuCalculus.ML
src/HOL/Modelcheck/MuCalculus.thy
src/HOL/Modelcheck/README.html
src/HOL/Modelcheck/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Modelcheck/CTL.thy	Fri May 16 15:29:41 1997 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +(*  Title:      HOL/Modelcheck/CTL.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +CTL = MuCalculus + 
    1.11 +
    1.12 +
    1.13 +types
    1.14 +  'a trans  = "('a * 'a) set"
    1.15 +
    1.16 +
    1.17 +consts
    1.18 +
    1.19 +  CEX   ::"['a trans,'a pred, 'a]=>bool" 
    1.20 +  EG    ::"['a trans,'a pred]=> 'a pred" 
    1.21 +
    1.22 +
    1.23 +
    1.24 +defs
    1.25 + 
    1.26 +CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
    1.27 +EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
    1.28 +
    1.29 +
    1.30 +
    1.31 +
    1.32 +
    1.33 +
    1.34 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Modelcheck/Example.ML	Fri May 16 15:29:41 1997 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title:      HOL/Modelcheck/Example.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     2.7 +    Copyright   1997  TU Muenchen
     2.8 +*)
     2.9 +
    2.10 +val reach_rws = [reach_def,INIT_def,N_def];
    2.11 +
    2.12 +
    2.13 +goal thy "reach (True,True,True)";
    2.14 +by (simp_tac (MC_ss addsimps reach_rws) 1);
    2.15 +
    2.16 +(*show the current proof state using the model checker syntax*)
    2.17 +setmp print_mode ["Eindhoven"] pr ();
    2.18 +
    2.19 +(*actually invoke the model checker*)
    2.20 +by (mc_tac 1);
    2.21 +
    2.22 +qed "reach_ex_thm1";
    2.23 +
    2.24 +
    2.25 +
    2.26 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Modelcheck/Example.thy	Fri May 16 15:29:41 1997 +0200
     3.3 @@ -0,0 +1,33 @@
     3.4 +(*  Title:      HOL/Modelcheck/Example.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     3.7 +    Copyright   1997  TU Muenchen
     3.8 +*)
     3.9 +
    3.10 +Example = MCSyn + 
    3.11 +
    3.12 +
    3.13 +types
    3.14 +    state = "bool * bool * bool"
    3.15 +
    3.16 +consts
    3.17 +
    3.18 +  INIT :: "state pred"
    3.19 +  N    :: "[state,state] => bool"
    3.20 +  reach:: "state pred"
    3.21 +
    3.22 +defs
    3.23 +  
    3.24 +  INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
    3.25 +
    3.26 +  N_def   "N x y  == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));   
    3.27 +	                  y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y)) 
    3.28 +                     in (~x1&~x2&~x3 & y1&~y2&~y3) |   
    3.29 +	                (x1&~x2&~x3 & ~y1&~y2&~y3) |   
    3.30 +	                (x1&~x2&~x3 & y1&y2&y3)    "
    3.31 +  
    3.32 +  reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
    3.33 +  
    3.34 +
    3.35 +end
    3.36 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Modelcheck/MCSyn.ML	Fri May 16 15:29:41 1997 +0200
     4.3 @@ -0,0 +1,46 @@
     4.4 +(*  Title:      HOL/Modelcheck/MCSyn.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4.7 +    Copyright   1997  TU Muenchen
     4.8 +*)
     4.9 +
    4.10 +fun mc_tac i state = 
    4.11 +let val sign = #sign (rep_thm state)
    4.12 +in 
    4.13 +case drop(i-1,prems_of state) of
    4.14 +   [] => Sequence.null |
    4.15 +   subgoal::_ => 
    4.16 +	let val concl = Logic.strip_imp_concl subgoal;
    4.17 +	    val OraAss = invoke_oracle(MCSyn.thy,sign,MCOracleExn concl);
    4.18 +	in
    4.19 +	((cut_facts_tac [OraAss] i) THEN (atac i)) state
    4.20 +        end
    4.21 +end;
    4.22 +
    4.23 +
    4.24 +goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
    4.25 +auto();
    4.26 +by (split_all_tac 1);
    4.27 +auto();
    4.28 +qed "split_paired_Ex";
    4.29 +
    4.30 +
    4.31 +goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    4.32 +  br ext 1;
    4.33 +  by (stac (surjective_pairing RS sym) 1);
    4.34 +  br refl 1;
    4.35 +qed "pair_eta_expand";
    4.36 +
    4.37 +local
    4.38 +  val lhss = [cterm_of (sign_of thy) (read "f::'a*'b=>'c")];
    4.39 +  val rew = mk_meta_eq pair_eta_expand;
    4.40 +
    4.41 +  fun proc _ (Abs _) = Some rew
    4.42 +    | proc _ _ = None;
    4.43 +in
    4.44 +  val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
    4.45 +end;
    4.46 +
    4.47 +
    4.48 +val MC_ss = (!simpset addsimprocs [pair_eta_expand_proc]) 
    4.49 +                      addsimps [split_paired_Ex,Let_def];
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Modelcheck/MCSyn.thy	Fri May 16 15:29:41 1997 +0200
     5.3 @@ -0,0 +1,33 @@
     5.4 +(*  Title:      HOL/Modelcheck/MCSyn.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Olaf M"uller, Jan Philipps, Robert Sandner
     5.7 +    Copyright   1997  TU Muenchen
     5.8 +*)
     5.9 +
    5.10 +MCSyn = MuCalculus + 
    5.11 +
    5.12 +syntax (Eindhoven output)
    5.13 +
    5.14 +  True		:: bool					("TRUE")
    5.15 +  False		:: bool					("FALSE")
    5.16 +
    5.17 +  Not		:: bool => bool				("NOT _" [40] 40)
    5.18 +  "op &"	:: [bool, bool] => bool			(infixr "AND" 35)
    5.19 +  "op |"	:: [bool, bool] => bool			(infixr "OR" 30)
    5.20 +
    5.21 +  "! " 		:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
    5.22 +  "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
    5.23 +  "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
    5.24 +  "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
    5.25 +   "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
    5.26 +
    5.27 +  "_idts"     	:: [pttrn, idts] => idts		("_,/_" [1, 0] 0)
    5.28 +  "_pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/_" [1, 0] 0)
    5.29 +
    5.30 +  "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
    5.31 +  "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
    5.32 +
    5.33 +oracle
    5.34 +  mk_mc_oracle
    5.35 +
    5.36 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Modelcheck/MuCalculus.ML	Fri May 16 15:29:41 1997 +0200
     6.3 @@ -0,0 +1,35 @@
     6.4 +(*  Title:      HOL/Modelcheck/MuCalculus.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     6.7 +    Copyright   1997  TU Muenchen
     6.8 +*)
     6.9 +
    6.10 +exception MCOracleExn of term;
    6.11 +exception MCFailureExn of string;
    6.12 +
    6.13 +
    6.14 +val trace_mc = ref false;
    6.15 +
    6.16 +
    6.17 +fun termtext sign term =
    6.18 +  setmp print_mode ["Eindhoven"]
    6.19 +    (Sign.string_of_term sign) term;
    6.20 +
    6.21 +fun call_mc s =
    6.22 +  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
    6.23 +
    6.24 +
    6.25 +fun mk_mc_oracle (sign, MCOracleExn trm) =
    6.26 +  let
    6.27 +    val tmtext = termtext sign trm;
    6.28 +    val debug = writeln ("MC debugger: " ^ tmtext);
    6.29 +    val result = call_mc tmtext;
    6.30 +  in
    6.31 +    if ! trace_mc then
    6.32 +      (writeln tmtext; writeln("----"); writeln result)
    6.33 +    else ();
    6.34 +    (case result of
    6.35 +      "TRUE\n"  =>  trm |
    6.36 +      "FALSE\n" => (error "MC oracle yields FALSE") |
    6.37 +    _ => (error ("MC syntax error: " ^ result)))
    6.38 +  end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Modelcheck/MuCalculus.thy	Fri May 16 15:29:41 1997 +0200
     7.3 @@ -0,0 +1,28 @@
     7.4 +(*  Title:      HOL/Modelcheck/MuCalculus.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     7.7 +    Copyright   1997  TU Muenchen
     7.8 +*)
     7.9 +
    7.10 +MuCalculus = HOL + Inductive +
    7.11 +
    7.12 +types
    7.13 + 'a pred = "'a=>bool" 
    7.14 +
    7.15 +consts
    7.16 +
    7.17 +  Charfun :: "'a set => 'a pred"
    7.18 +  mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
    7.19 +  nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
    7.20 +  monoP  :: "('a pred => 'a pred) => bool"
    7.21 +
    7.22 +defs 
    7.23 +
    7.24 +Charfun_def      "Charfun     == (% A.% x.x:A)"
    7.25 +monoP_def        "monoP f     == mono(Collect o f o Charfun)"
    7.26 +mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
    7.27 +nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
    7.28 +
    7.29 +end
    7.30 + 
    7.31 + 
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Modelcheck/README.html	Fri May 16 15:29:41 1997 +0200
     8.3 @@ -0,0 +1,28 @@
     8.4 +<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>
     8.5 +
     8.6 +<H3>Invoking Model Checkers in Isabelle/HOL </H3>
     8.7 +
     8.8 +Authors:     Olaf Mueller, Jan Philipps, Robert Sandner<BR>
     8.9 +Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
    8.10 +
    8.11 +
    8.12 +This directory contains four theories:
    8.13 +
    8.14 +<UL>
    8.15 +  <li>MuCalculus: A formalization of the relational mu calculus using the fixed point 
    8.16 +      theory Lfp and Gfp of HOL.<P>
    8.17 +  <li>CTL: A formulation of some CTL operators in the mu calculus.<P>
    8.18 +  <li>MCSyn: The definition of the output syntax "Eindhoven" tailored for the the model checker due to G. Janssen from Eindhoven using
    8.19 +         the print_mode facilities provided by Isabelle. <P>
    8.20 +  <li>Example: A simple reachability property is formulated in the mu calculus and checked 
    8.21 +       by the model checker simply by invoking the tactic mc_tac.
    8.22 +</UL>
    8.23 +
    8.24 +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. 
    8.25 +
    8.26 +
    8.27 +
    8.28 +</BODY></HTML>
    8.29 +
    8.30 +
    8.31 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Modelcheck/ROOT.ML	Fri May 16 15:29:41 1997 +0200
     9.3 @@ -0,0 +1,10 @@
     9.4 +(*  Title:      HOL/Modelcheck/ROOT.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     9.7 +    Copyright   1997  TU Muenchen
     9.8 +
     9.9 +This is the ROOT file for the Eindhoven Modelchecker example
    9.10 +*)
    9.11 +
    9.12 +
    9.13 +use_thy"Example";