FOLTLTermFunctions.scala 4.25 KB
 Christian Müller committed Mar 14, 2017 1 2 3 4 5 6 7 8 9 10 11 12 ``````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) `````` Christian Müller committed Mar 31, 2017 13 `````` case UnOp(make, t) => free(t, bound) `````` Christian Müller committed Mar 14, 2017 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 `````` // And, Or, Eq, Implies case BinOp(_, t1, t2) => free(t1, bound) ++ free(t2, 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 `````` Christian Müller committed Mar 27, 2017 41 `````` case Neg(Neg(t)) => t `````` Christian Müller committed Mar 14, 2017 42 43 44 45 46 47 48 49 50 `````` 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 `````` Christian Müller committed Mar 27, 2017 51 52 `````` // Equivalence case Eq(t1, t2) if t1 == t2 => True `````` Christian Müller committed Mar 14, 2017 53 `````` `````` Christian Müller committed Mar 27, 2017 54 55 56 57 `````` // Double Temporals case Finally(Finally(t)) => Finally(t) case Globally(Globally(t)) => Globally(t) `````` Christian Müller committed Mar 14, 2017 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 `````` // 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)) `````` Christian Müller committed Mar 31, 2017 86 `````` case UnOp(make, t1) => make(everywhere(trans, t1)) `````` Christian Müller committed Mar 14, 2017 87 88 89 90 91 `````` case BinOp(make, t1, t2) => make(everywhere(trans, t1), everywhere(trans, t2)) case x => x } } `````` Christian Müller committed Mar 31, 2017 92 93 94 95 96 97 98 99 100 101 102 103 104 `````` def collect[T](combine:(T,T) => T, empty:() =>T)(coll: PartialFunction[Term, T], t: Term): T = { if (coll.isDefinedAt(t)) coll(t) else t match { // Extractors case Quantifier(make, ps, t) => collect(combine, empty)(coll, t) case UnOp(make, t) => collect(combine, empty)(coll, t) case BinOp(make, t1, t2) => combine(collect(combine, empty)(coll, t1), collect(combine, empty)(coll, t2)) case x => empty() } } `````` Christian Müller committed Mar 14, 2017 105 106 107 108 109 110 111 112 113 114 115 116 `````` 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) }) } }``````