# HG changeset patch # User mueller # Date 862393888 -7200 # Node ID 3c4fc62d494cb2bd5e252b79820d539fa476132e # Parent 1fba53dcbf1d3262ca28734711f0604c7073bd5c remove -- new version in HOLCF/IOA/ABP; diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Abschannel.thy --- a/src/HOL/IOA/ABP/Abschannel.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,107 +0,0 @@ -(* Title: HOL/IOA/example/Abschannels.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1994 TU Muenchen - -The transmission channel -*) - -Abschannel = IOA + Action + Lemmas + List + - - -datatype ('a)act = S('a) | R('a) - - -consts - -ch_asig :: 'a act signature -ch_trans :: ('a act, 'a list)transition set -ch_ioa :: ('a act, 'a list)ioa - -rsch_actions :: 'm action => bool act option -srch_actions :: "'m action =>(bool * 'm) act option" - -srch_asig, -rsch_asig :: 'm action signature - -srch_trans :: ('m action, 'm packet list)transition set -rsch_trans :: ('m action, bool list)transition set - -srch_ioa :: ('m action, 'm packet list)ioa -rsch_ioa :: ('m action, bool list)ioa - - -defs - -srch_asig_def "srch_asig == asig_of(srch_ioa)" -rsch_asig_def "rsch_asig == asig_of(rsch_ioa)" - -srch_trans_def "srch_trans == trans_of(srch_ioa)" -rsch_trans_def "rsch_trans == trans_of(rsch_ioa)" - -srch_ioa_def "srch_ioa == rename ch_ioa srch_actions" -rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions" - - -(********************************************************** - G e n e r i c C h a n n e l - *********************************************************) - -ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" - -ch_trans_def "ch_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of S(b) => ((t = s) | (t = s @ [b])) | - R(b) => s ~= [] & - b = hd(s) & - ((t = s) | (t = tl(s))) }" - -ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)" - -(********************************************************** - C o n c r e t e C h a n n e l s b y R e n a m i n g - *********************************************************) - -rsch_actions_def "rsch_actions (akt) == - case akt of - Next => None | - S_msg(m) => None | - R_msg(m) => None | - S_pkt(packet) => None | - R_pkt(packet) => None | - S_ack(b) => Some(S(b)) | - R_ack(b) => Some(R(b))" - -srch_actions_def "srch_actions (akt) == - case akt of - Next => None | - S_msg(m) => None | - R_msg(m) => None | - S_pkt(p) => Some(S(p)) | - R_pkt(p) => Some(R(p)) | - S_ack(b) => None | - R_ack(b) => None" - - -end - - - - - - - - - - - - - - - - - - diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Abschannel_finite.thy --- a/src/HOL/IOA/ABP/Abschannel_finite.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -(* Title: HOL/IOA/example/Abschannels.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1994 TU Muenchen - -The transmission channel -- finite version -*) - -Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List + - -consts - -ch_fin_asig :: 'a act signature - -ch_fin_trans :: ('a act, 'a list)transition set - -ch_fin_ioa :: ('a act, 'a list)ioa - -srch_fin_asig, -rsch_fin_asig :: 'm action signature - -srch_fin_trans :: ('m action, 'm packet list)transition set -rsch_fin_trans :: ('m action, bool list)transition set - -srch_fin_ioa :: ('m action, 'm packet list)ioa -rsch_fin_ioa :: ('m action, bool list)ioa - -reverse :: 'a list => 'a list - -primrec - reverse List.list - reverse_Nil "reverse([]) = []" - reverse_Cons "reverse(x#xs) = reverse(xs)@[x]" - -defs - -srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)" -rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)" - -srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)" -rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)" - -srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa srch_actions" -rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa rsch_actions" - - -ch_fin_asig_def "ch_fin_asig == ch_asig" - -ch_fin_trans_def "ch_fin_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of S(b) => ((t = s) | - (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | - R(b) => s ~= [] & - b = hd(s) & - ((t = s) | (t = tl(s))) }" - -ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)" - -end - - - - - - - - - - - - - - - - - - diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Action.ML --- a/src/HOL/IOA/ABP/Action.ML Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* Title: HOL/IOA/example/Action.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Derived rules for actions -*) - -goal Action.thy "!!x. x = y ==> action_case a b c d e f g x = \ -\ action_case a b c d e f g y"; -by (Asm_simp_tac 1); - -Addcongs [result()]; diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Action.thy --- a/src/HOL/IOA/ABP/Action.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* Title: HOL/IOA/example/Action.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The set of all actions of the system -*) - -Action = Packet + -datatype 'm action = Next | S_msg ('m) | R_msg ('m) - | S_pkt ('m packet) | R_pkt ('m packet) - | S_ack (bool) | R_ack (bool) -end diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Check.ML --- a/src/HOL/IOA/ABP/Check.ML Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,170 +0,0 @@ - - - -(* ---------------------------------------------------------------- - P r o t o t y p e M o d e l C h e c k e r - ----------------------------------------------------------------*) - -fun check(extacts,intacts,string_of_a,startsI,string_of_s, - nexts,hom,transA,startsS) = - let fun check_s(s,unchecked,checked) = - let fun check_sa(unchecked,a) = - let fun check_sas(unchecked,t) = - (if a mem extacts then - (if transA(hom s,a,hom t) then ( ) - else (writeln("Error: Mapping of Externals!"); - string_of_s s; writeln""; - string_of_a a; writeln""; - string_of_s t;writeln"";writeln"" )) - else (if hom(s)=hom(t) then ( ) - else (writeln("Error: Mapping of Internals!"); - string_of_s s; writeln""; - string_of_a a; writeln""; - string_of_s t;writeln"";writeln"" )); - if t mem checked then unchecked else t ins unchecked) - in foldl check_sas (unchecked,nexts s a) end; - val unchecked' = foldl check_sa (unchecked,extacts @ intacts) - in (if s mem startsI then - (if hom(s) mem startsS then () - else writeln("Error: At start states!")) - else (); - checks(unchecked',s::checked)) end - and checks([],_) = () - | checks(s::unchecked,checked) = check_s(s,unchecked,checked) - in checks(startsI,[]) end; - - -(* ------------------------------------------------------ - A B P E x a m p l e - -------------------------------------------------------*) - -datatype msg = m | n | l; -datatype act = Next | S_msg of msg | R_msg of msg - | S_pkt of bool * msg | R_pkt of bool * msg - | S_ack of bool | R_ack of bool; - -(* -------------------- Transition relation of Specification -----------*) - -fun transA((u,s),a,(v,t)) = - (case a of - Next => v andalso t = s | - S_msg(q) => u andalso not(v) andalso t = s@[q] | - R_msg(q) => u = v andalso s = (q::t) | - S_pkt(b,q) => false | - R_pkt(b,q) => false | - S_ack(b) => false | - R_ack(b) => false); - - -(* ---------------------- Abstraction function --------------------------*) - -fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p)); - - -(* --------------------- Transition relation of Implementation ----------*) - -fun nexts (s as (env,p,a,q,b,ch1,ch2)) action = - (case action of - Next => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] | - S_msg(mornorl) => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] | - R_msg(mornorl) => if (q<>[] andalso mornorl=hd(q)) - then [(env,p,a,tl(q),b,ch1,ch2)] - else [] | - S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a) - then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl)) - then [s] - else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)]) - else [] | - R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl)) - then (if (h<>b andalso q=[]) - then [(env,p,a,q@[mornorl],not(b),ch1,ch2), - (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)] - else [s,(env,p,a,q,b,tl(ch1),ch2)]) - else [] | - S_ack(h) => if (h=b) - then (if (ch2<>[] andalso h=hd(rev(ch2))) - then [s] - else [s,(env,p,a,q,b,ch1,ch2@[h])]) - else [] | - R_ack(h) => if (ch2<>[] andalso hd(ch2)=h) - then (if h=a - then [(env,tl(p),not(a),q,b,ch1,ch2), - (env,tl(p),not(a),q,b,ch1,tl(ch2))] - else [s,(env,p,a,q,b,ch1,tl(ch2))]) - else []) - - -val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)]; -val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true), - S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false), - S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l), - S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)]; - - -(* ------------------------------------ - Input / Output utilities - ------------------------------------*) - -fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) = - let fun prec x = (prs ","; pre x) - in - (case lll of - [] => (prs lpar; prs rpar) - | x::lll => (prs lpar; pre x; seq prec lll; prs rpar)) - end; - -fun pr_bool true = output(std_out,"true") -| pr_bool false = output(std_out,"false"); - -fun pr_msg m = output(std_out,"m") -| pr_msg n = output(std_out,"n") -| pr_msg l = output(std_out,"l"); - -fun pr_act a = output(std_out, case a of - Next => "Next"| - S_msg(ma) => "S_msg(ma)" | - R_msg(ma) => "R_msg(ma)" | - S_pkt(b,ma) => "S_pkt(b,ma)" | - R_pkt(b,ma) => "R_pkt(b,ma)" | - S_ack(b) => "S_ack(b)" | - R_ack(b) => "R_ack(b)"); - -fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">"); - -val pr_bool_list = print_list("[","]",pr_bool); -val pr_msg_list = print_list("[","]",pr_msg); -val pr_pkt_list = print_list("[","]",pr_pkt); - -fun pr_tuple (env,p,a,q,b,ch1,ch2) = - (prs "{"; pr_bool env; prs ", "; pr_msg_list p; prs ", "; - pr_bool a; prs ", "; pr_msg_list q; prs ", "; - pr_bool b; prs ", "; pr_pkt_list ch1; prs ", "; - pr_bool_list ch2; prs "}"); - - - -(* --------------------------------- - Main function call - ---------------------------------*) - -(* -check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], - pr_tuple, nexts, hom, transA, [(true,[])]); -*) - - - - - -(* - Little test example - -datatype act = A; -fun transA(s,a,t) = (not(s)=t); -fun hom(i) = i mod 2 = 0; -fun nexts s A = [(s+1) mod 4]; -check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]); - -fun nexts s A = [(s+1) mod 5]; - -*) diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Correctness.ML --- a/src/HOL/IOA/ABP/Correctness.ML Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,392 +0,0 @@ - (* Title: HOL/IOA/example/Correctness.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -*) - -open Correctness; open Abschannel; open Abschannel_finite; -open Impl; open Impl_finite; - -goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)"; -by (Fast_tac 1); -qed"exis_elim"; - -Delsimps [split_paired_All]; -Addsimps - ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, - ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, - actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, - trans_of_def] @ asig_projections @ set_lemmas); - -val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, - rsch_fin_ioa_def, srch_fin_ioa_def, - ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def]; -Addsimps abschannel_fin; - -val impl_ioas = [Sender.sender_ioa_def,Receiver.receiver_ioa_def]; -val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def]; -val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def]; -Addcongs [let_weak_cong]; -Addsimps [Let_def, ioa_triple_proj, starts_of_par]; - -val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def]; -val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ - asig_projections @ set_lemmas; -Addsimps hom_ioas; - -Addsimps [reduce_Nil,reduce_Cons]; - - - -(* auxiliary function *) -fun rotate n i = EVERY(replicate n (etac revcut_rl i)); - -(* lemmas about reduce *) - -goal Correctness.thy "(reduce(l)=[]) = (l=[])"; - by (rtac iffI 1); - by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1); - by (Fast_tac 1); - by (List.list.induct_tac "l" 1); - by (Simp_tac 1); - by (Simp_tac 1); - by (rtac (expand_list_case RS iffD2) 1); - by (Asm_full_simp_tac 1); - by (REPEAT (rtac allI 1)); - by (rtac impI 1); - by (hyp_subst_tac 1); - by (rtac (expand_if RS ssubst) 1); - by (Asm_full_simp_tac 1); - by (Asm_full_simp_tac 1); -val l_iff_red_nil = result(); - -goal Correctness.thy "s~=[] --> hd(s)=hd(reduce(s))"; -by (List.list.induct_tac "s" 1); -by (Simp_tac 1); -by (case_tac "list =[]" 1); -by (Asm_full_simp_tac 1); -(* main case *) -by (rotate 1 1); -by (asm_full_simp_tac list_ss 1); -by (Simp_tac 1); -by (rtac (expand_list_case RS iffD2) 1); -by (asm_full_simp_tac list_ss 1); -by (REPEAT (rtac allI 1)); - by (rtac impI 1); -by (rtac (expand_if RS ssubst) 1); -by (REPEAT(hyp_subst_tac 1)); -by (etac subst 1); -by (Simp_tac 1); -qed"hd_is_reduce_hd"; - -(* to be used in the following Lemma *) -goal Correctness.thy "l~=[] --> reverse(reduce(l))~=[]"; -by (List.list.induct_tac "l" 1); -by (Simp_tac 1); -by (case_tac "list =[]" 1); -by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); -(* main case *) -by (rotate 1 1); -by (Asm_full_simp_tac 1); -by (cut_inst_tac [("l","list")] cons_not_nil 1); -by (Asm_full_simp_tac 1); -by (REPEAT (etac exE 1)); -by (Asm_simp_tac 1); -by (rtac (expand_if RS ssubst) 1); -by (hyp_subst_tac 1); -by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); -qed"rev_red_not_nil"; - -(* shows applicability of the induction hypothesis of the following Lemma 1 *) -goal Correctness.thy "!!l.[| l~=[] |] ==> \ -\ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))"; - by (Simp_tac 1); - by (rtac (expand_list_case RS iffD2) 1); - by (asm_full_simp_tac list_ss 1); - by (REPEAT (rtac allI 1)); - by (rtac impI 1); - by (rtac (expand_if RS ssubst) 1); - by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append, - (rev_red_not_nil RS mp)]) 1); -qed"last_ind_on_first"; - -val impl_ss = !simpset delsimps [reduce_Cons]; - -(* Main Lemma 1 for S_pkt in showing that reduce is refinement *) -goal Correctness.thy - "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then \ -\ reduce(l@[x])=reduce(l) else \ -\ reduce(l@[x])=reduce(l)@[x]"; -by (rtac (expand_if RS ssubst) 1); -by (rtac conjI 1); -(* --> *) -by (List.list.induct_tac "l" 1); -by (Simp_tac 1); -by (case_tac "list=[]" 1); - by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1); - by (rtac impI 1); -by (Simp_tac 1); -by (cut_inst_tac [("l","list")] cons_not_nil 1); - by (asm_full_simp_tac impl_ss 1); - by (REPEAT (etac exE 1)); - by (hyp_subst_tac 1); -by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1); -(* <-- *) -by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1); -by (List.list.induct_tac "l" 1); -by (Simp_tac 1); -by (case_tac "list=[]" 1); -by (cut_inst_tac [("l","list")] cons_not_nil 2); -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1); -by (auto_tac (!claset, - impl_ss addsimps [last_ind_on_first,l_iff_red_nil] - setloop split_tac [expand_if])); -by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1); -qed"reduce_hd"; - - -(* Main Lemma 2 for R_pkt in showing that reduce is refinement *) -goal Correctness.thy - "!! s. [| s~=[] |] ==> \ -\ if hd(s)=hd(tl(s)) & tl(s)~=[] then \ -\ reduce(tl(s))=reduce(s) else \ -\ reduce(tl(s))=tl(reduce(s))"; -by (cut_inst_tac [("l","s")] cons_not_nil 1); -by (Asm_full_simp_tac 1); -by (REPEAT (etac exE 1)); -by (Asm_full_simp_tac 1); -by (rtac (expand_if RS ssubst) 1); -by (rtac conjI 1); -by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2); -by (Step_tac 1); -by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil)); -by (Auto_tac()); -val reduce_tl =result(); - - -(******************************************************************* - C h a n n e l A b s t r a c t i o n - *******************************************************************) - -goal Correctness.thy - "is_weak_pmap reduce ch_ioa ch_fin_ioa"; -by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); -(* ---------------- main-part ------------------- *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (act.induct_tac "a" 1); -(* ----------------- 2 cases ---------------------*) -by (ALLGOALS (simp_tac (!simpset addsimps [externals_def]))); -(* fst case --------------------------------------*) - by (rtac impI 1); - by (rtac disjI2 1); -by (rtac reduce_hd 1); -(* snd case --------------------------------------*) - by (rtac impI 1); - by (REPEAT (etac conjE 1)); - by (etac disjE 1); -by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1); -by (etac (hd_is_reduce_hd RS mp) 1); -by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1); -by (rtac conjI 1); -by (etac (hd_is_reduce_hd RS mp) 1); -by (rtac (bool_if_impl_or RS mp) 1); -by (etac reduce_tl 1); -qed"channel_abstraction"; - -goal Correctness.thy - "is_weak_pmap reduce srch_ioa srch_fin_ioa"; -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def, - srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1); -qed"sender_abstraction"; - -goal Correctness.thy - "is_weak_pmap reduce rsch_ioa rsch_fin_ioa"; -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def, - srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1); -qed"receiver_abstraction"; - - -(* 3 thms that do not hold generally! The lucky restriction here is - the absence of internal actions. *) -goal Correctness.thy - "is_weak_pmap (%id.id) sender_ioa sender_ioa"; -by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); -by (TRY( - (rtac conjI 1) THEN -(* start states *) - (Fast_tac 1))); -(* main-part *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (Action.action.induct_tac "a" 1); -(* 7 cases *) -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); -qed"sender_unchanged"; - -(* 2 copies of before *) -goal Correctness.thy - "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; -by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); -by (TRY( - (rtac conjI 1) THEN - (* start states *) - (Fast_tac 1))); -(* main-part *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (Action.action.induct_tac "a" 1); -(* 7 cases *) -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); -qed"receiver_unchanged"; - -goal Correctness.thy - "is_weak_pmap (%id.id) env_ioa env_ioa"; -by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); -by (TRY( - (rtac conjI 1) THEN -(* start states *) - (Fast_tac 1))); -(* main-part *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (Action.action.induct_tac "a" 1); -(* 7 cases *) -by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); -qed"env_unchanged"; - -Delsimps [Collect_False_empty]; - -goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; -by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS(Simp_tac)); -val compat_single_ch = result(); - -(* totally the same as before *) -goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa"; -by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS(Simp_tac)); -val compat_single_fin_ch = result(); - -val ss = - !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def, - asig_of_def, actions_def, srch_trans_def, rsch_trans_def, - srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, - rsch_ioa_def, Sender.sender_trans_def, - Receiver.receiver_trans_def] @ set_lemmas); - -goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)"; -by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def, - asig_of_par,asig_comp_def,actions_def, - Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS Simp_tac); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_rec = result(); - -(* 5 proofs totally the same as before *) -goal Correctness.thy "compat_ioas receiver_ioa (srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS Simp_tac); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_rec_fin =result(); - -goal Correctness.thy "compat_ioas sender_ioa \ -\ (receiver_ioa || srch_ioa || rsch_ioa)"; -by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS(Simp_tac)); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_sen=result(); - -goal Correctness.thy "compat_ioas sender_ioa\ -\ (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (ss addsimps [empty_def, compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS(Simp_tac)); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_sen_fin =result(); - -goal Correctness.thy "compat_ioas env_ioa\ -\ (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"; -by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS(Simp_tac)); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_env=result(); - -goal Correctness.thy "compat_ioas env_ioa\ -\ (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (Simp_tac 1); -by (rtac set_ext 1); -by (Action.action.induct_tac "x" 1); -by (ALLGOALS Simp_tac); -by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); -val compat_env_fin=result(); - - -(* lemmata about externals of channels *) -goal Correctness.thy - "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \ -\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"; -by (simp_tac (!simpset addsimps [externals_def]) 1); -val ext_single_ch = result(); - - - - - -val ext_ss = [externals_of_par,ext_single_ch]; -val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec, - compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin]; -val abstractions = [env_unchanged,sender_unchanged, - receiver_unchanged,sender_abstraction,receiver_abstraction]; - - -(************************************************************************ - S o u n d n e s s o f A b s t r a c t i o n -*************************************************************************) - -val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def, - srch_fin_ioa_def, rsch_fin_ioa_def] @ - impl_ioas @ env_ioas); - -goal Correctness.thy - "is_weak_pmap abs system_ioa system_fin_ioa"; - -by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def, - rsch_fin_ioa_def] @ env_ioas @ impl_ioas) - addsimps [system_def, system_fin_def, abs_def, - impl_ioa_def, impl_fin_ioa_def, sys_IOA, - sys_fin_IOA]) 1); - -by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, - simp_tac (ss addsimps abstractions) 1, - rtac conjI 1])); - -by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); - -qed "system_refinement"; diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Correctness.thy --- a/src/HOL/IOA/ABP/Correctness.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -(* Title: HOL/IOA/example/Correctness.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The main correctness proof: System_fin implements System -*) - -Correctness = Solve + Env + Impl + Impl_finite + - -consts - -reduce :: 'a list => 'a list - -abs :: 'c -system_ioa :: "('m action, bool * 'm impl_state)ioa" -system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" - -primrec - reduce List.list - reduce_Nil "reduce [] = []" - reduce_Cons "reduce(x#xs) = - (case xs of - [] => [x] - | y#ys => (if (x=y) - then reduce xs - else (x#(reduce xs))))" - - -defs - -system_def - "system_ioa == (env_ioa || impl_ioa)" - -system_fin_def - "system_fin_ioa == (env_ioa || impl_fin_ioa)" - -abs_def "abs == - (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), - (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" - -rules - - sys_IOA "IOA system_ioa" - sys_fin_IOA "IOA system_fin_ioa" - -end - - diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Env.thy --- a/src/HOL/IOA/ABP/Env.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* Title: HOL/IOA/example/Impl.thy -by (Action.action.induct_tac "a" 1); - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The environment -*) - -Env = IOA + Action + - -types - -'m env_state = "bool" -(* give next bit to system *) - -consts - -env_asig :: 'm action signature -env_trans :: ('m action, 'm env_state)transition set -env_ioa :: ('m action, 'm env_state)ioa -next :: 'm env_state => bool - -defs - -env_asig_def - "env_asig == ({Next}, - UN m. {S_msg(m)}, - {})" - -env_trans_def "env_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - Next => t=True | - S_msg(m) => s=True & t=False | - R_msg(m) => False | - S_pkt(pkt) => False | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => False}" - -env_ioa_def "env_ioa == - (env_asig, {True}, env_trans)" - -end - diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Impl.thy --- a/src/HOL/IOA/ABP/Impl.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/IOA/example/Impl.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The implementation -*) - -Impl = Sender + Receiver + Abschannel + - -types - -'m impl_state -= "'m sender_state * 'm receiver_state * 'm packet list * bool list" -(* sender_state * receiver_state * srch_state * rsch_state *) - - -constdefs - - impl_ioa :: ('m action, 'm impl_state)ioa - "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" - - sen :: 'm impl_state => 'm sender_state - "sen == fst" - - rec :: 'm impl_state => 'm receiver_state - "rec == fst o snd" - - srch :: 'm impl_state => 'm packet list - "srch == fst o snd o snd" - - rsch :: 'm impl_state => bool list - "rsch == snd o snd o snd" - -end diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Impl_finite.thy --- a/src/HOL/IOA/ABP/Impl_finite.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -(* Title: HOL/IOA/example/Impl.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The implementation -*) - -Impl_finite = Sender + Receiver + Abschannel_finite + - -types - -'m impl_fin_state -= "'m sender_state * 'm receiver_state * 'm packet list * bool list" -(* sender_state * receiver_state * srch_state * rsch_state *) - -constdefs - - impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa - "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || - rsch_fin_ioa)" - - sen_fin :: 'm impl_fin_state => 'm sender_state - "sen_fin == fst" - - rec_fin :: 'm impl_fin_state => 'm receiver_state - "rec_fin == fst o snd" - - srch_fin :: 'm impl_fin_state => 'm packet list - "srch_fin == fst o snd o snd" - - rsch_fin :: 'm impl_fin_state => bool list - "rsch_fin == snd o snd o snd" - -end - diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Lemmas.ML --- a/src/HOL/IOA/ABP/Lemmas.ML Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: HOL/IOA/example/Lemmas.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -*) - -(* Logic *) - -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by(fast_tac (!claset addDs prems) 1); -qed "imp_conj_lemma"; - -goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)"; -by (Fast_tac 1); -val and_de_morgan_and_absorbe = result(); - -goal HOL.thy "(if C then A else B) --> (A|B)"; -by (rtac (expand_if RS ssubst) 1); -by (Fast_tac 1); -val bool_if_impl_or = result(); - -(* Sets *) - -val set_lemmas = - map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1])) - ["f(x) : (UN x. {f(x)})", - "f x y : (UN x y. {f x y})", - "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", - "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; - -(* 2 Lemmas to add to set_lemmas ... , used also for action handling, - namely for Intersections and the empty list (compatibility of IOA!) *) -goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; - by (rtac set_ext 1); - by (Fast_tac 1); -val singleton_set =result(); - -goal HOL.thy "((A|B)=False) = ((~A)&(~B))"; - by (Fast_tac 1); -val de_morgan = result(); - -(* Lists *) - -val list_ss = simpset_of "List"; - -goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))"; -by (List.list.induct_tac "l" 1); -by (simp_tac list_ss 1); -by (simp_tac list_ss 1); -val hd_append =result(); - -goal List.thy "l ~= [] --> (? x xs. l = (x#xs))"; - by (List.list.induct_tac "l" 1); - by (simp_tac list_ss 1); - by (Fast_tac 1); -qed"cons_not_nil"; diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Lemmas.thy --- a/src/HOL/IOA/ABP/Lemmas.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/IOA/example/Lemmas.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Arithmetic lemmas -*) - -Lemmas = Arith diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Packet.thy --- a/src/HOL/IOA/ABP/Packet.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/IOA/example/Packet.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Packets -*) - -Packet = Arith + - -types - - 'msg packet = "bool * 'msg" - -constdefs - - hdr :: 'msg packet => bool - "hdr == fst" - - msg :: 'msg packet => 'msg - "msg == snd" - -end diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/ROOT.ML --- a/src/HOL/IOA/ABP/ROOT.ML Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -(* Title: HOL/IOA/ABP/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -This is the ROOT file for the theory of I/O-Automata (ABP subdirectory). -The formalization is by a semantic model of I/O-Automata. -For details see - -@inproceedings{Nipkow-Slind-IOA, -author={Tobias Nipkow and Konrad Slind}, -title={{I/O} Automata in {Isabelle/HOL}}, -booktitle={Proc.\ TYPES Workshop 1994}, -publisher=Springer, -series=LNCS, -note={To appear}} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz - -and - -@inproceedings{Mueller-Nipkow, -author={Olaf M\"uller and Tobias Nipkow}, -title={Combining Model Checking and Deduction for {I/O}-Automata}, -booktitle={Proc.\ TACAS Workshop}, -organization={Aarhus University, BRICS report}, -year=1995} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz - -Should be executed in the subdirectory HOL/IOA/ABP. -*) - -goals_limit := 1; - -(*Load theories from ../meta_theory without generating HTML files - (has already been done by NTP/ROOT.ML)*) -val old_make_html = !make_html; -make_html := false; -loadpath := ["../meta_theory"]; - -use_thy "Solve"; - -make_html := old_make_html; -loadpath := ["."]; - - -use_thy "Correctness"; diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Read_me --- a/src/HOL/IOA/ABP/Read_me Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ -Isabelle Verification of the Alternating Bit Protocol by -combining IOA with Model Checking - -------------------------------------------------------------- - -Correctness.ML contains the proof of the abstraction from unbounded -channels to finite ones. - -Check.ML contains a simple ModelChecker prototype checking Spec against -the finite version of the ABP-protocol. diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Receiver.thy --- a/src/HOL/IOA/ABP/Receiver.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: HOL/IOA/example/Receiver.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The implementation: receiver -*) - -Receiver = List + IOA + Action + Lemmas + - -types - -'m receiver_state -= "'m list * bool" -(* messages mode *) - -consts - - receiver_asig :: 'm action signature - receiver_trans:: ('m action, 'm receiver_state)transition set - receiver_ioa :: ('m action, 'm receiver_state)ioa - rq :: 'm receiver_state => 'm list - rbit :: 'm receiver_state => bool - -defs - -rq_def "rq == fst" -rbit_def "rbit == snd" - -receiver_asig_def "receiver_asig == - (UN pkt. {R_pkt(pkt)}, - (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), - {})" - -receiver_trans_def "receiver_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - Next => False | - S_msg(m) => False | - R_msg(m) => (rq(s) ~= []) & - m = hd(rq(s)) & - rq(t) = tl(rq(s)) & - rbit(t)=rbit(s) | - S_pkt(pkt) => False | - R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then - rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else - rq(t) =rq(s) & rbit(t)=rbit(s) | - S_ack(b) => b = rbit(s) & - rq(t) = rq(s) & - rbit(t)=rbit(s) | - R_ack(b) => False}" - -receiver_ioa_def "receiver_ioa == - (receiver_asig, {([],False)}, receiver_trans)" - -end diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Sender.thy --- a/src/HOL/IOA/ABP/Sender.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: HOL/IOA/example/Sender.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The implementation: sender -*) - -Sender = IOA + Action + List + Lemmas + - -types - -'m sender_state = "'m list * bool" -(* messages Alternating Bit *) - -consts - -sender_asig :: 'm action signature -sender_trans :: ('m action, 'm sender_state)transition set -sender_ioa :: ('m action, 'm sender_state)ioa -sq :: 'm sender_state => 'm list -sbit :: 'm sender_state => bool - -defs - -sq_def "sq == fst" -sbit_def "sbit == snd" - -sender_asig_def - "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), - UN pkt. {S_pkt(pkt)}, - {})" - -sender_trans_def "sender_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - Next => if sq(s)=[] then t=s else False | - S_msg(m) => sq(t)=sq(s)@[m] & - sbit(t)=sbit(s) | - R_msg(m) => False | - S_pkt(pkt) => sq(s) ~= [] & - hdr(pkt) = sbit(s) & - msg(pkt) = hd(sq(s)) & - sq(t) = sq(s) & - sbit(t) = sbit(s) | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => if b = sbit(s) then - sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else - sq(t)=sq(s) & sbit(t)=sbit(s)}" - -sender_ioa_def "sender_ioa == - (sender_asig, {([],True)}, sender_trans)" - -end diff -r 1fba53dcbf1d -r 3c4fc62d494c src/HOL/IOA/ABP/Spec.thy --- a/src/HOL/IOA/ABP/Spec.thy Wed Apr 30 11:42:37 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: HOL/IOA/example/Spec.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -The specification of reliable transmission -*) - -Spec = List + IOA + Action + - -consts - -spec_sig :: 'm action signature -spec_trans :: ('m action, 'm list)transition set -spec_ioa :: ('m action, 'm list)ioa - -defs - -sig_def "spec_sig == (UN m.{S_msg(m)}, - UN m.{R_msg(m)} Un {Next}, - {})" - -trans_def "spec_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in - case fst(snd(tr)) - of - Next => t=s |\ (* Note that there is condition as in Sender *) - S_msg(m) => t = s@[m] | - R_msg(m) => s = (m#t) | - S_pkt(pkt) => False | - R_pkt(pkt) => False | - S_ack(b) => False | - R_ack(b) => False}" - -ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)" - -end