Commit cb231255 authored by Christian Müller's avatar Christian Müller

example

parent 305343f5
Workflow
forall x,s
P(s) -> Q += (x,s)
forall x,s
Q(s) -> R += (x,s)
Target
R(x,s)
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
class InvariantFilesTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val spec = ExampleWorkflows.parseExample("tests/simpleNoChoice2").get
val inv = Forall(List("x","s"), genEq("R", List("x","s")))
val (safe, msg) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
println(msg.toString())
safe should be(true)
}
def genEq(name:String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ 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