equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 types |
12 types |
13 'm env_state = bool -- {* give next bit to system *} |
13 'm env_state = bool -- {* give next bit to system *} |
14 |
14 |
15 constdefs |
15 definition |
16 env_asig :: "'m action signature" |
16 env_asig :: "'m action signature" where |
17 "env_asig == ({Next}, |
17 "env_asig == ({Next}, |
18 UN m. {S_msg(m)}, |
18 UN m. {S_msg(m)}, |
19 {})" |
19 {})" |
20 |
20 |
21 env_trans :: "('m action, 'm env_state)transition set" |
21 definition |
22 "env_trans == |
22 env_trans :: "('m action, 'm env_state)transition set" where |
23 {tr. let s = fst(tr); |
23 "env_trans = |
24 t = snd(snd(tr)) |
24 {tr. let s = fst(tr); |
25 in case fst(snd(tr)) |
25 t = snd(snd(tr)) |
26 of |
26 in case fst(snd(tr)) |
27 Next => t=True | |
27 of |
28 S_msg(m) => s=True & t=False | |
28 Next => t=True | |
29 R_msg(m) => False | |
29 S_msg(m) => s=True & t=False | |
30 S_pkt(pkt) => False | |
30 R_msg(m) => False | |
31 R_pkt(pkt) => False | |
31 S_pkt(pkt) => False | |
32 S_ack(b) => False | |
32 R_pkt(pkt) => False | |
33 R_ack(b) => False}" |
33 S_ack(b) => False | |
|
34 R_ack(b) => False}" |
34 |
35 |
35 env_ioa :: "('m action, 'm env_state)ioa" |
36 definition |
36 "env_ioa == (env_asig, {True}, env_trans,{},{})" |
37 env_ioa :: "('m action, 'm env_state)ioa" where |
|
38 "env_ioa = (env_asig, {True}, env_trans,{},{})" |
37 |
39 |
38 consts |
40 axiomatization |
39 "next" :: "'m env_state => bool" |
41 "next" :: "'m env_state => bool" |
40 |
42 |
41 end |
43 end |