34 constdefs |
34 constdefs |
35 (** Release some client_tokens **) |
35 (** Release some client_tokens **) |
36 |
36 |
37 client_rel_act ::i |
37 client_rel_act ::i |
38 "client_rel_act == |
38 "client_rel_act == |
39 {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel) |
39 {<s,t> \\<in> state*state. |
40 & t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) & |
40 \\<exists>nrel \\<in> nat. nrel = length(s`rel) & |
41 nrel < length(s`giv) & |
41 t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) & |
42 nth(nrel, s`ask) le nth(nrel, s`giv)}" |
42 nrel < length(s`giv) & |
|
43 nth(nrel, s`ask) le nth(nrel, s`giv)}" |
43 |
44 |
44 (** Choose a new token requirement **) |
45 (** Choose a new token requirement **) |
45 (** Including s'=s suppresses fairness, allowing the non-trivial part |
46 (** Including t=s suppresses fairness, allowing the non-trivial part |
46 of the action to be ignored **) |
47 of the action to be ignored **) |
47 |
48 |
48 client_tok_act :: i |
49 client_tok_act :: i |
49 "client_tok_act == {<s,t>:state*state. t=s | |
50 "client_tok_act == {<s,t> \\<in> state*state. t=s | |
50 (t = s(tok:=succ(s`tok mod NbT)))}" |
51 t = s(tok:=succ(s`tok mod NbT))}" |
51 |
52 |
52 client_ask_act :: i |
53 client_ask_act :: i |
53 "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
54 "client_ask_act == {<s,t> \\<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
54 |
55 |
55 client_prog :: i |
56 client_prog :: i |
56 "client_prog == |
57 "client_prog == |
57 mk_program({s:state. s`tok le NbT & s`giv = Nil & |
58 mk_program({s \\<in> state. s`tok le NbT & s`giv = Nil & |
58 s`ask = Nil & s`rel = Nil}, |
59 s`ask = Nil & s`rel = Nil}, |
59 {client_rel_act, client_tok_act, client_ask_act}, |
60 {client_rel_act, client_tok_act, client_ask_act}, |
60 UN G: preserves(lift(rel)) Int |
61 \\<Union>G \\<in> preserves(lift(rel)) Int |
61 preserves(lift(ask)) Int |
62 preserves(lift(ask)) Int |
62 preserves(lift(tok)). Acts(G))" |
63 preserves(lift(tok)). Acts(G))" |
63 end |
64 end |