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