Commit 60a69f09 authored by Christian Müller's avatar Christian Müller

invariants.zip

parent 1cbf5abf
......@@ -9,10 +9,13 @@ EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq(
"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
"ch.qos.logback" % "logback-classic" % "1.1.7",
"org.scalactic" %% "scalactic" % "3.0.4",
"org.scalatest" %% "scalatest" % "3.0.4",
"org.scalactic" %% "scalactic" % "3.0.4" % "test",
"org.scalatest" %% "scalatest" % "3.0.4" % "test",
"org.scala-graph" %% "graph-core" % "1.12.1",
"org.scala-graph" %% "graph-dot" % "1.12.1",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
)
assemblyJarName in assembly := "invariants.jar"
test in assembly := {}
mainClass in assembly := Some("de.tum.workflows.InvariantCLI")
addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.6")
package de.tum.workflows
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.Spec
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
import java.io.File
object InvariantCLI extends App with LazyLogging {
lazy val usage = """
Usage invariants.jar [--causal] [--elimChoice] FILE
FILE should be a path to a Workflow Description File.
If --causal is given, all agents are assumed to be causal, otherwise 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 (args.length == 0) {
logger.info(usage)
} else {
var causal = false
var elim = false
args.collect {
case "--causal" => causal = true
case "--elimChoice" => elim = true
}
val properties = InvProperties(!causal, elim)
val file = args.last
logger.info(s"Using $file")
val source = Source.fromFile(file).mkString
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
None
} else {
if (!spec.get.checkSanity()) {
logger.error(s"Sanity check of $file failed. Skipping file.")
None
} else {
Some(spec.get)
}
}
spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
}
def generate(name: String, spec: Spec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterStubbornSingleBS(spec)
Utils.check(name, "", invariant, spec, properties)
}
}
\ No newline at end of file
......@@ -4,6 +4,8 @@ import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import java.io.File
import java.io.PrintWriter
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvProperties
object Utils {
......@@ -60,4 +62,40 @@ object Utils {
writer.print(prop)
writer.close()
}
def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
val model = if (properties.stubborn) "stubborn" else "causal"
val filenames = s"${name}_${model}_${desc}"
// do not blow up the formula with auxilliary elimination
val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${filenames}_${i}.dot", s)
}
val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
true
}
val wfsize = graph.edges.size - 1
val invsizes = labelling.last.map(_._2.opsize())
val maxsize = invsizes.max
val avgsize = invsizes.sum / invsizes.size
Utils.write(s"${filenames}.metrics",
s"""Name: $name
Description: $desc
Invariant: $inv
Model: $model
Result: ${if (!res) "not " else ""}inductive
WF size: $wfsize
Time: $time ms
Proof steps: ${dot.size}
Strengthenings: ${strengthenings.size}
Largest Inv: ${maxsize}
Average Inv: ${avgsize}""")
res
}
def check(name:String, desc:String, inv:Formula, properties:InvProperties):Boolean = {
val spec = ExampleWorkflows.parseExample(name).get
check(name, desc, inv, spec, properties)
}
}
\ No newline at end of file
......@@ -44,9 +44,9 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
val noneg = !(f hasSubFormula {
case Neg(f:Fun) if f.isOracle() => true
})
val allvars = f hasSubFormula {
case f:Fun if f.isOracle && f.params == frees => true
}
val allvars = !(f hasSubFormula {
case f:Fun if f.isOracle && f.params != frees => true
})
noneg && allvars
}
......@@ -62,7 +62,7 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
)
// if using oracle, only single stmt
val saneoracly = if (b.isoracly) { b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents) } else true
if (!saneoracly) { logger.error(s"Oracles used wrongly in $b") }
// if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
pred.isEmpty // && saneoracly TODO: enable this later?
}
case Loop(steps) => isSane(steps)
......
......@@ -185,8 +185,8 @@ object FOTransformers extends LazyLogging {
// Check fragment
if (!neg.isBS()) {
logger.error("Trying to instantiate Existentials for wrong fragment")
logger.error(s"Formula was $f")
logger.warn("Trying to instantiate Existentials for wrong fragment -- Termination not guaranteed")
// logger.error(s"Formula was $f")
}
val (agents, inner) = FOTransformers.eliminateExistentials(neg)
......
package de.tum.workflows.tests
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows._
import de.tum.workflows.toz3.InvProperties
object TestUtils {
def check(name:String, desc:String, inv:Formula, properties:InvProperties) = {
val model = if (properties.stubborn) "stubborn" else "causal"
val filenames = s"${name}_${model}_${desc}"
val spec = ExampleWorkflows.parseExample(name).get
// do not blow up the formula with auxilliary elimination
val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${filenames}_${i}.dot", s)
}
val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
true
}
val wfsize = graph.edges.size - 1
val invsizes = labelling.last.map(_._2.opsize())
val maxsize = invsizes.max
val avgsize = invsizes.sum / invsizes.size
Utils.write(s"${filenames}.metrics",
s"""Name: $name
Description: $desc
Invariant: $inv
Model: $model
Result: ${if (!res) "not " else ""}inductive
WF size: $wfsize
Time: $time ms
Proof steps: ${dot.size}
Strengthenings: ${strengthenings.size}
Largest Inv: ${maxsize}
Average Inv: ${avgsize}""")
res
}
def checkSafeStubborn(name: String, inv: Formula):Boolean = {
checkSafeStubborn(name, "", inv)
}
......
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