build approxElim

examples/nonomitting/conference-acceptance.spec

 Workflow
 
 forallmay x:A,p:P
-	True -> Conf += (x,p)
+	True → Conf += (x,p)
 forallmay x:A,p:P
-	!Conf(x,p) -> Assign += (x,p)
+	!Conf(x,p) → Assign += (x,p)
 forall x:A,p:P
-	(Assign(x,p) ∧ O(x,p)) -> Acc += (x,p)
+	(Assign(x,p) ∧ O(x,p)) → Acc += (x,p)
 loop {
-	forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
-	forallmay x:A,p:P (Assign(x,p) ∧ O(x,p)) -> Acc += (x,p)
+	forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Acc(xb,p)) → Read += (xa,xb,p)
+	forallmay x:A,p:P (Assign(x,p)) → Acc += (x,p)
 }
 
 Declassify

src/main/scala/de/tum/niwo/Utils.scala

@@ -43,18 +43,23 @@ object Utils extends LazyLogging {
     ((t1 - t0) / 1000000, result)
   }
 
-  def clear() {
-    def recclear(folder: File) {
-      for (fol <- folder.listFiles() if fol.isDirectory()) {
-        recclear(fol)
-      }
-
-      folder.listFiles().foreach(_.delete())
+  private def recclear(folder: File) {
+    for (fol <- folder.listFiles() if fol.isDirectory()) {
+      recclear(fol)
     }
+    folder.listFiles().foreach(_.delete())
+  }
+
+  def clear() {
     val fol = new File(RESULTSFOLDER)
     fol.mkdirs()
     recclear(fol)
   }
+  def clear(name:String) {
+    val fol = new File(RESULTSFOLDER, name)
+    fol.mkdirs()
+    recclear(fol)
+  }
   
   def write(dir: String, filename:String, prop: String) {
     val file = new File(s"$RESULTSFOLDER/$dir/$filename")
@@ -68,8 +73,21 @@ object Utils extends LazyLogging {
     logger.info(s"Written $file")
   }
 
+
+  def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
+    clear(name)
+    infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties)
+  }
+
+  def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
+    val spec = Examples.parseExampleWF(name).get
+    check(name, desc, inv, spec, properties)
+  }
+
   def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = {
 
+    clear(name)
+
     val basename = name.split("/").last
     val filenames = s"$basename${if (desc.isEmpty) "" else s"_$desc"}"
 
@@ -82,7 +100,7 @@ object Utils extends LazyLogging {
     check(name, desc, invspec, properties)
   }
   
-  def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
+  private def infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
     val model = if (properties.stubborn) "stubborn" else "causal"
 
     val basename = name.split("/").last
@@ -111,9 +129,9 @@ object Utils extends LazyLogging {
     val labels = (for ((node, inv) <- labelling.last) yield {
       s"Node ${node}:\n${inv.pretty}\n"
     }).mkString("\n")
-    
+
     Utils.write(name, s"$filenames.invariants", labels)
-    
+
     val wfsize = graph.edges.size - 1
     val invsizes = labelling.last.map(_._2.opsize)
     val maxsize = invsizes.max
@@ -134,9 +152,4 @@ object Utils extends LazyLogging {
     )
     res
   }
-  
-  def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
-    val spec = Examples.parseExampleWF(name).get
-    check(name, desc, inv, spec, properties)
-  }
 }
\ No newline at end of file

src/main/scala/de/tum/niwo/blocks/Saturator.scala

+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)
+  }
+
+}

src/main/scala/de/tum/niwo/blocks/TSConverter.scala

