FOLTLTest.scala 4.8 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.workflows.tests
Christian Müller's avatar
tests  
Christian Müller committed
2
3
4
5
6
7

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
8
import de.tum.workflows.foltl.FOLTL
Christian Müller's avatar
Christian Müller committed
9
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
tests  
Christian Müller committed
10
11

class FOLTLTest extends FlatSpec {
Christian Müller's avatar
Christian Müller committed
12
13
14
  "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
15
16
17
18
19
20
21
22
23
24

  "Formula functions" should "generate inequalities" in {

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


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

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
  it should "double negation inside quantification" in {
    Forall("x", Neg(Neg(Var("x")))).simplify() should be (Forall("x", Var("x")))
  }

  it should "simplify trivial stuff" in {
    And(True, Var("y")).simplify() should be (Var("y"))
  }

  it should "simplify more trivial stuff" in {
    And(False, Var("y")).simplify() should be (False)
  }

  it should "simplify even more trivial stuff" in {
    And(Or(False, False), Var("y")).simplify() should be (False)
  }

Christian Müller's avatar
Christian Müller committed
57
58
  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
59
    f.simplify should be (Forall("x", Fun("f", "x")))
Christian Müller's avatar
Christian Müller committed
60
61
  }
  
Christian Müller's avatar
Christian Müller committed
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  "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
78
79
80
  it should "compute prenex form" in {
    val f = Forall("x", Exists("y", And("x", Forall("z", Or(Neg(Forall("a", "a")), "z")))))
    
Christian Müller's avatar
Christian Müller committed
81
    f.toPrenex should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a"), "z")))))))
Christian Müller's avatar
Christian Müller committed
82
83
84
85
  }
  
  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
86
    val p = f.toPrenex.simplify
Christian Müller's avatar
Christian Müller committed
87
    p should be (Forall("x","x"))
Christian Müller's avatar
Christian Müller committed
88
89
90
91
92
  }
  
  it should "work on implication" in {
    val f = Implies(Forall("a", "a"), Exists("x", "x"))
    
Christian Müller's avatar
Christian Müller committed
93
    f.toPrenex should be (Exists(List("a","x"), Or(Neg("a"), "x")))
Christian Müller's avatar
Christian Müller committed
94
95
96
97
98
  }
  
  it should "preserve BS" in {
    val f = And(Forall("a", "a"), Exists("z", "z"))
    
Christian Müller's avatar
Christian Müller committed
99
    f.toPrenex should be (Exists("z", Forall("a", And("a", "z"))))
Christian Müller's avatar
Christian Müller committed
100
101
  }
  
Christian Müller's avatar
Christian Müller committed
102
103
104
  it should "compute CNF" in {
    val f = Or(And("a", "b"), And("c","d"))
    
Christian Müller's avatar
Christian Müller committed
105
    f.toCNF.simplify should be (
Christian Müller's avatar
Christian Müller committed
106
107
108
109
      And.make(
          Or("a", "c"), Or("a","d"), 
          Or("b","c"), Or("b","d")
      )
Christian Müller's avatar
Christian Müller committed
110
111
112
    )
  }
  
113
114
115
  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
116
    f.toCNF.simplify should be (
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
      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
133
    f.toCNF.simplify should be (
134
135
136
137
138
139
140
141
142
      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
143
144
  it should "compute CNF for formulas with quantifiers" in {
    val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
Christian Müller's avatar
Christian Müller committed
145
    f.toCNF.simplify should be (
Christian Müller's avatar
Christian Müller committed
146
147
      Exists(List("c"), And.make(
          "c", 
Christian Müller's avatar
Christian Müller committed
148
          Or("c","d"), 
Christian Müller's avatar
Christian Müller committed
149
          Or("b","c"), 
Christian Müller's avatar
Christian Müller committed
150
          Or("b","d")
Christian Müller's avatar
Christian Müller committed
151
152
153
      ))    
    )
  }
Christian Müller's avatar
Christian Müller committed
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
  
  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")))
        ))
        
     f.toCNF should be (f)
  }
    
  "quantifier pushing" should "work" in {
    val f = Forall("x", And(Fun("f","x"), Fun("f","c")))
    FormulaFunctions.pushQuantifiers(f) should be (And(Forall("x", Fun("f","x")),Fun("f","c")))
  }
Christian Müller's avatar
tests  
Christian Müller committed
170
}