Commit 23439d04 authored by Christian Müller's avatar Christian Müller

easychairexamples

parent 2aa2d6c3
p cnf 3 2
3 0
-3 1 2 0
p cnf 35 44
7 0
-7 8 0
-7 9 0
-8 -1 -2 0
-9 10 0
-9 11 0
-10 -1 -3 0
-11 12 0
-11 13 0
-12 -4 -1 0
-13 14 0
-13 15 0
-14 -4 -5 0
-15 16 0
-15 17 0
-16 -4 -2 0
-17 18 0
-17 19 0
-18 -4 -3 0
-19 20 0
-19 21 0
-20 -1 -5 0
-21 22 0
-21 23 0
-22 -2 -3 0
-23 24 0
-23 25 0
-24 -6 -5 0
-25 26 0
-25 27 0
-26 -6 -3 0
-27 28 0
-27 29 0
-28 -5 -3 0
-29 30 0
-29 31 0
-30 -6 -2 0
-31 32 0
-31 33 0
-32 -5 -2 0
-33 34 0
-33 35 0
-34 -6 -1 0
-35 -6 -4 0
......@@ -8,7 +8,7 @@ forallmay x,p,r
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop {
forall xa,xb,p,r (A(x1,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
forallmay x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
Target
......
......@@ -7,8 +7,8 @@ forallmay x,p
forallmay x,p
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall xa,xb,p (A(xa,p) ∧ Acc(xb,p)) -> Acc += (xa,xb,p)
forall x,p (A(x,p) ∧ O(x,p,r)) -> Acc += (x,p)
forall xa,xb,p (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x,p (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
}
Declassify
......@@ -17,4 +17,4 @@ Declassify
Target
Acc(xa,xb,p)
Read(xa,xb,p)
Workflow
forallmay x,p
True -> Conf += (x,p)
forallmay x,p
!Conf(x,p) -> Ass += (x,p)
forallmay x,p,r
Ass(x,p) -> Review += (x,p,r)
loop {
forall xa,xb,p,r (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
Declassify
¬ Conf(xa,p)
Target
Read(xa,xb,p,r)
\ No newline at end of file
......@@ -2,7 +2,7 @@ Workflow
forallmay i True -> R += (i)
forallmay i,j (R(i) ∧ R(j)) -> S += (i,j)
forallmay i,j,k (S(i,j,k) ∧ S(i,j,k)) -> T += (i,j,k)
forallmay i,j,k (S(i,j) ∧ S(j,k)) -> T += (i,j,k)
Target
......
......@@ -2,7 +2,7 @@ Workflow
forallmay i True -> R += (i)
forallmay i,j (R(i) ∧ R(j)) -> S += (i,j)
forallmay i,j,k (S(i,j,k) ∧ S(i,j,k)) -> T += (i,j,k)
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
......
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