# HG changeset patch
# User wenzelm
# Date 935092150 -7200
# Node ID 743b22579a2f1e00d08f0459aad99421f443b9c9
# Parent  e49024d43c106f8023976974381da06c26ae5cd3
quite a lot of tuning and cleanup;

diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/Cockpit.ML
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Aug 19 21:49:10 1999 +0200
@@ -1,3 +1,4 @@
+
 val 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,
@@ -7,23 +8,20 @@
 		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 *)
-goal thy "cockpit =<| Info_while_Al";
-by (is_sim_tac thy aut_simps 1);
+Goal "cockpit =<| Info_while_Al";
+by (is_sim_tac aut_simps 1);
 qed"cockpit_implements_Info_while_Al";
 
-(* to prove that before any alarm arrives (and after each acknowledgement),
-	 info remains at None *)
-goal thy "cockpit =<| Info_before_Al";
-by (is_sim_tac thy aut_simps 1);       
+(* to prove that before any alarm arrives (and after each acknowledgment),
+   info remains at None *)
+Goal "cockpit =<| Info_before_Al";
+by (is_sim_tac aut_simps 1);       
 qed"cockpit_implements_Info_before_Al";
 
-(* to prove that before any alarm vould be acknowledged, it must be arrived *)
-goal thy "cockpit_hide =<| Al_before_Ack";
-by (is_sim_tac thy aut_simps 1);       
+(* to prove that before any alarm would be acknowledged, it must be arrived *)
+Goal "cockpit_hide =<| Al_before_Ack";
+by (is_sim_tac aut_simps 1);       
 by Auto_tac;
 qed"cockpit_implements_Al_before_Ack";
-
-*)	
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/Cockpit.thy
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Thu Aug 19 21:49:10 1999 +0200
@@ -1,80 +1,86 @@
-Cockpit = MuIOAOracle + 
 
