| author | wenzelm |
| Mon, 12 Jul 2010 20:35:10 +0200 | |
| changeset 37779 | 982b0668dcbd |
| parent 37778 | 87b5dfe00387 |
| child 37780 | 7e91b3f98c46 |
--- a/src/HOL/IsaMakefile Mon Jul 12 20:21:39 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Jul 12 20:35:10 2010 +0200 @@ -48,7 +48,6 @@ HOL-Metis_Examples \ HOL-MicroJava \ HOL-Mirabelle \ - HOL-Modelcheck \ HOL-Mutabelle \ HOL-NanoJava \ HOL-Nitpick_Examples \ @@ -794,18 +793,6 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF -## HOL-Modelcheck - -HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz - -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ - Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ - Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ - Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ - Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck - - ## HOL-Imperative_HOL HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz @@ -1353,7 +1340,6 @@ $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \ $(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \ $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \ - $(LOG)/HOL-Modelcheck.gz \ $(LOG)/HOL-Multivariate_Analysis.gz \ $(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \ $(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \
--- a/src/HOL/Modelcheck/CTL.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* Title: HOL/Modelcheck/CTL.thy - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory CTL -imports MuCalculus -begin - -types - 'a trans = "('a * 'a) set" - -definition CEX :: "['a trans,'a pred, 'a]=>bool" where - "CEX N f u == (? v. (f v & (u,v):N))" - -definition EG ::"['a trans,'a pred]=> 'a pred" where - "EG N f == nu (% Q. % u.(f u & CEX N Q u))" - -end
--- a/src/HOL/Modelcheck/EindhovenExample.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,40 +0,0 @@ -(* Title: HOL/Modelcheck/EindhovenExample.thy - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory EindhovenExample -imports EindhovenSyn CTL -begin - -types - state = "bool * bool * bool" - -definition INIT :: "state pred" where - "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" - -definition N :: "[state,state] => bool" where - "N == % (x1,x2,x3) (y1,y2,y3). - (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | - ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | - ( x1 & ~x2 & ~x3 & y1 & y2 & y3)" - -definition reach:: "state pred" where - "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" - -lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)" - by (simp add: INIT_def) - - -lemmas reach_rws = reach_def INIT_def N_def - -lemma reach_ex: "reach (True, True, True)" - apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *}) - txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *} - pr (Eindhoven) - txt {* actually invoke the model checker, try out after installing - the model checker: see the README file *} - apply (tactic {* mc_eindhoven_tac 1 *}) - done - -end
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,79 +0,0 @@ -(* Title: HOL/Modelcheck/EindhovenSyn.thy - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory EindhovenSyn -imports MuCalculus -begin - -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) - - All_binder :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10) - Ex_binder :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10) - "_lambda" :: "[pttrns, 'a] => 'b" ("(3L _./ _)" 10) - - "_idts" :: "[idt, idts] => idts" ("_,/_" [1, 0] 0) - "_pattern" :: "[pttrn, patterns] => pttrn" ("_,/_" [1, 0] 0) - - "Mu " :: "[idts, 'a pred] => 'a pred" ("(3[mu _./ _])" 1000) - "Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000) - -ML {* - val trace_eindhoven = Unsynchronized.ref false; -*} - -oracle mc_eindhoven_oracle = -{* -let - val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global; - - fun call_mc s = - 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 #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end; -in - fn cgoal => - let - val thy = Thm.theory_of_cterm cgoal; - val goal = Thm.term_of cgoal; - val s = eindhoven_term thy goal; - val debug = tracing ("MC debugger: " ^ s); - val result = call_mc s; - in - if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else (); - (case result of - "TRUE\n" => cgoal | - "FALSE\n" => error "MC oracle yields FALSE" | - _ => error ("MC syntax error: " ^ result)) - end -end -*} - -ML {* -fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) => - let - val thy = Thm.theory_of_thm state; - val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal)); - in cut_facts_tac [assertion] i THEN atac i end) i state; - -val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta")); - -val pair_eta_expand_proc = - Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"] - (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE); - -val Eindhoven_ss = - @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; -*} - -end
--- a/src/HOL/Modelcheck/MuCalculus.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: HOL/Modelcheck/MuCalculus.thy - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory MuCalculus -imports Main -begin - -types - 'a pred = "'a=>bool" - -definition Charfun :: "'a set => 'a pred" where - "Charfun == (% A.% x. x:A)" - -definition monoP :: "('a pred => 'a pred) => bool" where - "monoP f == mono(Collect o f o Charfun)" - -definition mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10) where - "mu f == Charfun(lfp(Collect o f o Charfun))" - -definition nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10) where - "nu f == Charfun(gfp(Collect o f o Charfun))" - -end
--- a/src/HOL/Modelcheck/MuckeExample1.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -(* Title: HOL/Modelcheck/MuckeExample1.thy - ID: $Id$ - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory MuckeExample1 -imports MuckeSyn -begin - -types - state = "bool * bool * bool" - -definition INIT :: "state pred" where - "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" - N :: "[state,state] => bool" - "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:: "state pred" - "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" - -lemmas reach_rws = INIT_def N_def reach_def - -lemma reach_ex1: "reach (True,True,True)" - apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *}) - apply (tactic {* mc_mucke_tac [] 1 *}) - done - -(*alternative*) -lemma reach_ex' "reach (True,True,True)" - by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *}) - -end
--- a/src/HOL/Modelcheck/MuckeExample2.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -(* Title: HOL/Modelcheck/MuckeExample2.thy - ID: $Id$ - Author: Olaf Mueller, Jan Philipps, Robert Sandner - Copyright 1997 TU Muenchen -*) - -theory MuckeExample2 -imports MuckeSyn -begin - -definition Init :: "bool pred" where - "Init x == x" - R :: "[bool,bool] => bool" - "R x y == (x & ~y) | (~x & y)" - Reach :: "bool pred" - "Reach == mu (%Q x. Init x | (? y. Q y & R y x))" - Reach2:: "bool pred" - "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))" - -lemmas Reach_rws = Init_def R_def Reach_def Reach2_def - -lemma Reach: "Reach2 True" - apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *}) - apply (tactic {* mc_mucke_tac [] 1 *}) - done - -(*alternative:*) -lemma Reach': "Reach2 True" - by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *}) - -end
--- a/src/HOL/Modelcheck/MuckeSyn.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,236 +0,0 @@ -(* Title: HOL/Modelcheck/MuckeSyn.thy - Author: Tobias Hamberger - Copyright 1999 TU Muenchen -*) - -theory MuckeSyn -imports MuCalculus -uses "mucke_oracle.ML" -begin - -(* extended with some operators and case treatment (which requires postprocessing with -transform_case (from MuCalculus) (TH) *) - -nonterminals - mutype - decl decls - cases_syn case_syn - -syntax (Mucke output) - True :: bool ("true") - False :: bool ("false") - Not :: "bool => bool" ("! _" [40] 40) - If :: "[bool, 'a, 'a] => 'a" ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10) - - "op &" :: "[bool, bool] => bool" (infixr "&" 35) - "op |" :: "[bool, bool] => bool" (infixr "|" 30) - "op -->" :: "[bool, bool] => bool" (infixr "->" 25) - "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) - "_not_equal" :: "['a, 'a] => bool" ("(_ !=/ _)" [51, 51] 50) - - All_binder :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10) - Ex_binder :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10) - - "_lambda" :: "[idts, 'a] => 'b" ("(3L _./ _)" 10) - "_applC" :: "[('b => 'a), cargs] => aprop" ("(1_/ '(_'))" [1000,1000] 999) - "_cargs" :: "['a, cargs] => cargs" ("_,/ _" [1000,1000] 1000) - - "_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0) - - "_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)") -(* "_pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0) - "_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *) - - "_decl" :: "[mutype,pttrn] => decl" ("_ _") - "_decls" :: "[decl,decls] => decls" ("_,/ _") - "" :: "decl => decls" ("_") - "_mu" :: "[decl,decls,'a pred] => 'a pred" ("mu _ '(_') _ ;") - "_mudec" :: "[decl,decls] => 'a pred" ("mu _ '(_') ;") - "_nu" :: "[decl,decls,'a pred] => 'a pred" ("nu _ '(_') _ ;") - "_nudec" :: "[decl,decls] => 'a pred" ("nu _ '(_') ;") - "_fun" :: "[decl,decls,'a pred] => 'a pred" ("_ '(_') _ ;") - "_dec" :: "[decl,decls] => 'a pred" ("_ '(_') ;") - - "_Ex" :: "[decl,idts,'a pred] => 'a pred" ("'((3exists _ _./ _)')") - "_All" :: "[decl,idts,'a pred] => 'a pred" ("'((3forall _ _./ _)')") - - "Mu " :: "[idts, 'a pred] => 'a pred" ("(3mu _./ _)" 1000) - "Nu " :: "[idts, 'a pred] => 'a pred" ("(3nu _./ _)" 1000) - - "_case_syntax":: "['a, cases_syn] => 'b" ("(case*_* / _ / esac*)" 10) - "_case1" :: "['a, 'b] => case_syn" ("(2*= _ :/ _;)" 10) - "" :: "case_syn => cases_syn" ("_") - "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ _") - -(*Terms containing a case statement must be post-processed with the - ML function transform_case. There, all asterikses before the "=" - will be replaced by the expression between the two asterisks - following "case" and the asterisk after esac will be deleted *) - -oracle mc_mucke_oracle = mk_mc_mucke_oracle - -ML {* -(* search_mu t searches for Mu terms in term t. In the case of nested Mu's, - it yields innermost one. If no Mu term is present, search_mu yields NONE -*) - -(* extended for treatment of nu (TH) *) -fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = - (case (search_mu t2) of - SOME t => SOME t - | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2)) - | search_mu ((Const("MuCalculus.nu",tp)) $ t2) = - (case (search_mu t2) of - SOME t => SOME t - | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2)) - | search_mu (t1 $ t2) = - (case (search_mu t1) of - SOME t => SOME t - | NONE => search_mu t2) - | search_mu (Abs(_,_,t)) = search_mu t - | search_mu _ = NONE; - - - - -(* seraching a variable in a term. Used in move_mus to extract the - term-rep of var b in hthm *) - -fun search_var s t = -case t of - t1 $ t2 => (case (search_var s t1) of - SOME tt => SOME tt | - NONE => search_var s t2) | - Abs(_,_,t) => search_var s t | - Var((s1,_),_) => if s = s1 then SOME t else NONE | - _ => NONE; - - -(* function move_mus: - Mucke can't deal with nested Mu terms. move_mus i searches for - Mu terms in the subgoal i and replaces Mu terms in the conclusion - by constants and definitions in the premises recursively. - - move_thm is the theorem the performs the replacement. To create NEW - names for the Mu terms, the indizes of move_thm are incremented by - max_idx of the subgoal. -*) - -local - - val move_thm = OldGoals.prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b" - (fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1, - REPEAT (resolve_tac prems 1)]); - - val sig_move_thm = Thm.theory_of_thm move_thm; - val bCterm = cterm_of sig_move_thm (the (search_var "b" (concl_of move_thm))); - val aCterm = cterm_of sig_move_thm (the (search_var "a" (hd(prems_of move_thm)))); - -in - -fun move_mus i state = -let val sign = Thm.theory_of_thm state; - val subgoal = nth (prems_of state) i; - val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *) - val redex = search_mu concl; - val idx = let val t = #maxidx (rep_thm state) in - if t < 0 then 1 else t+1 end; -in -case redex of - NONE => all_tac state | - SOME redexterm => - let val Credex = cterm_of sign redexterm; - val aiCterm = - cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm)); - val inst_move_thm = cterm_instantiate - [(bCterm,Credex),(aCterm,aiCterm)] move_thm; - in - ((rtac inst_move_thm i) THEN (dtac eq_reflection i) - THEN (move_mus i)) state - end -end; -end; - - -val call_mucke_tac = CSUBGOAL (fn (cgoal, i) => -let val OraAss = mc_mucke_oracle cgoal -in cut_facts_tac [OraAss] i end); - - -(* transforming fun-defs into lambda-defs *) - -val [eq] = OldGoals.goal Pure.thy "(!! x. f x == g x) ==> f == g"; - OldGoals.by (rtac (extensional eq) 1); -OldGoals.qed "ext_rl"; - -infix cc; - -fun NONE cc xl = xl - | (SOME x) cc xl = x::xl; - -fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z - | getargs (x $ (Var ((y,_),_))) = y; - -fun getfun ((x $ y) $ z) = getfun (x $ y) - | getfun (x $ _) = x; - -local - -fun delete_bold [] = [] -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_bold s end) - else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_bold s end) - else (x::delete_bold xs)); - -fun delete_bold_string s = implode(delete_bold (explode s)); - -in - -(* extension with removing bold font (TH) *) -fun mk_lam_def (_::_) _ _ = NONE - | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t - | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = - let val thy = theory_of_thm t; - val fnam = Syntax.string_of_term_global thy (getfun LHS); - val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS) - val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs); - in - SOME (OldGoals.prove_goal thy gl (fn prems => - [(REPEAT (rtac ext_rl 1)), (rtac t 1) ])) - end -| mk_lam_def [] _ t= NONE; - -fun mk_lam_defs ([]:thm list) = ([]: thm list) - | mk_lam_defs (t::l) = - (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l); - -end; - - -(* first simplification, then model checking *) - -val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta")); - -val pair_eta_expand_proc = - Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"] - (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE); - -val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; - - -(* the interface *) - -fun mc_mucke_tac defs i state = - (case try (nth (Thm.prems_of state)) i of - NONE => no_tac state - | SOME subgoal => - EVERY [ - REPEAT (etac thin_rl i), - cut_facts_tac (mk_lam_defs defs) i, - full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i, - move_mus i, call_mucke_tac i,atac i, - REPEAT (rtac refl i)] state); -*} - -end
--- a/src/HOL/Modelcheck/README.html Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> - -<!-- $Id$ --> - -<html> - -<head> - <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> - <title>HOL/Modelcheck</title> -</head> - -<body> - -<h2>Invoking Model Checkers in Isabelle/HOL</h2> - -This directory contains the basic setup for integration of some model -checkers in Isabelle/HOL, together with a few basic examples. - -<p> - -Currently, best results are achieved with the <a -href="http://iseran.ira.uka.de/~armin/mucke/"><em>Mucke</em></a> model -checker (version 0.3.5 is known to work). Theory <tt>MuCalculus</tt> -provides the syntactic and oracle interfaces, while -<tt>MuckeExample1</tt> and <tt>MuckeExample2</tt> demonstrate the -model checker tactic <tt>mc_mucke_tac</tt> in action. To run the -examples yourself, you only have to point <tt>MUCKE_HOME</tt> in -Isabelle's <tt>etc/settings</tt> to the place where the Mucke binary -has been installed. - -<p> - -In order to support more realistic applications, the <a -href="http://isabelle.in.tum.de/library/HOLCF/IOA/Modelcheck">HOLCF/IOA/Modelcheck</a> -session augments this basic mechanism by further infrastructure for -proofs about I/O automata. There is a separate <a -href="http://isabelle.in.tum.de/IOA/papers/IOA-modelcheck.pdf">paper</a> -available, describing model checking in Isabelle/IOA in more detail. - -</body> - -</html>
--- a/src/HOL/Modelcheck/ROOT.ML Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* Title: HOL/Modelcheck/ROOT.ML - ID: $Id$ - Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen - -Basic Modelchecker examples. -*) - -time_use_thy "CTL"; - - -(* Einhoven model checker *) - -(*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 (); - -time_use_thy "EindhovenSyn"; -if_eindhoven_enabled time_use_thy "EindhovenExample"; - - -(* Mucke -- mu-calculus model checker from Karlsruhe *) - -time_use_thy "MuckeSyn"; - -(*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 (); - -if_mucke_enabled time_use_thy "MuckeExample1"; -if_mucke_enabled time_use_thy "MuckeExample2";
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1054 +0,0 @@ - -val trace_mc = Unsynchronized.ref false; - - -(* transform_case post-processes output strings of the syntax "Mucke" *) -(* with respect to the syntax of the case construct *) -local - fun extract_argument [] = [] - | extract_argument ("*"::_) = [] - | extract_argument (x::xs) = x::(extract_argument xs); - - fun cut_argument [] = [] - | cut_argument ("*"::r) = r - | cut_argument (_::xs) = cut_argument xs; - - fun insert_case_argument [] s = [] - | insert_case_argument ("*"::"="::xl) (x::xs) = - (explode(x)@(" "::"="::(insert_case_argument xl (x::xs)))) - | insert_case_argument ("c"::"a"::"s"::"e"::"*"::xl) s = - (let - val arg=implode(extract_argument xl); - val xr=cut_argument xl - in - "c"::"a"::"s"::"e"::" "::(insert_case_argument xr (arg::s)) - end) - | insert_case_argument ("e"::"s"::"a"::"c"::"*"::xl) (x::xs) = - "e"::"s"::"a"::"c"::(insert_case_argument xl xs) - | insert_case_argument (x::xl) s = x::(insert_case_argument xl s); -in - -fun transform_case s = implode(insert_case_argument (explode s) []); - -end; - - -(* if_full_simp_tac is a tactic for rewriting non-boolean ifs *) -local - (* searching an if-term as below as possible *) - fun contains_if (Abs(a,T,t)) = [] | - contains_if (Const("HOL.If",T) $ b $ a1 $ a2) = - let - fun tn (Type(s,_)) = s | - tn _ = error "cannot master type variables in if term"; - val s = tn(body_type T); - in - if (s="bool") then [] else [b,a1,a2] - end | - contains_if (a $ b) = if ((contains_if b)=[]) then (contains_if a) - else (contains_if b) | - contains_if _ = []; - - fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(Syntax.variant_abs(a,T,t))) | - find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then - (if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b)) - else (a $ b,contains_if(a $ b))| - find_replace_term t = (t,[]); - - fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) | - if_substi (Const("HOL.If",T) $ b $ a1 $ a2) t = t | - if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b) - else (a$(if_substi b t)) | - if_substi t v = t; - - fun deliver_term (t,[]) = [] | - deliver_term (t,[b,a1,a2]) = - [ - Const("Trueprop",Type("fun",[Type("bool",[]),Type("prop",[])])) $ - ( -Const("op =",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) - $ t $ - ( -Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) - $ - ( -Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) - $ b $ (if_substi t a1)) - $ - ( -Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) - $ (Const("Not",Type("fun",[Type("bool",[]),Type("bool",[])])) $ b) $ (if_substi t a2)) - ))] | - deliver_term _ = - error "tactic failed due to occurence of malformed if-term" (* shouldnt occur *); - - fun search_if (*((Const("==",_)) $ _ $*) (a) = deliver_term(find_replace_term a); - - fun search_ifs [] = [] | - search_ifs (a::r) = - let - val i = search_if a - in - if (i=[]) then (search_ifs r) else i - end; -in - -fun if_full_simp_tac sset i state = -let val sign = Thm.theory_of_thm state; - val subgoal = nth (prems_of state) i; - val prems = Logic.strip_imp_prems subgoal; - val concl = Logic.strip_imp_concl subgoal; - val prems = prems @ [concl]; - val itrm = search_ifs prems; -in -if (itrm = []) then no_tac state else -( -let -val trm = hd(itrm) -in -( -OldGoals.push_proof(); -OldGoals.goalw_cterm [] (cterm_of sign trm); -OldGoals.by (simp_tac (global_simpset_of sign) 1); - let - val if_tmp_result = OldGoals.result() - in - ( - OldGoals.pop_proof(); - CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state) - end -) -end) -end; - -end; - -(********************************************************) -(* All following stuff serves for defining mk_mc_oracle *) -(********************************************************) - -(***************************************) -(* SECTION 0: some auxiliary functions *) - -fun list_contains_key [] _ = false | -list_contains_key ((a,l)::r) t = if (a=t) then true else (list_contains_key r t); - -fun search_in_keylist [] _ = [] | -search_in_keylist ((a,l)::r) t = if (a=t) then l else (search_in_keylist r t); - -(* delivers the part of a qualified type/const-name after the last dot *) -fun post_last_dot str = -let -fun fl [] = [] | -fl (a::r) = if (a=".") then [] else (a::(fl r)); -in -implode(rev(fl(rev(explode str)))) -end; - -(* OUTPUT - relevant *) -(* converts type to string by a mucke-suitable convention *) -fun type_to_string_OUTPUT (Type(a,[])) = post_last_dot a | -type_to_string_OUTPUT (Type("*",[a,b])) = - "P_" ^ (type_to_string_OUTPUT a) ^ "_AI_" ^ (type_to_string_OUTPUT b) ^ "_R" | -type_to_string_OUTPUT (Type(a,l)) = -let -fun ts_to_string [] = "" | -ts_to_string (a::[]) = type_to_string_OUTPUT a | -ts_to_string (a::l) = (type_to_string_OUTPUT a) ^ "_I_" ^ (ts_to_string l); -in -(post_last_dot a) ^ "_A_" ^ (ts_to_string l) ^ "_C" -end | -type_to_string_OUTPUT _ = -error "unexpected type variable in type_to_string"; - -(* delivers type of a term *) -fun type_of_term (Const(_,t)) = t | -type_of_term (Free(_,t)) = t | -type_of_term (Var(_,t)) = t | -type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(Syntax.variant_abs(x,t,trm)))]) | -type_of_term (a $ b) = -let - fun accept_fun_type (Type("fun",[x,y])) = (x,y) | - accept_fun_type _ = - error "no function type returned, where it was expected (in type_of_term)"; - val (x,y) = accept_fun_type(type_of_term a) -in -y -end | -type_of_term _ = -error "unexpected bound variable when calculating type of a term (in type_of_term)"; - -(* makes list [a1..an] and ty to type an -> .. -> a1 -> ty *) -fun fun_type_of [] ty = ty | -fun_type_of (a::r) ty = fun_type_of r (Type("fun",[a,ty])); - -(* creates a constructor term from constructor and its argument terms *) -fun con_term_of t [] = t | -con_term_of t (a::r) = con_term_of (t $ a) r; - -(* creates list of constructor terms *) -fun con_term_list_of trm [] = [] | -con_term_list_of trm (a::r) = (con_term_of trm a)::(con_term_list_of trm r); - -(* list multiplication *) -fun multiply_element a [] = [] | -multiply_element a (l::r) = (a::l)::(multiply_element a r); -fun multiply_list [] l = [] | -multiply_list (a::r) l = (multiply_element a l)@(multiply_list r l); - -(* To a list of types, delivers all lists of proper argument terms; tl has to *) -(* be a preprocessed type list with element type: (type,[(string,[type])]) *) -fun arglist_of sg tl [] = [[]] | -arglist_of sg tl (a::r) = -let -fun ispair (Type("*",x::y::[])) = (true,(x,y)) | -ispair x = (false,(x,x)); -val erg = -(if (fst(ispair a)) - then (let - val (x,y) = snd(ispair a) - in - con_term_list_of (Const("pair",Type("fun",[x,Type("fun",[y,a])]))) - (arglist_of sg tl [x,y]) - end) - else - (let - fun deliver_erg sg tl _ [] = [] | - deliver_erg sg tl typ ((c,tyl)::r) = let - val ft = fun_type_of (rev tyl) typ; - val trm = OldGoals.simple_read_term sg ft c; - in - (con_term_list_of trm (arglist_of sg tl tyl)) - @(deliver_erg sg tl typ r) - end; - val cl = search_in_keylist tl a; - in - deliver_erg sg tl a cl - end)) -in -multiply_list erg (arglist_of sg tl r) -end; - -(*******************************************************************) -(* SECTION 1: Robert Sandner's source was improved and extended by *) -(* generation of function declarations *) - -fun dest_Abs (Abs s_T_t) = s_T_t - | dest_Abs t = raise TERM("dest_Abs", [t]); - -(* -fun force_Abs (Abs s_T_t) = Abs s_T_t - | force_Abs t = Abs("x", hd(fst(strip_type (type_of t))), - (incr_boundvars 1 t) $ (Bound 0)); - -fun etaexp_dest_Abs t = dest_Abs (force_Abs t); -*) - -(* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw - and thm.instantiate *) -fun freeze_thaw t = - let val used = OldTerm.add_term_names (t, []) - and vars = OldTerm.term_vars t; - fun newName (Var(ix,_), (pairs,used)) = - let val v = Name.variant used (string_of_indexname ix) - in ((ix,v)::pairs, v::used) end; - val (alist, _) = List.foldr newName ([], used) vars; - fun mk_inst (Var(v,T)) = (Var(v,T), - Free ((the o AList.lookup (op =) alist) v, T)); - val insts = map mk_inst vars; - in subst_atomic insts t end; - -fun make_fun_type (a::b::l) = Type("fun",a::(make_fun_type (b::l))::[]) - | make_fun_type (a::l) = a; - -fun make_decl muckeType id isaType = - let val constMuckeType = Const(muckeType,isaType); - val constId = Const(id,isaType); - val constDecl = Const("_decl", make_fun_type [isaType,isaType,isaType]); - in (constDecl $ constMuckeType) $ constId end; - -fun make_MuTerm muDeclTerm ParamDeclTerm muTerm isaType = - let val constMu = Const("_mu", - make_fun_type [isaType,isaType,isaType,isaType]); - val t1 = constMu $ muDeclTerm; - val t2 = t1 $ ParamDeclTerm; - val t3 = t2 $ muTerm - in t3 end; - -fun make_MuDecl muDeclTerm ParamDeclTerm isaType = - let val constMu = Const("_mudec", - make_fun_type [isaType,isaType,isaType]); - val t1 = constMu $ muDeclTerm; - val t2 = t1 $ ParamDeclTerm - in t2 end; - -fun make_NuTerm muDeclTerm ParamDeclTerm muTerm isaType = - let val constMu = Const("_nu", - make_fun_type [isaType,isaType,isaType,isaType]); - val t1 = constMu $ muDeclTerm; - val t2 = t1 $ ParamDeclTerm; - val t3 = t2 $ muTerm - in t3 end; - -fun make_NuDecl muDeclTerm ParamDeclTerm isaType = - let val constMu = Const("_nudec", - make_fun_type [isaType,isaType,isaType]); - val t1 = constMu $ muDeclTerm; - val t2 = t1 $ ParamDeclTerm - in t2 end; - -fun is_mudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.mu",_)) $ t2)) = true - | is_mudef _ = false; - -fun is_nudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.nu",_)) $ t2)) = true - | is_nudef _ = false; - -fun make_decls sign Dtype (Const(str,tp)::n::Clist) = - let val const_decls = Const("_decls",make_fun_type [Dtype,Dtype,Dtype]); - val decl = make_decl (type_to_string_OUTPUT tp) str Dtype; - in - ((const_decls $ decl) $ (make_decls sign Dtype (n::Clist))) - end - | make_decls sign Dtype [Const(str,tp)] = - make_decl (type_to_string_OUTPUT tp) str Dtype; - - -(* make_mu_def transforms an Isabelle Mu-Definition into Mucke format - Takes equation of the form f = Mu Q. % x. t *) - -fun dest_atom (Const t) = dest_Const (Const t) - | dest_atom (Free t) = dest_Free (Free t); - -fun get_decls sign Clist (Abs(s,tp,trm)) = - let val VarAbs = Syntax.variant_abs(s,tp,trm); - in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs) - end - | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm - | get_decls sign Clist trm = (Clist,trm); - -fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) = - let val LHSStr = fst (dest_atom LHS); - val MuType = Type("bool",[]); (* always ResType of mu, also serves - as dummy type *) - val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *) - val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs)); - val PConsts = rev PCon_LHS; - val muDeclTerm = make_decl "bool" LHSStr MuType; - val PDeclsTerm = make_decls sign MuType PConsts; - val MuDefTerm = make_MuTerm muDeclTerm PDeclsTerm MMuTerm MuType; - in MuDefTerm end; - -fun make_mu_decl sign ((tt $ LHS) $ (ttt $ RHS)) = - let val LHSStr = fst (dest_atom LHS); - val MuType = Type("bool",[]); (* always ResType of mu, also serves - as dummy type *) - val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *) - val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs)); - val PConsts = rev PCon_LHS; - val muDeclTerm = make_decl "bool" LHSStr MuType; - val PDeclsTerm = make_decls sign MuType PConsts; - val MuDeclTerm = make_MuDecl muDeclTerm PDeclsTerm MuType; - in MuDeclTerm end; - -fun make_nu_def sign ((tt $ LHS) $ (ttt $ RHS)) = - let val LHSStr = fst (dest_atom LHS); - val MuType = Type("bool",[]); (* always ResType of mu, also serves - as dummy type *) - val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *) - val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs)); - val PConsts = rev PCon_LHS; - val muDeclTerm = make_decl "bool" LHSStr MuType; - val PDeclsTerm = make_decls sign MuType PConsts; - val NuDefTerm = make_NuTerm muDeclTerm PDeclsTerm MMuTerm MuType; - in NuDefTerm end; - -fun make_nu_decl sign ((tt $ LHS) $ (ttt $ RHS)) = - let val LHSStr = fst (dest_atom LHS); - val MuType = Type("bool",[]); (* always ResType of mu, also serves - as dummy type *) - val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *) - val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs)); - val PConsts = rev PCon_LHS; - val muDeclTerm = make_decl "bool" LHSStr MuType; - val PDeclsTerm = make_decls sign MuType PConsts; - val NuDeclTerm = make_NuDecl muDeclTerm PDeclsTerm MuType; - in NuDeclTerm end; - -fun make_FunMuckeTerm FunDeclTerm ParamDeclTerm Term isaType = - let val constFun = Const("_fun", - make_fun_type [isaType,isaType,isaType,isaType]); - val t1 = constFun $ FunDeclTerm; - val t2 = t1 $ ParamDeclTerm; - val t3 = t2 $ Term - in t3 end; - -fun make_FunMuckeDecl FunDeclTerm ParamDeclTerm isaType = - let val constFun = Const("_dec", - make_fun_type [isaType,isaType,isaType]); - val t1 = constFun $ FunDeclTerm; - val t2 = t1 $ ParamDeclTerm - in t2 end; - -fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true - | is_fundef (Const("==", _) $ _ $ Abs _) = true - | is_fundef _ = false; - -fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) = - let (* fun dest_atom (Const t) = dest_Const (Const t) - | dest_atom (Free t) = dest_Free (Free t); *) - val LHSStr = fst (dest_atom LHS); - val LHSResType = body_type(snd(dest_atom LHS)); - val LHSResTypeStr = type_to_string_OUTPUT LHSResType; -(* val (_,AbsType,RawTerm) = dest_Abs(RHS); -*) val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS; - val Consts_LHS = rev Consts_LHS_rev; - val PDeclsTerm = make_decls sign LHSResType Consts_LHS; - (* Boolean functions only, list necessary in general *) - val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType; - val MuckeDefTerm = make_FunMuckeTerm DeclTerm PDeclsTerm Free_RHS - LHSResType; - in MuckeDefTerm end; - -fun make_mucke_fun_decl sign ((_ $ LHS) $ RHS) = - let (* fun dest_atom (Const t) = dest_Const (Const t) - | dest_atom (Free t) = dest_Free (Free t); *) - val LHSStr = fst (dest_atom LHS); - val LHSResType = body_type(snd(dest_atom LHS)); - val LHSResTypeStr = type_to_string_OUTPUT LHSResType; -(* val (_,AbsType,RawTerm) = dest_Abs(RHS); -*) val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS; - val Consts_LHS = rev Consts_LHS_rev; - val PDeclsTerm = make_decls sign LHSResType Consts_LHS; - (* Boolean functions only, list necessary in general *) - val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType; - val MuckeDeclTerm = make_FunMuckeDecl DeclTerm PDeclsTerm LHSResType; -in MuckeDeclTerm end; - -fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) = - (let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]); - val TypeConst = Const (type_to_string_OUTPUT tp,tp); - val VarAbs = Syntax.variant_abs(str,tp,t); - val BoundConst = Const(fst VarAbs,tp); - val t1 = ExConst $ TypeConst; - val t2 = t1 $ BoundConst; - val t3 = elim_quantifications sign (snd VarAbs) - in t2 $ t3 end) - | elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) = - (let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]); - val TypeConst = Const (type_to_string_OUTPUT tp,tp); - val VarAbs = Syntax.variant_abs(str,tp,t); - val BoundConst = Const(fst VarAbs,tp); - val t1 = AllConst $ TypeConst; - val t2 = t1 $ BoundConst; - val t3 = elim_quantifications sign (snd VarAbs) - in t2 $ t3 end) - | elim_quantifications sign (t1 $ t2) = - (elim_quantifications sign t1) $ (elim_quantifications sign t2) - | elim_quantifications sign (Abs(_,_,t)) = elim_quantifications sign t - | elim_quantifications sign t = t; -fun elim_quant_in_list sign [] = [] - | elim_quant_in_list sign (trm::list) = - (elim_quantifications sign trm)::(elim_quant_in_list sign list); - -fun dummy true = writeln "True\n" | - dummy false = writeln "Fals\n"; - -fun transform_definitions sign [] = [] - | transform_definitions sign (trm::list) = - if is_mudef trm - then (make_mu_def sign trm)::(transform_definitions sign list) - else - if is_nudef trm - then (make_nu_def sign trm)::(transform_definitions sign list) - else - if is_fundef trm - then (make_mucke_fun_def sign trm)::(transform_definitions sign list) - else trm::(transform_definitions sign list); - -fun terms_to_decls sign [] = [] - | terms_to_decls sign (trm::list) = - if is_mudef trm - then (make_mu_decl sign trm)::(terms_to_decls sign list) - else - if is_nudef trm - then (make_nu_decl sign trm)::(terms_to_decls sign list) - else - if is_fundef trm - then (make_mucke_fun_decl sign trm)::(terms_to_decls sign list) - else (transform_definitions sign list); - -fun transform_terms sign list = -let val DefsOk = transform_definitions sign list; -in elim_quant_in_list sign DefsOk -end; - -fun string_of_terms sign terms = -let fun make_string sign [] = "" | - make_string sign (trm::list) = - Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list -in - Print_Mode.setmp ["Mucke"] (make_string sign) terms -end; - -fun callmc s = - let - 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, _) = bash_output (mucke ^ " -nb -res " ^ File.shell_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 contains at_post string_contains string_at_post; - - val is_blank : string -> bool = - fn " " => true | "\t" => true | "\n" => true | "\^L" => true - | "\160" => true | _ => false; - - fun delete_blanks [] = [] - | delete_blanks (":"::xs) = delete_blanks xs - | delete_blanks (x::xs) = - if (is_blank x) then (delete_blanks xs) - else x::(delete_blanks xs); - - fun delete_blanks_string s = implode(delete_blanks (explode s)); - - fun [] contains [] = true - | [] contains s = false - | (x::xs) contains s = (is_prefix (op =) s (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 - -fun extract_result goal answer = - 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 - (answer_with_info_lines) (* orelse (general_answer) *) - end; - -end; - -(**************************************************************) -(* SECTION 2: rewrites case-constructs over complex datatypes *) -local - -(* check_case checks, whether a term is of the form a $ "(case x of ...)", *) -(* where x is of complex datatype; the second argument of the result is *) -(* the number of constructors of the type of x *) -fun check_case sg tl (a $ b) = -let - (* tl_contains_complex returns true in the 1st argument when argument type is *) - (* complex; the 2nd argument is the number of constructors *) - fun tl_contains_complex [] _ = (false,0) | - tl_contains_complex ((a,l)::r) t = - let - fun check_complex [] p = p | - check_complex ((a,[])::r) (t,i) = check_complex r (t,i+1) | - check_complex ((a,_)::r) (t,i) = check_complex r (true,i+1); - in - if (a=t) then (check_complex l (false,0)) else (tl_contains_complex r t) - end; - fun check_head_for_case sg (Const(s,_)) st 0 = - if (post_last_dot(s) = (st ^ "_case")) then true else false | - check_head_for_case sg (a $ (Const(s,_))) st 0 = - if (post_last_dot(s) = (st ^ "_case")) then true else false | - check_head_for_case _ _ _ 0 = false | - check_head_for_case sg (a $ b) st n = check_head_for_case sg a st (n-1) | - check_head_for_case _ _ _ _ = false; - fun qtn (Type(a,_)) = a | - qtn _ = error "unexpected type variable in check_case"; - val t = type_of_term b; - val (bv,n) = tl_contains_complex tl t - val st = post_last_dot(qtn t); -in - if (bv) then ((check_head_for_case sg a st n),n) else (false,n) -end | -check_case sg tl trm = (false,0); - -(* enrich_case_with_terms enriches a case term with additional *) -(* conditions according to the context of the case replacement *) -fun enrich_case_with_terms sg [] t = t | -enrich_case_with_terms sg [trm] (Abs(x,T,t)) = -let - val v = Syntax.variant_abs(x,T,t); - val f = fst v; - val s = snd v -in -(Const("Ex",Type("fun",[Type("fun",[T,Type("bool",[])]),Type("bool",[])])) $ -(Abs(x,T, -abstract_over(Free(f,T), -Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) -$ -(Const("op =",Type("fun",[T,Type("fun",[T,Type("bool",[])])])) $ (Free(f,T)) $ trm) -$ s)))) -end | -enrich_case_with_terms sg (a::r) (Abs(x,T,t)) = - enrich_case_with_terms sg [a] (Abs(x,T,(enrich_case_with_terms sg r t))) | -enrich_case_with_terms sg (t::r) trm = -let val ty = type_of_term t -in -(Const("Ex",Type("fun",[Type("fun",[ ty ,Type("bool",[])]),Type("bool",[])])) $ -Abs("a", ty, -Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) -$ -(Const("op =",Type("fun",[ ty ,Type("fun",[ ty ,Type("bool",[])])])) $ Bound(0) $ t) -$ -enrich_case_with_terms sg r (trm $ (Bound(length(r)))))) -end; - -fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t = -let - fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(Syntax.variant_abs(x,T,t))) | - heart_of_trm t = t; - fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) | - replace_termlist_with_args sg _ trm _ [a] _ ([],[]) = - if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else - (enrich_case_with_terms sg a trm) | - replace_termlist_with_args sg tl trm con [] t (l1,l2) = - (replace_termlist_with_constrs sg tl l1 l2 t) | - replace_termlist_with_args sg tl trm con (a::r) t (l1,l2) = - let - val tty = type_of_term t; - val con_term = con_term_of con a; - in - (Const("HOL.If",Type("fun",[Type("bool",[]), - Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $ - (Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $ - t $ con_term) $ - (if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else - (enrich_case_with_terms sg a trm)) $ - (replace_termlist_with_args sg tl trm con r t (l1,l2))) - end; - val arglist = arglist_of sg tl (snd c); - val tty = type_of_term t; - val con_typ = fun_type_of (rev (snd c)) tty; - val con = OldGoals.simple_read_term sg con_typ (fst c); -in - replace_termlist_with_args sg tl a con arglist t (l1,l2) -end | -replace_termlist_with_constrs _ _ _ _ _ = -error "malformed arguments in replace_termlist_with_constrs" (* shouldnt occur *); - -(* rc_in_termlist constructs a cascading if with the case terms in trm_list, *) -(* which were found in rc_in_term (see replace_case) *) -fun rc_in_termlist sg tl trm_list trm = -let - val ty = type_of_term trm; - val constr_list = search_in_keylist tl ty; -in - replace_termlist_with_constrs sg tl trm_list constr_list trm -end; - -in - -(* replace_case replaces each case statement over a complex datatype by a cascading if; *) -(* it is normally called with a 0 in the 4th argument, it is positive, if in the course *) -(* of calculation, a "case" is discovered and then indicates the distance to that case *) -fun replace_case sg tl (a $ b) 0 = -let - (* rc_in_term changes the case statement over term x to a cascading if; the last *) - (* indicates the distance to the "case"-constant *) - fun rc_in_term sg tl (a $ b) l x 0 = - (replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) | - rc_in_term sg tl _ l x 0 = rc_in_termlist sg tl l x | - rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) | - rc_in_term sg _ trm _ _ n = - error("malformed term for case-replacement: " ^ (Syntax.string_of_term_global sg trm)); - val (bv,n) = check_case sg tl (a $ b); -in - if (bv) then - (let - val t = (replace_case sg tl a n) - in - rc_in_term sg tl t [] b n - end) - else ((replace_case sg tl a 0) $ (replace_case sg tl b 0)) -end | -replace_case sg tl (a $ b) 1 = a $ (replace_case sg tl b 0) | -replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) | -replace_case sg tl (Abs(x,T,t)) _ = -let - val v = Syntax.variant_abs(x,T,t); - val f = fst v; - val s = snd v -in - Abs(x,T,abstract_over(Free(f,T),replace_case sg tl s 0)) -end | -replace_case _ _ t _ = t; - -end; - -(*******************************************************************) -(* SECTION 3: replacing variables being part of a constructor term *) - -(* transforming terms so that nowhere a variable is subterm of *) -(* a constructor term; the transformation uses cascading ifs *) -fun remove_vars sg tl (Abs(x,ty,trm)) = -let -(* checks freeness of variable x in term *) -fun xFree x (a $ b) = if (xFree x a) then true else (xFree x b) | -xFree x (Abs(a,T,trm)) = xFree x trm | -xFree x (Free(y,_)) = if (x=y) then true else false | -xFree _ _ = false; -(* really substitues variable x by term c *) -fun real_subst sg tl x c (a$b) = (real_subst sg tl x c a) $ (real_subst sg tl x c b) | -real_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,real_subst sg tl x c trm) | -real_subst sg tl x c (Free(y,t)) = if (x=y) then c else Free(y,t) | -real_subst sg tl x c t = t; -(* substituting variable x by term c *) -fun x_subst sg tl x c (a $ b) = -let - val t = (type_of_term (a $ b)) -in - if ((list_contains_key tl t) andalso (xFree x (a$b))) - then (real_subst sg tl x c (a$b)) else ((x_subst sg tl x c a) $ (x_subst sg tl x c b)) -end | -x_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,x_subst sg tl x c trm) | -x_subst sg tl x c t = t; -(* genearting a cascading if *) -fun casc_if sg tl x ty (c::l) trm = -let - val arglist = arglist_of sg tl (snd c); - val con_typ = fun_type_of (rev (snd c)) ty; - val con = OldGoals.simple_read_term sg con_typ (fst c); - fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *) - casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm | - casc_if2 sg tl x con (a::r) ty trm cl = - Const("HOL.If",Type("fun",[Type("bool",[]), - Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]) - ])) $ - (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $ - Free(x,ty) $ (real_subst sg tl x (con_term_of con a) (Free(x,ty)))) $ - (x_subst sg tl x (con_term_of con a) trm) $ - (casc_if2 sg tl x con r ty trm cl) | - casc_if2 sg tl x con [] ty trm cl = casc_if sg tl x ty cl trm; -in - casc_if2 sg tl x con arglist ty trm l -end | -casc_if _ _ _ _ [] trm = trm (* should never occur *); -fun if_term sg tl x ty trm = -let - val tyC_list = search_in_keylist tl ty; -in - casc_if sg tl x ty tyC_list trm -end; -(* checking whether a variable occurs in a constructor term *) -fun constr_term_contains_var sg tl (a $ b) x = -let - val t = type_of_term (a $ b) -in - if ((list_contains_key tl t) andalso (xFree x (a$b))) then true - else - (if (constr_term_contains_var sg tl a x) then true - else (constr_term_contains_var sg tl b x)) -end | -constr_term_contains_var sg tl (Abs(y,ty,trm)) x = - constr_term_contains_var sg tl (snd(Syntax.variant_abs(y,ty,trm))) x | -constr_term_contains_var _ _ _ _ = false; -val vt = Syntax.variant_abs(x,ty,trm); -val tt = remove_vars sg tl (snd(vt)) -in -if (constr_term_contains_var sg tl tt (fst vt)) -(* fst vt muss frei vorkommen, als ECHTER TeilKonstruktorterm *) -then (Abs(x,ty, - abstract_over(Free(fst vt,ty), - if_term sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) (fst vt) ty tt))) -else Abs(x,ty,abstract_over(Free(fst vt,ty),tt)) -end | -remove_vars sg tl (a $ b) = (remove_vars sg tl a) $ (remove_vars sg tl b) | -remove_vars sg tl t = t; - -(* dissolves equalities "=" of boolean terms, where one of them is a complex term *) -fun remove_equal sg tl (Abs(x,ty,trm)) = Abs(x,ty,remove_equal sg tl trm) | -remove_equal sg tl (Const("op =",Type("fun",[Type("bool",[]), - Type("fun",[Type("bool",[]),Type("bool",[])])])) $ lhs $ rhs) = -let -fun complex_trm (Abs(_,_,_)) = true | -complex_trm (_ $ _) = true | -complex_trm _ = false; -in -(if ((complex_trm lhs) orelse (complex_trm rhs)) then -(let -val lhs = remove_equal sg tl lhs; -val rhs = remove_equal sg tl rhs -in -( -Const("op &", -Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ -(Const("op -->", - Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ - lhs $ rhs) $ -(Const("op -->", - Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ - rhs $ lhs) -) -end) -else -(Const("op =", - Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ - lhs $ rhs)) -end | -remove_equal sg tl (a $ b) = (remove_equal sg tl a) $ (remove_equal sg tl b) | -remove_equal sg tl trm = trm; - -(* rewrites constructor terms (without vars) for mucke *) -fun rewrite_dt_term sg tl (Abs(x,ty,t)) = Abs(x,ty,(rewrite_dt_term sg tl t)) | -rewrite_dt_term sg tl (a $ b) = -let - -(* OUTPUT - relevant *) -(* transforms constructor term to a mucke-suitable output *) -fun term_OUTPUT sg (Const(@{const_name Pair},_) $ a $ b) = - (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) | -term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) | -term_OUTPUT sg (Const(s,t)) = post_last_dot s | -term_OUTPUT _ _ = -error "term contains an unprintable constructor term (in term_OUTPUT)"; - -fun contains_bound i (Bound(j)) = if (j>=i) then true else false | -contains_bound i (a $ b) = if (contains_bound i a) then true else (contains_bound i b) | -contains_bound i (Abs(_,_,t)) = contains_bound (i+1) t | -contains_bound _ _ = false; - -in - if (contains_bound 0 (a $ b)) - then ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b)) - else - ( - let - val t = type_of_term (a $ b); - in - if (list_contains_key tl t) then (Const((term_OUTPUT sg (a $ b)),t)) else - ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b)) - end) -end | -rewrite_dt_term sg tl t = t; - -fun rewrite_dt_terms sg tl [] = [] | -rewrite_dt_terms sg tl (a::r) = -let - val c = (replace_case sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) a 0); - val rv = (remove_vars sg tl c); - val rv = (remove_equal sg tl rv); -in - ((rewrite_dt_term sg tl rv) - :: (rewrite_dt_terms sg tl r)) -end; - -(**********************************************************************) -(* SECTION 4: generating type declaration and preprocessing type list *) - -fun make_type_decls [] tl = "" | -make_type_decls ((a,l)::r) tl = -let -fun comma_list_of [] = "" | -comma_list_of (a::[]) = a | -comma_list_of (a::r) = a ^ "," ^ (comma_list_of r); - -(* OUTPUT - relevant *) -(* produces for each type of the 2nd argument its constant names (see *) -(* concat_constr) and appends them to prestring (see concat_types) *) -fun generate_constnames_OUTPUT prestring [] _ = [prestring] | -generate_constnames_OUTPUT prestring ((Type("*",[a,b]))::r) tl = - generate_constnames_OUTPUT prestring (a::b::r) tl | -generate_constnames_OUTPUT prestring (a::r) tl = -let - fun concat_constrs [] _ = [] | - concat_constrs ((c,[])::r) tl = c::(concat_constrs r tl) | - concat_constrs ((c,l)::r) tl = - (generate_constnames_OUTPUT (c ^ "_I_") l tl) @ (concat_constrs r tl); - fun concat_types _ [] _ _ = [] | - concat_types prestring (a::q) [] tl = [prestring ^ a] - @ (concat_types prestring q [] tl) | - concat_types prestring (a::q) r tl = - (generate_constnames_OUTPUT (prestring ^ a ^ "_I_") r tl) - @ (concat_types prestring q r tl); - val g = concat_constrs (search_in_keylist tl a) tl; -in - concat_types prestring g r tl -end; - -fun make_type_decl a tl = -let - val astr = type_to_string_OUTPUT a; - val dl = generate_constnames_OUTPUT "" [a] tl; - val cl = comma_list_of dl; -in - ("enum " ^ astr ^ " {" ^ cl ^ "};\n") -end; -in - (make_type_decl a tl) ^ (make_type_decls r tl) -end; - -fun check_finity gl [] [] true = true | -check_finity gl bl [] true = (check_finity gl [] bl false) | -check_finity _ _ [] false = -error "used datatypes are not finite" | -check_finity gl bl ((t,cl)::r) b = -let -fun listmem [] _ = true | -listmem (a::r) l = if member (op =) l a then (listmem r l) else false; -fun snd_listmem [] _ = true | -snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false; -in -(if (snd_listmem cl gl) then (check_finity (t::gl) bl r true) -else (check_finity gl ((t,cl)::bl) r b)) -end; - -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 | -extract_hd sg (Var(_,_) $ r) = extract_hd sg r | -extract_hd sg (a $ b) = extract_hd sg a | -extract_hd sg (Const(s,t)) = post_last_dot s | -extract_hd _ _ = -error "malformed constructor term in a induct-theorem"; -fun list_of_param_types sg tl pl (_ $ Abs(_,t,r)) = -let - fun select_type [] [] t = t | - select_type (a::r) (b::s) t = - if (t=b) then a else (select_type r s t) | - select_type _ _ _ = - error "wrong number of argument of a constructor in a induct-theorem"; -in - (select_type tl pl t) :: (list_of_param_types sg tl pl r) -end | -list_of_param_types sg tl pl (Const("Trueprop",_) $ r) = list_of_param_types sg tl pl r | -list_of_param_types _ _ _ _ = []; -fun split_constr sg tl pl a = (extract_hd sg a,list_of_param_types sg tl pl a); -fun split_constrs _ _ _ [] = [] | -split_constrs sg tl pl (a::r) = (split_constr sg tl pl a) :: (split_constrs sg tl pl r); -fun new_types [] = [] | -new_types ((t,l)::r) = -let - fun ex_bool [] = [] | - ex_bool ((Type("bool",[]))::r) = ex_bool r | - ex_bool ((Type("*",[a,b]))::r) = ex_bool (a::b::r) | - ex_bool (s::r) = s:: (ex_bool r); - val ll = ex_bool l -in - (ll @ (new_types r)) -end; -in - if member (op =) done a - then (preprocess_td sg b done) - else - (let - fun qtn (Type(a,tl)) = (a,tl) | - qtn _ = error "unexpected type variable in preprocess_td"; - 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 induct_rule = PureThy.get_thm sg (s ^ ".induct"); - val pl = param_types (concl_of induct_rule); - val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule); - val ntl = new_types l; - in - ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done))) - end) -end; - -fun extract_type_names_prems sg [] = [] | -extract_type_names_prems sg (a::b) = -let -fun analyze_types sg [] = [] | -analyze_types sg [Type(a,[])] = -(let - val s = (Syntax.string_of_typ_global sg (Type(a,[]))) -in - (if (s="bool") then ([]) else ([Type(a,[])])) -end) | -analyze_types sg [Type("*",l)] = analyze_types sg l | -analyze_types sg [Type("fun",l)] = analyze_types sg l | -analyze_types sg [Type(t,l)] = ((Type(t,l))::(analyze_types sg l)) | -analyze_types sg (a::l) = (analyze_types sg [a]) @ (analyze_types sg l); -fun extract_type_names sg (Const("==",_)) = [] | -extract_type_names sg (Const("Trueprop",_)) = [] | -extract_type_names sg (Const(_,typ)) = analyze_types sg [typ] | -extract_type_names sg (a $ b) = (extract_type_names sg a) @ (extract_type_names sg b) | -extract_type_names sg (Abs(x,T,t)) = (analyze_types sg [T]) @ (extract_type_names sg t) | -extract_type_names _ _ = []; -in - (extract_type_names sg a) @ extract_type_names_prems sg b -end; - -(**********************************************************) - -fun mk_mc_mucke_oracle csubgoal = - let - val sign = Thm.theory_of_cterm csubgoal; - val subgoal = Thm.term_of csubgoal; - - val Freesubgoal = freeze_thaw subgoal; - - val prems = Logic.strip_imp_prems Freesubgoal; - val concl = Logic.strip_imp_concl Freesubgoal; - - val Muckedecls = terms_to_decls sign prems; - val decls_str = string_of_terms sign Muckedecls; - - val type_list = (extract_type_names_prems sign (prems@[concl])); - 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); - - val mprems = rewrite_dt_terms sign ctl prems; - val mconcl = rewrite_dt_terms sign ctl [concl]; - - val Muckeprems = transform_terms sign mprems; - val prems_str = transform_case(string_of_terms sign Muckeprems); - - val Muckeconcl = elim_quant_in_list sign mconcl; - val concl_str = transform_case(string_of_terms sign Muckeconcl); - - val MCstr = ( - "/**** type declarations: ****/\n" ^ type_str ^ - "/**** declarations: ****/\n" ^ decls_str ^ - "/**** definitions: ****/\n" ^ prems_str ^ - "/**** formula: ****/\n" ^ concl_str ^";"); - val result = callmc MCstr; - in -(if !trace_mc then - (writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/")) - else (); -(case (extract_result concl_str result) of - true => cterm_of sign (Logic.strip_imp_concl subgoal) | - false => (error ("Mucke couldn't solve subgoal: \n" ^result)))) - end;
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -theory Cockpit -imports MuIOAOracle -begin - -datatype 'a action = Alarm 'a | Info 'a | Ack 'a -datatype event = NONE | PonR | Eng | Fue - - -text {* - This cockpit automaton is a deeply simplified version of the - control component of a helicopter alarm system considered in a study - of ESG. Some properties will be proved by using model checker - mucke. *} - -automaton cockpit = - signature - actions "event action" - inputs "Alarm a" - outputs "Ack a", "Info a" - states - APonR_incl :: bool - info :: event - initially "info = NONE & ~APonR_incl" - transitions - "Alarm a" - post info := "if (a=NONE) then info else a", - APonR_incl := "if (a=PonR) then True else APonR_incl" - "Info a" - pre "(a=info)" - "Ack a" - pre "(a=PonR --> APonR_incl) & (a=NONE --> ~APonR_incl)" - post info := "NONE", - APonR_incl := "if (a=PonR) then False else APonR_incl" - -automaton cockpit_hide = hide_action "Info a" in cockpit - -text {* - Subsequent automata express the properties to be proved, see also - Cockpit.ML *} - -automaton Al_before_Ack = - signature - actions "event action" - inputs "Alarm a" - outputs "Ack a" - states - APonR_incl :: bool - initially "~APonR_incl" - transitions - "Alarm a" - post APonR_incl:="if (a=PonR) then True else APonR_incl" - "Ack a" - pre "(a=PonR --> APonR_incl)" - post APonR_incl:="if (a=PonR) then False else APonR_incl" - -automaton Info_while_Al = - signature - actions "event action" - inputs "Alarm a" - outputs "Ack a", "Info i" - states - info_at_Pon :: bool - initially "~info_at_Pon" - transitions - "Alarm a" - post - info_at_Pon:="if (a=PonR) then True else (if (a=NONE) then info_at_Pon else False)" - "Info a" - pre "(a=PonR) --> info_at_Pon" - "Ack a" - post info_at_Pon:="False" - -automaton Info_before_Al = - signature - actions "event action" - inputs "Alarm a" - outputs "Ack a", "Info i" - states - info_at_NONE :: bool - initially "info_at_NONE" - transitions - "Alarm a" - post info_at_NONE:="if (a=NONE) then info_at_NONE else False" - "Info a" - pre "(a=NONE) --> info_at_NONE" - "Ack a" - post info_at_NONE:="True" - -lemmas aut_simps = - cockpit_def cockpit_asig_def cockpit_trans_def - cockpit_initial_def cockpit_hide_def - Al_before_Ack_def Al_before_Ack_asig_def - Al_before_Ack_initial_def Al_before_Ack_trans_def - Info_while_Al_def Info_while_Al_asig_def - Info_while_Al_initial_def Info_while_Al_trans_def - Info_before_Al_def Info_before_Al_asig_def - Info_before_Al_initial_def Info_before_Al_trans_def - - -(* to prove, that info is always set at the recent alarm *) -lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al" -apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) -done - -(* to prove that before any alarm arrives (and after each acknowledgment), - info remains at None *) -lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al" -apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) -done - -(* to prove that before any alarm would be acknowledged, it must be arrived *) -lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack" -apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) -apply auto -done - -end
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,302 +0,0 @@ -theory MuIOA -imports IOA "../../../HOL/Modelcheck/MuckeSyn" -begin - -consts - Internal_of_A :: "'a => bool" - Internal_of_C :: "'a => bool" - Start_of_A :: "'a => bool" - Start_of_C :: "'a => bool" - Trans_of_A :: "'a => 'b => bool" - Trans_of_C :: "'a => 'b => bool" - IntStep_of_A :: "'a => bool" - IntStepStar_of_A :: "'a => bool" - Move_of_A :: "'a => 'b => bool" - isSimCA :: "'a => bool" - -ML {* - -(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy). - There, implementation relations for I/O automatons are proved using - the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *) - -exception SimFailureExn of string; - -val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"]; -val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def", - thm "asig_internals_def", thm "actions_def"]; -val comp_simps = [thm "par_def", thm "asig_comp_def"]; -val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"]; -val hide_simps = [thm "hide_def", thm "hide_asig_def"]; -val rename_simps = [thm "rename_def", thm "rename_set_def"]; - -local - -exception malformed; - -fun fst_type (Type(@{type_name prod},[a,_])) = a | -fst_type _ = raise malformed; -fun snd_type (Type(@{type_name prod},[_,a])) = a | -snd_type _ = raise malformed; - -fun element_type (Type("set",[a])) = a | -element_type t = raise malformed; - -fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = -let -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); -val sig_typ = fst_type aut_typ; -val int_typ = fst_type sig_typ -in -Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $ - (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA) -end -| -IntC sg t = -error("malformed automaton def for IntC:\n" ^ (Syntax.string_of_term_global sg t)); - -fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = -let -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); -val st_typ = fst_type(snd_type aut_typ) -in -Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA -end -| -StartC sg t = -error("malformed automaton def for StartC:\n" ^ (Syntax.string_of_term_global sg t)); - -fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = -let -val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); -val tr_typ = fst_type(snd_type(snd_type aut_typ)) -in -Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA -end -| -TransC sg t = -error("malformed automaton def for TransC:\n" ^ (Syntax.string_of_term_global sg t)); - -fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = -let -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); -val sig_typ = fst_type aut_typ; -val int_typ = fst_type sig_typ -in -Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $ - (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA) -end -| -IntA sg t = -error("malformed automaton def for IntA:\n" ^ (Syntax.string_of_term_global sg t)); - -fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = -let -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); -val st_typ = fst_type(snd_type aut_typ) -in -Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA -end -| -StartA sg t = -error("malformed automaton def for StartA:\n" ^ (Syntax.string_of_term_global sg t)); - -fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = -let -val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); -val tr_typ = fst_type(snd_type(snd_type aut_typ)) -in -Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA -end -| -TransA sg t = -error("malformed automaton def for TransA:\n" ^ (Syntax.string_of_term_global sg t)); - -fun delete_ul [] = [] -| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_ul s end) - else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_ul s end) - else (x::delete_ul xs)); - -fun delete_ul_string s = implode(delete_ul (explode s)); - -fun type_list_of sign (Type(@{type_name prod},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) | -type_list_of sign a = [(Syntax.string_of_typ_global sign a)]; - -fun structured_tuple l (Type(@{type_name prod},s::t::_)) = -let -val (r,str) = structured_tuple l s; -in -(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")") -end | -structured_tuple (a::r) t = (r,a) | -structured_tuple [] _ = raise malformed; - -fun varlist_of _ _ [] = [] | -varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r); - -fun string_of [] = "" | -string_of (a::r) = a ^ " " ^ (string_of r); - -fun tupel_typed_of _ _ _ [] = "" | -tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a | -tupel_typed_of sign s n (a::r) = - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r); - -fun double_tupel_typed_of _ _ _ _ [] = "" | -double_tupel_typed_of sign s t n [a] = - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ - t ^ (Int.toString(n)) ^ "::" ^ a | -double_tupel_typed_of sign s t n (a::r) = - s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ - t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r); - -fun tupel_of _ _ _ [] = "" | -tupel_of sign s n [a] = s ^ (Int.toString(n)) | -tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r); - -fun double_tupel_of _ _ _ _ [] = "" | -double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^ - t ^ (Int.toString(n)) | -double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^ - t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r); - -fun eq_string _ _ _ [] = "" | -eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^ - t ^ (Int.toString(n)) | -eq_string s t n (a::r) = - s ^ (Int.toString(n)) ^ " = " ^ - t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r); - -fun merge_var_and_type [] [] = "" | -merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) | -merge_var_and_type _ _ = raise malformed; - -in - -fun mk_sim_oracle (csubgoal, thl) = - let - val sign = Thm.theory_of_cterm csubgoal; - val subgoal = Thm.term_of csubgoal; - in - (let - val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) sign; - val concl = Logic.strip_imp_concl subgoal; - val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl)); - val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl)); - val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl)); - val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl)); - val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl)); - val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl)); - - val action_type_str = - Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl))))); - - val abs_state_type_list = - type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl))))); - val con_state_type_list = - type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl))))); - - val tupel_eq = eq_string "s" "t" 0 abs_state_type_list; - - val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list; - val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list; - val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list; - val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list; - - val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list; - val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list; - val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list; - val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list; - val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list; - val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list; - val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list; - val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list; - val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list; - val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list; - - val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list; - val abs_post_varlist = varlist_of 0 "t" abs_state_type_list; - val abs_u_varlist = varlist_of 0 "u" abs_state_type_list; - val abs_v_varlist = varlist_of 0 "v" abs_state_type_list; - val con_pre_varlist = varlist_of 0 "cs" con_state_type_list; - val con_post_varlist = varlist_of 0 "ct" con_state_type_list; - - val abs_post_str = string_of abs_post_varlist; - val abs_u_str = string_of abs_u_varlist; - val con_post_str = string_of con_post_varlist; - - val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list; - val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list; - val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list; - val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list; - - val abs_pre_tupel_struct = snd( -structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl)))))); - val abs_post_tupel_struct = snd( -structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl)))))); - val con_pre_tupel_struct = snd( -structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl)))))); - val con_post_tupel_struct = snd( -structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl)))))); -in -( -OldGoals.push_proof(); -OldGoals.Goal -( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^ - "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ - "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^ - "). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^ - "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^ - "). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^ - "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ - ")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^ - "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ - ")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^ - "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ - "). ? (a::(" ^ action_type_str ^ - ")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^ - ")) --> (IntStepStar_of_A = mu (% P (" ^ abs_s_t_tupel_typed ^ - "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^ - ") & P(" ^ abs_u_t_tupel ^ ")))" ^ - ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ - ")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ - ")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^ - ". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^ - "Trans_of_A (" ^ abs_u_v_tupel ^ ") a & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^ - ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ - "). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^ - ". Trans_of_C (" ^ con_s_t_tupel ^ ") a -->" ^ " (? " ^ abs_post_str ^ - ". Move_of_A (" ^ abs_s_t_tupel ^ ") a & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^ - ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^ - ". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^ - ")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))"); -OldGoals.by (REPEAT (rtac impI 1)); -OldGoals.by (REPEAT (dtac eq_reflection 1)); -(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) -OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) - delsimps [not_iff, @{thm split_part}]) - addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ - rename_simps @ ioa_simps @ asig_simps)) 1); -OldGoals.by (full_simp_tac - (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1); -OldGoals.by (REPEAT (if_full_simp_tac - (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1)); -OldGoals.by (call_mucke_tac 1); -(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) -OldGoals.by (atac 1); -OldGoals.result(); -OldGoals.pop_proof(); -Thm.cterm_of sign (Logic.strip_imp_concl subgoal) -) -end) -handle malformed => -error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal)) -end; - -end - -*} - -end
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -theory MuIOAOracle -imports MuIOA -begin - -oracle sim_oracle = mk_sim_oracle - -ML {* -(* call_sim_tac invokes oracle "Sim" *) -fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) => -let val OraAss = sim_oracle (csubgoal,thm_list); -in cut_facts_tac [OraAss] i end); - - -val ioa_implements_def = thm "ioa_implements_def"; - -(* is_sim_tac makes additionally to call_sim_tac some simplifications, - which are suitable for implementation realtion formulas *) -fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) => - EVERY [REPEAT (etac thin_rl i), - simp_tac (ss addsimps [ioa_implements_def]) i, - rtac conjI i, - rtac conjI (i+1), - TRY(call_sim_tac thm_list (i+2)), - TRY(atac (i+2)), - REPEAT(rtac refl (i+2)), - simp_tac (ss addsimps (thm_list @ - comp_simps @ restrict_simps @ hide_simps @ - rename_simps @ ioa_simps @ asig_simps)) (i+1), - simp_tac (ss addsimps (thm_list @ - comp_simps @ restrict_simps @ hide_simps @ - rename_simps @ ioa_simps @ asig_simps)) (i)]); - -*} - -end
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOLCF/IOA/Modelcheck/ROOT.ML - Author: Olaf Mueller and Tobias Hamberger, TU Muenchen - -Modelchecker setup for I/O automata. -*) - -time_use_thy "MuIOAOracle"; - -(*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 (); - -(*examples*) -if_mucke_enabled time_use_thy "Cockpit"; -if_mucke_enabled time_use_thy "Ring3";
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,118 +0,0 @@ -theory Ring3 -imports MuIOAOracle -begin - -datatype token = Leader | id0 | id1 | id2 | id3 | id4 - -datatype Comm = - Zero_One token | One_Two token | Two_Zero token | - Leader_Zero | Leader_One | Leader_Two - -definition - Greater :: "[token, token] => bool" where - "Greater x y = - (x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) | - (x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)" - - -(*the ring is the composition of aut0, aut1 and aut2*) - -automaton aut0 = - signature - actions Comm - inputs "Two_Zero t" - outputs "Zero_One t","Leader_Zero" - states - idf :: token - initially "idf=id0 | idf = id3" - transitions - "Two_Zero t" - transrel - "if (t=id0 | t=id3) then (idf'=Leader) else - (if (Greater t idf) then (idf'=t) else (idf'=idf))" - "Zero_One t" - pre "t=idf" - "Leader_Zero" - pre "idf=Leader" - -automaton aut1 = - signature - actions Comm - inputs "Zero_One t" - outputs "One_Two t","Leader_One" - states - idf :: token - initially "idf=id1 | idf=id4" - transitions - "Zero_One t" - transrel - "if (t=id1 | t=id4) then (idf'=Leader) else - (if (Greater t idf) then (idf'=t) else (idf'=idf))" - "One_Two t" - pre "t=idf" - "Leader_One" - pre "idf=Leader" - -automaton aut2 = - signature - actions Comm - inputs "One_Two t" - outputs "Two_Zero t","Leader_Two" - states - idf :: token - initially "idf=id2" - transitions - "One_Two t" - transrel - "if (t=id2) then (idf'=Leader) else - (if (Greater t idf) then (idf'=t) else (idf'=idf))" - "Two_Zero t" - pre "t=idf" - "Leader_Two" - pre "idf=Leader" - -automaton ring = compose aut0, aut1, aut2 - - -(*one_leader expresses property that at most one component declares - itself to leader*) - -automaton one_leader = - signature - actions Comm - outputs "Zero_One t","One_Two t","Two_Zero t","Leader_Zero","Leader_One","Leader_Two" - states - leader :: token - initially "leader=Leader" - transitions - "Zero_One t" - pre "True" - "One_Two t" - pre "True" - "Two_Zero t" - pre "True" - "Leader_Zero" - pre "leader=id0 | leader=Leader" - post leader:="id0" - "Leader_One" - pre "leader=id1 | leader=Leader" - post leader:="id1" - "Leader_Two" - pre "leader=id2 | leader=Leader" - post leader:="id2" - -lemmas aut_simps = - Greater_def one_leader_def - one_leader_asig_def one_leader_trans_def one_leader_initial_def - ring_def aut0_asig_def aut0_trans_def aut0_initial_def aut0_def - aut1_asig_def aut1_trans_def aut1_initial_def aut1_def - aut2_asig_def aut2_trans_def aut2_initial_def aut2_def - -(* property to prove: at most one (of 3) members of the ring will - declare itself to leader *) -lemma at_most_one_leader: "ring =<| one_leader" -apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) -apply auto -done - -end
--- a/src/HOLCF/IsaMakefile Mon Jul 12 20:21:39 2010 +0200 +++ b/src/HOLCF/IsaMakefile Mon Jul 12 20:35:10 2010 +0200 @@ -6,10 +6,16 @@ default: HOLCF images: HOLCF IOA -test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ +test: \ + HOLCF-FOCUS \ + HOLCF-IMP \ HOLCF-Library \ HOLCF-Tutorial \ - IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex + HOLCF-ex \ + IOA-ABP \ + IOA-NTP \ + IOA-Storage \ + IOA-ex all: images test @@ -189,16 +195,6 @@ @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP -## IOA-Modelcheck - -IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz - -$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ - IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ - IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy - @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck - - ## IOA-Storage IOA-Storage: IOA $(LOG)/IOA-Storage.gz @@ -223,6 +219,5 @@ @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ - $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \ - $(LOG)/HOLCF-Library.gz \ + $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \ $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz