Saturator.scala 1.83 KB
Newer Older
 Christian Müller committed Mar 22, 2019 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 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 ``````package de.tum.niwo.blocks import de.tum.niwo.foltl.FOLTL.{And, Formula, Or} import de.tum.niwo.foltl.FormulaFunctions object Saturator { def saturate(ts:TransitionSystem): TransitionSystem = { val allpredicates = ts.sig.allpredicates def saturateGuard(f:Formula) = { val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f) // part 1: Add equalities in CNF // FIXME: this may add too many eqs, since annotations T1, T2 are ignored val witheqs = for (c <- clauses) yield { val ineqs = for (pred <- allpredicates; pos <- FormulaFunctions.getPositiveArguments(c, pred.name); neg <- FormulaFunctions.getNegativeArguments(c, pred.name) ) yield { FormulaFunctions.eq(pos, neg) } c ++ ineqs } // do not rewrap quantifiers here val cnfwitheqs = And.make(witheqs.map(Or.make)) // part 2: Add inequalities in DNF val (_, dnfclauses) = FormulaFunctions.toDNFClauses(cnfwitheqs) val withineqs = for (c <- dnfclauses) yield { val ineqs = for (pred <- allpredicates; pos <- FormulaFunctions.getPositiveArguments(c, pred.name); neg <- FormulaFunctions.getNegativeArguments(c, pred.name) ) yield { FormulaFunctions.ineq(pos, neg) } c ++ ineqs } val dnfwithineqs = Or.make(withineqs.map(And.make)) // val theta = dnfwithineqs.toCNF // FIXME this should use theta if equalities would actually be introduced val newform = FormulaFunctions.rewrapQuantifiers(quantifiers, cnfwitheqs).simplify newform } val newsteps = ts.steps.map(_.mapStatements{ case SetStmt(guard, fun, tuple) => SetStmt(saturateGuard(guard), fun, tuple) }) ts.copy(steps = newsteps) } }``````