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

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

8
object Saturator extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
9 10 11 12 13 14 15 16 17 18 19 20 21

  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;
Christian Müller's avatar
Christian Müller committed
22 23 24
                         trace <- List(None, Some(Properties.T1), Some(Properties.T2));
                         pos <- FormulaFunctions.getPositiveArguments(c, pred.name, trace);
                         neg <- FormulaFunctions.getNegativeArguments(c, pred.name, trace)
Christian Müller's avatar
Christian Müller committed
25 26 27 28 29 30
        ) yield {
          FormulaFunctions.eq(pos, neg)
        }
        c ++ ineqs
      }

31
      if (witheqs != clauses) {
Christian Müller's avatar
Christian Müller committed
32
        logger.info(s"Saturation introduces equalities for guard $f")
33 34
      }

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
      val dnfwithineqs = Z3BSFO.simplifyBS(Or.make(withineqs.map(And.make)))
      //      val theta = dnfwithineqs.toCNF

      val result = if (dnfclauses != withineqs) {
Christian Müller's avatar
Christian Müller committed
54
        logger.info(s"Saturation introduces inequalities for guard $f")
55 56 57 58
        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)
  }

}