# HG changeset patch
# User wenzelm
# Date 935085313 -7200
# Node ID fe09a0c5cebe192125ee0b1e47c9687691c88fa2
# Parent  5a50de9141b5e2947a3f3f169f8acde63e371b68
quite a lot of tuning an cleanup;

diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/CTL.thy
--- 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
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/EindhovenSyn.ML
--- 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 @@
     Copyright   1997  TU Muenchen
 *)
 
-
-
-
-
-
-
-
 fun mc_eindhoven_tac i state =
 let val sign = #sign (rep_thm state)
 in 
@@ -43,5 +36,8 @@
 
 
 val Eindhoven_ss =
-  simpset() addsimprocs [pair_eta_expand_proc]
-    addsimps [split_paired_Ex, Let_def];
+  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+
+(*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 ();
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/EindhovenSyn.thy
--- 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
 
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/MuCalculus.thy
--- 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 @@
     Copyright   1997  TU Muenchen
 *)
 
-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
- 
- 
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/MuckeExample1.ML
--- 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'";
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/MuckeExample2.ML
--- 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'";
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/MuckeSyn.ML
--- 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] 
-                      addsimps [split_paired_Ex,Let_def];
+val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
 
-(* 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 ();
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/ROOT.ML
--- 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
-    Copyright   1997  TU Muenchen
+    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";
diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/mucke_oracle.ML
--- 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===";
     val short_answer = delete_blanks_string answer;
+    val answer_with_info_lines = short_answer string_contains search_text_true;
+    val general_answer = short_answer string_at_post "true" 
   in
-    short_answer string_contains search_text_true
+    (answer_with_info_lines) orelse (general_answer)
   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);