author wenzelm Thu, 19 Aug 1999 19:55:13 +0200 changeset 7295 fe09a0c5cebe parent 7294 5a50de9141b5 child 7296 81286f228b2d
quite a lot of tuning an cleanup;
 src/HOL/Modelcheck/CTL.thy file | annotate | diff | comparison | revisions src/HOL/Modelcheck/EindhovenSyn.ML file | annotate | diff | comparison | revisions src/HOL/Modelcheck/EindhovenSyn.thy file | annotate | diff | comparison | revisions src/HOL/Modelcheck/MuCalculus.thy file | annotate | diff | comparison | revisions src/HOL/Modelcheck/MuckeExample1.ML file | annotate | diff | comparison | revisions src/HOL/Modelcheck/MuckeExample2.ML file | annotate | diff | comparison | revisions src/HOL/Modelcheck/MuckeSyn.ML file | annotate | diff | comparison | revisions src/HOL/Modelcheck/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Modelcheck/mucke_oracle.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Modelcheck/CTL.thy	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/CTL.thy	Thu Aug 19 19:55:13 1999 +0200
@@ -10,22 +10,12 @@
types
'a trans  = "('a * 'a) set"

-
consts
-
-  CEX   ::"['a trans,'a pred, 'a]=>bool"
-  EG    ::"['a trans,'a pred]=> 'a pred"
-
-
+  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))"
-
-
-
-
-
+  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```
```--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -4,13 +4,6 @@
*)

-
-
-
-
-
-
-
fun mc_eindhoven_tac i state =
let val sign = #sign (rep_thm state)
in
@@ -43,5 +36,8 @@

val Eindhoven_ss =
+
+(*check if user has pmu installed*)
+fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
+fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();```
```--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Aug 19 19:55:13 1999 +0200
@@ -50,7 +50,12 @@
(Sign.string_of_term sign) term;

fun call_mc s =
-  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
+  let
+    val eindhoven_home = getenv "EINDHOVEN_HOME";
+    val pmu =
+      if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
+      else eindhoven_home ^ "/pmu";
+  in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;

in
```
```--- a/src/HOL/Modelcheck/MuCalculus.thy	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy	Thu Aug 19 19:55:13 1999 +0200
@@ -4,10 +4,10 @@
*)

-MuCalculus = HOL + Inductive +
+MuCalculus = Main +

types
- 'a pred = "'a=>bool"
+ 'a pred = "'a=>bool"

consts

@@ -16,7 +16,7 @@
nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
monoP  :: "('a pred => 'a pred) => bool"

-defs
+defs

Charfun_def      "Charfun     == (% A.% x. x:A)"
monoP_def        "monoP f     == mono(Collect o f o Charfun)"
@@ -24,5 +24,3 @@
nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"

end
-
- ```
```--- a/src/HOL/Modelcheck/MuckeExample1.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeExample1.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -6,16 +6,12 @@

val reach_rws = [INIT_def,N_def,reach_def];

-(*
-goal thy "reach (True,True,True)";
+Goal "reach (True,True,True)";
by (simp_tac (Mucke_ss addsimps reach_rws) 1);
-by (mc_mucke_tac thy [] 1);
+by (mc_mucke_tac [] 1);
qed "reach_ex_thm1";

-(* Alternative: *)
-goal thy "reach (True,True,True)";
-by (mc_mucke_tac thy reach_rws 1);
-qed "reach_ex_thm1";
-
-*)
-
+(*alternative*)
+Goal "reach (True,True,True)";
+by (mc_mucke_tac reach_rws 1);
+qed "reach_ex_thm1'";```
```--- a/src/HOL/Modelcheck/MuckeExample2.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeExample2.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -9,20 +9,12 @@
(* trace_mc := true; *)
val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];

-(*
-
-goal thy "Reach2 True";
+Goal "Reach2 True";
by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
-by (mc_mucke_tac thy [] 1);
+by (mc_mucke_tac [] 1);
qed "Reach_thm";

-(* Alternative: *)
+(*alternative:*)
goal thy "Reach2 True";
-by (mc_mucke_tac thy Reach_rws 1);
-qed "Reach_thm";
-
-
-*)
-
-
-
+by (mc_mucke_tac Reach_rws 1);
+qed "Reach_thm'";```
```--- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -82,10 +82,10 @@

(* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *)
(* Normally t can be user-instantiated by the value thy of the Isabelle context     *)
-fun call_mucke_tac t i state =
+fun call_mucke_tac i state =
let val sign = #sign (rep_thm state);
val (subgoal::_) = drop(i-1,prems_of state);
-    val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal,t));
+    val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal));
in
(cut_facts_tac [OraAss] i) state
end;
@@ -147,12 +147,7 @@

(* first simplification, then model checking *)

-goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
-by (Simp_tac 1);
-qed "split_paired_Ex";
-
-
-goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+goalw Prod.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;
@@ -169,24 +164,22 @@
end;

-val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc]

-(* the Interface *)
+
+(* the interface *)

-(* type of mc_tac has changed: an argument t of type thy was inserted;  *)
-(* t can be user-instantiated by the value thy of the Isabelle context; *)
-(* furthermore, tactic was extended by full_simp_tac  (TH) *)
-fun mc_mucke_tac t defs i state =
-let val sign = #sign (rep_thm state);
-in
-case drop(i-1,prems_of state) of
-   [] => PureGeneral.Seq.empty |
-   subgoal::_ =>
-		EVERY[REPEAT(etac thin_rl i),
-                        cut_facts_tac (mk_lam_defs defs) i,
-                 full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
-                        move_mus i, call_mucke_tac t i,atac i,
-                        REPEAT(rtac refl i)] state
-end;
+fun mc_mucke_tac defs i state =
+  (case drop (i - 1, Thm.prems_of state) of
+    [] => PureGeneral.Seq.empty
+  | subgoal :: _ =>
+      EVERY [
+        REPEAT (etac thin_rl i),
+        cut_facts_tac (mk_lam_defs defs) i,
+        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
+        move_mus i, call_mucke_tac i,atac i,
+        REPEAT (rtac refl i)] state);

