Commit 44acea29 authored by Christian Müller's avatar Christian Müller

parser

parent acdef60c
...@@ -40,8 +40,8 @@ test in assembly := {} ...@@ -40,8 +40,8 @@ test in assembly := {}
//assemblyJarName in assembly := "niwo-ts.jar" assemblyJarName in assembly := "niwo-ts.jar"
//mainClass in assembly := Some("de.tum.niwo.TSCLI") mainClass in assembly := Some("de.tum.niwo.TSCLI")
assemblyJarName in assembly := "niwo-wf.jar" //assemblyJarName in assembly := "niwo-wf.jar"
mainClass in assembly := Some("de.tum.niwo.WFCLI") //mainClass in assembly := Some("de.tum.niwo.WFCLI")
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
B(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
Oracle(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
Invariant
∀ix:A,ip:P. (Assign#t1(ix,ip) <-> Assign#t2(ix,ip)),
∀ix:A,ip:P. (Conf#t1(ix,ip) <-> Conf#t2(ix,ip)),
∀iy:A,ip:P. ((Assign#t1(xt, ip) ∧ Assign#t1(iy,ip)) ⟹ (
(∀iq:P,ir:R. (Review#t1(iy,iq,ir) <-> Review#t2(iy,iq,ir))) ∧
(¬informed#t1(iy)) ∧
(∀iq:P,ir:R. (Read#t1(iy,iq,ir) <-> Read#t2(iy,iq,ir))) ∧
(∀iq:P. (Conf#t1(xt,ip) ⟹ Conf#t1(iy,iq))) ∧
(∀iz:A, iq:P. ((Assign#t1(iy, iq) ∧ Assign#t1(iz, iq)) ⟹ Assign#t1(iz,ip)))
)),
∀iy:A,ip:P,ir:R. (Review#t1(iy,ip,ir) ⟹ Assign#t1(iy,ip)),
∀iy:A,ip:P,ir:R. (Review#t2(iy,ip,ir) ⟹ Assign#t2(iy,ip))
Target
Read(xt:A, pt:P, rt:R)
Causality
a:A
...@@ -13,12 +13,25 @@ object TSCLI extends App with LazyLogging { ...@@ -13,12 +13,25 @@ object TSCLI extends App with LazyLogging {
Usage niwo-ts.jar FILE Usage niwo-ts.jar FILE
FILE should be a path to a FO Safety Game Description File. FILE should be a path to a FO Safety Game Description File.
If --elimChoice is given, all A predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to A predicates not changing over time.
If --approxElim is given, second order quantifier elimination is further approximated by not computing CNF for formulas that are too large.
This achieves a tremendous speed boost at the cost of accuracy.
""" """
if (args.length != 1) { if (args.length == 0) {
logger.info(usage) logger.info(usage)
} else { } else {
var elim = false
var approxelim = false
args.collect {
case "--elimChoice" => elim = true
case "--approxElim" => approxelim = true
}
val properties = InvProperties(stubborn = true, eliminateA = elim, approxElim = approxelim)
val file = args.last val file = args.last
logger.info(s"Using $file") logger.info(s"Using $file")
...@@ -30,7 +43,6 @@ object TSCLI extends App with LazyLogging { ...@@ -30,7 +43,6 @@ object TSCLI extends App with LazyLogging {
if (!spec.get.isSane) { if (!spec.get.isSane) {
logger.error(s"Sanity check of $file failed. Skipping file.") logger.error(s"Sanity check of $file failed. Skipping file.")
} else { } else {
val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)
Utils.check(new File(file).getName.stripSuffix(".spec"), "", spec.get, properties) Utils.check(new File(file).getName.stripSuffix(".spec"), "", spec.get, properties)
} }
} }
......
...@@ -16,9 +16,11 @@ object WFCLI extends App with LazyLogging { ...@@ -16,9 +16,11 @@ object WFCLI extends App with LazyLogging {
Usage niwo-wf.jar [--stubborn] [--elimChoice] FILE Usage niwo-wf.jar [--stubborn] [--elimChoice] FILE
FILE should be a path to a Workflow Description File. FILE should be a path to a Workflow Description File.
If --stubborn is given, all agents are assumed to be stubborn ignoring the model given in the specification file. If --stubborn is given, all agents are assumed to be stubborn.
If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance) If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to choice predicates not changing over time. With elimChoice turned off, that corresponds to choice predicates not changing over time.
If --approxElim is given, second order quantifier elimination is further approximated by not computing CNF for formulas that are too large.
This achieves a tremendous speed boost at the cost of accuracy.
""" """
if (args.length == 0) { if (args.length == 0) {
...@@ -27,11 +29,13 @@ object WFCLI extends App with LazyLogging { ...@@ -27,11 +29,13 @@ object WFCLI extends App with LazyLogging {
var causal = true var causal = true
var elim = false var elim = false
var approxelim = false
args.collect { args.collect {
case "--stubborn" => causal = false case "--stubborn" => causal = false
case "--elimChoice" => elim = true case "--elimChoice" => elim = true
case "--approxElim" => approxelim = true
} }
val properties = InvProperties(!causal, elim) val properties = InvProperties(stubborn = !causal, eliminateA = elim, approxElim = approxelim)
val file = args.last val file = args.last
......
...@@ -22,7 +22,7 @@ object Workflow { ...@@ -22,7 +22,7 @@ object Workflow {
} }
// TODO: make causals a set; // TODO: make causals a set;
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging { case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var], inv: Option[Formula] = None) extends Spec with LazyLogging {
override def toString: String = { override def toString: String = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target" s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
} }
......
...@@ -41,7 +41,7 @@ object InvariantGenerator { ...@@ -41,7 +41,7 @@ object InvariantGenerator {
val conclusion = genEq(spec.target) val conclusion = genEq(spec.target)
// TODO: tail here? // TODO: tail here?
Forall(spec.target.params.tail, conclusion).simplify And(Forall(spec.target.params.tail, conclusion), And.make(spec.inv.toList)).simplify
// Constants // Constants
// conclusion // conclusion
} }
......
...@@ -26,7 +26,7 @@ trait FormulaParser extends RegexParsers with PackratParsers with LazyLogging { ...@@ -26,7 +26,7 @@ trait FormulaParser extends RegexParsers with PackratParsers with LazyLogging {
def FINALLY: Parser[Finally] = ("F" | "♢") ~> TERM ^^ (t => Finally(t)) def FINALLY: Parser[Finally] = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
def TUPLE: Parser[List[Var]] = "(" ~> repsep(TYPEDVAR, ",") <~ ")" def TUPLE: Parser[List[Var]] = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN: Parser[Fun] = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) } def FUN: Parser[Fun] = VAR ~ (("#" ~> VAR)?) ~ TUPLE ^^ { case f ~ thread ~ tup => Fun(f.name, thread.map(_.name), tup) }
def EQ: Parser[Formula] = def EQ: Parser[Formula] =
(VAR <~ "=") ~ VAR ^^ { case v1 ~ v2 => Equal(v1, v2) } | (VAR <~ "=") ~ VAR ^^ { case v1 ~ v2 => Equal(v1, v2) } |
(VAR <~ "≠") ~ VAR ^^ { case v1 ~ v2 => Neg(Equal(v1, v2)) } (VAR <~ "≠") ~ VAR ^^ { case v1 ~ v2 => Neg(Equal(v1, v2)) }
......
...@@ -92,9 +92,18 @@ object WorkflowParser extends RegexParsers with PackratParsers with FormulaParse ...@@ -92,9 +92,18 @@ object WorkflowParser extends RegexParsers with PackratParsers with FormulaParse
private def SPEC: Parser[NISpec] = private def SPEC: Parser[NISpec] =
"Workflow" ~! WORKFLOW ~ "Workflow" ~! WORKFLOW ~
(("Declassify" ~> DECLASS)?) ~ (("Declassify" ~> DECLASS)?) ~
(("Invariant" ~> repsep(TERM, ","))?) ~
("Target" ~> FUN) ~ ("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ tar ~ causals => NISpec(w, toMap(decl.toList), True, tar, causals.getOrElse(List())) case _ ~ w ~ decl ~ inv ~ tar ~ causals => {
// temporary typing sig
val sig = w.sig.copy(w.sig.as,
w.sig.constas,
w.sig.bs,
w.sig.preds,
w.sig.constants ++ tar.params ++ causals.toList.flatten)
NISpec(w, toMap(decl.toList), True, tar, causals.getOrElse(List()), inv.map(list => And.make(list.map(inferFormulaTypes(sig, _)))))
}
} }
private def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = { private def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
......
...@@ -109,7 +109,7 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging { ...@@ -109,7 +109,7 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
} }
// single choice // single choice
it should "prove unrolled causal conference with single choice" in { ignore should "prove unrolled causal conference with single choice" in {
val name = "omitting/conference_unrolled_withB" val name = "omitting/conference_unrolled_withB"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties( assert(checkSafe(name, "", inv, InvProperties(
...@@ -161,34 +161,34 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging { ...@@ -161,34 +161,34 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
))) )))
} }
it should "prove causal omitting/conference_fixed for a given invariant" in { it should "prove causal omitting/conference_withB for a given invariant" in {
val name = "omitting/conference_withB" val name = "omitting/conference_invariant_synthesis"
// val inv = InvariantGenerator.invariantNoninterSingleBS _ // val inv = InvariantGenerator.invariantNoninterSingleBS _
import InvariantGenerator.genEq // import InvariantGenerator.genEq
//
val x = Var("ix","A") // val x = Var("ix","A")
val xt = Var("xt","A") // val xt = Var("xt","A")
val y = Var("iy", "A") // val y = Var("iy", "A")
val z = Var("iz","A") // val z = Var("iz","A")
val p = Var("ip","P") // val p = Var("ip","P")
val q = Var("iq","P") // val q = Var("iq","P")
val r = Var("ir","R") // val r = Var("ir","R")
val ceq = Forall(List(x, p), genEq("Conf", List(x,p))) // val ceq = Forall(List(x, p), genEq("Conf", List(x,p)))
val asseq = Forall(List(x, p), genEq("Assign", List(x,p))) // val asseq = Forall(List(x, p), genEq("Assign", List(x,p)))
//
val xyass = Forall(List(y,p), (Fun("Assign", List(xt,p)) land Fun("Assign", List(y, p))) --> // val xyass = Forall(List(y,p), (Fun("Assign", List(xt,p)) land Fun("Assign", List(y, p))) -->
( // (
Forall(List(q,r), genEq("Review", List(y,q,r))) land // Forall(List(q,r), genEq("Review", List(y,q,r))) land
Neg(Fun("informed", List(y))) land // Neg(Fun("informed", List(y))) land
Forall(List(q,r), genEq("Read", List(y,q,r))) land // Forall(List(q,r), genEq("Read", List(y,q,r))) land
Forall(List(q), Fun("Conf", List(xt, p)) --> Fun("Conf", List(y, q))) land // Forall(List(q), Fun("Conf", List(xt, p)) --> Fun("Conf", List(y, q))) land
Forall(List(z,q), (Fun ("Assign", List(y, q)) land Fun("Assign", List(z,q))) --> // Forall(List(z,q), (Fun ("Assign", List(y, q)) land Fun("Assign", List(z,q))) -->
Fun("Assign", List(z,p)) // Fun("Assign", List(z,p))
) // )
) // )
) // )
// val readimplass = Forall(List(y, q, r), Fun("Read", List(y,p,r)) --> Fun("Assign", List(y,p))) //// val readimplass = Forall(List(y, q, r), Fun("Read", List(y,p,r)) --> Fun("Assign", List(y,p)))
val revimplass = Forall(List(y, p, r), Fun("Review", List(y,p,r)) --> Fun("Assign", List(y,p))) // val revimplass = Forall(List(y, p, r), Fun("Review", List(y,p,r)) --> Fun("Assign", List(y,p)))
// val rt = Var("rt","R") // val rt = Var("rt","R")
...@@ -205,10 +205,13 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging { ...@@ -205,10 +205,13 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
// val parsed = invs.map(TransitionSystemParser.parseFormula(_)) // val parsed = invs.map(TransitionSystemParser.parseFormula(_))
// logger.info(parsed.mkString) // logger.info(parsed.mkString)
// val ip = And.make(parsed.map(_.get)) // val ip = And.make(parsed.map(_.get))
val invs = List(asseq, ceq, xyass.in("t1"), revimplass.in("t1"), revimplass.in("t2")) // val invs = List(asseq, ceq, xyass.in("t1"), revimplass.in("t1"), revimplass.in("t2"))
// val rt = Var("rt","R") // val rt = Var("rt","R")
val inv = (spec:NISpec) => And.make(InvariantGenerator.invariantNoninterSingleBS(spec), And.make(invs)) val inv = (spec:NISpec) => {
And.make(InvariantGenerator.invariantNoninterSingleBS(spec))
}
// val inv = InvariantGenerator.invariantNoninterSingleBS _ // val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties( assert(checkSafe(name, "", inv, InvProperties(
......
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