Commit 9efcecbe authored by Christian Müller's avatar Christian Müller

add invariants

parent 81b7e2b3
......@@ -16,26 +16,26 @@ import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
object Main extends App with LazyLogging {
val MAXAGENTS = 8
val FOLDER = "results"
val checkinvariants = true
def clear() {
def recclear(folder:File) {
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) {
def write(name: String, prop: String) {
val file = new File(name)
file.getParentFile.mkdirs()
val writer = new PrintWriter(file)
......@@ -43,48 +43,64 @@ object Main extends App with LazyLogging {
writer.close()
}
def writeExample(name: String, spec:Spec, prop: Formula) {
def timeNoninter(spec:Spec) = {
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv, true)
}
s"Noninterference Invariant (took $t ms):\n$msg\n"
}
def timeAllEqual(spec:Spec) = {
val inv = InvariantChecker.invariantAllEqual(spec)
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv, true)
}
s"All Equal Invariant (took $t ms):\n$msg\n"
}
def writeExample(name: String, spec: Spec, prop: Formula) {
var metrics = List[String]()
write(s"${name}.foltl", prop.pretty())
metrics :+= s"${name}.foltl: ${prop.opsize()}"
if (!FormulaFunctions.checkSanity(prop)) {
logger.error("Property didn't pass sanity check")
return
}
// Do FOLTL to LTL
if (spec.w.isomitting) {
logger.info("Omitting spec - no embedding in LTL possible")
} else {
logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
val (agents, res) = LTL.eliminateExistentials(prop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
return
}
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
metrics :+= s"Universe: $universe"
metrics :+= s"Universe: $universe"
write(s"${name}.ltl", ltlprop.toString())
write(s"${name}.ppltl", ltlprop.pretty())
}
write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
logger.info(s"Written all files for $name")
}
def generate(name: String, spec:Spec) {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
......@@ -97,40 +113,41 @@ object Main extends App with LazyLogging {
val cprop = Properties.noninterCausal(spec)
writeExample(s"$FOLDER/${name}_causal", spec, cprop)
}
if (checkinvariants) {
val inv = InvariantChecker.invariantNoninterStubborn(spec)
val (t,(safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv, true)
}
val noninter = s"Noninterference Invariant (took $t ms):\n$msg"
write(s"$FOLDER/${name}.inv", noninter)
def invariants = List(
timeNoninter _,
timeAllEqual _
)
def msgs = invariants.map(_(spec))
write(s"$FOLDER/${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, _))
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)
generateExample(k)
}
}
// clear()
// generateExample("omitting/conference")
// generateExample("tests/declasstest")
// clear()
// generateExample("omitting/conference")
// generateExample("tests/declasstest")
generateAllExamples()
}
\ No newline at end of file
......@@ -115,4 +115,10 @@ object InvariantChecker extends LazyLogging {
Forall(agent, premise 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
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