in citp
in cloud

select #CITP# .
loop init .

*** 1 ***
(goal CLOUD |-
ceq true = false if statusp(S:Sys,I:Client)= updated /\ statusc(S:Sys)= idlec[nonexec metadata "inv1"];
ceq true = false if statusp(S:Sys,I:Client)= gotval /\ statusc(S:Sys)= idlec[nonexec metadata "inv2"];
ceq true = false if statusp(S:Sys,J:Client)= updated /\ statusp(S:Sys,I:Client)= gotval[nonexec metadata "inv3"];
ceq true = false if(I:Client ~ J:Client)= false /\ statusp(S:Sys,J:Client)= gotval /\ statusp(S:Sys,I:Client)= gotval[nonexec metadata "inv4"];
ceq true = false if(I:Client ~ J:Client)= false /\ statusp(S:Sys,J:Client)= updated /\ statusp(S:Sys,I:Client)= updated[nonexec metadata "inv5"];)
*** 2 ***
(ind on S:Sys red)
*** 3 ***
(tc red ca red ca red imp red)
*** 4 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 5 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 6 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 7 ***
(. init inv3 by J:Client <- J#4 ; I:Client <- z#2)
*** 8 ***
(. init inv5 by J:Client <- J#4 ; I:Client <- I#3)
*** 9 ***
(. init inv5 by J:Client <- J#4 ; I:Client <- I#3)
*** 10 ***
(. init inv3 by J:Client <- I#3 ; I:Client <- z#2)
*** 11 ***
(. init inv4 by J:Client <- J#4 ; I:Client <- I#3)
*** 12 ***
(. init inv4 by J:Client <- J#4 ; I:Client <- I#3)
*** 13 ***
(. init inv4 by J:Client <- J#4 ; I:Client <- I#3)
*** 14 ***
(. init inv4 by J:Client <- J#4 ; I:Client <- I#3)
*** 15 ***
(. init inv4 by J:Client <- J#4 ; I:Client <- I#3)
*** 16 ***
(. init inv3 by J:Client <- J#3 ; I:Client <- I#4)
*** 17 ***
(. init inv3 by J:Client <- J#3 ; I:Client <- I#4)
*** 18 ***
(. init inv3 by J:Client <- J#3 ; I:Client <- I#4)
*** 19 ***
(. init inv3 by J:Client <- J#3 ; I:Client <- I#4)
*** 20 ***
(. init inv3 by J:Client <- J#3 ; I:Client <- I#4)
*** 21 ***
(. init inv4 by J:Client <- z#2 ; I:Client <- I#4)
*** 22 ***
(. init inv1 by I:Client <- I#3)
*** 23 ***
(. init inv1 by I:Client <- I#3)
*** 24 ***
(. init inv1 by I:Client <- I#3)
*** 25 ***
(. init inv2 by I:Client <- I#3)
*** 26 ***
(. init inv2 by I:Client <- I#3)
*** 27 ***
(. init inv2 by I:Client <- I#3)
*** 28 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 29 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 30 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 31 ***
(. init inv1 by I:Client <- I#3)
*** 32 ***
(. init inv2 by I:Client <- I#3)
*** 33 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 34 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 35 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 36 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 37 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 38 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 39 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 40 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 41 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 42 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 43 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 44 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 45 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 46 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 47 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 48 ***
(. init inv1 by I:Client <- I#3)
*** 49 ***
(. init inv1 by I:Client <- I#3)
*** 50 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- z#2)
*** 51 ***
(. init inv1 by I:Client <- I#3)
*** 52 ***
(. init inv1 by I:Client <- I#3)
*** 53 ***
(. init inv2 by I:Client <- I#3)
*** 54 ***
(. init inv2 by I:Client <- I#3)
*** 55 ***
(. init inv3 by I:Client <- I#3 ; J:Client <- z#2)
*** 56 ***
(. init inv2 by I:Client <- I#3)
*** 57 ***
(. init inv2 by I:Client <- I#3)
*** 58 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 59 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 60 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 61 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 62 ***
(. init inv5 by I:Client <- I#3 ; J:Client <- J#4)
*** 63 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 64 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 65 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 66 ***
(. init inv2 by I:Client <- J#4)
*** 67 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 68 ***
(. init inv4 by I:Client <- I#3 ; J:Client <- J#4)
*** 69 ***
(. init inv2 by I:Client <- I#3)
*** 70 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 71 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 72 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 73 ***
(. init inv1 by I:Client <- J#3)
*** 74 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 75 ***
(. init inv3 by I:Client <- I#4 ; J:Client <- J#3)
*** 76 ***
(. init inv1 by I:Client <- I#3)
*** 77 ***
(. init inv1 by I:Client <- I#3)
*** 78 ***
(. init inv1 by I:Client <- I#3)
*** 79 ***
(. init inv1 by I:Client <- I#3)
*** 80 ***
(. init inv2 by I:Client <- I#3)
*** 81 ***
(. init inv2 by I:Client <- I#3)
*** 82 ***
(. init inv2 by I:Client <- I#3)
*** 83 ***
(. init inv2 by I:Client <- I#3)