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

build inspector

parent e47aefd4
package de.tum.workflows
import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
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
import de.tum.workflows.toz3.InvProperties
object InvariantInspector extends App with LazyLogging {
def inspect(name: String) {"Generating $name")
val optspec = ExampleWorkflows.parseExample(name)
if (!optspec.isDefined) {
logger.error(s"Not a valid spec: $name")
val spec = optspec.get"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterStubbornSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val (result, graph, afterlabels, proven, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), InvProperties.DEFAULT)
(result, dot)
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
write(s"${name}.inv", msg)
for ((s, i) <- dot.zipWithIndex) {
write(s"${name}_${i}.dot", s)
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
\ No newline at end of file
......@@ -54,6 +54,7 @@ object MainInvariants extends App with LazyLogging {
// generateExample("nonomitting/conference")
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
\ No newline at end of file
......@@ -10,6 +10,7 @@ import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory
import de.tum.workflows.ltl.FOTransformers
object MainLTL extends App with LazyLogging {
Supports Markdown
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