12 constdefs |
12 constdefs |
13 distr_follows :: [i, i, i, i =>i] =>i |
13 distr_follows :: [i, i, i, i =>i] =>i |
14 "distr_follows(A, In, iIn, Out) == |
14 "distr_follows(A, In, iIn, Out) == |
15 (lift(In) IncreasingWrt prefix(A)/list(A)) Int |
15 (lift(In) IncreasingWrt prefix(A)/list(A)) Int |
16 (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int |
16 (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int |
17 Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients}) |
17 Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |
18 guarantees |
18 guarantees |
19 (INT n: Nclients. |
19 (\\<Inter>n \\<in> Nclients. |
20 lift(Out(n)) |
20 lift(Out(n)) |
21 Fols |
21 Fols |
22 (%s. sublist(s`In, |
22 (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n})) |
23 {k:nat. k<length(s`iIn) & nth(k, s`iIn) = n})) |
|
24 Wrt prefix(A)/list(A))" |
23 Wrt prefix(A)/list(A))" |
25 |
24 |
26 distr_allowed_acts :: [i=>i]=>i |
25 distr_allowed_acts :: [i=>i]=>i |
27 "distr_allowed_acts(Out) == |
26 "distr_allowed_acts(Out) == |
28 {D:program. AllowedActs(D) = |
27 {D:program. AllowedActs(D) = |
29 cons(id(state), UN G:(INT n:nat. preserves(lift(Out(n)))). Acts(G))}" |
28 cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}" |
30 |
29 |
31 distr_spec :: [i, i, i, i =>i]=>i |
30 distr_spec :: [i, i, i, i =>i]=>i |
32 "distr_spec(A, In, iIn, Out) == |
31 "distr_spec(A, In, iIn, Out) == |
33 distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)" |
32 distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)" |
34 |
33 |
37 iIn :: i (*destinations of items to distribute*) |
36 iIn :: i (*destinations of items to distribute*) |
38 Out :: i=>i (*distributed items*) |
37 Out :: i=>i (*distributed items*) |
39 A :: i (*the type of items being distributed *) |
38 A :: i (*the type of items being distributed *) |
40 D :: i |
39 D :: i |
41 assumes |
40 assumes |
42 var_assumes "In:var & iIn:var & (ALL n. Out(n):var)" |
41 var_assumes "In:var & iIn:var & (\\<forall>n. Out(n):var)" |
43 all_distinct_vars "ALL n. all_distinct([In, iIn, iOut(n)])" |
42 all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])" |
44 type_assumes "type_of(In)=list(A) & type_of(iIn)=list(nat) & |
43 type_assumes "type_of(In)=list(A) & type_of(iIn)=list(nat) & |
45 (ALL n. type_of(Out(n))=list(A))" |
44 (\\<forall>n. type_of(Out(n))=list(A))" |
46 default_val_assumes "default_val(In)=Nil & |
45 default_val_assumes "default_val(In)=Nil & |
47 default_val(iIn)=Nil & |
46 default_val(iIn)=Nil & |
48 (ALL n. default_val(Out(n))=Nil)" |
47 (\\<forall>n. default_val(Out(n))=Nil)" |
49 distr_spec "D:distr_spec(A, In, iIn, Out)" |
48 distr_spec "D:distr_spec(A, In, iIn, Out)" |
50 end |
49 end |