added translation from IOA to mucalculus and corresponding modelchecker examples;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,29 @@
+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,
+		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 *)
+goal thy "cockpit =<| Info_while_Al";
+by (is_sim_tac thy 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);       
+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);       
+by Auto_tac;
+qed"cockpit_implements_Al_before_Ack";
+
+*)	

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,80 @@
+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 *)
+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 "Info a" in cockpit
+
+(* following automatons express the properties to be proved, see 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"
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,276 @@
+(* 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 SimFailureExn of string;
+
+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];
+
+local
+
+exception malformed;
+
+fun fst_type (Type("*",[a,_])) = a |
+fst_type _ = raise malformed; 
+fun snd_type (Type("*",[_,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" ^ (Sign.string_of_term 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" ^ (Sign.string_of_term 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" ^ (Sign.string_of_term 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" ^ (Sign.string_of_term 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" ^ (Sign.string_of_term 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" ^ (Sign.string_of_term sg t));
+
+fun is_prefix [] s = true
+| is_prefix (p::ps) [] = false
+| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
+
+fun delete_ul [] = []
+| delete_ul (x::xs) = if (is_prefix ("\^["::"["::"4"::"m"::[]) (x::xs))
+        then (let val (_::_::_::s) = xs in delete_ul s end)
+        else (if (is_prefix ("\^["::"["::"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("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
+type_list_of sign a = [(Sign.string_of_typ sign a)];
+
+fun structured_tuple l (Type("*",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 ^ (BasisLibrary.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 ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a |
+tupel_typed_of sign s n (a::r) =
+ s ^ (BasisLibrary.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 ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a |
+double_tupel_typed_of sign s t n (a::r) =
+ s ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
+
+fun tupel_of _ _ _ [] = "" |
+tupel_of sign s n [a] = s ^ (BasisLibrary.Int.toString(n)) |
+tupel_of sign s n (a::r) = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
+
+fun double_tupel_of _ _ _ _ [] = "" |
+double_tupel_of sign s t n [a] = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^
+				 t ^ (BasisLibrary.Int.toString(n)) |
+double_tupel_of sign s t n (a::r) = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^
+		t ^ (BasisLibrary.Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
+
+fun eq_string _ _ _ [] = "" |
+eq_string s t n [a] = s ^ (BasisLibrary.Int.toString(n)) ^ " = " ^
+			 t ^ (BasisLibrary.Int.toString(n)) |
+eq_string s t n (a::r) =
+ s ^ (BasisLibrary.Int.toString(n)) ^ " = " ^
+ t ^ (BasisLibrary.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 (sign, SimOracleExn (subgoal,t,thl)) =
+(let
+	val concl = (Logic.strip_imp_concl subgoal);
+
+	val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
+	val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
+	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
+	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
+	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
+	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
+	
+	val action_type_str =
+	Sign.string_of_typ 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
+(
+push_proof();
+goal t 
+( "(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 ^ "))");
+by (REPEAT (rtac impI 1));
+by (REPEAT (dtac eq_reflection 1));
+(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
+by (full_simp_tac ((simpset() delsimps [not_iff,split_part])
+			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
+                                        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);
+(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
+by (atac 1);
+result();
+pop_proof();
+Logic.strip_imp_concl subgoal
+)
+end)
+handle malformed =>
+error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,15 @@
+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
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,40 @@
+(*
+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 = 
+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));
+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 =
+let val sign = #sign (rep_thm state);
+in
+case drop(i-1,prems_of state) of
+        [] => PureGeneral.Seq.empty |
+        subgoal::_ => EVERY[REPEAT(etac thin_rl i),
+                        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(atac (i+2)), 
+                        REPEAT(rtac refl (i+2)),
+	 		simp_tac (simpset() addsimps (thm_list @
+				comp_simps @ restrict_simps @ hide_simps @
+				rename_simps @  ioa_simps @ asig_simps)) (i+1),
+		 	simp_tac (simpset() addsimps (thm_list @
+				comp_simps @ restrict_simps @ hide_simps @
+				rename_simps @ ioa_simps @ asig_simps)) (i)] state
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,6 @@
+MuIOAOracle = MuIOA +
+
+oracle
+Sim = mk_sim_oracle
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOL/IOA/Modelcheck/ROOT.ML
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1997  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.
+*)
+
+goals_limit := 1;
+
+add_path"~/isabelle/src/HOL/Modelcheck";
+use"~/isabelle/src/HOL/Modelcheck/mucke_oracle.ML";
+use_thy"MuIOAOracle";
+use_thy"Cockpit";
+use_thy"Ring3";
+
+reset_path();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.ML	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,14 @@
+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];
+
+(* 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); 
+by Auto_tac;
+qed"at_most_one_leader";
+*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Thu Apr 22 11:09:05 1999 +0200
@@ -0,0 +1,90 @@
+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
+
+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)"
+
+(* 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"
+
+end