Fixes/tidies of explicit LTL model checking (mostly from Joachim Klein): DRA products correctly include all initial states, and probabilities are ampped back correctly.

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

prism/src/explicit/DTMCModelChecker.java

@@ -28,7 +28,6 @@ package explicit;
 
 import java.io.File;
 import java.util.BitSet;
-import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 import java.util.Vector;
@@ -270,15 +269,11 @@ public class DTMCModelChecker extends ProbModelChecker
 		double[] probsProductDbl = probsProduct.getDoubleArray();
 		double[] probsDbl = new double[model.getNumStates()];
 
-		LinkedList<Integer> queue = new LinkedList<Integer>();
-		for (int s : model.getInitialStates())
-			queue.add(s);
-
-		for (int i = 0; i < invMap.length; i++) {
-			int j = invMap[i];
-			int s = j / draSize;
-			// TODO: check whether this is the right way to compute probabilities in the original model
-			probsDbl[s] = Math.max(probsDbl[s], probsProductDbl[i]);
+		// Get the probabilities for the original model by taking the initial states
+		// of the product and projecting back to the states of the original model
+		for (int i : modelProduct.getInitialStates()) {
+			int s = invMap[i] / draSize;
+			probsDbl[s] = probsProductDbl[i];
 		}
 
 		probs = StateValues.createFromDoubleArray(probsDbl, model);

prism/src/explicit/LTLModelChecker.java

@@ -130,8 +130,7 @@ public class LTLModelChecker extends PrismComponent
 	 * @param dra The DRA
 	 * @param dtmc The DTMC
 	 * @param labelBS BitSets giving the set of states for each AP in the DRA
-	 * @return a Pair consisting of the product DTMC and a map from 
-	 *   (s_i * draSize + q_j) to the right state in the DRA product 
+	 * @return The product DTMC and a list of each of its states (s,q), encoded as (s * draSize + q) 
 	 */
 	public Pair<Model, int[]> constructProductMC(DRA<BitSet> dra, DTMC dtmc, Vector<BitSet> labelBS) throws PrismException
 	{
@@ -153,14 +152,20 @@ public class LTLModelChecker extends PrismComponent
 		int map[] = new int[prodNumStates];
 		Arrays.fill(map, -1);
 
-		// Initial states
-		for (int s_0 : dtmc.getInitialStates()) {
-			// Get BitSet representing APs (labels) satisfied by initial state s_0
+		// As we need results for all states of the original model,
+		// we explore states of the product starting from those that
+		// correspond to *all* states of the original model.
+		// These are designated as initial states of the model
+		// (a) to ensure reachability is done for these states; and
+		// (b) to later identify the corresponding product state for each model state 
+		for (int s_0 = 0; s_0 < dtmc.getNumStates(); s_0++) {
+			// Get BitSet representing APs (labels) satisfied by state s_0
 			for (int k = 0; k < numAPs; k++) {
 				s_labels.set(k, labelBS.get(k).get(s_0));
 			}
 			// Find corresponding initial state in DRA
 			int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels);
+			// Add (initial) state to product
 			queue.add(new Point(s_0, q_0));
 			prodModel.addState();
 			prodModel.addInitialState(prodModel.getNumStates() - 1);
@@ -197,6 +202,7 @@ public class LTLModelChecker extends PrismComponent
 			}
 		}
 
+		// Build a mapping from state indices to states (s,q), encoded as (s * draSize + q) 
 		int invMap[] = new int[prodModel.getNumStates()];
 		for (int i = 0; i < map.length; i++) {
 			if (map[i] != -1) {
@@ -214,8 +220,7 @@ public class LTLModelChecker extends PrismComponent
 	 * @param dra The DRA
 	 * @param mdp The MDP
 	 * @param labelBS BitSets giving the set of states for each AP in the DRA
-	 * @return a Pair consisting of the product DTMC and a map from 
-	 *   (s_i * draSize + q_j) to the right state in the DRA product 
+	 * @return The product DTMC and a list of each of its states (s,q), encoded as (s * draSize + q) 
 	 */
 	public Pair<NondetModel, int[]> constructProductMDP(DRA<BitSet> dra, MDP mdp, Vector<BitSet> labelBS) throws PrismException
 	{
@@ -237,14 +242,20 @@ public class LTLModelChecker extends PrismComponent
 		int map[] = new int[prodNumStates];
 		Arrays.fill(map, -1);
 
-		// Initial states
-		for (int s_0 : mdp.getInitialStates()) {
-			// Get BitSet representing APs (labels) satisfied by initial state s_0
+		// As we need results for all states of the original model,
+		// we explore states of the product starting from those that
+		// correspond to *all* states of the original model.
+		// These are designated as initial states of the model
+		// (a) to ensure reachability is done for these states; and
+		// (b) to later identify the corresponding product state for each model state 
+		for (int s_0 = 0; s_0 < mdp.getNumStates(); s_0++) {
+			// Get BitSet representing APs (labels) satisfied by state s_0
 			for (int k = 0; k < numAPs; k++) {
 				s_labels.set(k, labelBS.get(k).get(s_0));
 			}
 			// Find corresponding initial state in DRA
 			int q_0 = dra.getEdgeDestByLabel(dra.getStartState(), s_labels);
+			// Add (initial) state to product
 			queue.add(new Point(s_0, q_0));
 			prodModel.addState();
 			prodModel.addInitialState(prodModel.getNumStates() - 1);
@@ -286,6 +297,7 @@ public class LTLModelChecker extends PrismComponent
 			}
 		}
 
+		// Build a mapping from state indices to states (s,q), encoded as (s * draSize + q) 
 		int invMap[] = new int[prodModel.getNumStates()];
 		for (int i = 0; i < map.length; i++) {
 			if (map[i] != -1) {

prism/src/explicit/MDPModelChecker.java

@@ -28,7 +28,6 @@ package explicit;
 
 import java.util.BitSet;
 import java.util.Iterator;
-import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 import java.util.Vector;
@@ -291,15 +290,11 @@ public class MDPModelChecker extends ProbModelChecker
 		double[] probsProductDbl = probsProduct.getDoubleArray();
 		double[] probsDbl = new double[model.getNumStates()];
 
-		LinkedList<Integer> queue = new LinkedList<Integer>();
-		for (int s : model.getInitialStates())
-			queue.add(s);
-
-		for (int i = 0; i < invMap.length; i++) {
-			int j = invMap[i];
-			int s = j / draSize;
-			// TODO: check whether this is the right way to compute probabilities in the original model
-			probsDbl[s] = Math.max(probsDbl[s], probsProductDbl[i]);
+		// Get the probabilities for the original model by taking the initial states
+		// of the product and projecting back to the states of the original model
+		for (int i : modelProduct.getInitialStates()) {
+			int s = invMap[i] / draSize;
+			probsDbl[s] = probsProductDbl[i];
 		}
 
 		probs = StateValues.createFromDoubleArray(probsDbl, model);