Commit dc18ea40 authored by Christian Müller's avatar Christian Müller
Browse files

measure scripts, better examples

parent a9050f9d
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a) ∧ ¬ T3(a)) -> T4 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> T += (b, a)
forallmay a,b
(T3(a) ∧ T4(b)) -> U += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
U(a1, a2)
Causality
ca, cb, cc
......@@ -3,12 +3,12 @@ Workflow
forallmay x:A,p:P
True -> Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) -> Ass += (x,p)
forallmay x:A,p:P
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
!Conf(x,p) -> Assign += (x,p)
forall x:A,p:P
(Assign(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall xa:A,xb:A,p:P (Ass(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:A,p:P (Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:A,p:P (Assign(x,p) ∧ O(x,p)) -> Acc += (x,p)
}
Declassify
......
......@@ -16,3 +16,7 @@ O(x:X,p:P,r:R): G ¬ Conf(xt:X,p:P)
Target
Comm(xt:X, yt:X, pt:P)
Causality
a:X
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
Target
J(x,y)
Workflow
forallmay i True -> R += (i)
forallmay i,j (R(i) ∧ R(j)) -> S += (i,j)
forallmay i,j,k (S(i,j) ∧ S(j,k)) -> T += (i,j,k)
forallmay i,j,k,l (T(i,j,k) ∧ T(j,k,l)) -> U += (i,j,k,l)
Target
U(u,v,w,x)
\ No newline at end of file
Workflow
loop {
choose {
forallmay x:User, i:Info
Written(i, x) → Read += (x, i)
} {
forallmay x:User, i:Info
Oracle(i, x) → Written += (i, x)
}
}
Declassify
Oracle(i:Info,x:User): F (Written(u:User, i:Info))
Target
Read(u:User, info:Info)
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> S += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
S(a1, a2)
Causality
ca, cb
Workflow
forallmay i True -> R += (i)
forallmay i,j (R(i)) -> S += (i,j)
Target
S(x,y)
Workflow
forallmay i True -> R += (i)
forallmay i,j (R(i) ∧ R(j)) -> S += (i,j)
forallmay i,j,k (S(i,j) ∧ S(j,k)) -> T += (i,j,k)
forallmay i,j (R(i)) -> S += (i,j)
forallmay i,j,k (S(i,j)) -> T += (i,j,k)
Target
......
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