FOLTL.scala 11.6 KB
Newer Older
1
package de.tum.niwo.foltl
Christian Müller's avatar
Christian Müller committed
2

3
import de.tum.niwo.Utils
Christian Müller's avatar
src  
Christian Müller committed
4

Christian Müller's avatar
Christian Müller committed
5
import scala.util.matching.Regex
6

Christian Müller's avatar
Christian Müller committed
7 8 9
//import de.tum.workflows.foltl.TermFunctions._

object FOLTL {
10
  abstract class Formula {
Christian Müller's avatar
Christian Müller committed
11
    lazy val simplify: Formula = FormulaFunctions.simplify(this)
Christian Müller's avatar
Christian Müller committed
12 13

    lazy val freeVars: Set[Var] = FormulaFunctions.freeVars(this)
Christian Müller's avatar
ineq  
Christian Müller committed
14
    lazy val boundVars: Set[Var] = FormulaFunctions.boundVars(this)
Christian Müller's avatar
Christian Müller committed
15 16
    lazy val opsize: Int = FormulaFunctions.opsize(this)

Christian Müller's avatar
Christian Müller committed
17 18 19 20 21 22 23 24 25 26 27
    def everywhere(trans: PartialFunction[Formula, Formula]): Formula = FormulaFunctions.everywhere(trans, this)
    def assumeEmpty(name: String): Formula = FormulaFunctions.assumeEmpty(this, name)
    def assumeEmpty(names: List[String]): Formula = FormulaFunctions.assumeAllEmpty(this, names)
    def in(name: String): Formula = FormulaFunctions.annotate(this, name)
    def in(name: String, ignore: Set[String]): Formula = FormulaFunctions.annotate(this, name, ignore)
    def collect[T](coll: PartialFunction[Formula, List[T]]):List[T] = FormulaFunctions.collect(coll, this)
    def hasSubFormula(coll: PartialFunction[Formula, Boolean]):Boolean = FormulaFunctions.hasSubFormula(coll, this)

    def toPrenex: Formula = FormulaFunctions.toPrenex(this)
    def toNegNf: Formula = FormulaFunctions.toNegNf(this)
    def toCNF: Formula = FormulaFunctions.toCNF(this)
Christian Müller's avatar
Christian Müller committed
28
    def toDNF: Formula = FormulaFunctions.toDNF(this)
Christian Müller's avatar
Christian Müller committed
29 30

    lazy val isBS: Boolean = FormulaFunctions.isBS(this)
Christian Müller's avatar
src  
Christian Müller committed
31
    lazy val isUniversal: Boolean = FormulaFunctions.isU(this)
Christian Müller's avatar
Christian Müller committed
32
    lazy val isQFree: Boolean = FormulaFunctions.isQFree(this)
Christian Müller's avatar
Christian Müller committed
33 34 35

