Small optimisation in LTL model checking: reduce number of propositions used in deterministic automaton by checking for negations.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10002 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/LTLModelChecker.java

@@ -37,6 +37,8 @@ import java.util.List;
 import java.util.Map;
 import java.util.Vector;
 
+import jdd.JDD;
+import jdd.JDDNode;
 import parser.State;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
@@ -134,9 +136,9 @@ public class LTLModelChecker extends PrismComponent
 	/**
 	 * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
 	 * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result
-	 * is also returned. As an optimisation, model checking that results in true/false for all states is converted to an
-	 * actual true/false, and duplicate results are given the same label. BitSets giving the states which satisfy each label
-	 * are put into the vector {@code labelBS}, which should be empty when this function is called.
+	 * is also returned. As an optimisation, expressions that results in true/false for all states are converted to an
+	 * actual true/false, and duplicate results (or their negations) reuse the same label. BitSets giving the states which
+	 * satisfy each label are put into the vector labelDDs, which should be empty when this function is called.
 	 */
 	public Expression checkMaximalStateFormulas(ProbModelChecker mc, Model model, Expression expr, Vector<BitSet> labelBS) throws PrismException
 	{
@@ -159,6 +161,16 @@ public class LTLModelChecker extends PrismComponent
 				sv.clear();
 				return new ExpressionLabel("L" + i);
 			}
+			// Also, see if we already have the negation of this result
+			// (in which case, reuse it)
+			BitSet bsNeg = new BitSet(model.getNumStates());
+			bsNeg.set(0, model.getNumStates());
+			bsNeg.andNot(bs);
+			i = labelBS.indexOf(bsNeg);
+			if (i != -1) {
+				sv.clear();
+				return Expression.Not(new ExpressionLabel("L" + i));
+			}
 			// Otherwise, add result to list, return new label
 			labelBS.add(bs);
 			return new ExpressionLabel("L" + (labelBS.size() - 1));

prism/src/prism/LTLModelChecker.java

@@ -89,9 +89,9 @@ public class LTLModelChecker extends PrismComponent
 	/**
 	 * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
 	 * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result
-	 * is also returned. As an optimisation, model checking that results in true/false for all states is converted to an
-	 * actual true/false, and duplicate results are given the same label. BDDs giving the states which satisfy each label
-	 * are put into the vector  labelDDs, which should be empty when this function is called.
+	 * is also returned. As an optimisation, expressions that results in true/false for all states are converted to an
+	 * actual true/false, and duplicate results (or their negations) reuse the same label. BDDs giving the states which
+	 * satisfy each label are put into the vector labelDDs, which should be empty when this function is called.
 	 */
 	public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs) throws PrismException
 	{
@@ -115,6 +115,17 @@ public class LTLModelChecker extends PrismComponent
 				JDD.Deref(dd);
 				return new ExpressionLabel("L" + i);
 			}
+			// Also, see if we already have the negation of this result
+			// (in which case, reuse it)
+			JDD.Ref(dd);
+			JDD.Ref(model.getReach());
+			JDDNode ddNeg = JDD.And(JDD.Not(dd), model.getReach());
+			i = labelDDs.indexOf(ddNeg);
+			JDD.Deref(ddNeg);
+			if (i != -1) {
+				JDD.Deref(dd);
+				return Expression.Not(new ExpressionLabel("L" + i));
+			}
 			// Otherwise, add result to list, return new label
 			labelDDs.add(dd);
 			return new ExpressionLabel("L" + (labelDDs.size() - 1));