InvariantFilesTest.scala 953 Bytes
Newer Older
Christian Müller's avatar
example  
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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)
  }
}