Commit cd87a6ce authored by Christian Müller's avatar Christian Müller

fix easychair spec

parent 425a4261
p cnf 107 116
31 0
p cnf 83 92
23 0
-23 24 0
-23 31 0
-24 25 0
-24 26 0
-25 -1 2 0
-26 27 0
-26 28 0
-27 -3 4 0
-28 29 0
-28 30 0
-29 1 -2 0
-30 3 -4 0
-31 32 0
-31 39 0
-32 33 0
-32 34 0
-33 -1 2 0
-33 -5 6 0
-34 35 0
-34 36 0
-35 -3 4 0
-35 -7 8 0
-36 37 0
-36 38 0
-37 1 -2 0
-38 3 -4 0
-37 5 -6 0
-38 7 -8 0
-39 40 0
-39 47 0
-40 41 0
-40 42 0
-41 -5 6 0
-41 -9 10 0
-42 43 0
-42 44 0
-43 -7 8 0
-43 -11 12 0
-44 45 0
-44 46 0
-45 5 -6 0
-46 7 -8 0
-45 9 -10 0
-46 11 -12 0
-47 48 0
-47 63 0
-47 55 0
-48 49 0
-48 50 0
-49 -9 10 0
-49 -13 14 0
-50 51 0
-50 52 0
-51 -11 12 0
-51 -15 16 0
-52 53 0
-52 54 0
-53 -13 14 0
-54 55 0
-54 56 0
-55 -15 16 0
-56 57 0
-56 58 0
-57 9 -10 0
-58 59 0
-58 60 0
-59 13 -14 0
-60 61 0
-60 62 0
-61 11 -12 0
-62 15 -16 0
-53 13 -14 0
-54 15 -16 0
-55 56 0
-55 57 0
-56 -17 -18 0
-57 58 0
-57 59 0
-58 -17 -19 0
-59 60 0
-59 61 0
-60 -20 -17 0
-61 62 0
-61 63 0
-62 -20 -21 0
-63 64 0
-63 79 0
-64 65 0
-64 66 0
-65 -17 18 0
-66 67 0
-66 68 0
-67 -19 20 0
-68 69 0
-68 70 0
-69 -21 22 0
-70 71 0
-70 72 0
-71 -23 24 0
-72 73 0
-72 74 0
-73 17 -18 0
-74 75 0
-74 76 0
-75 21 -22 0
-76 77 0
-76 78 0
-77 19 -20 0
-78 23 -24 0
-63 65 0
-64 -20 -18 0
-65 66 0
-65 67 0
-66 -20 -19 0
-67 68 0
-67 69 0
-68 -17 -21 0
-69 70 0
-69 71 0
-70 -18 -19 0
-71 72 0
-71 73 0
-72 -22 -21 0
-73 74 0
-73 75 0
-74 -22 -19 0
-75 76 0
-75 77 0
-76 -21 -19 0
-77 78 0
-77 79 0
-78 -22 -18 0
-79 80 0
-79 81 0
-80 -25 -26 0
-80 -21 -18 0
-81 82 0
-81 83 0
-82 -25 -27 0
-83 84 0
-83 85 0
-84 -28 -25 0
-85 86 0
-85 87 0
-86 -28 -29 0
-87 88 0
-87 89 0
-88 -28 -26 0
-89 90 0
-89 91 0
-90 -28 -27 0
-91 92 0
-91 93 0
-92 -25 -29 0
-93 94 0
-93 95 0
-94 -26 -27 0
-95 96 0
-95 97 0
-96 -30 -29 0
-97 98 0
-97 99 0
-98 -30 -27 0
-99 100 0
-99 101 0
-100 -29 -27 0
-101 102 0
-101 103 0
-102 -30 -26 0
-103 104 0
-103 105 0
-104 -29 -26 0
-105 106 0
-105 107 0
-106 -30 -25 0
-107 -30 -28 0
-82 -22 -17 0
-83 -22 -20 0
......@@ -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)
!Conf(x,p) -> Assign += (x,p)
forallmay x:A,p:P,r:R
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
(Assign(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (Assign(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
Target
......
......@@ -7,14 +7,14 @@ forallmay x:A,p:P
forallmay x:A,p:P
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall xa:A,xb:A,p:P (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:A,p:P (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
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)
}
Declassify
¬ Conf(xa,p)
Target
Read(xa:A,xb:A,p:P)
Causality
a:A
......@@ -3,11 +3,11 @@ Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x:X,p:P
!Conf(x,p) -> Ass += (x,p)
!Conf(x,p) -> Assign += (x,p)
forall x:X,p:P,r:R
(Ass(x,p) ∧ O(p,r)) -> Read += (x,p,r)
(Assign(x,p) ∧ O(p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
......
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