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

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions}
Christian Müller's avatar
tests  
Christian Müller committed
9 10

class FOLTLTest extends FlatSpec {
Christian Müller's avatar
Christian Müller committed
11 12 13
  "Formulas" should "be constructed correctly" in {
    True  Var("x") should be (Implies(True, Var("x")))
  }
Christian Müller's avatar
tests  
Christian Müller committed
14 15 16 17 18 19

  "Formula functions" should "generate inequalities" in {

    val f = ForallOtherThan("x", List("y", "z"), Globally("x"))
    val res = f.removeOTQuantifiers()
    res should be(
Christian Müller's avatar
Christian Müller committed
20
      Forall("x", Implies(And(Neg(Equiv("x", "y")), Neg(Equiv("x", "z"))), Globally("x")))
Christian Müller's avatar
tests  
Christian Müller committed
21 22 23
    )
    
    val f2 = ForallOtherThan(List("x","y"), "z", Globally("x"))
Christian Müller's avatar
Christian Müller committed
24
    val res2 = f2.removeOTQuantifiers()
Christian Müller's avatar
tests  
Christian Müller committed
25
    res2 should be(
Christian Müller's avatar
Christian Müller committed
26
      Forall(List("x","y"), Implies(And(Neg(Equiv("x", "z")), Neg(Equiv("y", "z"))), Globally("x")))
Christian Müller's avatar
tests  
Christian Müller committed
27 28
    )
  }
Christian Müller's avatar
Christian Müller committed
29
  
Christian Müller's avatar
Christian Müller committed
30 31
  "Simplification" should "simplify equal things" in {
    val t = Forall("x", Fun("S", "x"))
Christian Müller's avatar
Christian Müller committed
32
    And(t, t).simplify should be (t)
Christian Müller's avatar
Christian Müller committed
33
  }
34

Christian Müller's avatar
Christian Müller committed
35
  it should "make lists" in {
Christian Müller's avatar
Christian Müller committed
36
    And.make("c", "d", "e", "d" lor "e").simplify should be ("c" land ("d" land ("e" land ("d" lor "e"))).simplify)
Christian Müller's avatar
Christian Müller committed
37 38
  }

39

Christian Müller's avatar
Christian Müller committed
40
  it should "simplify double negation" in {
Christian Müller's avatar
Christian Müller committed
41
    Neg(Neg(True)).simplify should be(True)
Christian Müller's avatar
Christian Müller committed
42 43
  }

44
  it should "double negation inside quantification" in {
Christian Müller's avatar
Christian Müller committed
45
    Forall("x", Neg(Neg(Var("x")))).simplify should be (Forall("x", Var("x")))
46 47 48
  }

  it should "simplify trivial stuff" in {
Christian Müller's avatar
Christian Müller committed
49
    And(True, Var("y")).simplify should be (Var("y"))
50 51 52
  }

  it should "simplify more trivial stuff" in {
Christian Müller's avatar
Christian Müller committed
53
    And(False, Var("y")).simplify should be (False)
54 55 56
  }

  it should "simplify even more trivial stuff" in {
Christian Müller's avatar
Christian Müller committed
57
    And(Or(False, False), Var("y")).simplify should be (False)
58 59
  }

Christian Müller's avatar
Christian Müller committed
60 61
  it should "simplify quantors" in {
    val f = And(Forall("x", Fun("f", "x")), Forall("x", Fun("f", "x")))
Christian Müller's avatar
Christian Müller committed
62
    f.simplify should be (Forall("x", Fun("f", "x")))
Christian Müller's avatar
Christian Müller committed
63 64
  }
  
Christian Müller's avatar
Christian Müller committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
  "Parallel rename" should "work on simple functions" in {
    val f = And("a", Fun("f", List("b","a")))
    
    val res = f.parallelRename(List("a","b"), List("c","a"))
    
    res should be (And("c", Fun("f", List("a","c"))))
  }
  