-datatype ('a)action = Alarm 'a | Info 'a | Ack 'a
+Cockpit = MuIOAOracle +
+
+datatype 'a action = Alarm 'a | Info 'a | Ack 'a
 datatype event = None | PonR | Eng | Fue
 
-(* 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 *)
+
+(*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"
+  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 "Info a" in cockpit
 
-(* following automatons express the properties to be proved, see Cockpit.ML *)
+
+(*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"
+  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"
+  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"
+  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"
 
 end
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Aug 19 21:49:10 1999 +0200
@@ -1,8 +1,9 @@
+
 (* 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 SimOracleExn of (term*theory*(thm list));
+exception SimOracleExn of (term*(thm list));
 exception SimFailureExn of string;
 
 val ioa_simps = [asig_of_def,starts_of_def,trans_of_def];
@@ -161,7 +162,7 @@
 
 in
 
-fun mk_sim_oracle (sign, SimOracleExn (subgoal,t,thl)) =
+fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) =
 (let
 	val concl = (Logic.strip_imp_concl subgoal);
 
@@ -225,7 +226,7 @@
 in
 (
 push_proof();
-goal t 
+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 ^
@@ -262,7 +263,7 @@
                                         rename_simps @ ioa_simps @ asig_simps)) 1);
 by (full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) 1);
 by (REPEAT (if_full_simp_tac (simpset() delsimps [not_iff,split_part]) 1));
-by (call_mucke_tac t 1);
+by (call_mucke_tac 1);
 (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
 by (atac 1);
 result();
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Aug 19 21:49:10 1999 +0200
@@ -1,15 +1,16 @@
+
 MuIOA = IOA + MuckeSyn +
 
 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
+  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
 
 end
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Aug 19 21:49:10 1999 +0200
@@ -1,25 +1,16 @@
-(*
-Folgende Theoremlisten wurden in MuIOA.ML definiert: 
-val ioa_simps = [asig_of_def,starts_of_def,trans_of_def];
-val asig_simps = [asig_inputs_def,asig_outputs_def,asig_internals_def,actions_def];
-val comp_simps = [par_def,asig_comp_def];
-val restrict_simps = [restrict_def,restrict_asig_def];
-val hide_simps = [hide_def,hide_asig_def];
-val rename_simps = [rename_def,rename_set_def];
-*)
 
 (* call_sim_tac invokes oracle "Sim" *)
-fun call_sim_tac theory thm_list i state = 
+fun call_sim_tac thm_list i state = 
 let val sign = #sign (rep_thm state);
         val (subgoal::_) = drop(i-1,prems_of state);
-        val OraAss = invoke_oracle theory "Sim" (sign,SimOracleExn (subgoal,theory,thm_list));
+        val OraAss = invoke_oracle MuIOAOracle.thy "Sim" (sign,SimOracleExn (subgoal,thm_list));
 in
 (cut_facts_tac [OraAss] i) state
 end;
 
 (* is_sim_tac makes additionally to call_sim_tac some simplifications,
 	which are suitable for implementation realtion formulas *)
-fun is_sim_tac theory thm_list i state =
+fun is_sim_tac thm_list i state =
 let val sign = #sign (rep_thm state);
 in
 case drop(i-1,prems_of state) of
@@ -28,7 +19,7 @@
                         simp_tac (simpset() addsimps [ioa_implements_def]) i,
                         rtac conjI i,
                         rtac conjI (i+1),
-			TRY(call_sim_tac theory thm_list (i+2)),
+			TRY(call_sim_tac thm_list (i+2)),
 			TRY(atac (i+2)), 
                         REPEAT(rtac refl (i+2)),
 	 		simp_tac (simpset() addsimps (thm_list @
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Aug 19 21:49:10 1999 +0200
@@ -1,6 +1,7 @@
+
 MuIOAOracle = MuIOA +
 
 oracle
-Sim = mk_sim_oracle
+  Sim = mk_sim_oracle
 
 end
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/ROOT.ML
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Aug 19 21:49:10 1999 +0200
@@ -1,10 +1,8 @@
 (*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
     ID:         $Id$
-    Author:     Olaf Mueller
-    Copyright   1997  TU Muenchen
+    Author:     Olaf Mueller and Tobias Hamberger, TU Muenchen
 
-This is the ROOT file for the formalization of a semantic model of
-I/O-Automata.  See the README.html file for details.
+Modelchecker setup for I/O automata.
 *)
 
 goals_limit := 1;
@@ -12,5 +10,7 @@
 use "../../../HOL/Modelcheck/mucke_oracle.ML";
 use_thy "../../../HOL/Modelcheck/MuckeSyn";
 use_thy "MuIOAOracle";
-use_thy "Cockpit";
-use_thy "Ring3";
+
+(*examples*)
+if_mucke_enabled use_thy "Cockpit";
+if_mucke_enabled use_thy "Ring3";
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/Ring3.ML
--- a/src/HOLCF/IOA/Modelcheck/Ring3.ML	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.ML	Thu Aug 19 21:49:10 1999 +0200
@@ -1,14 +1,16 @@
+
 val 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];
+  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 *)
-goal thy "ring =<| one_leader";
-(* by (is_sim_tac thy aut_simps 1); 
+Goal "ring =<| one_leader";
+(*
+FIXME
+by (is_sim_tac aut_simps 1); 
 by Auto_tac;
 qed"at_most_one_leader";
 *)
-
diff -r e49024d43c10 -r 743b22579a2f src/HOLCF/IOA/Modelcheck/Ring3.thy
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy	Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Thu Aug 19 21:49:10 1999 +0200
@@ -1,90 +1,104 @@
+
 Ring3 = MuIOAOracle +
 
 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
 
-consts
-Greater :: [token, token] => bool
+datatype Comm =
+  Zero_One token | One_Two token | Two_Zero token |
+  Leader_Zero | Leader_One | Leader_Two
 
-defs
-Greater_def
-"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)"
+constdefs
+  Greater :: [token, token] => bool
+  "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 *)
+
+(*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"
+  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"
+  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"
+  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
+automaton ring = compose aut0, aut1, aut2
+
 
-(* one_leader expresses property that at most one component declares itself to leader *)
+(*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"
+  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"
+
 
 end