Saturator.scala 2.17 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
package de.tum.niwo.blocks

3 4 5
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
6
import de.tum.niwo.foltl.FormulaFunctions
7
import de.tum.niwo.toz3.Z3BSFO
Christian Müller's avatar
Christian Müller committed
8

9
object Saturator extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

  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
      }

31 32 33 34
      if (witheqs != clauses) {
        logger.info(s"Saturation introduced equalities in CNF for guard $f")
      }

Christian Müller's avatar
Christian Müller committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
      // 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
      }
50 51 52 53 54 55 56 57 58
      val dnfwithineqs = Z3BSFO.simplifyBS(Or.make(withineqs.map(And.make)))
      //      val theta = dnfwithineqs.toCNF

      val result = if (dnfclauses != withineqs) {
        logger.warn(s"Saturation introduces inequalities for guard $f")
        dnfwithineqs.toCNF
      } else {
        cnfwitheqs
      }
Christian Müller's avatar
Christian Müller committed
59

60
      val newform = FormulaFunctions.rewrapQuantifiers(quantifiers, result).simplify
Christian Müller's avatar
Christian Müller committed
61 62 63 64 65 66 67 68 69 70 71 72

      newform
    }

    val newsteps = ts.steps.map(_.mapStatements{
      case SetStmt(guard, fun, tuple) => SetStmt(saturateGuard(guard), fun, tuple)
    })

    ts.copy(steps = newsteps)
  }

}