  it should "work on quantors" in {
    val f = And("a", Exists("a", Fun("f", List("b","a"))))
    
    val res = f.parallelRename(List("a","b"), List("c","a"))
    
    res should be (And("c", Exists("a", Fun("f", List("a","a")))))
  }
  
Christian Müller's avatar
Christian Müller committed
81
  "Formulas" should "compute prenex form" in {
Christian Müller's avatar
Christian Müller committed
82
    val f = Forall("x", Exists("y", And("x", Forall("z", Or(Neg(Forall("a", "a" land "y")), "z")))))
Christian Müller's avatar
Christian Müller committed
83
    
Christian Müller's avatar
Christian Müller committed
84
    f.toPrenex.simplify should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a" land "y"), "z")))))).simplify)
Christian Müller's avatar
Christian Müller committed
85 86 87 88
  }
  
  it should "rebind several things" in {
    val f = And.make(Forall("x", "x"), Forall("x", "x"), Forall("x","x"))
Christian Müller's avatar
Christian Müller committed
89
    val p = f.toPrenex.simplify
Christian Müller's avatar
Christian Müller committed
90
    p should be (Forall("x","x"))
Christian Müller's avatar
Christian Müller committed
91 92 93 94 95
  }
  
  it should "work on implication" in {
    val f = Implies(Forall("a", "a"), Exists("x", "x"))
    
Christian Müller's avatar
Christian Müller committed
96
    f.toPrenex should be (Exists(List("a","x"), Or(Neg("a"), "x")))
Christian Müller's avatar
Christian Müller committed
97 98 99 100 101
  }
  
  it should "preserve BS" in {
    val f = And(Forall("a", "a"), Exists("z", "z"))
    
Christian Müller's avatar
Christian Müller committed
102
    f.toPrenex should be (Exists("z", Forall("a", And("a", "z"))))
Christian Müller's avatar
Christian Müller committed
103 104
  }
  
105 106 107
  it should "compute CNF" in {
    val f = Or(And("a", "b"), And("c","d"))
    
Christian Müller's avatar
Christian Müller committed
108
    f.toCNF.simplify should be (
Christian Müller's avatar
Christian Müller committed
109 110 111 112
      And.make(
          Or("a", "c"), Or("a","d"), 
          Or("b","c"), Or("b","d")
      )
113 114
    )
  }
115

Christian Müller's avatar
Christian Müller committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
  it should "compute DNF" in {
    val f = Neg(("a" lor "b") land ("c" lor "d"))

    f.toDNF.simplify should be (
      (Neg("a") land Neg("b")) lor (Neg("c") land Neg("d"))
    )
  }

  it should "compute quantified DNF" in {
    val f = Exists("x", Fun("a", "c") lor Fun("a", "x"))

    f.toDNF.simplify should be (f)

    val f2 = Exists("x", Fun("a", "c") land Fun("a", "x"))

    f2.toDNF.simplify should be (f2)
  }

134 135 136 137 138 139 140
  it should "compute nested quantprefixes" in {
    val x = Var("x", "S")
    val f = Forall(x, Forall(x, Fun("f",x)))
    FormulaFunctions.collectQuantifiers(f) should be {
      List((false, List(x, x)))
    }
  }
141
  
142 143 144
  it should "also compute CNF" in {
    val f = Or.make(And("a", "b"), And("c","d"), And("e", "f"))
    
Christian Müller's avatar
Christian Müller committed
145
    f.toCNF.simplify should be (
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
      And.make(
          Or.make("a", "c", "e"),
          Or.make("a", "c", "f"),
          Or.make("a","d", "e"),
          Or.make("a","d","f"),
          Or.make("b","c","e"), 
          Or.make("b","c","f"), 
          Or.make("b","d","e"),
          Or.make("b","d","f")
      )
    )
  }
  
  it should "also compute CNF for weird structural things" in {
    val f = Or.make(And("a", "b"), And("c","d"), Or("e", "f"))
    
Christian Müller's avatar
Christian Müller committed
162
    f.toCNF.simplify should be (
163 164 165 166 167 168 169 170
      And.make(
          Or.make("a", "c", "e", "f"),
          Or.make("a","d", "e", "f"),
          Or.make("b","c","e", "f"), 
          Or.make("b","d","e", "f")
      )
    )
  }
Christian Müller's avatar
Christian Müller committed
171 172 173 174

