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

testing

parent 5c198d52
package de.tum.workflows
import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
object Main extends App with LazyLogging {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
def invariants = List(
InvariantChecker.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
)
def msgs = for (inv <- invariants) yield {
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv(spec), true)
}
s"Proving Invariant (took $t ms):\n$msg\n"
}
write(s"${name}.inv", msgs.mkString("\n"))
}
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
if (!spec.isDefined) {
logger.error(s"Not a valid spec: $name")
}
spec.map(generate(name, _))
}
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
generateExample(k)
}
}
clear()
generateExample("nonomitting/conference")
// generateExample("tests/declasstest")
// generateAllExamples()
}
\ No newline at end of file
...@@ -15,33 +15,9 @@ import de.tum.workflows.blocks.Spec ...@@ -15,33 +15,9 @@ import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker import de.tum.workflows.toz3.InvariantChecker
object Main extends App with LazyLogging { object MainLTL extends App with LazyLogging {
val MAXAGENTS = 8 val MAXAGENTS = 8
val FOLDER = "results"
val checkinvariants = true
def clear() {
def recclear(folder: File) {
for (fol <- folder.listFiles() if fol.isDirectory()) {
recclear(fol)
}
folder.listFiles().foreach(_.delete())
}
val fol = new File(FOLDER)
fol.mkdirs()
recclear(fol)
}
def write(name: String, prop: String) {
val file = new File(name)
file.getParentFile.mkdirs()
val writer = new PrintWriter(file)
writer.print(prop)
writer.close()
}
def writeExample(name: String, spec: Spec, prop: Formula) { def writeExample(name: String, spec: Spec, prop: Formula) {
...@@ -95,25 +71,7 @@ object Main extends App with LazyLogging { ...@@ -95,25 +71,7 @@ object Main extends App with LazyLogging {
if (!spec.causals.isEmpty) { if (!spec.causals.isEmpty) {
logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}") logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
val cprop = Properties.noninterCausal(spec) val cprop = Properties.noninterCausal(spec)
writeExample(s"$FOLDER/${name}_causal", spec, cprop) writeExample(s"${name}_causal", spec, cprop)
}
if (checkinvariants) {
def invariants = List(
InvariantChecker.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
)
def msgs = for (inv <- invariants) yield {
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv(spec), true)
}
s"Proving Invariant (took $t ms):\n$msg\n"
}
write(s"$FOLDER/${name}.inv", msgs.mkString("\n"))
} }
} }
......
...@@ -2,9 +2,13 @@ package de.tum.workflows ...@@ -2,9 +2,13 @@ package de.tum.workflows
import de.tum.workflows.blocks._ import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.foltl.FOLTL._
import java.io.File
import java.io.PrintWriter
object Utils { object Utils {
val RESULTSFOLDER = "results"
def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = { def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = {
if (string.isEmpty) "" else string.mkString(start, mid, end) if (string.isEmpty) "" else string.mkString(start, mid, end)
} }
...@@ -25,11 +29,32 @@ object Utils { ...@@ -25,11 +29,32 @@ object Utils {
def indentLines(s: String) = { def indentLines(s: String) = {
s.lines.map(" " + _).mkString("\n") s.lines.map(" " + _).mkString("\n")
} }
def time[R](block: => R) = { def time[R](block: => R) = {
val t0 = System.nanoTime() val t0 = System.nanoTime()
val result = block // call-by-name val result = block // call-by-name
val t1 = System.nanoTime() val t1 = System.nanoTime()
((t1 - t0)/1000000, result) ((t1 - t0) / 1000000, result)
}
def clear() {
def recclear(folder: File) {
for (fol <- folder.listFiles() if fol.isDirectory()) {
recclear(fol)
}
folder.listFiles().foreach(_.delete())
}
val fol = new File(RESULTSFOLDER)
fol.mkdirs()
recclear(fol)
}
def write(name: String, prop: String) {
val file = new File(s"$RESULTSFOLDER/$name")
file.getParentFile.mkdirs()
val writer = new PrintWriter(file)
writer.print(prop)
writer.close()
} }
} }
\ No newline at end of file
...@@ -84,9 +84,19 @@ object FormulaFunctions extends LazyLogging { ...@@ -84,9 +84,19 @@ object FormulaFunctions extends LazyLogging {
if (t == t1) t1 else simplify(t1) if (t == t1) t1 else simplify(t1)
} }
def eliminateImplication(f: Formula) = { def eliminateImplication(f: Formula):Formula = {
f everywhere { f everywhere {
case Implies(f1, f2) => Or(Neg(f1), f2) case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
}
}
def eliminateEq(f:Formula):Formula = {
f everywhere {
case Eq(f1, f2) => {
val e1 = eliminateEq(f1)
val e2 = eliminateEq(f2)
And(Implies(e1, e2), Implies(e2, e1))
}
} }
} }
...@@ -278,7 +288,9 @@ object FormulaFunctions extends LazyLogging { ...@@ -278,7 +288,9 @@ object FormulaFunctions extends LazyLogging {
// logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}") // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
FormulaFunctions.fixBinding(f, Set())._1 FormulaFunctions.fixBinding(f, Set())._1
} else f } else f
eliminateImplication(bound).simplify()
val noeq = eliminateEq(bound)
eliminateImplication(noeq).simplify()
} }
def generateName(base: Var, bound: Set[Var]) = { def generateName(base: Var, bound: Set[Var]) = {
......
...@@ -109,7 +109,7 @@ object LTL extends LazyLogging { ...@@ -109,7 +109,7 @@ object LTL extends LazyLogging {
/** /**
* Instantiates universals in EA formulae. * Instantiates universals in EA formulae.
* Does not change quantifier structure, but returns formula in NegNF * Resulting formula is in E* with all existentials outermost and in NegNF
*/ */
def instantiateUniversals(f:Formula) = { def instantiateUniversals(f:Formula) = {
// Check fragment // Check fragment
......
...@@ -17,6 +17,7 @@ import org.omg.CORBA.TIMEOUT ...@@ -17,6 +17,7 @@ import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.Properties import de.tum.workflows.foltl.Properties
import de.tum.workflows.foltl.FormulaFunctions
object InvariantChecker extends LazyLogging { object InvariantChecker extends LazyLogging {
...@@ -28,13 +29,15 @@ object InvariantChecker extends LazyLogging { ...@@ -28,13 +29,15 @@ object InvariantChecker extends LazyLogging {
cfg.put("timeout", TIMEOUT.toString()) cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg) val ctx = new Context(cfg)
val qe = ctx.mkTactic("qe") // val qe = ctx.mkTactic("qe")
val default = ctx.mkTactic("smt") // val default = ctx.mkTactic("smt")
val t = ctx.andThen(qe, default) // val t = ctx.andThen(qe, default)
// val s = ctx.mkSolver(t)
val s = ctx.mkSolver(t) val s = ctx.mkSolver()
s.add(Z3.translate(f, ctx)) // Checking QFree
s.add(Z3QFree.translate(f, ctx))
// Send to z3 // Send to z3
val c = s.check() val c = s.check()
...@@ -79,11 +82,18 @@ object InvariantChecker extends LazyLogging { ...@@ -79,11 +82,18 @@ object InvariantChecker extends LazyLogging {
} }
val univfree = LTL.instantiateUniversals(tocheck) val univfree = LTL.instantiateUniversals(tocheck)
// univfree is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(univfree)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = LTL.eliminatePredicates(stripped)
// val test3 = univfree.pretty() // val test3 = stripped.pretty()
// println(test3) // println(test3)
checkOnZ3(univfree.simplify()) checkOnZ3(satform.simplify())
} }
def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = { def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {
......
...@@ -258,15 +258,15 @@ object Z3 extends LazyLogging { ...@@ -258,15 +258,15 @@ object Z3 extends LazyLogging {
val sb = new StringBuilder() val sb = new StringBuilder()
val consts = model.getConstDecls() // val consts = model.getConstDecls()
//
val vals = consts.map(_.apply()) // val vals = consts.map(_.apply())
val typedvals = vals.groupBy(_.getSort) // val typedvals = vals.groupBy(_.getSort)
//
sb ++= "Universe:\n" // sb ++= "Universe:\n"
for ((k, v) <- typedvals) { // for ((k, v) <- typedvals) {
sb ++= s"Type $k: ${v.mkString(",")}\n" // sb ++= s"Type $k: ${v.mkString(",")}\n"
} // }
sb ++= "Evaluations:\n" sb ++= "Evaluations:\n"
val sortedConsts = model.getConstDecls().sortBy(_.getName.toString()) val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
......
...@@ -69,6 +69,7 @@ object Z3QFree extends LazyLogging { ...@@ -69,6 +69,7 @@ object Z3QFree extends LazyLogging {
} }
case Var(x,t) => { case Var(x,t) => {
// FIXME: Here we're just assuming all Variables are Boolean
ctx.mkBoolConst(x) ctx.mkBoolConst(x)
} }
} }
......
...@@ -11,36 +11,31 @@ import com.microsoft.z3.Model ...@@ -11,36 +11,31 @@ import com.microsoft.z3.Model
object Test extends App { object Test extends App {
println(List(true, false, false).reduceLeft(_ && _)) val TIMEOUT = 30000 // in milliseconds
println(List(true).reduceLeft(_ && _))
println(List(false).reduceLeft(_ && _)) val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
println(List().foldLeft(true)((_:Boolean) && (_:Boolean)))
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)
// val TIMEOUT = 30000 // in milliseconds 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(toZ3.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:")
// toZ3.printModel(model)
} }
\ 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