TestUtils.scala 1.15 KB
Newer Older
1 2 3
package de.tum.workflows.tests

import de.tum.workflows.toz3.InvariantChecker
Christian Müller's avatar
Christian Müller committed
4
import de.tum.workflows.Utils._
5 6
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows._
Christian Müller's avatar
Christian Müller committed
7
import de.tum.workflows.toz3.InvProperties
8 9

object TestUtils {
Christian Müller's avatar
Christian Müller committed
10
  
Christian Müller's avatar
Christian Müller committed
11 12 13 14 15 16 17 18 19
  def checkSafeStubborn(name: String, inv: Formula):Boolean = {
    checkSafeStubborn(name, "", inv)
  }
  
  def checkSafeStubbornNoElim(name: String, inv: Formula):Boolean = {
    check(name, "noelim", inv, InvProperties(true, false))
  }
      
  def checkSafeStubborn(name: String, desc:String, inv: Formula) = {
20
    check(name, desc, inv, InvProperties(true, true, true))
Christian Müller's avatar
Christian Müller committed
21 22
  }
  
23 24
  def checkSafeCausalNoElim(name: String, inv: Formula):Boolean = {
    checkSafeCausalNoElim(name, "", inv)
Christian Müller's avatar
Christian Müller committed
25
  }
26 27

  def checkSafeCausalNoElim(name: String, desc:String, inv: Formula) = {
Christian Müller's avatar
Christian Müller committed
28
    check(name, desc, inv, InvProperties(false, false))
Christian Müller's avatar
Christian Müller committed
29 30
  }
  
31
  def checkSafeCausalElim(name: String, desc:String, inv: Formula) = {
32
    check(name, s"${desc}_elim", inv, InvProperties(false, true, true))
Christian Müller's avatar
Christian Müller committed
33 34
  }
  
35 36 37
  def genEq(name: String, params: List[Var]) = {
    val o1 = Fun(name, Some("t1"), params)
    val o2 = Fun(name, Some("t2"), params)
Christian Müller's avatar
Christian Müller committed
38
    Equiv(o1, o2)
39 40
  }
}