    def removeOTQuantifiers(): Formula = FormulaFunctions.removeOTQuantifiers(this)
    def parallelRename(vars: List[Var], newvars: List[Var]): Formula = FormulaFunctions.parallelRename(this, vars, newvars)
36

Christian Müller's avatar
Christian Müller committed
37
    lazy val bracketed: String = this match {
38
      case _: BinOp => "(" + this + ")"
Christian Müller's avatar
Christian Müller committed
39
      case _        => this.toString
40
    }
Christian Müller's avatar
Christian Müller committed
41

Christian Müller's avatar
Christian Müller committed
42 43
    // single arrow is for maps
    def -->(f2: Formula) = Implies(this, f2)
Christian Müller's avatar
Christian Müller committed
44
    def (f2: Formula) = Implies(this, f2)
Christian Müller's avatar
Christian Müller committed
45 46
    def land(f2: Formula) = And(this, f2)
    def /\(f2: Formula) = And(this, f2)
Christian Müller's avatar
Christian Müller committed
47
    def (f2: Formula) = And(this, f2)
Christian Müller's avatar
src  
Christian Müller committed
48
    def lor(f2: Formula) = Or(this, f2)
Christian Müller's avatar
Christian Müller committed
49
    def (f2: Formula) = Or(this, f2)
Christian Müller's avatar
Christian Müller committed
50
    def \/(f2: Formula) = Or(this, f2)
51

Christian Müller's avatar
Christian Müller committed
52
    // TODO: better line breaking
Christian Müller's avatar
Christian Müller committed
53
    lazy val pretty: String = {
Christian Müller's avatar
Christian Müller committed
54
      val remeq = this.everywhere {
Christian Müller's avatar
Christian Müller committed
55 56
        case Equiv(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
          Equiv(t1, Fun("eq", List()))
Christian Müller's avatar
Christian Müller committed
57
      }
Christian Müller's avatar
Christian Müller committed
58

Christian Müller's avatar
Christian Müller committed
59
      val s = remeq.toString
Christian Müller's avatar
Christian Müller committed
60
      val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
61 62

      // indent
Christian Müller's avatar
Christian Müller committed
63
      var opens = 0
64 65 66 67 68 69 70 71
      val indented = for (line <- broken.lines) yield {
        val indent = " " * (opens * 2)
        val ret = indent + line
        opens += line.count(_ == '(')
        opens -= line.count(_ == ')')
        ret
      }
      indented.reduce(_ + "\n" + _)
Christian Müller's avatar
Christian Müller committed
72
    }
73 74 75 76 77 78 79

    def toTypedString: String = {
      this.everywhere {
        case v:Var => Var(v.withType)
        case f:Fun => Var(f.toTypedString)
      }.toString
    }
Christian Müller's avatar
Christian Müller committed
80 81
  }

82 83
  case object True extends Formula
  case object False extends Formula
Christian Müller's avatar
Christian Müller committed
84

85 86 87
  object Var {
    val DEFAULT_TYPE = "T"
  }
Christian Müller's avatar
Christian Müller committed
88
  case class Var(name: String, typ: String = Var.DEFAULT_TYPE) extends Formula {
Christian Müller's avatar
Christian Müller committed
89 90
    override def toString = s"$name"
    def withType = s"$name:$typ"
Christian Müller's avatar
Christian Müller committed
91
  }
92

Christian Müller's avatar
Christian Müller committed
93
  object Fun {
94
    def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
Christian Müller's avatar
Christian Müller committed
95
  }
Christian Müller's avatar
src  
Christian Müller committed
96
  object FunNameFromVar {
Christian Müller's avatar
Christian Müller committed
97
    val PredicateNoParam: Regex = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?".r
Christian Müller's avatar
src  
Christian Müller committed
98 99 100 101 102 103 104 105 106

