PreconditionTest.scala 2.68 KB
Newer Older
1
package de.tum.niwo.tests
Christian Müller's avatar
Christian Müller committed
2 3 4 5

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7 8 9
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions
10
import de.tum.niwo.invariants.Preconditions
Christian Müller's avatar
Christian Müller committed
11 12 13

class PreconditionTest extends FlatSpec {

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
  // TODO: These tests don't work as we now depend on the spec
//  "Preconditions" should "work on simple blocks" in {
//    
//    // forall a,b S(a) -> R += (a,b)
//    val s = Add(Fun("S", List("a")), "R", List("a", "b"))
//    val b = ForallMayBlock(List("a","b"), "choice1", List(s))
//    val f = Fun("R", Some("t1"), List("x", "y"))
//    
//    val pre = Preconditions.weakestPrecondition(f, b)
//    
//    pre should be (
//      FormulaFunctions.annotate(
//       Or(Fun("R", List("x","y")), And(Fun("S", List("x")), Fun("choice1", List("x","y")))),
//       "t1"
//      )
//    )
//    
//    val f2 = Fun("R", Some("t1"), List("a", "b"))
//    val pre2 = Preconditions.weakestPrecondition(f2, b)
//    
//    pre2 should be (
//      FormulaFunctions.annotate(
//       Or(Fun("R", List("a","b")), And(Fun("S", List("a")), Fun("choice1", List("a","b")))),
//       "t1"
//      )
39
//    )s
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
//  }
//  
//  it should "work on omitting workflows" in {
//    // forall a,b S(a,b) -> R += (a)
//    val s = Add(Fun("S", List("a","b")), "R", List("b"))
//    val b = ForallMayBlock(List("a","b"), "choice1", List(s))
//   
//    val f = Fun("R", Some("t1"), List("x"))
//    val pre = Preconditions.weakestPrecondition(f, b)
//    
//    pre should be (
//      FormulaFunctions.annotate(
//       Or(Fun("R", List("x")), Exists("a", And(Fun("S", List("a", "x")), Fun("choice1", List("a","x"))))),
//       "t1"
//      )
//    )
//  }
Christian Müller's avatar
Christian Müller committed
57
  
58 59 60 61 62 63 64 65 66 67 68 69 70 71
//  it should "work on blocks with several statements" in {
//    // forall a,b
//    //   R(a,b) -> S += b
//    //   S(a) -> T -= (a,b)
//    val s1 = Add(Fun("R", List("a","b")), "S", List("b"))
//    val s2 = Remove(Fun("S", List("b")), "T", List("a"))
//    val b = ForallMayBlock(List("a","b"), "choice1", List(s1, s2))
//   
//    val f = Exists("x", And(Fun("S", Some("t1"), List("x")), Fun("T", Some("t2"), List("y"))))
//    
//    val pre = Preconditions.weakestPrecondition(f, b, spec, false)
//    
//    val res1 = FormulaFunctions.annotate(
//        Or(Fun("S", List("x")), Exists("a", And(Fun("R", List("a", "x")), Fun("choice1", List("a","x"))))),
Christian Müller's avatar
Christian Müller committed
72
//        "t1").simplify
73 74
//    val res2 = FormulaFunctions.annotate(
//        And(Fun("T",List("y")), Forall("b", Neg(And(Fun("S", List("b")), Fun("choice1", List("y","b")))))),
Christian Müller's avatar
Christian Müller committed
75
//        "t2").simplify
76 77 78 79 80
//    
//    pre should be (
//      Exists("x", And(res1, res2))
//    )
//  }
Christian Müller's avatar
Christian Müller committed
81 82
  
}