(fmod LABELC is sort LabelC . ops idlec busy : -> LabelC . ceq true = false if idlec = busy . --- op _~_ : LabelC LabelC -> Bool [comm] . vars A B : LabelC . eq A ~ A = true . eq idlec ~ busy = false . endfm) (fmod LABELP is sort LabelP . ops idlep gotval updated : -> LabelP . ceq true = false if idlep = gotval . ceq true = false if idlep = updated . ceq true = false if gotval = updated . --- op _~_ : LabelP LabelP -> Bool[comm] . vars A B : LabelP . eq A ~ A = true . eq idlep ~ gotval = true . eq idlep ~ updated = false . eq gotval ~ updated = false . endfm) (fth CLOUD is pr LABELC . pr LABELP . pr NAT . sorts Client Sys . op _~_ : Client Client -> Bool [comm]. vars I J : Client . eq I ~ I = true . ceq I = J if I ~ J [nonexec]. --- constructors --- op init : -> Sys [ctor]. ops modval getval update gotoidle : Sys Client -> Sys [ctor]. --- observers --- op statusc : Sys -> LabelC . op valc : Sys -> Nat . op statusp : Sys Client -> LabelP . op valp : Sys Client -> Nat . op tmp : Sys Client -> Nat . --- var S : Sys . --- init --- eq statusc(init) = idlec . eq statusp(init,I) = idlep . --- modval --- op new : Sys Client -> Nat . --- eq statusc(modval(S,I)) = statusc(S) . eq valc(modval(S,I)) = valc(S) . eq statusp(modval(S,I),J) = statusp(S,J) . ceq valp(modval(S,I),J) = new(S,I) if J = I /\ statusp(S,I) = idlep /\ statusc(S) = idlec [metadata "CA-m1"]. ceq valp(modval(S,I),J) = valp(S,J) if J ~ I = false [metadata "CA-m2"]. ceq valp(modval(S,I),J) = valp(S,J) if statusp(S,I) ~ idlep = false [metadata "CA-m3"]. ceq valp(modval(S,I),J) = valp(S,J) if statusc(S) ~ idlec = false [metadata "CA-m4"]. eq tmp(modval(S,I),J) = tmp(S,J) . --- getval --- ceq statusc(getval(S,I)) = busy if statusp(S,I) = idlep /\ statusc(S) = idlec . ceq statusc(getval(S,I)) = statusc(S) if statusp(S,I) ~ idlep = false . ceq statusc(getval(S,I)) = statusc(S) if statusc(S) ~ idlec = false . eq valc(getval(S,I)) = valc(S) . ceq statusp(getval(S,I),J) = gotval if J = I /\ statusp(S,I) = idlep /\ statusc(S) = idlec [metadata "CA-1"]. ceq statusp(getval(S,I),J) = statusp(S,J) if J ~ I = false [metadata "CA-2"]. ceq statusp(getval(S,I),J) = statusp(S,J) if statusp(S,I) ~ idlep = false[metadata "CA-3"]. ceq statusp(getval(S,I),J) = statusp(S,J) if statusc(S) ~ idlec = false [metadata "CA-4"]. eq valp(getval(S,I),J) = valp(S,J) . ceq tmp(getval(S,I),J) = valc(S) if J = I /\ statusp(S,I) = idlep /\ statusc(S) = idlec [metadata "CA-1"]. ceq tmp(getval(S,I),J) = tmp(S,J) if J ~ I = false [metadata "CA-2"]. ceq tmp(getval(S,I),J) = tmp(S,J) if statusp(S,I) ~ idlep = false[metadata "CA-3"]. ceq tmp(getval(S,I),J) = tmp(S,J) if statusc(S) ~ idlec = false [metadata "CA-4"]. --- update --- eq statusc(update(S,I)) = statusc(S) . ceq valc(update(S,I)) = valp(S,I) if statusc(S) = busy /\ statusp(S,I) = gotval /\ tmp(S,I) <= valp(S,I) [metadata "CA-c1"]. ceq valc(update(S,I)) = valc(S) if statusc(S) ~ busy = false [metadata "CA-c2"]. ceq valc(update(S,I)) = valc(S) if statusp(S,I) ~ gotval = false [metadata "CA-c3"]. ceq valc(update(S,I)) = valc(S) if valp(S,I) < tmp(S,I) [metadata "CA-c4"]. ceq statusp(update(S,I),J)= updated if J = I /\ statusp(S,I)= gotval /\ statusc(S)= busy . ceq statusp(update(S,I),J)= statusp(S,J) if J ~ I = false . ceq statusp(update(S,I),J)= statusp(S,J) if statusp(S,I) ~ gotval = false . ceq statusp(update(S,I),J)= statusp(S,J) if statusc(S) ~ busy = false . ceq valp(update(S,I),J) = tmp(S,J) if J = I /\ statusp(S,I)= gotval /\ statusc(S)= busy /\ valp(S,I) < tmp(S,I) [metadata "CA-p1"]. ceq valp(update(S,I),J) = valp(S,J) if J ~ I = false /\ statusp(S,I)= gotval /\ statusc(S)= busy /\ valp(S,I)< tmp(S,I) [metadata "CA-p2"]. ceq valp(update(S,I),J) = valp(S,J) if J = I /\ statusp(S,I)~ gotval = false[metadata "CA-p3"]. ceq valp(update(S,I),J) = valp(S,J) if J = I /\ statusc(S) ~ busy = false [metadata "CA-p4"]. ceq valp(update(S,I),J) = valp(S,J) if J = I /\ tmp(S,I) <= valp(S,I) [metadata "CA-p5"]. ceq tmp(update(S,I),J) = valp(S,J) if J = I /\ statusp(S,I)= gotval /\ statusc(S) = busy /\ tmp(S,I)<= valp(S,I). ceq tmp(update(S,I),J) = tmp(S,J) if J ~ I = false /\ statusp(S,I)= gotval /\ statusc(S) = busy /\ tmp(S,I)<= valp(S,I). ceq tmp(update(S,I),J) = tmp(S,J) if J = I /\ statusp(S,I)~ gotval = false . ceq tmp(update(S,I),J) = tmp(S,J) if J = I /\ statusc(S)~ busy = false . ceq tmp(update(S,I),J) = tmp(S,J) if J = I /\ valp(S,I)< tmp(S,I) . --- gotoidle --- ceq statusc(gotoidle(S,I)) = idlec if statusc(S) = busy /\ statusp(S,I) = updated . ceq statusc(gotoidle(S,I)) = statusc(S) if statusc(S) ~ busy = false . ceq statusc(gotoidle(S,I)) = statusc(S) if statusp(S,I) ~ updated = false . eq valc(gotoidle(S,I)) = valc(S). ceq statusp(gotoidle(S,I),J) = idlep if J = I /\ statusp(S,I) = updated /\ statusc(S) = busy [metadata "CA-g1"]. ceq statusp(gotoidle(S,I),J) = statusp(S,J) if J ~ I = false [metadata "CA-g2"]. ceq statusp(gotoidle(S,I),J) = statusp(S,J) if statusp(S,I)~ updated = false[metadata "CA-g3"]. ceq statusp(gotoidle(S,I),J) = statusp(S,J) if statusc(S)~ busy = false [metadata "CA-g4"]. eq valp(gotoidle(S,I),J) = valp(S,J). ceq tmp(gotoidle(S,I),J) = 0 if J = I /\ statusp(S,I) = updated /\ statusc(S) = busy . ceq tmp(gotoidle(S,I),J) = tmp(S,J) if J ~ I = false . ceq tmp(gotoidle(S,I),J) = tmp(S,J) if statusp(S,I)~ updated = false . ceq tmp(gotoidle(S,I),J) = tmp(S,J) if statusc(S)~ busy = false . --- endfth) (fth CLOUDL is inc CLOUD . var S : Sys . var I : Client . ceq [lemma-inv1]: tmp(S,I) = valc(S) if statusp(S,I) = gotval [nonexec]. endfth) (goal CLOUDL |- ceq valp(S:Sys,I:Client) = valc(S:Sys) if statusp(S:Sys,I:Client) = updated ;) (set ind on S:Sys .) (apply SI .) --- init --- (apply TC IP RD .) --- getval --- (apply TC CA IP RD .) --- gotoidle --- (apply TC CA IP RD .) --- modval --- (apply TC CA IP RD .) --- update --- (apply TC CA RD .) --- 1. draw the proof tree correspoding to the partial proof above --- 2. complete the proof --- 3. draw the rest of the proof tree