+(*check if user has mucke installed*)
+fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
+fun if_mucke_enabled f x = if mucke_enabled () then f x else ();```
```--- a/src/HOL/Modelcheck/ROOT.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -1,13 +1,23 @@
(*  Title:      HOL/Modelcheck/ROOT.ML
ID:         \$Id\$
-    Author:     Olaf Mueller, Tobias Hamberger, Robert Sandner
+    Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen

-This is the ROOT file for the Modelchecker examples
+Basic Modelchecker examples.
*)

-use_thy"EindhovenExample";
+
+(* Mucke -- mu-calculus model checker from Karlsruhe *)
+
+use "mucke_oracle.ML";
+use_thy "MuckeSyn";

-use"mucke_oracle.ML";
-use_thy"MuckeExample1";
-use_thy"MuckeExample2";
+if_mucke_enabled use_thy "MuckeExample1";
+if_mucke_enabled use_thy "MuckeExample2";
+
+
+(* Einhoven model checker *)
+
+use_thy "CTL";
+use_thy "EindhovenSyn";
+
+if_eindhoven_enabled use_thy "EindhovenExample";```
```--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -1,4 +1,4 @@
-exception MuckeOracleExn of term * theory;
+exception MuckeOracleExn of term;

val trace_mc = ref false;

@@ -494,16 +494,36 @@

fun callmc s =
let
-    val path = Path.unpack "tmp.mu";
-    val _ = File.write path s;
-    val result = execute "mucke -nb tmp";
-  in File.rm path; result end;
+    val mucke_home = getenv "MUCKE_HOME";
+    val mucke =
+      if mucke_home = "" then error "Environment variable MUCKE_HOME not set"
+      else mucke_home ^ "/mucke";
+    val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
+    val _ = File.write mucke_input_file s;
+    val result = execute (mucke ^ " -nb " ^ (File.sysify_path mucke_input_file));
+  in
+    if not (!trace_mc) then (File.rm mucke_input_file) else ();
+    result
+  end;

(* extract_result looks for true value before *)
(* finishing line "===..." of mucke output    *)
+(* ------------------------------------------ *)
+(* Be Careful:                                *)
+(* If the mucke version changes, some changes *)
+(* have also to be made here:                 *)
+(* In extract_result, the value               *)
+(* answer_with_info_lines checks the output   *)
+(* of the muche version, where the output     *)
+(* finishes with information about memory and *)
+(* time (segregated from the "true" value by  *)
+(* a line of equality signs).                 *)
+(* For older versions, where this line does   *)
+(* exist, value general_answer checks whether *)
+(* "true" stand at the end of the output.     *)
local

-infix is_prefix_of contains string_contains;
+infix is_prefix_of contains at_post string_contains string_at_post;

val is_blank : string -> bool =
fn " " => true | "\t" => true | "\n" => true | "\^L" => true
@@ -525,8 +545,14 @@
| [] contains s = false
| (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);

+  fun [] at_post [] = true
+    | [] at_post s = false
+    | (x::xs) at_post s = (s = (x::xs)) orelse (xs at_post s);
+
fun s string_contains s1 =
(explode s) contains (explode s1);
+  fun s string_at_post s1 =
+      (explode s) at_post (explode s1);

in

@@ -534,8 +560,10 @@
let
val search_text_true = "istrue===";
in
end;

end;
@@ -907,8 +935,8 @@
else (check_finity gl ((t,cl)::bl) r b))
end;

-fun preprocess_td sg t [] done = [] |
-preprocess_td sg t (a::b) done =
+fun preprocess_td sg [] done = [] |
+preprocess_td sg (a::b) done =
let
fun extract_hd sg (_ \$ Abs(_,_,r)) = extract_hd sg r |
extract_hd sg (Const("Trueprop",_) \$ r) = extract_hd sg r |
@@ -945,7 +973,7 @@
end;
in
if (a mem done)
-        then (preprocess_td sg t b done)
+        then (preprocess_td sg b done)
else
(let
fun qtn (Type(a,tl)) = (a,tl) |
@@ -953,11 +981,11 @@
val s =  post_last_dot(fst(qtn a));
fun param_types ((Const("Trueprop",_)) \$ (_ \$ (Var(_,Type(_,t)))))  = t |
param_types _ = error "malformed induct-theorem in preprocess_td";
-	 val pl = param_types (concl_of (get_thm t (s ^ ".induct")));
-         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm t (s ^ ".induct")));
+	 val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
+         val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
val ntl = new_types l;
in
-        ((a,l) :: (preprocess_td sg t (ntl @ b) (a :: done)))
+        ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
end)
end;

@@ -988,7 +1016,7 @@
(**********************************************************)
(* mk_mc_oracle:  new argument of MuckeOracleExn: source_thy *)

-fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal,source_thy)) =
+fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) =
let 	val Freesubgoal = freeze_thaw subgoal;

val prems = Logic.strip_imp_prems Freesubgoal;
@@ -998,7 +1026,7 @@
val decls_str = string_of_terms sign Muckedecls;

val type_list = (extract_type_names_prems sign (prems@[concl]));
-	val ctl =  preprocess_td sign source_thy type_list [];
+	val ctl =  preprocess_td sign type_list [];
val b = if (ctl=[]) then true else (check_finity [Type("bool",[])] [] ctl false);
val type_str = make_type_decls ctl
((Type("bool",[]),("True",[])::("False",[])::[])::ctl);```