--- 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 @@
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 ();
--- 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 @@
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
-
-
--- 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]
- 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 ();
--- 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";
--- 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);