FOLTLTermFunctions.scala 4.28 KB
Newer Older
 Christian Müller committed Mar 14, 2017 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 `````` Christian Müller committed Mar 27, 2017 45 `````` case Neg(Neg(t)) => t `````` Christian Müller committed Mar 14, 2017 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 `````` Christian Müller committed Mar 27, 2017 55 56 `````` // Equivalence case Eq(t1, t2) if t1 == t2 => True `````` Christian Müller committed Mar 14, 2017 57 `````` `````` Christian Müller committed Mar 27, 2017 58 59 60 61 `````` // Double Temporals case Finally(Finally(t)) => Finally(t) case Globally(Globally(t)) => Globally(t) `````` Christian Müller committed Mar 14, 2017 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) }) } }``````