package de.tum.workflows.ltl.tests import org.scalatest.FlatSpec import org.scalatest.Matchers._ import org.scalatest.Inspectors._ import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.Implicits._ import de.tum.workflows.blocks._ import de.tum.workflows.Preconditions import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.ExampleWorkflows import de.tum.workflows.toz3.InvariantChecker import de.tum.workflows.Encoding._ import de.tum.workflows.Utils import de.tum.workflows.Encoding import de.tum.workflows.ExampleWorkflows import de.tum.workflows.toz3.InvariantChecker class NonOmittingInvariantFilesTest extends FlatSpec { "InvariantChecker" should "prove simple things safe" in { val name = "tests/simpleNoChoice2" val inv = Forall(List("x", "s"), genEq("R", List("x", "s"))) assert(checkSafe(name, inv)) } it should "prove simple loops safe" in { val name = "tests/loopexampleNoOracle" val inv = Forall(List("x", "s"), genEq("R", List("x", "s"))) assert(checkSafe(name, inv)) } it should "prove simple loops safe and iterate" in { val name = "tests/loopexampleNoOracle" val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s"))) assert(checkSafe(name, inv)) } it should "fail on oracly things" in { val name = "tests/simpleChoice" val inv = Forall(List("x", "s"), genEq("R", List("x", "s"))) assert(!checkSafe(name, inv)) } it should "fail on loopy oracly things" in { val name = "tests/loopexample" val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s"))) assert(!checkSafe(name, inv)) } def checkSafe(name: String, inv: Formula) = { val spec = ExampleWorkflows.parseExample(name).get val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true) Utils.write(s"${name}.dot", dot) res } def genEq(name: String, params: List[Var]) = { val o1 = Fun(name, Some("t1"), params) val o2 = Fun(name, Some("t2"), params) Eq(o1, o2) } }