FOLTLTermFunctions.scala 4.28 KB
Newer Older
Christian Müller's avatar
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
36
37
38
39
40
41
42
43
44
package de.tum.workflows.foltl

import FOLTL._

object TermFunctions {

  def freeVars(t: Term) = {
    def free(t: Term, bound: Set[Var]): Set[Var] = {
      t match {
        // Extractors
        // Exists, Forall
        case Quantifier(_, ps, t)  => free(t, bound ++ ps)
        case Until(t1, t2)         => free(t1, bound) ++ free(t2, bound)
        case Next(t1)              => free(t1, bound)
        case Globally(t1)          => free(t1, bound)
        case Finally(t1)           => free(t1, bound)
        // And, Or, Eq, Implies
        case BinOp(_, t1, t2)      => free(t1, bound) ++ free(t2, bound)
        case Neg(t1)               => free(t1, bound)

        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
        case Fun(_, _, ps)         => (ps.toSet -- bound)
        case v: Var if !bound(v)   => Set(v)
        case x                     => Set()
      }
    }
    free(t, Set())
  }

  def simplify(t: Term): Term = {
    val simp: PartialFunction[Term, Term] = {
      // Push negation inward
      case Neg(Or(t1, t2))                        => And(Neg(t1), Neg(t2))
      case Neg(And(t1, t2))                       => Or(Neg(t1), Neg(t2))
      case Neg(Globally(t))                       => Finally(Neg(t))
      case Neg(Finally(t))                        => Globally(Neg(t))
      case Neg(Next(t))                           => Next(Neg(t))
      case Neg(Forall(vars, t))                   => Exists(vars, Neg(t))
      case Neg(Exists(vars, t))                   => Forall(vars, Neg(t))
      case Neg(Implies(t1, t2))                   => And(t1, Neg(t2))

      // Simple laws
      case Neg(True)                              => False
      case Neg(False)                             => True
45
      case Neg(Neg(t))                            => t
Christian Müller's avatar
Christian Müller committed
46
47
48
49
50
51
52
53
54
      case Or(True, t)                            => True
      case Or(t, True)                            => True
      case Or(False, t)                           => t
      case Or(t, False)                           => t
      case And(False, t)                          => False
      case And(t, False)                          => False
      case And(True, t)                           => t
      case And(t, True)                           => t

55
56
      // Equivalence
      case Eq(t1, t2)                 if t1 == t2 => True
Christian Müller's avatar
Christian Müller committed
57

58
59
60
61
      
      // Double Temporals
      case Finally(Finally(t))                    => Finally(t)
      case Globally(Globally(t))                  => Globally(t)
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

      // Remove quantifiers if empty
      case Quantifier(qmake, xs, t) if xs.isEmpty => t
      case Quantifier(qmake, xs, True)            => True
      case Quantifier(qmake, xs, False)           => False

      // Remove variables from quantifiers if not used in the body
      //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
      //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
      //
      //      // Split off binops from quantifiers
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(t1, qmake(xs, t2))
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(qmake(xs, t1), t2)
    }

    val t1 = everywhere(simp, t)
    if (t == t1) t1 else simplify(t1)
  }

  def everywhere(trans: PartialFunction[Term, Term], t: Term): Term = {
    if (trans.isDefinedAt(t))
      trans(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
        case Until(t1, t2)           => Until(everywhere(trans, t1), everywhere(trans, t2))
        case Finally(t1)             => Finally(everywhere(trans, t1))
        case Globally(t1)            => Globally(everywhere(trans, t1))
        case Next(t1)                => Next(everywhere(trans, t1))
        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
        case Neg(t1)                 => Neg(everywhere(trans, t1))

        case x                       => x
      }
  }
  
  def assumeEmpty(t: Term, name: String) = {
    t.everywhere({
      case Fun(f, _, _) if f == name => False
    })
  }

  def annotate(t: Term, name: String) = {
    t.everywhere({
      case Fun(f, None, xs) => Fun(f, Some(name), xs)
    })
  }
}