8 imports IOA.IOA Action |
8 imports IOA.IOA Action |
9 begin |
9 begin |
10 |
10 |
11 definition |
11 definition |
12 spec_sig :: "'m action signature" where |
12 spec_sig :: "'m action signature" where |
13 sig_def: "spec_sig = (UN m.{S_msg(m)}, |
13 sig_def: "spec_sig = (\<Union>m.{S_msg(m)}, |
14 UN m.{R_msg(m)}, |
14 \<Union>m.{R_msg(m)}, |
15 {})" |
15 {})" |
16 |
16 |
17 definition |
17 definition |
18 spec_trans :: "('m action, 'm list)transition set" where |
18 spec_trans :: "('m action, 'm list)transition set" where |
19 trans_def: "spec_trans = |
19 trans_def: "spec_trans = |
20 {tr. let s = fst(tr); |
20 {tr. let s = fst(tr); |
21 t = snd(snd(tr)) |
21 t = snd(snd(tr)) |
22 in |
22 in |
23 case fst(snd(tr)) |
23 case fst(snd(tr)) |
24 of |
24 of |
25 S_msg(m) => t = s@[m] | |
25 S_msg(m) \<Rightarrow> t = s@[m] | |
26 R_msg(m) => s = (m#t) | |
26 R_msg(m) \<Rightarrow> s = (m#t) | |
27 S_pkt(pkt) => False | |
27 S_pkt(pkt) \<Rightarrow> False | |
28 R_pkt(pkt) => False | |
28 R_pkt(pkt) \<Rightarrow> False | |
29 S_ack(b) => False | |
29 S_ack(b) \<Rightarrow> False | |
30 R_ack(b) => False | |
30 R_ack(b) \<Rightarrow> False | |
31 C_m_s => False | |
31 C_m_s \<Rightarrow> False | |
32 C_m_r => False | |
32 C_m_r \<Rightarrow> False | |
33 C_r_s => False | |
33 C_r_s \<Rightarrow> False | |
34 C_r_r(m) => False}" |
34 C_r_r(m) \<Rightarrow> False}" |
35 |
35 |
36 definition |
36 definition |
37 spec_ioa :: "('m action, 'm list)ioa" where |
37 spec_ioa :: "('m action, 'm list)ioa" where |
38 ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})" |
38 ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})" |
39 |
39 |