  // TODO: Here, rebinding would be possible because of
  // ∃x. f(x) ∨ ∃x. g(x) = ∃x. f(x) ∨ g(x)
  it should "compute CNF for formulas with quantifiers" ignore {
175
    val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
Christian Müller's avatar
Christian Müller committed
176
    f.toCNF.simplify should be (
Christian Müller's avatar
Christian Müller committed
177 178
      Exists(List("c"), And.make(
          "c", 
Christian Müller's avatar
Christian Müller committed
179
          Or("c","d"), 
Christian Müller's avatar
Christian Müller committed
180
          Or("b","c"), 
Christian Müller's avatar
Christian Müller committed
181
          Or("b","d")
182 183 184
      ))    
    )
  }
Christian Müller's avatar
Christian Müller committed
185 186 187 188 189 190 191 192 193
  
  it should "not fail at doing so" in {
    val f = Forall(List("xt","pt","yt","p"), And.make(
        Neg(Fun("B", List("xt","pt"))),
        Neg(Fun("B", List("yt","p"))),
        Neg(Fun("B", List("yt","pt"))),
        Neg(Fun("Conf",Some("t1"),List("xt","p")))
        ))
        
Christian Müller's avatar
Christian Müller committed
194 195 196 197 198
     f.toCNF should be (FormulaFunctions.pushUniversalQuantifiers(f))

    True.toCNF should be (True)
    False.toCNF should be (False)

Christian Müller's avatar
Christian Müller committed
199
  }
Christian Müller's avatar
src  
Christian Müller committed
200 201 202 203 204 205

  val x = Fun("f", "x")
  val y = Fun("f", "y")
  val z = Fun("f", "z")
  val c = Fun("f", "c")
  val d = Fun("g", Nil)
Christian Müller's avatar
Christian Müller committed
206 207 208
    
  "quantifier pushing" should "work" in {
    val f = Forall("x", And(Fun("f","x"), Fun("f","c")))
Christian Müller's avatar
src  
Christian Müller committed
209 210 211 212 213 214 215
    FormulaFunctions.pushUniversalQuantifiers(f) should be (And(Forall("x", Fun("f","x")),Fun("f","c")))

    val f2 = Forall(List("x", "y"), Fun("a", List()))
    FormulaFunctions.pushUniversalQuantifiers(f2) should be (Fun("a", List()))

    val f3 = Forall(List("x", "y", "z"), (x land y) lor (z land c land d))
    FormulaFunctions.pushUniversalQuantifiers(f3) should be (
Christian Müller's avatar
Christian Müller committed
216
      (Forall("x", x) land Forall("y", y)) lor (Forall("z", z) land c land d).simplify
Christian Müller's avatar
src  
Christian Müller committed
217 218 219
    )


Christian Müller's avatar
Christian Müller committed
220
  }
Christian Müller's avatar
src  
Christian Müller committed
221

Christian Müller's avatar
Christian Müller committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252
  "Universe instantiation" should "work" in {

    val universe = Map(
      "A" -> List(Var("x","A"), Var("y","A")),
      "B" -> List(Var("b","B")),
      "C" -> List()
    )
    val a = Var("a", "A")
    val b = Var("b", "A")
    val xa = Var("x", "A")
    val ya = Var("y", "A")
    val za = Var("z","A")

    val tests = Map(
      True -> True,
      False -> False,
      Forall(Var("z","A"), Fun("f", List(Var("z", "A")))) ->
        And.make(Fun("f", List(Var("x", "A"))), Fun("f", List(Var("y", "A")))),
      Exists(Var("z","B"), Fun("f", List(Var("z", "B")))) ->
        Fun("f", List(Var("b", "B"))),
      Forall(Var("c","C"), Fun("f", List(Var("c", "C")))) ->
        True,
      Forall(a, Exists(b, Fun("f", List(a, b)))) ->
        And.make(Or.make(Fun("f", List(xa, xa)), Fun("f", List(xa, ya))),
          Or.make(Fun("f", List(ya, xa)), Fun("f", List(ya, ya))))
    )
    for ((from, to) <- tests) {
      FOTransformers.eliminateQuantifiers(from, universe) should be (to)
    }
  }

Christian Müller's avatar
src  
Christian Müller committed
253

Christian Müller's avatar
tests  
Christian Müller committed
254
}