@@ -19,21 +19,21 @@ object TSConverter extends LazyLogging {
     val elaboratefun = (b:SimpleWFBlock[_]) => elaborate(b, spec, properties)
     val elaborated = everywhere(w.steps, elaboratefun)
 
-    // Map WFLoop/Nondet to TSLoop/TSNondet
-    // Map Add/Remove statements to SetStmt
-    val steps = elaborated.map(s => toTSBlock(s)(w.sig, properties))
-
-    // Add choice predicates to As
     // FIXME: Add causals to constants, add informedness for causal agents
     val newsig = if (!properties.stubborn) {
       w.sig.copy(
         preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
-        constants = spec.causals.toSet ++ w.sig.constants
+        constants = spec.causals.toSet ++ spec.constants ++ w.sig.constants
       )
     } else {
       w.sig
     }
 
+    // Map WFLoop/Nondet to TSLoop/TSNondet
+    // Map Add/Remove statements to SetStmt
+    val steps = elaborated.map(s => toTSBlock(s)(newsig, properties))
+
+
     val ts = TransitionSystem(newsig, steps)
 
     InvariantSpec(ts, spec.axioms, invgen(spec))
@@ -65,7 +65,7 @@ object TSConverter extends LazyLogging {
 
   def toSetStmt(s:Statement[_], sig:Signature, properties:InvProperties): SetStmt = {
 
-    val frees = s.guard.freeVars -- s.tuple.toSet -- sig.constants
+    val frees = (s.guard.freeVars -- s.tuple.toSet) -- sig.constants
 
     // Quantify free, non-const variables
     val guard = s match {
@@ -89,24 +89,25 @@ object TSConverter extends LazyLogging {
 
     val guardfix = if (!b.isoracly && b.pred.isDefined) {
       // is "normal" may block
+
       val choice = Fun(b.pred.get, b.agents)
+      val first = b.agents.head
 
-      val fixed = for (s <- b.steps) yield {
-        val first = s.tuple.head
-        val inner = if (first.typ == spec.target.params.head.typ) {
-          if (properties.stubborn) {
+      if (first.typ == spec.target.params.head.typ) {
+        for (s <- b.steps) yield {
+          val inner = if (properties.stubborn) {
             choice.in(T1)
           } else {
             val inf = Fun(INFNAME, List(b.agents.head))
             Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
           }
-        } else {
-          choice
+          val newguard = And(s.guard, inner)
+          s.update(guard = newguard)
         }
-        val newguard = And(s.guard, inner)
-        s.update(guard = newguard)
+      } else {
+        logger.warn(s"First agent of tuple in block: $b can not be informed - skipping introduction of choice predicate")
+        b.steps
       }
-      fixed
     } else {
       b.steps
     }

src/main/scala/de/tum/niwo/blocks/TransitionSystem.scala

@@ -6,6 +6,9 @@ import de.tum.niwo.foltl.Properties
 import de.tum.niwo.parser.ParserUtils
 
 case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var]) {
+
+  lazy val allpredicates: Set[Fun] = as ++ bs ++ constas ++ preds
+
   override def toString: String =
   {
     def mkString(set:Set[Fun]) = set.map(_.toTypedString).mkString(",")
@@ -124,19 +127,28 @@ trait NondetChoice[T <: NondetChoice[T, B], B <: Block] extends Block {
   }
 }
 
-sealed trait TSBlock extends Block
+sealed trait TSBlock extends Block {
+  // TODO: maybe move this to general blocks?
+  def mapStatements(f:SetStmt => SetStmt):TSBlock
+}
 
 case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock[SimpleTSBlock, SetStmt] with TSBlock {
   override def toString: String = steps.mkString("{", "\n  ", "}")
   def toTypedString: String = steps.map(_.toTypedString).mkString("{", "\n  ", "}")
   override def update(newsteps: List[SetStmt]): SimpleTSBlock = copy(newsteps)
+
+  override def mapStatements(f: SetStmt => SetStmt): TSBlock = update(steps.map(f))
 }
 
 case class TSLoop(steps:List[TSBlock]) extends Loop[TSLoop, TSBlock] with TSBlock {
   type B = TSBlock
   override def update(steps:List[TSBlock] = steps):TSLoop = copy(steps)
+
+  override def mapStatements(f: SetStmt => SetStmt): TSBlock = update(steps.map(_.mapStatements(f)))
 }
 case class TSNondetChoice(left:List[TSBlock], right:List[TSBlock]) extends NondetChoice[TSNondetChoice, TSBlock] with TSBlock {
   type B = TSBlock
   override def update(left:List[TSBlock] = left, right:List[TSBlock] = right):TSNondetChoice = copy(left, right)
+
+  override def mapStatements(f: SetStmt => SetStmt): B = update(left.map(_.mapStatements(f)), right.map(_.mapStatements(f)))
 }

src/main/scala/de/tum/niwo/blocks/Workflow.scala

@@ -27,12 +27,12 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axiom
     s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
   }
 
+  // FIXME: why is this not part of the sig?
   lazy val constants:Set[Var] = {
     // Treat free variables in the declassification as constants
     declass.values.flatMap {
       case (params, f) => f.freeVars -- params
     }.toSet
-    // TODO: How to check for more constants?
   }
 
   def isSane(): Boolean = {

src/main/scala/de/tum/niwo/foltl/FOLTL.scala

@@ -25,6 +25,7 @@ object FOLTL {
     def toPrenex: Formula = FormulaFunctions.toPrenex(this)
     def toNegNf: Formula = FormulaFunctions.toNegNf(this)
     def toCNF: Formula = FormulaFunctions.toCNF(this)
+    def toDNF: Formula = FormulaFunctions.toDNF(this)
 
     lazy val isBS: Boolean = FormulaFunctions.isBS(this)
     lazy val isUniversal: Boolean = FormulaFunctions.isU(this)

src/main/scala/de/tum/niwo/foltl/FOTransformers.scala

@@ -46,7 +46,7 @@ object FOTransformers extends LazyLogging {
     }
   }
   
-  def eliminateDoubleQuantifiers(f:Formula) = {
+  def eliminateDoubleQuantifiers(f:Formula): Formula = {
     def elimSub(f:Formula, bound:Set[Var]):Formula = {
       f everywhere {
         // filter out all that are contained in bound
@@ -56,7 +56,7 @@ object FOTransformers extends LazyLogging {
     elimSub(f.toNegNf, Set())
   }
   
-  def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties) = {
+  def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties): Formula = {
     logger.debug(s"Eliminating universal second order predicate $AUX")
 
     val cnf = if (!props.approxElim) f.toCNF else f.toNegNf
@@ -68,7 +68,7 @@ object FOTransformers extends LazyLogging {
     repld.simplify
   }
 
-  def eliminateBPredicate(f:Formula, B:Fun) = {
+  def eliminateBPredicate(f:Formula, B:Fun): (Formula, Formula) = {
     val NAME = B.name
 
     // SOQE: \exists B. f <-> f'
@@ -84,6 +84,9 @@ object FOTransformers extends LazyLogging {
     val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
 
     // Group clauses by positive/negative occurences
+    val getPositiveBArguments = FormulaFunctions.getPositiveArguments(_, NAME)
+    val getNegativeBArguments = FormulaFunctions.getNegativeArguments(_, NAME)
+
     def ispositive(clause: List[Formula]) =
       getPositiveBArguments(clause).nonEmpty
 
@@ -97,29 +100,6 @@ object FOTransformers extends LazyLogging {
         case _ => false
       }
     }
-    def getPositiveBArguments(clause: List[Formula]):Set[List[Var]] = {
-      clause flatMap {
-        case Fun(NAME, _, vars) => List(vars)
-        case _ => List()
-      } toSet
-    }
-    def getNegativeBArguments(clause: List[Formula]):Set[List[Var]] = {
-      clause flatMap {
-        case Neg(Fun(NAME, _, vars))=> List(vars)
-        case _ => List()
-      } toSet
-    }
-
-    def ineq(l1:List[Var], l2:List[Var]) = {
-      if (l1.size != l2.size) {
-        logger.warn("Trying to generate inequalities for different sized vectors")
-      }
-      val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
-        case (x, y) if x.name <= y.name => Neg(Equal(x,y))
-        case (x, y)  => Neg(Equal(y,x))
-      }.toSet
-      Or.make(ineqs.toList)
-    }
 
     val E = clauses.filter(c => !ispositive(c) && !isnegative(c))
     val F = clauses.filter(c => ispositive(c) && !isnegative(c))
@@ -146,7 +126,7 @@ object FOTransformers extends LazyLogging {
     val hls = H.map(c => Or.make(pruneBs(c)))
 
     val FGineq = for ((fi, fargs) <- fis.zip(Fargs); (gk, gargs) <- gks.zip(Gargs); farg <- gargs; garg <- gargs) yield {
-      Or.make(fi, gk, ineq(farg, garg))
+      Or.make(fi, gk, FormulaFunctions.ineq(farg, garg))
     }
     val fFGineq = And.make(FGineq)
     val simpfFGineq = Z3BSFO.simplifyBS(fFGineq)  // FIXME: is this correct? there are no quantifiers binding stuff
@@ -186,7 +166,7 @@ object FOTransformers extends LazyLogging {
    * Gobble up all outermost existential quantifiers
    * Needs to have non-conflicting bindings
    */
-  def eliminateExistentials(t:Formula) = {
+  def eliminateExistentials(t:Formula): (List[Var], Formula) = {
     
     def coll:PartialFunction[Formula, List[Var]] = {
       case Exists(a, term) => a ++ term.collect(coll)
@@ -260,7 +240,7 @@ object FOTransformers extends LazyLogging {
   /**
    * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
    */
-  def eliminatePredicates(t: Formula) = {
+  def eliminatePredicates(t: Formula): Formula = {
     t.everywhere({
       case f:Fun => f.encodeToVar()
     })
@@ -270,7 +250,7 @@ object FOTransformers extends LazyLogging {
    * Instantiates universals in EA formulae.
    * Resulting formula is in E* with all existentials outermost and in NegNF
    */
-  def instantiateUniversals(f:Formula) = {
+  def instantiateUniversals(f:Formula): Formula = {
 
     // Check fragment
     if (!f.isBS) {
@@ -290,7 +270,7 @@ object FOTransformers extends LazyLogging {
    * Instantiates existentials in AE formulae.
    * Resulting formula is in NegNF
    */
-  def abstractExistentials(f:Formula) = {
+  def abstractExistentials(f:Formula): Formula = {
     val neg = Neg(f).toNegNf.simplify
     
     // Check fragment

src/main/scala/de/tum/niwo/foltl/FormulaFunctions.scala

@@ -2,6 +2,7 @@ package de.tum.niwo.foltl
 
 import FOLTL._
 import com.typesafe.scalalogging.LazyLogging
+import de.tum.niwo.foltl.FOTransformers.logger
 
 import scala.annotation.tailrec
 
@@ -545,7 +546,6 @@ object FormulaFunctions extends LazyLogging {
   def toPrenex(f: Formula): Formula = {
     val negnf = f.toNegNf.simplify
 
-    // TODO: test fix bindings
     val simp = fixBinding(negnf)
 //    val simp = negnf
 
@@ -588,37 +588,37 @@ object FormulaFunctions extends LazyLogging {
 //    } else {
 //      logger.warn("Using internal CNF conversion - may blow up")
 
-      // FIXME: can we do it without prenex? may be expensive later on
-      val normalized = f.toPrenex.simplify
-      logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
+    // FIXME: can we do it without prenex? may be expensive later on
+    val normalized = f.toPrenex.simplify
+    logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
 
-      val quantifiers = FormulaFunctions.collectQuantifiers(normalized)
+    val quantifiers = FormulaFunctions.collectQuantifiers(normalized)
 
-      // normalized is now Quantifiers, then only And/Or with Negation inside
-      // no simplification here
-      val cnf1 = toCNFSub(normalized)
+    // normalized is now Quantifiers, then only And/Or with Negation inside
+    // no simplification here
+    val cnf1 = toCNFSub(normalized)
 
-      // Inspect clauses
-      val clauses = FOTransformers.collectClauses(cnf1)
+    // Inspect clauses
+    val clauses = FOTransformers.collectClauses(cnf1)
 
-      // Simplify clauses
-      // TODO: improve, don't sort by tostring
-      val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())
+    // Simplify clauses
+    // TODO: improve, don't sort by tostring
+    val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())
 
-      // Remove trivial clauses
-      val notrivials = sorted.filterNot(c => {
-        c.exists(f => c.contains(Neg(f)))
-      })
+    // Remove trivial clauses
+    val notrivials = sorted.filterNot(c => {
+      c.exists(f => c.contains(Neg(f)))
+    })
 
-      // TODO improve runtime
-      val simped = notrivials.filterNot(c => notrivials.exists(c2 => {
-        // check if c is superset of c2
-        //      c != c2 && c.startsWith(c2)
-        c != c2 && c.forall(f => c2.contains(f))
-      }))
+    // TODO improve runtime
+    val simped = notrivials.filterNot(c => notrivials.exists(c2 => {
+      // check if c is superset of c2
+      //      c != c2 && c.startsWith(c2)
+      c != c2 && c.forall(f => c2.contains(f))
+    }))
 //      logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")
-      logger.debug(s"Resulting CNF has ${sorted.size} clauses")
-      (quantifiers, simped)
+    logger.debug(s"Resulting CNF has ${sorted.size} clauses")
+    (quantifiers, simped)
 //    }
   }
 
@@ -629,6 +629,26 @@ object FormulaFunctions extends LazyLogging {
       newform
   }
 
+  def toDNFClauses(f:Formula):(List[(Boolean, List[Var])], List[List[Formula]]) = {
+    val simp = f.toPrenex.simplify
+    val quantifiers = collectQuantifiers(simp)
+    val stripped = stripQuantifiers(simp)
+
+    val (_, cnfclauses) = toCNFClauses(Neg(stripped))
+
+    // Negate all single valued
+    val dnfclauses = cnfclauses.map(_.map(Neg(_).simplify))
+
+    (quantifiers, dnfclauses)
+  }
+
+  def toDNF(f: Formula): Formula = {
+    val (quantifiers, clauses) = toDNFClauses(f)
+    val form = Or.make(clauses.map(And.make))
+    val newform = rewrapQuantifiers(quantifiers, form)
+    newform
+  }
+
   /**
    * Resolves a universally quantified predicate
    * Blows up the formula exponentially due to CNF
@@ -670,4 +690,37 @@ object FormulaFunctions extends LazyLogging {
     removed.simplify
 
   }
+
+  def getPositiveArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
+    clause flatMap {
+      case Fun(NAME, _, vars) => List(vars)
+      case _ => List()
+    } toSet
+  }
+  def getNegativeArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
+    clause flatMap {
+      case Neg(Fun(NAME, _, vars))=> List(vars)
+      case _ => List()
+    } toSet
+  }
+  def ineq(l1:List[Var], l2:List[Var]): Formula = {
+    if (l1.size != l2.size) {
+      logger.warn("Trying to generate inequalities for different sized vectors")
+    }
+    val ineqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
+      case (x, y) if x.name <= y.name => Neg(Equal(x,y))
+      case (x, y)  => Neg(Equal(y,x))
+    }.toSet
+    Or.make(ineqs.toList)
+  }
+  def eq(l1:List[Var], l2:List[Var]):Formula = {
+    if (l1.size != l2.size) {
+      logger.warn("Trying to generate equalities for different sized vectors")
+    }
+    val eqs = l1.zip(l2).filterNot(x => x._1 == x._2).map {
+      case (x, y) if x.name <= y.name => Equal(x,y)
+      case (x, y)  => Equal(y,x)
+    }.toSet
+    And.make(eqs.toList)
+  }
 }
\ No newline at end of file

src/main/scala/de/tum/niwo/graphs/TSGraphEncoding.scala

@@ -40,7 +40,7 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging {
     val sourcenode = g.get(sourceid)
     val nodes = sourcenode.withKind(BreadthFirst).filterNot(_ == sourcenode)
 
-    // this could 1. be more functional, 2. not just give up for loops
+    // TODO: this could 1. be more functional, 2. not just give up for loops
     var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())
 
     // initially all untouched
@@ -64,32 +64,37 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging {
     */
   def divergedMap(g:TSGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Boolean] = {
 
-    val sourceid = 0
-    val sourcenode = g.get(sourceid)
-    val nodes = sourcenode.withKind(BreadthFirst).filterNot(_ == sourcenode)
+    val anames = sig.as.map(_.name)
 
-    // this could 1. be more functional, 2. not just give up for loops
-    var map:Map[g.NodeT, Boolean] = Map().withDefault(_ => true)
+    // Node diverges locally if it has an incoming edge that touches an A that might differ
+    def divergeslocally(node:g.NodeT) = {
+      node.incoming.exists(stmt =>
+        stmt.steps.exists(_.guard.hasSubFormula{
+          // FIXME: this would be the TS correct version
+          // case Fun(name, None, _) if anames.contains(name) => true
 
-    // initially not diverged
-    map = map.updated(g.get(sourceid), false)
+          // This is the WF correct version
+          case f:Fun if f.isOracle => true
+        }))
+    }
 
-    for (elem <- nodes) {
-      // If all predecessors are known
-      if (elem.diPredecessors.forall(map.contains(_))) {
-        // disjunction over all incoming edges
-        // if an incoming edge is diverged, this is also
-        val divergedPredecessor = elem.diPredecessors.exists(map(_))
-        // if the guard contains an A, also diverging
-        val anames = sig.as.map(_.name)
-        val touchedOracle = elem.incoming.exists(stmt =>
-          stmt.steps.exists(_.guard.hasSubFormula{
-            case Fun(name, _, _) if anames.contains(name) => true
-          })
-        )
-        map = map.updated(elem, divergedPredecessor || touchedOracle)
-      }
+
+    // find all nodes where divergence could happen locally
+    val divergenodes = (for (node <- g.nodes
+                            if divergeslocally(node)) yield {
+      node
+    }).toSet
+
+    // diverge all nodes that can be reached from a local divergence
+    // This is O(n^2), could be improved
+    val reachablenodes = for (
+      node <- divergenodes;
+      reachnode <- node.withKind(BreadthFirst)
+    ) yield {
+      reachnode
     }
-    map
+
+    val map = (for (node <- reachablenodes) yield node -> true).toMap
+    map.withDefault(_ => false)
   }
 }

src/main/scala/de/tum/niwo/invariants/InvariantChecker.scala

@@ -43,7 +43,13 @@ object InvariantChecker extends LazyLogging {
   }
 
   def checkInvariantFPLabelling(spec: InvariantSpec, properties:InvProperties) = {
-    val graph = TSGraphEncoding.toGraph(spec.ts)
+
+    // if approximating A-elim, saturate theta with equalities
+    val ts = if (properties.approxElim) {
+      Saturator.saturate(spec.ts)
+    } else { spec.ts }
+
+    val graph = TSGraphEncoding.toGraph(ts)
     type Node = graph.NodeT
     type Edge = graph.EdgeT
 
@@ -142,7 +148,7 @@ object InvariantChecker extends LazyLogging {
     val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
     
     val dot1 = labellings.zip(proven).reverse
-    val dot2 = dot1.map(tup => WFGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
+    val dot2 = dot1.map(tup => TSGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
       t._2.pretty
     })), tup._2))
 

src/main/scala/de/tum/niwo/invariants/Preconditions.scala

@@ -122,7 +122,7 @@ object Preconditions extends LazyLogging {
         oless.hasSubFormula { case Fun(b.name, _, _) => true }
       )
 
-      if (occuringBs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
+      if (occuringBs.nonEmpty && diverged) {
         logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
       }
 

src/main/scala/de/tum/niwo/parser/ParserUtils.scala

@@ -62,7 +62,7 @@ object ParserUtils extends LazyLogging {
   def buildSig(preds: List[Fun]) = {
     // Filter to just the first
     val filtered = preds.groupBy(_.name).map(_._2.head).toSet
-    val oracles = filtered.filter(_.isOracle)
+    val oracles = filtered.filter(_.isOracle) ++ filtered.filter(_.isAux)
     val constinputs = filtered.filter(_.isConstInput)
     val bs = filtered.filter(_.isB)
     val rels = filtered -- oracles -- constinputs -- bs

src/main/scala/de/tum/niwo/parser/WorkflowParser.scala

@@ -9,25 +9,29 @@ import scala.util.parsing.combinator._
 
 object WorkflowParser extends RegexParsers with PackratParsers with FormulaParser with LazyLogging {
   
-  private def addChoicePredicates(blocks: List[WFBlock]): List[WFBlock] = {
+  private def addChoicePredicates(blocks: List[WFBlock]): (List[WFBlock], Set[Fun]) = {
     var i = -1; // start at 0
     def next() = {
       i = i + 1
       i
     }
+    var list:List[Fun] = Nil
 
     def addChoice(blocks: List[WFBlock], next:() => Int):List[WFBlock] = {
       blocks match {
         case ForallMayWFBlock(v, _, stmts) :: xs =>