Commit 47d29a28 authored by Christian Müller's avatar Christian Müller

add examples

parent 1e8f5880
forallmay x,p
True -> Conf += (x,p)
forallmay x,p
!Conf(x,p) -> Ass += (x,p)
forallmay x,p,r
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop {
forall x,y,p,r (A(x,p) ∧ Review(y,p,r)) -> Read += (x,y,p,r)
forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
forallmay x,p
True -> Conf += (x,p)
forallmay x,p
!Conf(x,p) -> Ass += (x,p)
forallmay x,p
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall x,y,p (A(x,p) ∧ Acc(y,p)) -> Read += (x,y,p)
forall x,p (A(x,p) ∧ O(x,p,r)) -> Acc += (x,p)
}
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 x,y,p,r (A(x,p) ∧ Review(y,p,r)) -> Read += (x,y,p,r)
forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
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,l (T(i,j,k) ∧ T(j,k,l)) -> U += (i,j,k,l)
forallmay x,s True -> Q += (x,s)
loop {
forall x,y,s R(y,s) -> S += (x,y,s)
forall x,s Q(x,s) -> R += (x,s)
}
\ No newline at end of file
forall x,y,s R(y,s) → S += (x,y,s)
forall x,s Q(x,s) → R += (x,s)
}
......@@ -35,6 +35,13 @@ object ExampleWorkflows extends LazyLogging {
// stubborn: counterexample (R is exactly O)
"simpleNoChoice" -> Fun("R", List("x","s")),
// stubborn: no counterexample (no oracle)
"simpleChoiceNoOracle" -> Fun("R", List("x","s"))
"simpleChoiceNoOracle" -> Fun("R", List("x","s")),
// stubborn: no counterexample
"easychairNoOracle" -> Fun("Read", List("x","y","p","r")),
// stubborn: no counterexample (TODO: still missing declass, ce for now)
"easychair" -> Fun("Read", List("x","y","p","r")),
// no counterexample
"linear" -> Fun("U", List("x", "y", "z", "q")),
"easychair3NoOracle" -> Fun("Read", List("x","y","p"))
)
}
......@@ -3,7 +3,4 @@ object Test extends App {
val agents = List("a", "b", "c")
println(agents.combinations(2).toList)
}
\ No newline at end of file
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