38 |
38 |
39 (** Including s'=s suppresses fairness, allowing the non-trivial part |
39 (** Including s'=s suppresses fairness, allowing the non-trivial part |
40 of the action to be ignored **) |
40 of the action to be ignored **) |
41 |
41 |
42 tok_act :: "(state*state) set" |
42 tok_act :: "(state*state) set" |
43 "tok_act == {(s,s'). s'=s | (EX t: atMost Max. s' = s (|tok := t|))}" |
43 "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}" |
44 |
44 |
|
45 (* |
|
46 "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
|
47 *) |
|
48 |
|
49 |
45 ask_act :: "(state*state) set" |
50 ask_act :: "(state*state) set" |
46 "ask_act == {(s,s'). s'=s | |
51 "ask_act == {(s,s'). s'=s | |
47 (s' = s (|ask := ask s @ [tok s]|) & |
52 (s' = s (|ask := ask s @ [tok s]|))}" |
48 size (ask s) = size (rel s))}" |
|
49 |
53 |
50 Cli_prg :: state program |
54 Client :: state program |
51 "Cli_prg == mk_program ({s. tok s : atMost Max & |
55 "Client == mk_program ({s. tok s : atMost NbT & |
52 giv s = [] & |
56 giv s = [] & ask s = [] & rel s = []}, |
53 ask s = [] & |
57 {rel_act, tok_act, ask_act})" |
54 rel s = []}, |
|
55 {rel_act, tok_act, ask_act})" |
|
56 |
58 |
57 giv_meets_ask :: state set |
59 giv_meets_ask :: state set |
58 "giv_meets_ask == |
60 "giv_meets_ask == |
59 {s. size (giv s) <= size (ask s) & |
61 {s. size (giv s) <= size (ask s) & |
60 (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}" |
62 (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}" |