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

add target to wf spec file

parent 47d29a28
...@@ -27,8 +27,11 @@ nondeter_sat (int argc, char** argv) ...@@ -27,8 +27,11 @@ nondeter_sat (int argc, char** argv)
} }
aalta_formula* af; aalta_formula* af;
printf("Simplifying ...");
af = aalta_formula(in).unique(); af = aalta_formula(in).unique();
af = af->simplify (); af = af->simplify ();
printf("Checking satisfiability...");
nondeter_checker ch (af); nondeter_checker ch (af);
......
p cnf 15 17 p cnf 35 44
5 0 7 0
-5 6 0
-5 7 0
-6 -1 -2 0
-7 8 0 -7 8 0
-7 9 0 -7 9 0
-8 -1 -3 0 -8 -1 -2 0
-9 10 0 -9 10 0
-9 11 0 -9 11 0
-10 -1 -4 0 -10 -1 -3 0
-11 12 0 -11 12 0
-11 13 0 -11 13 0
-12 -2 -3 0 -12 -4 -1 0
-13 14 0 -13 14 0
-13 15 0 -13 15 0
-14 -2 -4 0 -14 -4 -5 0
-15 -3 -4 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
Workflow
forallmay x,p forallmay x,p
True -> Conf += (x,p) True -> Conf += (x,p)
forallmay x,p forallmay x,p
...@@ -5,7 +7,10 @@ forallmay x,p ...@@ -5,7 +7,10 @@ forallmay x,p
forallmay x,p,r forallmay x,p,r
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r) (Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop { loop {
forall x,y,p,r (A(x,p) ∧ Review(y,p,r)) -> Read += (x,y,p,r) 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) forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
} }
Target
(Conf(x,p) ∧ Read(xa, xb, p, r))
Workflow
forallmay x,p forallmay x,p
True -> Conf += (x,p) True -> Conf += (x,p)
forallmay x,p forallmay x,p
...@@ -5,7 +7,10 @@ forallmay x,p ...@@ -5,7 +7,10 @@ forallmay x,p
forallmay x,p forallmay x,p
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p) (Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop { loop {
forall x,y,p (A(x,p) ∧ Acc(y,p)) -> Read += (x,y,p) 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 x,p (A(x,p) ∧ O(x,p,r)) -> Acc += (x,p)
} }
Target
(Conf(xa, p) ∧ Acc(xa,xb,p))
Workflow
forallmay x,p forallmay x,p
True -> Conf += (x,p) True -> Conf += (x,p)
forallmay x,p forallmay x,p
...@@ -5,7 +7,10 @@ forallmay x,p ...@@ -5,7 +7,10 @@ forallmay x,p
forallmay x,p,r forallmay x,p,r
Ass(x,p) -> Review += (x,p,r) Ass(x,p) -> Review += (x,p,r)
loop { loop {
forall x,y,p,r (A(x,p) ∧ Review(y,p,r)) -> Read += (x,y,p,r) 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) forall x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
} }
Target
(Conf(xa,p) ∧ Read(xa,xb,p,r))
\ No newline at end of file
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)
Target
T(x,y,z)
Workflow
forallmay i True -> R += (i) forallmay i True -> R += (i)
forallmay i,j (R(i) ∧ R(j)) -> S += (i,j) 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,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 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
forallmay x,s O(s) -> Q += (x,s) forallmay x,s O(s) -> Q += (x,s)
loop { loop {
forall x,y,s R(y,s) -> S += (x,y,s) forall x,y,s R(y,s) -> S += (x,y,s)
forall x,s Q(x,s) -> R += (x,s) forall x,s Q(x,s) -> R += (x,s)
} }
\ No newline at end of file
Target
S(x,y,s)
Workflow
forallmay x,s True -> Q += (x,s) forallmay x,s True -> Q += (x,s)
loop { loop {
forall x,y,s R(y,s) → S += (x,y,s) forall x,y,s R(y,s) → S += (x,y,s)
forall x,s Q(x,s) → R += (x,s) forall x,s Q(x,s) → R += (x,s)
} }
Target
S(x,y,s)
Workflow
forallmay x,s
O(s) -> R += (x,s)
Target
R(x,s)
\ No newline at end of file
forallmay x,s
O(s) -> R += (x,s)
\ No newline at end of file
Workflow
forallmay x,s forallmay x,s
True -> R += (x,s) True -> R += (x,s)
\ No newline at end of file Target
R(x,s)
Workflow
forall x,s
O(s) -> R += (x,s)
Target
R(x,s)
\ No newline at end of file
forall x,s
O(s) -> R += (x,s)
\ No newline at end of file
...@@ -10,38 +10,19 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -10,38 +10,19 @@ import com.typesafe.scalalogging.LazyLogging
object ExampleWorkflows extends LazyLogging { object ExampleWorkflows extends LazyLogging {
val folder = new File("examples") val FOLDER = new File("examples")
val ENDING = ".spec"
val examples = (for (f <- folder.listFiles() if f.isFile() && f.getName.endsWith(".wf")) yield { val examples = (for (f <- FOLDER.listFiles() if f.isFile() && f.getName.endsWith(".wf")) yield {
val s = Source.fromFile(f).mkString val s = Source.fromFile(f).mkString
val wf = WorkflowParser.parseWorkflow(s) val spec = WorkflowParser.parseSpec(s)
if (!wf.successful) { if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $wf") logger.error(s"Parsing of $f unsuccessful: $spec")
} }
// drop file ending // drop file ending
val name = f.getName.replace(".wf", "") val name = f.getName.replace(ENDING, "")
name -> wf.get name -> (spec.get._1, spec.get._2)
}) toMap }) toMap
val targets = Map(
// stubborn: counterexample (S is copied from R and Q)
"prevexample" -> Fun("S", List("x","y","s")),
// stubborn: no counterexample (no oracle)
"prevexampleNoOracle" -> Fun("S", List("x","y","s")),
// stubborn: counterexample (R is exactly O cap choice0)
"simpleChoice" -> Fun("R", List("x", "s")),
// stubborn: counterexample (R is exactly O)
"simpleNoChoice" -> Fun("R", List("x","s")),
// stubborn: no counterexample (no oracle)
"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"))
)
} }
...@@ -16,11 +16,11 @@ object Main extends App with LazyLogging { ...@@ -16,11 +16,11 @@ object Main extends App with LazyLogging {
def generateExample(name: String) { def generateExample(name: String) {
logger.info(s"Generating $name") logger.info(s"Generating $name")
val w = ExampleWorkflows.examples(name) val (wf, target) = ExampleWorkflows.examples(name)
stubbornnoninter(name, w, ExampleWorkflows.targets(name)) stubbornnoninter(name, wf, target)
} }
def stubbornnoninter(name: String, w: Workflow, target: Fun) { def stubbornnoninter(name: String, w: Workflow, target: Term) {
logger.info(s"Encoding Workflow:\n$w") logger.info(s"Encoding Workflow:\n$w")
logger.info("Using only stubborn agents") logger.info("Using only stubborn agents")
val t1 = "pi1" val t1 = "pi1"
......
...@@ -20,4 +20,10 @@ object Utils { ...@@ -20,4 +20,10 @@ object Utils {
def allchoices(w: Workflow) = { def allchoices(w: Workflow) = {
w.steps flatMap (collectChoices _) toSet w.steps flatMap (collectChoices _) toSet
} }
def allagents(t: Term) = {
t.collect({
case Fun(_, _, as) => as
})
}
} }
\ No newline at end of file
...@@ -49,18 +49,19 @@ object WorkflowParser extends RegexParsers { ...@@ -49,18 +49,19 @@ object WorkflowParser extends RegexParsers {
} }
def VAR = "[a-zA-Z]+".r ^^ { str => Var(str) } def VAR = "[a-zA-Z][a-zA-Z0-9]*".r ^^ { str => Var(str) }
def tt = "True" ^^ { _ => True } def tt = "True" ^^ { _ => True }
def ff = "False" ^^ { _ => False } def ff = "False" ^^ { _ => False }
def AND = TERM ~ "∧" ~ TERM ^^ { case t1 ~ _ ~ t2 => And(t1, t2) } def AND = repsep(SIMPLETERM, "∧") ^^ { case ts => And.make(ts) }
def OR = TERM ~ "∨" ~ TERM ^^ { case t1 ~ _ ~ t2 => Or(t1, t2) } def OR = repsep(SIMPLETERM, "∨") ^^ { case ts => Or.make(ts) }
def NEG = ("¬" | "!") ~ TERM ^^ { case _ ~ t => Neg(t) } def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
def TUPLE = "(" ~> repsep(VAR, ",") <~ ")" def TUPLE = "(" ~> repsep(VAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) } def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def TERM:Parser[Term] = (tt | ff | FUN | "(" ~> AND <~ ")" | "(" ~> OR <~ ")" | NEG) def SIMPLETERM = (tt | ff | FUN )
def TERM:Parser[Term] = (SIMPLETERM | "(" ~> AND <~ ")" | "(" ~> OR <~ ")" | NEG )
def ADD = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) } def ADD = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
def REM = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) } def REM = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
...@@ -77,5 +78,8 @@ object WorkflowParser extends RegexParsers { ...@@ -77,5 +78,8 @@ object WorkflowParser extends RegexParsers {
Workflow(buildSig(choiceblocks), choiceblocks) Workflow(buildSig(choiceblocks), choiceblocks)
}} }}
def SPEC = "Workflow" ~> WORKFLOW ~ "Target" ~ TERM ^^ { case w ~ _ ~ t => (w, t) }
def parseWorkflow(s: String) = parseAll(WORKFLOW, s) def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
def parseSpec(s: String) = parseAll(SPEC, s)
} }
...@@ -37,7 +37,7 @@ object Noninterference { ...@@ -37,7 +37,7 @@ object Noninterference {
object Properties { object Properties {
// include optimizations for choices // include optimizations for choices
def noninterStubborn(w: Workflow, target: Fun) = { def noninterStubborn(w: Workflow, target: Term) = {
val t1 = "t1" val t1 = "t1"
val t2 = "t2" val t2 = "t2"
...@@ -46,15 +46,14 @@ object Properties { ...@@ -46,15 +46,14 @@ object Properties {
val cfg = sanecfg(graph) val cfg = sanecfg(graph)
val sem = exec(w.sig, graph) val sem = exec(w.sig, graph)
val agents = target.params.map(s => Var("a" + s.name)) val agents = allagents(target)
val newtarget = Fun(target.name, agents)
// choice and node predicates are equal in both runs (stubborn) // choice and node predicates are equal in both runs (stubborn)
val nodes = nodepredicates(graph) map (_.name) val nodes = nodepredicates(graph) map (_.name)
val choices = allchoices(w) map (_.name) val choices = allchoices(w) map (_.name)
val equals = nodes ++ choices val equals = nodes ++ choices
val noninter = Exists(agents, Finally(Neg(Eq(newtarget.in(t1), newtarget.in(t2))))) val noninter = Exists(agents, Finally(Neg(Eq(target.in(t1), target.in(t2)))))
// maybe add exists t1, t2. phi? // maybe add exists t1, t2. phi?
And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter) And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
......
...@@ -17,7 +17,7 @@ import de.tum.workflows.ExampleWorkflows ...@@ -17,7 +17,7 @@ import de.tum.workflows.ExampleWorkflows
class EncodingTest extends FlatSpec { class EncodingTest extends FlatSpec {
val w = ExampleWorkflows.examples("simpleChoice") val w = ExampleWorkflows.examples("simpleChoice")._1
// shorthands // shorthands
val n0 = Fun("n0", List()) val n0 = Fun("n0", List())
...@@ -103,7 +103,7 @@ class EncodingTest extends FlatSpec { ...@@ -103,7 +103,7 @@ class EncodingTest extends FlatSpec {
Stubborn("ax", choices, t1, t2), Stubborn("ax", choices, t1, t2),
Finally(Exists("as", Neg(Eq(ce.in(t1), ce.in(t2)))))))) Finally(Exists("as", Neg(Eq(ce.in(t1), ce.in(t2))))))))
val prop = Properties.noninterStubborn(w, Fun("R", List("x", "s"))) val prop = Properties.noninterStubborn(w, Fun("R", List("ax", "as")))
val (agents, res) = LTL.eliminateExistentials(prop) val (agents, res) = LTL.eliminateExistentials(prop)
......
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