Saturator.scala 1.83 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 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)
  }

}