prism.StateModelChecker: add handleMaximalStateFormulas

This method provides a variant of the recursive computation
of maximal state subformulas during LTL model checking.
Here, the satisfaction sets of maximal state subformulas
are directly attached using fresh labels to the model,
and the formula is transformed appropriately.


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

prism/src/prism/StateModelChecker.java

@@ -28,9 +28,11 @@ package prism;
 
 import java.io.File;
 import java.io.FileNotFoundException;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Set;
 import java.util.TreeSet;
+import java.util.Vector;
 
 import mtbdd.PrismMTBDD;
 import dv.DoubleVector;
@@ -40,6 +42,7 @@ import parser.*;
 import parser.ast.*;
 import parser.ast.ExpressionFilter.FilterOperator;
 import parser.type.*;
+import parser.visitor.ReplaceLabels;
 
 // Base class for model checkers - does state-based evaluations (no temporal/probabilistic)
 
@@ -1455,6 +1458,47 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return resVals;
 	}
 
+	/**
+	 * Method for handling the recursive part of PCTL* checking, i.e.,
+	 * recursively checking maximal state subformulas and replacing them
+	 * with labels and the corresponding satisfaction sets.
+	 * <br>
+	 * Extracts maximal state formula from an LTL path formula,
+	 * model checks them (with the current model checker and the current model)
+	 * and replaces them with ExpressionLabel objects that correspond
+	 * to freshly generated labels attached to the model.
+	 * <br>
+	 * Returns the modified Expression.
+	 *
+	 * @param expr the expression (a path formula)
+	 */
+	public Expression handleMaximalStateFormulas(Expression expr) throws PrismException
+	{
+		Vector<JDDNode> labelDD = new Vector<JDDNode>();
+
+		// construct LTL model checker, using this model checker instance
+		// (which is specialised for the model type) for the recursive
+		// model checking computation
+		LTLModelChecker ltlMC = new LTLModelChecker(this);
+
+		// check the maximal state subformulas and gather
+		// the satisfaction sets in labelBS, with index i
+		// in the vector corresponding to label Li in the
+		// returned formula
+		Expression exprNew = ltlMC.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDD);
+
+		HashMap<String, String> labelReplacements = new HashMap<String, String>();
+		for (int i=0; i < labelDD.size(); i++) {
+			String currentLabel = "L"+i;
+			// Attach satisfaction set for Li to the model, record necessary
+			// label renaming
+			String newLabel = model.addUniqueLabelDD("phi", labelDD.get(i), getDefinedLabelNames());
+			labelReplacements.put(currentLabel, newLabel);
+		}
+		// rename the labels
+		return (Expression) exprNew.accept(new ReplaceLabels(labelReplacements));
+	}
+
 	// Utility functions for symbolic model checkers 
 	
 	/**