Commit 8f5e5d7d authored by Christian Müller's avatar Christian Müller

fixed linear from atva

parent 26635823
Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x:X,p:P
!Conf(x,p) -> Assign += (x,p)
forall x:X,y:X,p:P,q:P
(Conf(x,p) ∧ ¬ Conf(y,p) ∧ Assign(x,p) ∧ Assign(y,q)) -> Assign -= (y,q)
forall x:X,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
Target
Comm(xt:X, yt:X, pt:P)
Causality
a:X
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment