77 receiver_ioa :: "('m action, 'm receiver_state)ioa" where |
77 receiver_ioa :: "('m action, 'm receiver_state)ioa" where |
78 "receiver_ioa = |
78 "receiver_ioa = |
79 (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" |
79 (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})" |
80 |
80 |
81 lemma in_receiver_asig: |
81 lemma in_receiver_asig: |
82 "S_msg(m) ~: actions(receiver_asig)" |
82 "S_msg(m) \<notin> actions(receiver_asig)" |
83 "R_msg(m) : actions(receiver_asig)" |
83 "R_msg(m) \<in> actions(receiver_asig)" |
84 "S_pkt(pkt) ~: actions(receiver_asig)" |
84 "S_pkt(pkt) \<notin> actions(receiver_asig)" |
85 "R_pkt(pkt) : actions(receiver_asig)" |
85 "R_pkt(pkt) \<in> actions(receiver_asig)" |
86 "S_ack(b) : actions(receiver_asig)" |
86 "S_ack(b) \<in> actions(receiver_asig)" |
87 "R_ack(b) ~: actions(receiver_asig)" |
87 "R_ack(b) \<notin> actions(receiver_asig)" |
88 "C_m_s ~: actions(receiver_asig)" |
88 "C_m_s \<notin> actions(receiver_asig)" |
89 "C_m_r : actions(receiver_asig)" |
89 "C_m_r \<in> actions(receiver_asig)" |
90 "C_r_s ~: actions(receiver_asig)" |
90 "C_r_s \<notin> actions(receiver_asig)" |
91 "C_r_r(m) : actions(receiver_asig)" |
91 "C_r_r(m) \<in> actions(receiver_asig)" |
92 by (simp_all add: receiver_asig_def actions_def asig_projections) |
92 by (simp_all add: receiver_asig_def actions_def asig_projections) |
93 |
93 |
94 lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def |
94 lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def |
95 |
95 |
96 end |
96 end |