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

strategies in resulting files

parent c823d8b8
...@@ -30,3 +30,4 @@ Compile / unmanagedJars ++= { ...@@ -30,3 +30,4 @@ Compile / unmanagedJars ++= {
//assemblyJarName in assembly := "invariants.jar" //assemblyJarName in assembly := "invariants.jar"
//test in assembly := {} //test in assembly := {}
//mainClass in assembly := Some("de.tum.workflows.InvariantCLI") //mainClass in assembly := Some("de.tum.workflows.InvariantCLI")
# /bin/bash # /bin/bash
TIMEOUT=20m TIMEOUT=20m
shopt -s globstar
for RUN in 1 for RUN in 1
do do
for FILE in results/*.ltl for FILE in results/**/*.ltl
do do
NAME=$(basename ${FILE} .ltl) NAME=$(basename ${FILE} .ltl)
METRICS="results/${NAME}.metrics" METRICS="results/${NAME}.metrics"
......
# /bin/bash # /bin/bash
TIMEOUT=20s TIMEOUT=20s
shopt -s globstar
for FILE in results/*.ltl for FILE in results/**/*.ltl
do do
FOLDER=$(dirname ${FILE})
NAME=$(basename ${FILE} .ltl) NAME=$(basename ${FILE} .ltl)
METRICS="results/${NAME}.metrics" METRICS="${FOLDER}/${NAME}.metrics"
echo "Measuring ${FILE}" echo "Measuring ${FILE}"
echo "Metrics File: ${METRICS}" echo "Metrics File: ${METRICS}"
......
addSbtPlugin("com.github.xuwei-k" % "sbt-class-diagram" % "0.2.1")
Strategies:
strategy for B(a1,b1): ∀ n2:T. ((a1 = n2) ∨ ¬ leq(a1,n2) ∨ ¬ (a1 = b1)) ∧ ∀ n3:T. (¬ btw(b1,a1,n3) ∨ ¬ leq(a1,n3))
\ No newline at end of file
...@@ -39,7 +39,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -39,7 +39,7 @@ object InvariantInspector extends App with LazyLogging {
val (t, (res, dot)) = time { val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true) // InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val (result, graph, afterlabels, proven, dot, time) = val (result, graph, afterlabels, proven, strategies, dot, time) =
InvariantChecker.checkInvariantFPLabelling(invspec, props) InvariantChecker.checkInvariantFPLabelling(invspec, props)
// non-omitting conference linear inspection // non-omitting conference linear inspection
...@@ -77,7 +77,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -77,7 +77,7 @@ object InvariantInspector extends App with LazyLogging {
write(name, s"${name}.inv", msg) write(name, s"${name}.inv", msg)
for ((s, i) <- dot.zipWithIndex) { for ((s, i) <- dot.zipWithIndex) {
write(name, s"${name}_${i}.dot", s) write(name, s"${name}_$i.dot", s)
} }
} }
......
...@@ -41,6 +41,6 @@ object LTLCLI extends App with LazyLogging { ...@@ -41,6 +41,6 @@ object LTLCLI extends App with LazyLogging {
} }
} }
spec.map(MainLTL.generate(new File(file).getName.stripSuffix(".spec"), _, stubborn)) spec.map(MainLTLWorkflows.generate(new File(file).getName.stripSuffix(".spec"), _, stubborn))
} }
} }
\ No newline at end of file
package de.tum.niwo
import foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.Utils._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.blocks.{InvariantSpec, NISpec}
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.owltransformer.OwlTransformer
object MainLTLTransitionSystems extends App with LazyLogging {
def writeExample(name: String, spec: InvariantSpec, prop: Formula) {
val MAX_AGENTS = 8
var metrics = List[String]()
write(name, s"$name.foltl", prop.pretty)
metrics :+= s"$name.foltl: ${prop.opsize}"
if (!FormulaFunctions.checkSanity(prop)) {
logger.error("Property didn't pass sanity check")
return
}
logger.info("Embedding FOLTL formula in LTL")
val (agents, res) = FOTransformers.eliminateExistentials(prop)
val universe = agents.map(_.withType).mkString(", ")
logger.info(s"Using universe $universe")
if (agents.groupBy(_.typ).exists(_._2.size > MAX_AGENTS)) {
logger.error(s"Universe has more than $MAX_AGENTS agents for a single type. Aborting.")
return
}
val quantfree = FOTransformers.eliminateUniversals(res, agents)
val ltlprop = FOTransformers.eliminatePredicates(quantfree)
metrics :+= s"$name.ltl: ${ltlprop.opsize}"
metrics :+= s"Universe: $universe"
write(name, s"$name.ltl", ltlprop.toString())
write(name, s"$name.ppltl", ltlprop.pretty)
// val owlform = OwlTransformer.toOwl(ltlprop)
//
// // simplify owl
// val (t1,simped) = time {
// SimplifierFactory.apply(owlform.formula(), SimplifierFactory.Mode.SYNTACTIC_FIXPOINT)
// }
// write(name, s"$name.owlltl",simped.toString)
// logger.info(s"Simplified owl formula in $t1 ms")
// val (t2, sat) = time {
// // check owl sat
// logger.info("Checking satisfiability")
// // LanguageAnalysis.isSatisfiable(simped)
//
// OwlTransformer.isSatisfiable(simped)
// }
// logger.info(s"Found LTL formula to be satisfiable: $sat in $t2 ms")
//
// metrics :+= s"Satisfiable: $sat"
// metrics :+= s"Owl simplification $t1 ms"
// metrics :+= s"Owl runtime: $t2 ms"
write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
}
def generate(name: String, spec: InvariantSpec) {
logger.info(s"Encoding Spec:\n$spec")
// TODO: Check if correct fragment
logger.info (s"Computing invariant for target ${spec.inv} using only stubborn agents")
val prop = Properties.singletrace (spec)
writeExample (s"${name}_invspec", spec, prop)
}
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = Examples.parseExampleTS(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
}
spec.foreach(generate(name, _))
}
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- Examples.tsexamples.keys.toList.sorted) {
generateExample(k)
}
}
// clear()
// generateExample("nonomitting/conference")
// generateExample("tests/declasstest")
generateExample("tstests/easychair_singletrace")
// generateExample("tests/simpleChoiceNoOracle")
// generateAllExamples()
}
...@@ -9,11 +9,9 @@ import de.tum.niwo.blocks.NISpec ...@@ -9,11 +9,9 @@ import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.foltl.FOTransformers import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.owltransformer.OwlTransformer import de.tum.niwo.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory
object MainLTL extends App with LazyLogging { object MainLTLWorkflows extends App with LazyLogging {
def writeExample(name: String, spec: NISpec, prop: Formula) { def writeExample(name: String, spec: NISpec, prop: Formula) {
...@@ -45,38 +43,39 @@ object MainLTL extends App with LazyLogging { ...@@ -45,38 +43,39 @@ object MainLTL extends App with LazyLogging {
metrics :+= s"$name.ltl: ${ltlprop.opsize}" metrics :+= s"$name.ltl: ${ltlprop.opsize}"
metrics :+= s"Universe: $universe" metrics :+= s"Universe: $universe"
write(name, s"$name.ltl", ltlprop.toString()) // So aalta doesnt throw up
val ltlstring = ltlprop.toString.replace("#","_")
write(name, s"$name.ltl", ltlstring)
write(name, s"$name.ppltl", ltlprop.pretty) write(name, s"$name.ppltl", ltlprop.pretty)
val owlform = OwlTransformer.toOwl(ltlprop) val owlform = OwlTransformer.toOwl(ltlprop)
// simplify owl // simplify owl
val (t1,simped) = time { // val (t1,simped) = time {
SimplifierFactory.apply(owlform.formula(), SimplifierFactory.Mode.SYNTACTIC_FIXPOINT) // SimplifierFactory.apply(owlform.formula(), SimplifierFactory.Mode.SYNTACTIC_FIXPOINT)
} // }
write(name, s"$name.owlltl",simped.toString) // write(name, s"$name.owlltl",simped.toString)
logger.info(s"Simplified owl formula in $t1 ms") // logger.info(s"Simplified owl formula in $t1 ms")
val (t2, sat) = time { // val (t2, sat) = time {
// check owl sat // // check owl sat
logger.info("Checking satisfiability") // logger.info("Checking satisfiability")
// LanguageAnalysis.isSatisfiable(simped) //// LanguageAnalysis.isSatisfiable(simped)
//
OwlTransformer.isSatisfiable(simped) // OwlTransformer.isSatisfiable(simped)
} // }
logger.info(s"Found LTL formula to be satisfiable: $sat in $t2 ms") // logger.info(s"Found LTL formula to be satisfiable: $sat in $t2 ms")
//
metrics :+= s"Satisfiable: $sat" // metrics :+= s"Satisfiable: $sat"
metrics :+= s"Owl simplification $t1 ms" // metrics :+= s"Owl simplification $t1 ms"
metrics :+= s"Owl runtime: $t2 ms" // metrics :+= s"Owl runtime: $t2 ms"
write(name, s"$name.metrics", metrics.mkString("", "\n", "\n")) write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
} }
def generate(name: String, spec: NISpec, onlystubborn:Boolean) { def generate(name: String, spec: NISpec, onlystubborn:Boolean) {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
// Do FOLTL to LTL // Do FOLTL to LTL
if (spec.w.isomitting) { if (spec.w.isomitting) {
logger.info("Omitting spec - no embedding in LTL possible") logger.info("Omitting spec - no embedding in LTL possible")
......
package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import java.io.File
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.parser.{TransitionSystemParser, WorkflowParser}
object TSCLI extends App with LazyLogging {
lazy val usage = """
Usage niwo-ts.jar FILE
FILE should be a path to a FO Safety Game Description File.
"""
if (args.length != 1) {
logger.info(usage)
} else {
val file = args.last
logger.info(s"Using $file")
val source = Utils.using(Source.fromFile(file)) { source => source.mkString }
val spec = TransitionSystemParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
} else {
if (!spec.get.isSane) {
logger.error(s"Sanity check of $file failed. Skipping file.")
} else {
val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)
Utils.check(new File(file).getName.stripSuffix(".spec"), "", spec.get, properties)
}
}
}
}
...@@ -9,6 +9,8 @@ import de.tum.niwo.toz3.Z3BSFO ...@@ -9,6 +9,8 @@ import de.tum.niwo.toz3.Z3BSFO
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding} import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.invariants.{InvProperties, InvariantChecker} import de.tum.niwo.invariants.{InvProperties, InvariantChecker}
import org.checkerframework.checker.units.qual.s
import scalax.collection.edge.Implicits.+
object Utils extends LazyLogging { object Utils extends LazyLogging {
...@@ -116,7 +118,7 @@ object Utils extends LazyLogging { ...@@ -116,7 +118,7 @@ object Utils extends LazyLogging {
InvSpecInstantiator.instantiate(spec, u) InvSpecInstantiator.instantiate(spec, u)
).getOrElse(spec) ).getOrElse(spec)
val (res, graph, labelling, provens, dot, time) = val (res, graph, labelling, provens, strategies, dot, time) =
InvariantChecker.checkInvariantFPLabelling(fixspec, properties) InvariantChecker.checkInvariantFPLabelling(fixspec, properties)
logger.info(s"Invariant was ${spec.inv}") logger.info(s"Invariant was ${spec.inv}")
...@@ -135,33 +137,44 @@ object Utils extends LazyLogging { ...@@ -135,33 +137,44 @@ object Utils extends LazyLogging {
true true
} }
// .invariants
val labels = (for ((node, inv) <- labelling.last) yield { val labels = (for ((node, inv) <- labelling.last) yield {
s"Node ${node}:\n${inv.pretty}\n" s"Node ${node}:\n${inv.pretty}\n"
}).mkString("\n") }).mkString("\n")
Utils.write(name, s"$filenames.invariants", labels) Utils.write(name, s"$filenames.invariants", labels)
// .strategies
val strats = strategies.last.values.foldLeft("")(_ + _)
val stratfile = s"Strategies:\n${Utils.indentLines(strats)}"
Utils.write(name, s"$filenames.strategies", stratfile)
// .metrics
val wfsize = graph.edges.size - 1 val wfsize = graph.edges.size - 1
val invsizes = labelling.last.map(_._2.opsize) val invsizes = labelling.last.map(_._2.opsize)
val maxsize = invsizes.max val maxsize = invsizes.max
val avgsize = invsizes.sum / invsizes.size val avgsize = invsizes.sum / invsizes.size
Utils.write(name, s"$filenames.metrics", Utils.write(name, s"$filenames.metrics",
s"""Name: $name s"""Name: $name
|Description: $desc |Description: $desc
| Invariant: | Invariant:
|${spec.inv.pretty.linesIterator.map(s => " " + s).mkString("\n")} |${spec.inv.pretty.linesIterator.map(s => " " + s).mkString("\n")}
| Model: $model | Model: $model
| Result: ${if (!res) "not " else ""}inductive | Result: ${if (!res) "not " else ""}inductive
| WF size: $wfsize | WF size: $wfsize
| Time: $time ms | Time: $time ms
| Proof steps: ${dot.size} | Proof steps: ${dot.size}
| Strengthenings: ${strengthenings.size} | Strengthenings: ${strengthenings.size}
| Largest Inv: $maxsize | Largest Inv: $maxsize
| Average Inv: $avgsize | Average Inv: $avgsize
| Properties: $properties | Properties: $properties
| """.stripMargin | """.stripMargin
) )
res res
} }
// Will be obsolete in Scala 2.13
def using[A, B <: {def close(): Unit}] (closeable: B) (f: B => A): A =
try { f(closeable) } finally { closeable.close() }
} }
\ No newline at end of file
package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import java.io.File
import de.tum.niwo.LTLCLI.args
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.WorkflowParser
object TSCLI extends App with LazyLogging {
lazy val usage = """
Usage niwo-ts.jar FILE
FILE should be a path to a Workflow Description File.
It will be transformed into a First Order Safety Game and then solved.
If --stubborn is given, all agents are assumed to be stubborn, regardless of the specification in the file.
"""
if (args.length == 0) {
logger.info(usage)
} else {
var stubborn = false
args.collect {
case "--stubborn" => stubborn = true
}
val file = args.last
logger.info(s"Using $file")
val source = Utils.using(Source.fromFile(file)) { source => source.mkString }
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
} else {
if (!spec.get.isSane) {
logger.error(s"Sanity check of $file failed. Skipping file.")
} else {
val inv = InvariantGenerator.invariantNoninterSingleBS _
val properties = InvProperties(stubborn = stubborn, approxElim = true, eliminateA = true, eliminateB = true)
Utils.check(new File(file).getName.stripSuffix(".spec"), "", inv, spec.get, properties)
}
}
}
}
...@@ -93,7 +93,7 @@ object FOTransformers extends LazyLogging { ...@@ -93,7 +93,7 @@ object FOTransformers extends LazyLogging {
repld.simplify repld.simplify
} }
def eliminateBPredicate(f:Formula, B:Fun): (Formula, Formula) = { def eliminateBPredicate(f:Formula, B:Fun): (Formula, String) = {
val NAME = B.name val NAME = B.name
// SOQE: \exists B. f <-> f' // SOQE: \exists B. f <-> f'
...@@ -187,7 +187,7 @@ object FOTransformers extends LazyLogging { ...@@ -187,7 +187,7 @@ object FOTransformers extends LazyLogging {
logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq") logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq")
} }
(felimq, z3fsolq) (felimq, s"strategy for ${B.updatedParams(freeparams)}: $z3fsolq\n")
} }
/** /**
......
package de.tum.niwo.foltl package de.tum.niwo.foltl
import de.tum.niwo.Implicits._ import de.tum.niwo.Implicits._
import de.tum.niwo.graphs.WFGraphEncoding._
import de.tum.niwo.foltl.LTLEncoding._ import de.tum.niwo.foltl.LTLEncoding._
import de.tum.niwo.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
...@@ -122,9 +122,28 @@ object Properties { ...@@ -122,9 +122,28 @@ object Properties {
val T1 = "t1" val T1 = "t1"
val T2 = "t2" val T2 = "t2"
val INFNAME = "informed" val INFNAME = "informed"
def singletrace(spec:InvariantSpec): Formula = {
import de.tum.niwo.graphs.TSGraphEncoding._
val graph = toGraph(spec.ts)
val cfg = sanecfg(graph)
// TODO: this still believes the graph is a WFGraph
val sem = exec(spec.ts.sig, graph)
val empties = spec.ts.sig.preds.map( pred => Forall(pred.params, Neg(pred)) )
val emptyaxiom = And.make(empties.toList)
val inv = Finally(Neg(spec.inv))
And.make(cfg, sem, emptyaxiom, spec.axioms, inv)
}
// include optimizations for choices // include optimizations for choices
def noninterStubborn(spec: NISpec) = { def noninterStubborn(spec: NISpec): Formula = {
import de.tum.niwo.graphs.WFGraphEncoding._
val graph = toGraph(spec.w) val graph = toGraph(spec.w)
val cfg = sanecfg(graph) val cfg = sanecfg(graph)
...@@ -145,7 +164,8 @@ object Properties { ...@@ -145,7 +164,8 @@ object Properties {
And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter) And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
} }
def noninterCausal(spec:NISpec) = { def noninterCausal(spec:NISpec): Formula = {
import de.tum.niwo.graphs.WFGraphEncoding._
val graph = toGraph(spec.w) val graph = toGraph(spec.w)
val cfg = sanecfg(graph) val cfg = sanecfg(graph)
......
...@@ -9,6 +9,7 @@ import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph ...@@ -9,6 +9,7 @@ import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding} import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding} import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding}
import de.tum.niwo.Utils import de.tum.niwo.Utils
import de.tum.niwo.graphs.TSGraphEncoding.TSGraph
import scala.annotation.tailrec import scala.annotation.tailrec
...@@ -40,15 +41,15 @@ object InvariantChecker extends LazyLogging { ...@@ -40,15 +41,15 @@ object InvariantChecker extends LazyLogging {
post: Formula, post: Formula,
properties:InvProperties, properties:InvProperties,
untouched:Set[String], untouched:Set[String],
diverged:Boolean): ((Status, Solver), Formula) = {