    def unapply(s: String): Option[(String, Option[String])] = {
      s match {
        case PredicateNoParam(name, null, _*) => Some((name, None))
        case PredicateNoParam(name, _, ind, _*)  => Some((name, Some(ind)))
        case _                                 => None
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
107
  object FunFromVar {
Christian Müller's avatar
Christian Müller committed
108
    val Predicate: Regex = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)".r
Christian Müller's avatar
Christian Müller committed
109

Christian Müller's avatar
Christian Müller committed
110 111
    def getVars(s: String): List[Var] = {
      val split = s split "_"
Christian Müller's avatar
Christian Müller committed
112 113 114 115
      if (split.length > 1) {
        split.drop(1).map(str => {
          val Array(name, typ) = str.split("#")
          Var(name, typ)
Christian Müller's avatar
Christian Müller committed
116
        }).toList
Christian Müller's avatar
Christian Müller committed
117 118 119 120 121 122
      } else {
        List()
      }
    }

    def unapply(s: String): Option[Fun] = {
Christian Müller's avatar
Christian Müller committed
123
      s match {
Christian Müller's avatar
Christian Müller committed
124 125 126
        case Predicate(name, null, _, tup, _*) => Some(Fun(name, None, getVars(tup)))
        case Predicate(name, _, ind, tup, _*)  => Some(Fun(name, Some(ind), getVars(tup)))
        case _                                 => None
Christian Müller's avatar
Christian Müller committed
127 128 129
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
130

131
  case class Fun(name: String, ind: Option[String], params: List[Var]) extends Formula {
Christian Müller's avatar
Christian Müller committed
132
    override def toString: String = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
133 134
    override def toTypedString: String = name + Utils.mkString(ind, "(", "", ")") + params.map(_.withType).mkString("(", ",", ")")

Christian Müller's avatar
Christian Müller committed
135
    def updatedParams(index: Int, p: Var) = Fun(name, ind, params.updated(index, p))
Christian Müller's avatar
Christian Müller committed
136
    def updatedParams(list: List[Var]) = Fun(name, ind, list)
Christian Müller's avatar
Christian Müller committed
137

Christian Müller's avatar
Christian Müller committed
138 139 140 141
    def isOracle: Boolean = name.startsWith("O")
    def isConstInput: Boolean = name.startsWith("I")
    def isAux: Boolean = name.startsWith("choice")
    def isB: Boolean = name.startsWith("B")
Christian Müller's avatar
Christian Müller committed
142

Christian Müller's avatar
Christian Müller committed
143
    def encodeToVar(): Var = {
Christian Müller's avatar
Christian Müller committed
144 145 146
      val pi = if (ind.isDefined) "#" + ind.get else ""
      val tup = params.map(p => p.name + "#" + p.typ)
      Var(name + pi + Utils.mkString(tup, "_", "_", ""))
Christian Müller's avatar
Christian Müller committed
147
    }
Christian Müller's avatar
Christian Müller committed
148
    def encodeName(): String = {
Christian Müller's avatar
src  
Christian Müller committed
149 150 151
      val pi = if (ind.isDefined) "#" + ind.get else ""
      name + pi
    }
Christian Müller's avatar
Christian Müller committed
152 153
  }

154
  trait Quantifier extends Formula {
Christian Müller's avatar
Christian Müller committed
155
    def make: (List[Var], Formula) => Formula
Christian Müller's avatar
Christian Müller committed
156 157
    def qname: String
    def vars: List[Var]
158
    def t: Formula
159

Christian Müller's avatar
Christian Müller committed
160
    override def toString: String = {
161
      // show types only in quantifiers
Christian Müller's avatar
Christian Müller committed
162
      qname + " " + vars.map(_.withType).mkString(",") + ". " + t.bracketed
Christian Müller's avatar
Christian Müller committed
163 164
    }
  }
165

Christian Müller's avatar
Christian Müller committed
166
  object Quantifier {
Christian Müller's avatar
Christian Müller committed
167
    def unapply(q: Quantifier) = Some((q.make, q.vars, q.t))
Christian Müller's avatar
Christian Müller committed
168
    def make(m: (List[Var], Formula) => Quantifier, l:List[Var], f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
169 170 171 172
      if (l.isEmpty) f else m(l, f)
    }
  }
  object Exists {
Christian Müller's avatar
Christian Müller committed
173
    def make: (List[Var], Formula) => Formula = Quantifier.make(Exists.apply, _:List[Var], _:Formula)
Christian Müller's avatar
Christian Müller committed
174 175
  }
  object Forall {
Christian Müller's avatar
Christian Müller committed
176
    def make: (List[Var], Formula) => Formula = Quantifier.make(Forall.apply, _:List[Var], _:Formula)
Christian Müller's avatar
Christian Müller committed
177 178
  }
  object ForallOtherThan {
Christian Müller's avatar
Christian Müller committed
179
    def make(l:List[Var], otherthan:List[Var], f:Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
180 181 182 183
      if (otherthan.isEmpty || l.isEmpty) { Forall.make(l, f) } else {
        ForallOtherThan(l, otherthan, f)
      }
    }
Christian Müller's avatar
Christian Müller committed
184
  }
185
  case class Exists(vars: List[Var], t: Formula) extends Quantifier {
Christian Müller's avatar
Christian Müller committed
186
    val qname = "∃"
Christian Müller's avatar
Christian Müller committed
187
    val make: (List[Var], Formula) => Formula = Quantifier.make(Exists.apply, _, _)
Christian Müller's avatar
Christian Müller committed
188
  }
Christian Müller's avatar
Christian Müller committed
189 190 191 192
//  object Exists {
//    def apply(v:Var, t:Formula) = Exists(List(v), t)
//    def apply(tup:(Var, Var), t:Formula) = Exists(List(tup._1, tup._2), t)
//  }
193
  case class Forall(vars: List[Var], t: Formula) extends Quantifier {
Christian Müller's avatar
Christian Müller committed
194
    val qname = "∀"
Christian Müller's avatar
Christian Müller committed
195
    val make: (List[Var], Formula) => Formula = Quantifier.make(Forall.apply, _, _)
Christian Müller's avatar
Christian Müller committed
196
  }
Christian Müller's avatar
Christian Müller committed
197 198 199 200
//  object Forall {
//    def apply(v:Var, t:Formula) = Forall(List(v), t)
//    def apply(tup:(Var, Var), t:Formula) = Forall(List(tup._1, tup._2), t)
//  }
Christian Müller's avatar
Christian Müller committed
201
  case class ForallOtherThan(vars: List[Var], otherthan: List[Var], t: Formula) extends Quantifier {
Christian Müller's avatar
Christian Müller committed
202
    val qname = "∀"
Christian Müller's avatar
Christian Müller committed
203
    val make = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula)
Christian Müller's avatar
Christian Müller committed
204 205
    override def toString: String = {
      s"$qname ${vars.map(_.withType).mkString(",")} ∉ {${otherthan.map(_.withType).mkString(",")}}. ${t.bracketed}"
Christian Müller's avatar
Christian Müller committed
206 207
    }
  }
Christian Müller's avatar
Christian Müller committed
208

209
  trait TemporalFormula extends Formula
Christian Müller's avatar
Christian Müller committed
210

211
  case class Next(t: Formula) extends TemporalFormula with UnOp {
Christian Müller's avatar
Christian Müller committed
212
    val make = Next.apply
Christian Müller's avatar
Christian Müller committed
213
    val opname = "X"
Christian Müller's avatar
Christian Müller committed
214
  }
215
  case class Globally(t: Formula) extends TemporalFormula with UnOp {
Christian Müller's avatar
Christian Müller committed
216
    val make = Globally.apply
Christian Müller's avatar
Christian Müller committed
217
    val opname = "G"
Christian Müller's avatar
Christian Müller committed
218
  }
Christian Müller's avatar
Christian Müller committed
219

220
  case class Finally(t: Formula) extends TemporalFormula with UnOp {
Christian Müller's avatar
Christian Müller committed
221
    val make = Finally.apply
Christian Müller's avatar
Christian Müller committed
222
    val opname = "F"
Christian Müller's avatar
Christian Müller committed
223
  }
224

225
  case class Until(t1: Formula, t2: Formula) extends TemporalFormula with BinOp {
Christian Müller's avatar
Christian Müller committed
226
    val make = Until.apply
Christian Müller's avatar
Christian Müller committed
227 228
    val opname = "U"
  }
Christian Müller's avatar
Christian Müller committed
229

Christian Müller's avatar
Christian Müller committed
230
  object WUntil {
Christian Müller's avatar
Christian Müller committed
231
    def apply(t1: Formula, t2: Formula) = Or(Until(t1, t2), Globally(t1))
Christian Müller's avatar
Christian Müller committed
232
  }
233

234 235
  trait UnOp extends Formula {
    def make: Formula => UnOp
Christian Müller's avatar
Christian Müller committed
236
    def opname: String
237
    def t: Formula
238

Christian Müller's avatar
Christian Müller committed
239
    override def toString: String = opname + " " + t.bracketed
Christian Müller's avatar
Christian Müller committed
240
  }
241

Christian Müller's avatar
Christian Müller committed
242
  object UnOp {
Christian Müller's avatar
Christian Müller committed
243
    def unapply(unop: UnOp): Some[(Formula => UnOp, Formula)] = {
Christian Müller's avatar
Christian Müller committed
244
      Some((unop.make, unop.t))
Christian Müller's avatar
Christian Müller committed
245 246 247
    }
  }

248 249
  trait BinOp extends Formula {
    def make: (Formula, Formula) => BinOp
Christian Müller's avatar
Christian Müller committed
250
    def opname: String
251 252
    def t1: Formula
    def t2: Formula
253

Christian Müller's avatar
Christian Müller committed
254
    override def toString:String = {
Christian Müller's avatar
Christian Müller committed
255
      (t1, t2) match {
Christian Müller's avatar
Christian Müller committed
256 257 258
        case (t1: BinOp, t2: BinOp) if opname == t1.opname && opname == t2.opname => t1 + " " + opname + " " + t2
        case (t1: BinOp, _) if opname == t1.opname => t1 + " " + opname + " " + t2.bracketed
        case (_, t2: BinOp) if opname == t2.opname => t1.bracketed + " " + opname + " " + t2
Christian Müller's avatar
Christian Müller committed
259
        case _ => t1.bracketed + " " + opname + " " + t2.bracketed
Christian Müller's avatar
Christian Müller committed
260 261 262
      }
    }
  }
263

Christian Müller's avatar
Christian Müller committed
264
  object BinOp {
Christian Müller's avatar
Christian Müller committed
265
    def unapply(binop: BinOp): Some[((Formula, Formula) => BinOp, Formula, Formula)] = {
Christian Müller's avatar
Christian Müller committed
266 267
      Some((binop.make, binop.t1, binop.t2))
    }
268

Christian Müller's avatar
Christian Müller committed
269
    // TODO: make tail-recursive list left hanging?
Christian Müller's avatar
Christian Müller committed
270 271 272 273 274 275 276 277 278 279
//    @tailrec
//    def makeL(make: (Formula, Formula) => Formula, l: Seq[Formula], Empty: Formula, acc:Formula): Formula = {
//        l.toList match {
//          case Empty :: xs => makeL(make, xs, Empty, acc)
//          case x :: xs => if (acc == Empty)
//            makeL(make, xs, Empty, x) else
//            makeL(make, xs, Empty, make(acc, x))
//          case List() => acc
//        }
//    }
280 281 282
      def makeL(make: (Formula, Formula) => Formula, l: Seq[Formula], Empty: Formula): Formula = {
          def inner(l:List[Formula]):Formula = {
            l match {
Christian Müller's avatar
Christian Müller committed
283
              case List(x) => x
284 285
              case Empty :: xs => inner(xs)
              case x :: xs => make(x, inner(xs))
Christian Müller's avatar
Christian Müller committed
286 287
              case List() => Empty
            }
288 289 290 291
          }
          // Filter unique
          inner(l.toList.distinct)
      }
Christian Müller's avatar
Christian Müller committed
292
  }
Christian Müller's avatar
Christian Müller committed
293

294
  object Or {
Christian Müller's avatar
Christian Müller committed
295
    def make(terms: List[Formula]): Formula = {
Christian Müller's avatar
Christian Müller committed
296
      BinOp.makeL(Or.apply, terms, False)
Christian Müller's avatar
Christian Müller committed
297
    }
Christian Müller's avatar
Christian Müller committed
298
    def make(terms: Formula*): Formula = {
Christian Müller's avatar
Christian Müller committed
299
      BinOp.makeL(Or.apply, terms, False)
300 301
    }
  }
Christian Müller's avatar
Christian Müller committed
302

303
  case class Or(t1: Formula, t2: Formula) extends BinOp {
Christian Müller's avatar
Christian Müller committed
304
    val opname = "∨"
Christian Müller's avatar
Christian Müller committed
305
    val make = Or.apply
Christian Müller's avatar
Christian Müller committed
306
  }
Christian Müller's avatar
Christian Müller committed
307

308
  object And {
Christian Müller's avatar
Christian Müller committed
309
    def make(terms: List[Formula]): Formula = {
Christian Müller's avatar
Christian Müller committed
310
      BinOp.makeL(And.apply, terms, True)
311
    }
Christian Müller's avatar
Christian Müller committed
312
    def make(terms: Formula*): Formula = {
Christian Müller's avatar
Christian Müller committed
313
      BinOp.makeL(And.apply, terms, True)
Christian Müller's avatar
Christian Müller committed
314
    }
315
  }
Christian Müller's avatar
Christian Müller committed
316

317
  case class And(t1: Formula, t2: Formula) extends BinOp {
Christian Müller's avatar
Christian Müller committed
318
    val opname = "∧"
Christian Müller's avatar
Christian Müller committed
319
    val make = And.apply
Christian Müller's avatar
Christian Müller committed
320
  }
Christian Müller's avatar
Christian Müller committed
321

Christian Müller's avatar
Christian Müller committed
322
  case class Equiv(t1: Formula, t2: Formula) extends BinOp {
Christian Müller's avatar
Christian Müller committed
323
    val opname = "↔"
Christian Müller's avatar
Christian Müller committed
324
    val make = Equiv.apply
Christian Müller's avatar
Christian Müller committed
325
  }
Christian Müller's avatar
Christian Müller committed
326
  object Equiv {
Christian Müller's avatar
Christian Müller committed
327
    def make(terms: List[Formula]): Formula = {
Christian Müller's avatar
Christian Müller committed
328
      BinOp.makeL(Equiv.apply, terms, True)
Christian Müller's avatar
Christian Müller committed
329
    }
Christian Müller's avatar
Christian Müller committed
330
    def make(terms: Formula*): Formula = {
Christian Müller's avatar
Christian Müller committed
331 332 333 334 335 336 337 338 339
      BinOp.makeL(Equiv.apply, terms, True)
    }
  }

  case class Equal(t1: Formula, t2: Formula) extends BinOp {
    val opname = "="
    val make = Equal.apply
  }
  object Equal {
Christian Müller's avatar
Christian Müller committed
340
    def make(terms: List[Formula]): Formula = {
Christian Müller's avatar
Christian Müller committed
341 342
      BinOp.makeL(Equal.apply, terms, True)
    }
Christian Müller's avatar
Christian Müller committed
343
    def make(terms: Formula*): Formula = {
Christian Müller's avatar
Christian Müller committed
344
      BinOp.makeL(Equal.apply, terms, True)
Christian Müller's avatar
Christian Müller committed
345 346 347
    }
  }

348
  case class Implies(t1: Formula, t2: Formula) extends BinOp {
Christian Müller's avatar
Christian Müller committed
349
    val opname = "→"
Christian Müller's avatar
Christian Müller committed
350
    val make = Implies.apply
Christian Müller's avatar
Christian Müller committed
351
  }
Christian Müller's avatar
Christian Müller committed
352
  object Implies {
Christian Müller's avatar
Christian Müller committed
353
    def make(terms: List[Formula]): Formula = {
Christian Müller's avatar
Christian Müller committed
354
      BinOp.makeL(Implies.apply, terms, True)
Christian Müller's avatar
Christian Müller committed
355
    }
Christian Müller's avatar
Christian Müller committed
356
    def make(terms: Formula*): Formula = {
Christian Müller's avatar
Christian Müller committed
357
      BinOp.makeL(Implies.apply, terms, True)
Christian Müller's avatar
Christian Müller committed
358 359
    }
  }
360
  case class Neg(t: Formula) extends UnOp {
Christian Müller's avatar
Christian Müller committed
361
    val make = Neg.apply
Christian Müller's avatar
Christian Müller committed
362 363 364 365
    val opname = "¬"
  }

}