Skip to content

GitLab

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

add results

parent cb231255
Hide whitespace changes
Inline Side-by-side
examples/tests/simpleNoChoice2.spec
View file @ e31ba0ec
......@@ -3,7 +3,7 @@ Workflow
forall x,s
P(s) -> Q += (x,s)
forall x,s
Q(s) -> R += (x,s)
Q(x,s) -> R += (x,s)
Target
......
src/main/scala/de/tum/workflows/Encoding.scala
View file @ e31ba0ec
......@@ -195,25 +195,34 @@ object Encoding extends LazyLogging {
// And.make(List(cfg, sanity, sem, init))
// }
def toDot(g: WorkflowGraph, labels:Map[WorkflowGraph#NodeT, String]) = {
def toDot(g: WorkflowGraph)(labels:Map[WorkflowGraph#NodeT, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph(
directed = true,
id = Some("Invariant Labelling"))
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleBlock =>
case label: SimpleBlock => {
val green = edges.contains(innerEdge.edge)
val color = List(DotAttr("color", if (green) "green" else "red"))
val labelled = if (label.nonEmpty) {
DotAttr("label", label.toString) :: color
} else { color }
Some((
root,
DotEdgeStmt(
source.toString,
target.toString,
if (label.nonEmpty) List(DotAttr("label", label.toString))
else Nil)))
labelled
)
))
}
}
}
def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] =
Some(root, DotNodeStmt(innerNode.toString, List(DotAttr("label", labels(innerNode)))))
Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + labels(innerNode))))))
g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
}
......
src/main/scala/de/tum/workflows/MainInvariants.scala
View file @ e31ba0ec
......@@ -14,16 +14,15 @@ import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
object MainInvariants extends App with LazyLogging {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
def invariant =
InvariantChecker.invariantNoninterStubbornBS _
InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
......@@ -31,8 +30,7 @@ object MainInvariants extends App with LazyLogging {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
InvariantChecker.checkInvariantFP(spec.w, invariant(spec), true)
}
val worked = res.isDefined
val msg = s"Invariant was ${if (worked) "" else "not "}proven (took $t ms)\n"
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
write(s"${name}.inv", msg)
write(s"${name}.dot", dot)
......
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @ e31ba0ec
......@@ -37,18 +37,21 @@ object FOLTL {
def ∨ (f2:Formula) = Or(this, f2)
def pretty(): String = {
val s = this.toString
val remeq = this.everywhere {
case Eq(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
Eq(t1, Fun("eq", List()))
}
val s = remeq.toString
val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
// indent
var opens = 0;
val indented = for (line <- broken.lines) yield {
val indent = " " * (opens * 2)
val ret = indent + line
opens += line.count(_ == '(')
opens -= line.count(_ == ')')
ret
}
indented.reduce(_ + "\n" + _)
......
src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala
View file @ e31ba0ec
......@@ -186,6 +186,12 @@ object FormulaFunctions extends LazyLogging {
case Fun(f, None, xs) => Fun(f, Some(name), xs)
})
}
def annotateOverwrite(t: Formula, Name1:String, name: String) = {
t.everywhere({
case Fun(f, Some(Name1), xs) => Fun(f, Some(name), xs)
})
}
def annotate(t: Formula, name: String, ignore: Set[String]) = {
t.everywhere({
......
src/main/scala/de/tum/workflows/foltl/Properties.scala
View file @ e31ba0ec
......@@ -145,9 +145,6 @@ object Properties {
def noninterCausal(spec:Spec) = {
val t1 = "t1"
val t2 = "t2"
val graph = toGraph(spec.w)
val cfg = sanecfg(graph)
val sem = exec(spec.w.sig, graph)
......@@ -172,6 +169,6 @@ object Properties {
val agentmodel = Exists(spec.causals, And.make(stubs, causals, noninter))
// maybe add exists t1, t2. phi?
And.make(cfg, sem.in(t1, nodes), sem.in(t2, nodes), agentmodel)
And.make(cfg, sem.in(T1, nodes), sem.in(T2, nodes), agentmodel)
}
}
src/main/scala/de/tum/workflows/ltl/LTL.scala
View file @ e31ba0ec
......@@ -58,15 +58,15 @@ object LTL extends LazyLogging {
def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
if (agents.isEmpty) {
logger.warn("Agent list empty")
}
// if (agents.isEmpty) {
// logger.warn("Agent list empty")
// }
val universe = agents.groupBy(_.typ)
def instantiate(tup:List[Var],t:Formula,universe:Map[String,List[FOLTL.Var]]) = {
if(!tup.forall(v => universe.contains(v.typ))) {
// everything is valid for quantifiers over empty sets
logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
// logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
True
} else {
val replacements = comb(tup.map(_.typ), universe)
......
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
View file @ e31ba0ec
package de.tum.workflows.toz3
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
import java.util.HashMap
import scalax.collection.edge.LDiEdge // labeled directed edge
import scala.annotation.tailrec
// labeled directed edge
import com.microsoft.z3.Context
import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.Properties
import de.tum.workflows.Encoding
import de.tum.workflows.Implicits._
import de.tum.workflows.Preconditions
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions
import scalax.collection.Graph
import de.tum.workflows.Encoding.WorkflowGraph
import scala.annotation.tailrec
import de.tum.workflows.ltl.LTL
object InvariantChecker extends LazyLogging {
......@@ -98,13 +93,13 @@ object InvariantChecker extends LazyLogging {
type Edge = graph.EdgeT
@tailrec
def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): Option[Map[Node, Formula]] = {
def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): (Boolean, Map[Node, Formula], Set[Edge]) = {
// check if done, i.e. all edges proven
val toProve = (graph.edges -- proven)
if (toProve.isEmpty) {
logger.info("Everything proven. Terminating.")
Some(labels)
(true, labels, proven)
} else {
// take one edge to prove
......@@ -113,7 +108,8 @@ object InvariantChecker extends LazyLogging {
// try to prove
val pre = labels(next._1)
val post = labels(next._2)
val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, next._1.hasPredecessors)
val isfirst = !next._1.hasPredecessors
val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, isfirst)
if (status == Status.UNSATISFIABLE) {
// Negation of implication unsat
......@@ -124,18 +120,27 @@ object InvariantChecker extends LazyLogging {
// Negation of implication sat
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable
val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next))
val (status2, solver2) = checkOnZ3(newinv)
val newlabels = labels.updated(next._1, newinv)
val newproven = proven.filterNot(_._1 == next._1)
if (status2 == Status.UNSATISFIABLE) {
// Negation of newinv still unsat, newinv still sat
checkInvariantRec(newlabels, newproven)
// never relabel initial node
if (!isfirst) {
val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next))
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
val newlabels = labels.updated(next._1, newinv)
val invalidated = proven.filter(_._2 == next._1)
val newproven = (proven -- invalidated) + next
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false
logger.info(s"Relabeling ${next._1}. Continuing.")
checkInvariantRec(newlabels, newproven)
} else {
logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
(false, newlabels, newproven)
}
} else {
logger.info("New invariant not satisfiable. Terminating.")
None
logger.info("Would have to relabel initial node. Terminating.")
(false, labels, proven)
}
}
}
......@@ -143,13 +148,12 @@ object InvariantChecker extends LazyLogging {
// create labelling
val labels = (for (n <- graph.nodes) yield { n -> inv }) toMap
val result = checkInvariantRec(labels, Set())
val dot = Encoding.toDot(graph, labels.map(t => (t._1, t._2.pretty())))
val (result, afterlabels, proven) = checkInvariantRec(labels, Set())
val dot = Encoding.toDot(graph)(afterlabels.map(t => (t._1, t._2.pretty())), proven)
(result, dot)
}
def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
// Build graph
......@@ -193,49 +197,4 @@ object InvariantChecker extends LazyLogging {
}
(safe, msg)
}
def genEq(f: Fun, p: List[Var]) = {
val newf = f.parallelRename(f.params, p)
Eq(newf.in(T1), newf.in(T2))
}
def invariantNoninterStubborn(spec: Spec) = {
val agent = spec.target.params(0)
val premise = And.make(for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
})
val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
val quant = r.params.drop(1)
Forall(quant, genEq(r, agent :: quant))
})
Forall(agent, premise → conclusion).simplify()
}
def invariantNoninterStubbornBS(spec: Spec) = {
val agent = spec.target.params(0)
val premise = for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
}
val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
val quant = r.params.drop(1)
Forall(quant, genEq(r, agent :: quant))
})
Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
}
def invariantAllEqual(spec: Spec) = {
And.make(for (r <- spec.w.sig.preds.toList) yield {
Forall(r.params, genEq(r, r.params))
})
}
}
\ No newline at end of file
src/main/scala/de/tum/workflows/toz3/InvariantGenerator.scala 0 → 100644
View file @ e31ba0ec
package de.tum.workflows.toz3
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
object InvariantGenerator {
def genEq(f: Fun, p: List[Var]) = {
val newf = f.parallelRename(f.params, p)
Eq(newf.in(T1), newf.in(T2))
}
def invariantNoninterStubborn(spec: Spec) = {
val agent = spec.target.params(0)
val premise = And.make(for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
})
val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
val quant = r.params.drop(1)
Forall(quant, genEq(r, agent :: quant))
})
Forall(agent, premise → conclusion).simplify()
}
def invariantNoninterStubbornBS(spec: Spec) = {
val agent = spec.target.params(0)
val premise = for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
}
val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
val quant = r.params.drop(1)
Forall(quant, genEq(r, agent :: quant))
})
Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
}
def invariantAllEqual(spec: Spec) = {
And.make(for (r <- spec.w.sig.preds.toList) yield {
Forall(r.params, genEq(r, r.params))
})
}
}
\ No newline at end of file
src/test/scala/Test.scala
View file @ e31ba0ec
......@@ -8,34 +8,50 @@ import org.omg.CORBA.TIMEOUT
import de.tum.workflows.Implicits._
import com.microsoft.z3.Model
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.Utils
object Test extends App {
val TIMEOUT = 30000 // in milliseconds
val name = "tests/loopexample"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
val spec = ExampleWorkflows.parseExample(name).get
val (safe, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
assert(safe) // should be safe
Utils.write(s"${name}.dot", dot)
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
// val TIMEOUT = 30000 // in milliseconds
//
// val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
//
// val cfg = new HashMap[String, String]()
// cfg.put("timeout", TIMEOUT.toString())
//
// val ctx = new Context(cfg)
//
// val qe = ctx.mkTactic("qe")
// val default = ctx.mkTactic("smt")
// val t = ctx.andThen(qe, default)
//
// val s = ctx.mkSolver(t)
//
// s.add(Z3.translate(easyForm, ctx))
// val c = s.check()
// val model = s.getModel()
//
// println(s"Z3 model:\n${model}")
//
// val consts = model.getConstDecls()
// println(consts(0).getName)
//
// println("MODEL:")
// Z3.printModel(model)
val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
val qe = ctx.mkTactic("qe")
val default = ctx.mkTactic("smt")
val t = ctx.andThen(qe, default)
val s = ctx.mkSolver(t)
s.add(Z3.translate(easyForm, ctx))
val c = s.check()
val model = s.getModel()
println(s"Z3 model:\n${model}")
val consts = model.getConstDecls()
println(consts(0).getName)
println("MODEL:")
Z3.printModel(model)
}
\ No newline at end of file
src/test/scala/de/tum/workflows/ltl/tests/FOLTLTest.scala
View file @ e31ba0ec
......@@ -9,9 +9,7 @@ import de.tum.workflows.Implicits._
class FOLTLTest extends FlatSpec {
"Formulas" should "be constructed correctly" in {
True → Var("x") should be (Implies(True, Var("x")))
}
"Formula functions" should "generate inequalities" in {
......
src/test/scala/de/tum/workflows/ltl/tests/InvariantFilesTest.scala
View file @ e31ba0ec
......@@ -11,25 +11,53 @@ import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
class InvariantFilesTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val name = "tests/simpleNoChoice2"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
assert(checkSafe(name, inv))
}
val spec = ExampleWorkflows.parseExample("tests/simpleNoChoice2").get
val inv = Forall(List("x","s"), genEq("R", List("x","s")))
val (safe, msg) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
it should "prove simple loops safe" in {
val name = "tests/loopexampleNoOracle"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
assert(checkSafe(name, inv))
}
it should "prove simple loops safe and iterate" in {
val name = "tests/loopexampleNoOracle"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
assert(checkSafe(name, inv))
}
println(msg.toString())
safe should be(true)
it should "fail on oracly things" in {
val name = "tests/simpleChoice"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
assert(!checkSafe(name, inv))
}
it should "fail on loopy oracly things" in {
val name = "tests/loopexample"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
assert(!checkSafe(name, inv))
}
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
Utils.write(s"${name}.dot", dot)
res
}
def genEq(name:String, params: List[Var]) = {
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
src/test/scala/de/tum/workflows/ltl/tests/InvariantTest.scala
View file @ e31ba0ec
......@@ -11,29 +11,30 @@ import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
class InvariantTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val spec = ExampleWorkflows.parseExample("nonomitting/conference").get
// val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val inv = InvariantChecker.invariantNoninterStubbornBS(spec)
val added = Or(Neg(Fun("Assign", List(Var("x","A"), Var("p","P")))),
Neg(Fun("Conf", List(Var("x","A"), Var("p","P")))))
val both = Forall(List(Var("x","A"), Var("p","P")), And(added.in("t1"), added.in("t2")))
val newinv = And(inv, both)
val (safe, msg) = InvariantChecker.checkInvariantOnce(spec.w, newinv, true)
println(msg.toString())
safe should be(true)
}
// "InvariantChecker" should "prove simple things safe" in {
//
// val spec = ExampleWorkflows.parseExample("nonomitting/conference").get
//
//// val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
//
// val inv = InvariantGenerator.invariantNoninterStubbornBS(spec)
//
// val added = Or(Neg(Fun("Assign", List(Var("x","A"), Var("p","P")))),
// Neg(Fun("Conf", List(Var("x","A"), Var("p","P")))))
//
// val both = Forall(List(Var("x","A"), Var("p","P")), And(added.in("t1"), added.in("t2")))
//
// val newinv = And(inv, both)
//
// val (safe, msg) = InvariantChecker.checkInvariantOnce(spec.w, newinv, true)