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

examples

parent 71179b3a
p cnf 35 44
7 0
-7 8 0
-7 9 0
-8 -1 -2 0
-9 10 0
-9 11 0
-10 -3 -4 0
-11 12 0
-11 13 0
-12 -3 -5 0
-13 14 0
-13 15 0
-14 -3 -2 0
-15 16 0
-15 17 0
-16 -6 -1 0
p cnf 255 359
17 0
-17 18 0
-17 19 0
-18 -6 -3 0
-18 -1 -2 0
-19 20 0
-19 21 0
-20 -6 -4 0
-20 -1 -3 0
-21 22 0
-21 23 0
-22 -6 -2 0
-22 -1 -4 0
-23 24 0
-23 25 0
-24 -6 -5 0
-24 -1 -5 0
-25 26 0
-25 27 0
-26 -1 -3 0
-26 -3 -6 0
-27 28 0
-27 29 0
-28 -1 -4 0
-28 -3 -7 0
-29 30 0
-29 31 0
-30 -1 -5 0
-30 -3 -8 0
-31 32 0
-31 33 0
-32 -4 -2 0
-32 -3 -9 0
-33 34 0
-33 35 0
-34 -4 -5 0
-35 -2 -5 0
-34 -3 -10 0
-35 36 0
-35 37 0
-36 -3 -11 0
-37 38 0
-37 39 0
-38 -1 -12 0
-39 40 0
-39 41 0
-40 -1 -13 0
-41 42 0
-41 43 0
-42 -1 -14 0
-43 44 0
-43 45 0
-44 -1 -6 0
-45 46 0
-45 47 0
-46 -1 -7 0
-47 48 0
-47 49 0
-48 -1 -8 0
-49 50 0
-49 51 0
-50 -1 -9 0
-51 52 0
-51 53 0
-52 -1 -10 0
-53 54 0
-53 55 0
-54 -1 -11 0
-55 56 0
-55 57 0
-56 -1 -15 0
-57 58 0
-57 59 0
-58 -5 -12 0
-59 60 0
-59 61 0
-60 -5 -14 0
-61 62 0
-61 63 0
-62 -5 -6 0
-63 64 0
-63 65 0
-64 -5 -7 0
-65 66 0
-65 67 0
-66 -5 -11 0
-67 68 0
-67 69 0
-68 -2 -3 0
-69 70 0
-69 71 0
-70 -2 -12 0
-71 72 0
-71 73 0
-72 -2 -13 0
-73 74 0
-73 75 0
-74 -2 -14 0
-75 76 0
-75 77 0
-76 -2 -6 0
-77 78 0
-77 79 0
-78 -2 -7 0
-79 80 0
-79 81 0
-80 -2 -8 0
-81 82 0
-81 83 0
-82 -2 -9 0
-83 84 0
-83 85 0
-84 -2 -10 0
-85 86 0
-85 87 0
-86 -2 -11 0
-87 88 0
-87 89 0
-88 -2 -15 0
-89 90 0
-89 91 0
-90 -16 -4 0
-91 92 0
-91 93 0
-92 -16 -5 0
-93 94 0
-93 95 0
-94 -16 -3 0
-95 96 0
-95 97 0
-96 -16 -12 0
-97 98 0
-97 99 0
-98 -16 -13 0
-99 100 0
-99 101 0
-100 -16 -14 0
-101 102 0
-101 103 0
-102 -16 -6 0
-103 104 0
-103 105 0
-104 -16 -7 0
-105 106 0
-105 107 0
-106 -16 -8 0
-107 108 0
-107 109 0
-108 -16 -9 0
-109 110 0
-109 111 0
-110 -16 -10 0
-111 112 0
-111 113 0
-112 -16 -11 0
-113 114 0
-113 115 0
-114 -16 -15 0
-115 116 0
-115 117 0
-116 -3 -12 0
-117 118 0
-117 119 0
-118 -3 -13 0
-119 120 0
-119 121 0
-120 -3 -14 0
-121 122 0
-121 123 0
-122 -3 -15 0
-123 124 0
-123 125 0
-124 -12 -14 0
-125 126 0
-125 127 0
-126 -12 -6 0
-127 128 0
-127 129 0
-128 -12 -7 0
-129 130 0
-129 131 0
-130 -12 -11 0
-131 132 0
-131 133 0
-132 -13 -14 0
-133 134 0
-133 135 0
-134 -13 -6 0
-135 136 0
-135 137 0
-136 -13 -7 0
-137 138 0
-137 139 0
-138 -13 -8 0
-139 140 0
-139 141 0
-140 -13 -9 0
-141 142 0
-141 143 0
-142 -13 -10 0
-143 144 0
-143 145 0
-144 -13 -11 0
-145 146 0
-145 147 0
-146 -13 -15 0
-147 148 0
-147 149 0
-148 -14 -6 0
-149 150 0
-149 151 0
-150 -14 -7 0
-151 152 0
-151 153 0
-152 -14 -11 0
-153 154 0
-153 155 0
-154 -6 -7 0
-155 156 0
-155 157 0
-156 -6 -11 0
-157 158 0
-157 159 0
-158 -7 -11 0
-159 160 0
-159 161 0
-160 -8 -9 0
-161 162 0
-161 163 0
-162 -8 -10 0
-163 164 0
-163 165 0
-164 -8 -11 0
-165 166 0
-165 167 0
-166 -8 -15 0
-167 168 0
-167 169 0
-168 -9 -10 0
-169 170 0
-169 171 0
-170 -9 -11 0
-171 172 0
-171 173 0
-172 -9 -15 0
-173 174 0
-173 175 0
-174 -10 -11 0
-175 176 0
-175 177 0
-176 -10 -15 0
-177 178 0
-177 179 0
-178 -7 -15 0
-179 180 0
-179 181 0
-180 -6 -15 0
-181 182 0
-181 183 0
-182 -14 -15 0
-183 184 0
-183 185 0
-184 -12 -15 0
-185 186 0
-185 187 0
-186 -5 -15 0
-187 188 0
-187 189 0
-188 -4 -15 0
-189 190 0
-189 191 0
-190 -4 -11 0
-191 192 0
-191 193 0
-192 -7 -10 0
-193 194 0
-193 195 0
-194 -6 -10 0
-195 196 0
-195 197 0
-196 -14 -10 0
-197 198 0
-197 199 0
-198 -12 -10 0
-199 200 0
-199 201 0
-200 -5 -10 0
-201 202 0
-201 203 0
-202 -4 -10 0
-203 204 0
-203 205 0
-204 -7 -9 0
-205 206 0
-205 207 0
-206 -6 -9 0
-207 208 0
-207 209 0
-208 -14 -9 0
-209 210 0
-209 211 0
-210 -12 -9 0
-211 212 0
-211 213 0
-212 -5 -9 0
-213 214 0
-213 215 0
-214 -4 -9 0
-215 216 0
-215 217 0
-216 -7 -8 0
-217 218 0
-217 219 0
-218 -6 -8 0
-219 220 0
-219 221 0
-220 -14 -8 0
-221 222 0
-221 223 0
-222 -12 -8 0
-223 224 0
-223 225 0
-224 -5 -8 0
-225 226 0
-225 227 0
-226 -4 -8 0
-227 228 0
-227 229 0
-228 -4 -7 0
-229 230 0
-229 231 0
-230 -4 -6 0
-231 232 0
-231 233 0
-232 -4 -14 0
-233 234 0
-233 235 0
-234 -12 -13 0
-235 236 0
-235 237 0
-236 -5 -13 0
-237 238 0
-237 239 0
-238 -4 -13 0
-239 240 0
-239 241 0
-240 -4 -12 0
-241 242 0
-241 243 0
-242 -5 -3 0
-243 244 0
-243 245 0
-244 -4 -3 0
-245 246 0
-245 247 0
-246 -16 -2 0
-247 248 0
-247 249 0
-248 -5 -2 0
-249 250 0
-249 251 0
-250 -4 -2 0
-251 252 0
-251 253 0
-252 -4 -5 0
-253 254 0
-253 255 0
-254 -16 -1 0
-255 -11 -15 0
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)
Declassify
O(x): F (T1(x))
Target
S(a1, a2)
Causality
ca
......@@ -20,7 +20,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): F (T1(x) ∨ T2(x) ∨ T3(x))
Target
......
Workflow
forallmay i,j True -> 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)
......@@ -14,8 +14,8 @@ forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
forall i,j M(i,j) -> N += (i,j)
forall i,j N(i,j) -> O += (i,j)
forall i,j N(i,j) -> P += (i,j)
Target
O(x,y)
P(x,y)
Workflow
forallmay i,j True -> 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)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
forall i,j M(i,j) -> N += (i,j)
forall i,j N(i,j) -> P += (i,j)
Target
P(x,y)
......@@ -14,13 +14,13 @@ forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
forall i,j M(i,j) -> N += (i,j)
forall i,j N(i,j) -> O += (i,j)
forall i,j O(i,j) -> P += (i,j)
forall i,j N(i,j) -> P += (i,j)
forall i,j P(i,j) -> Q += (i,j)
forall i,j Q(i,j) -> R += (i,j)
forall i,j R(i,j) -> S += (i,j)
forall i,j S(i,j) -> T += (i,j)
forall i,j T(i,j) -> U += (i,j)
Target
T(x,y)
U(x,y)
Workflow
forallmay i,j True -> 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)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
forall i,j M(i,j) -> N += (i,j)
forall i,j N(i,j) -> P += (i,j)
forall i,j P(i,j) -> Q += (i,j)
forall i,j Q(i,j) -> R += (i,j)
forall i,j R(i,j) -> S += (i,j)
forall i,j S(i,j) -> T += (i,j)
forall i,j T(i,j) -> U += (i,j)
Target
U(x,y)
......@@ -12,9 +12,12 @@ loop {
Declassify
Oracle(i:Info,x:User): F (Written(u:User, i:Info))
Oracle(i:Info,x:User): F (Written(i:Info, u:User))
Target
Read(u:User, info:Info)
Causality
ac:User
Measurement Mon May 15 17:10:11 WEST 2017
results/causal2_causal.ltl:
FOLTL length: 6801
LTL length: 47672
sat
real 195.31
user 195.14
sys 0.16
Finished successfully
results/causal2_stubborn.ltl:
FOLTL length: 5078
LTL length: 6880
unsat
real 26.73
user 26.73
sys 0.00
Finished successfully
results/causal3_causal.ltl:
FOLTL length: 12974
LTL length: 213970
Timeout after 15m
results/causal3_stubborn.ltl:
FOLTL length: 9368
LTL length: 14608
unsat
real 51.34
user 51.31
sys 0.02
Finished successfully
results/easychair3_causal.ltl:
FOLTL length: 5857
LTL length: 51702
sat
real 17.84
user 17.74
sys 0.09
Finished successfully
results/easychair3_stubborn.ltl:
FOLTL length: 5073
LTL length: 7482
unsat
real 2.19
user 2.17
sys 0.01
Finished successfully
results/easychair_causal.ltl:
FOLTL length: 6318
LTL length: 108512
sat
real 41.61
user 41.36
sys 0.24
Finished successfully
results/easychair_linear_causal.ltl:
FOLTL length: 4693
LTL length: 44240
sat
real 8.49
user 8.39
sys 0.10
Finished successfully
results/easychair_linear_stubborn.ltl:
FOLTL length: 3851
LTL length: 4787
unsat
real 0.75
user 0.75
sys 0.00
Finished successfully
results/easychair_stubborn.ltl:
FOLTL length: 5452
LTL length: 8304
unsat
real 2.14
user 2.14
sys 0.00
Finished successfully
results/linear10_stubborn.ltl:
FOLTL length: 13662
LTL length: 26551
sat
real 0.89
user 0.82
sys 0.06
Finished successfully
results/notebook_stubborn.ltl:
FOLTL length: 1413
LTL length: 952
unsat
real 0.00
user 0.00
sys 0.00
Finished successfully
results/tree2_stubborn.ltl:
FOLTL length: 1122
LTL length: 1567
unsat
real 0.08
user 0.08
sys 0.00
Finished successfully
results/tree3_stubborn.ltl:
FOLTL length: 2067
LTL length: 12596
unsat
real 6.20
user 6.17
sys 0.03
Finished successfully
results/tree4_stubborn.ltl:
FOLTL length: 3356
LTL length: 145751
Timeout after 15m
results/typedtree2_stubborn.ltl:
FOLTL length: 1122
LTL length: 677
unsat
real 0.03
user 0.02
sys 0.00
Finished successfully
results/typedtree3_stubborn.ltl:
FOLTL length: 2067
LTL length: 1208
unsat
real 0.09
user 0.09
sys 0.00
Finished successfully
results/typedtree4_stubborn.ltl:
FOLTL length: 3356
LTL length: 1925
unsat
real 0.21
user 0.21
sys 0.00
Finished successfully
results/typedtree5_stubborn.ltl:
FOLTL length: 5037
LTL length: 2852
unsat
real 0.41
user 0.40
sys 0.00
Finished successfully
......@@ -52,9 +52,14 @@ object Encoding extends LazyLogging {
}
case NondetChoice(l1, l2) => {
val newnodes1 = n1 +: (0 until l1.size - 1).toList.map(_ => makeNode()) :+ n2
// make sure that at least one of the two branches has one node, so they will never build 2 edges between the same node
val newl1 = if (l1.length == l2.length && l1.length == 1) {
l1 :+ makeId()
} else l1
val newnodes1 = n1 +: (0 until newl1.size - 1).toList.map(_ => makeNode()) :+ n2
val edgenodes1 = newnodes1.sliding(2).toList
val edges1 = for ((step, List(start, end)) <- l1.zip(edgenodes1)) yield {
val edges1 = for ((step, List(start, end)) <- newl1.zip(edgenodes1)) yield {
makeblock(step, start, end, makeNode, makeId)
}
val newnodes2 = n1 +: (0 until l2.size - 1).toList.map(_ => makeNode()) :+ n2
......
......@@ -81,8 +81,8 @@ object Main extends App with LazyLogging {
folder.mkdirs()
folder.listFiles().foreach(_.delete())
// Fill results
for ((k, value) <- ExampleWorkflows.examples) {
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
generateExample(k)
}
}
\ No newline at end of file
......@@ -9,15 +9,22 @@ import com.typesafe.scalalogging.LazyLogging
object WorkflowParser extends RegexParsers with LazyLogging {
def addChoicePredicates(blocks: List[Block]) = {
def addChoice(blocks: List[Block], next:Int):List[Block] = {
var i = -1; // start at 0
def next() = {
i = i + 1
i
}
def addChoice(blocks: List[Block], next:() => Int):List[Block] = {
blocks match {
case ForallMayBlock(v, _, stmts) :: xs => ForallMayBlock(v, s"choice$next", stmts) :: addChoice(xs, next + 1)
case Loop(blocks) :: xs => Loop(addChoice(blocks, next)) :: addChoice(xs, next + blocks.size)
case ForallMayBlock(v, _, stmts) :: xs => ForallMayBlock(v, s"choice${next()}", stmts) :: addChoice(xs, next)
case Loop(blocks) :: xs => Loop(addChoice(blocks, next)) :: addChoice(xs, next)
case NondetChoice(left, right) :: xs => NondetChoice(addChoice(left, next), addChoice(right, next)) :: addChoice(xs, next)
case x :: xs => x :: addChoice(xs, next)
case Nil => Nil
}
}
addChoice(blocks, 0)
addChoice(blocks, next)
}
def allpredicates(list: List[Block]) = {
......
......@@ -82,7 +82,7 @@ object Declassification extends {
def apply(spec: Spec) = {
val sameoracles = for ((o,t) <- spec.declass) yield {
// Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(And(t.in(T1), t.in(T2)), Globally(Eq(o.in(T1), o.in(T2)))))
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Globally(Eq(o.in(T1), o.in(T2)))))
}
And.make(sameoracles)
}
......
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