diff --git a/examples/omitting/conference_linear_safe.spec b/examples/omitting/conference_linear_safe.spec new file mode 100644 index 0000000000000000000000000000000000000000..d8b3600eaed29d9cdb41be30f8f5611f43d8cb67 --- /dev/null +++ b/examples/omitting/conference_linear_safe.spec @@ -0,0 +1,24 @@ +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