From 67f34d1de29f8bccc842d4506a24b15896ff8613 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 19 Jul 2017 12:29:17 +0000
Subject: [PATCH] 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 | 44 ++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 2374c6e7..71ccc8ed 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/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 
 	
 	/**