equal
deleted
inserted
replaced
13 'm sender_state = "'m list * bool multiset * bool multiset * bool * bool" |
13 'm sender_state = "'m list * bool multiset * bool multiset * bool * bool" |
14 (* messages #sent #received header mode *) |
14 (* messages #sent #received header mode *) |
15 |
15 |
16 consts |
16 consts |
17 |
17 |
18 sender_asig :: "'m action signature" |
18 sender_asig :: 'm action signature |
19 sender_trans :: "('m action, 'm sender_state)transition set" |
19 sender_trans :: ('m action, 'm sender_state)transition set |
20 sender_ioa :: "('m action, 'm sender_state)ioa" |
20 sender_ioa :: ('m action, 'm sender_state)ioa |
21 sq :: "'m sender_state => 'm list" |
21 sq :: 'm sender_state => 'm list |
22 ssent,srcvd :: "'m sender_state => bool multiset" |
22 ssent,srcvd :: 'm sender_state => bool multiset |
23 sbit :: "'m sender_state => bool" |
23 sbit :: 'm sender_state => bool |
24 ssending :: "'m sender_state => bool" |
24 ssending :: 'm sender_state => bool |
25 |
25 |
26 defs |
26 defs |
27 |
27 |
28 sq_def "sq == fst" |
28 sq_def "sq == fst" |
29 ssent_def "ssent == fst o snd" |
29 ssent_def "ssent == fst o snd" |