Refactoring in explicit EC computation (but MDP model checking stil not working).

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

prism/src/explicit/ECComputer.java

@@ -61,6 +61,13 @@ public abstract class ECComputer extends PrismComponent
 	 */
 	public abstract void computeMECStates() throws PrismException;
 
+	/**
+	 * Compute states of all maximal end components (MECs) contained within {@code states}, and store them.
+	 * They can be retrieved using {@link #getMECStates()}.
+	 * @param states BitSet for the set of containing states
+	 */
+	public abstract void computeMECStates(BitSet states) throws PrismException;
+
 	/**
 	 * Get the list of states for computed MECs.
 	 */

prism/src/explicit/ECComputerDefault.java

@@ -39,8 +39,8 @@ import prism.PrismComponent;
 import prism.PrismException;
 
 /**
- * EXplicit maximal end component computer for a nondeterministic model such as MDP.
- * Implements the algorithm from:
+ * Explicit maximal end component computer for a nondeterministic model such as an MDP.
+ * Implements the algorithm from p.48 of:
  * Luca de Alfaro. Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)
  */
 public class ECComputerDefault extends ECComputer
@@ -65,33 +65,53 @@ public class ECComputerDefault extends ECComputer
 	@Override
 	public void computeMECStates() throws PrismException
 	{
-		SubNondetModel submodel = null;
-		List<BitSet> L = new ArrayList<BitSet>();
+		// Look within set of all reachable states
+		BitSet reach = new BitSet();
+		reach.set(0, model.getNumStates());
+		computeMECStates(reach);
+	}
+
+	@Override
+	public void computeMECStates(BitSet states) throws PrismException
+	{
+		mecs = findEndComponents(states, null); //TODO
+	}
+
+	@Override
+	public List<BitSet> getMECStates()
+	{
+		return mecs;
+	}
+
+	// Computation
 
-		BitSet initialModel = new BitSet();
-		initialModel.set(0, model.getNumStates());
-		L.add(initialModel);
+	/**
+	 * Find all accepting maximal end components (MECs) contained within {@code states},
+	 * where acceptance is defined as those which intersect with {@code filter}.
+	 * (If {@code filter} is null, the acceptance condition is trivially satisfied.)
+	 * @param states BitSet for the set of containing states
+	 * @param filter BitSet for the set of accepting states
+	 * @return a list of BitSets representing the MECs
+	 */
+	private List<BitSet> findEndComponents(BitSet states, BitSet filter) throws PrismException
+	{
+		// Initialise L with set of all states to look in
+		List<BitSet> L = new ArrayList<BitSet>();
+		L.add(states);
 
 		boolean changed = true;
 		while (changed) {
 			changed = false;
 			BitSet E = L.remove(0);
-			submodel = restrict(model, E);
+			SubNondetModel submodel = restrict(model, E);
 			List<BitSet> sccs = translateStates(submodel, computeSCCs(submodel));
 			L = replaceEWithSCCs(L, E, sccs);
 			changed = canLBeChanged(L, E);
 		}
-		mecs = L;
-	}
 
-	@Override
-	public List<BitSet> getMECStates()
-	{
-		return mecs;
+		return L;
 	}
 
-	// Computation
-
 	private Set<BitSet> processedSCCs = new HashSet<BitSet>();
 
 	private boolean canLBeChanged(List<BitSet> L, BitSet E)

prism/src/explicit/LTLModelChecker.java

@@ -357,17 +357,17 @@ public class LTLModelChecker extends PrismComponent
 
 		for (BitSet mec : mecs) {
 			boolean isLEmpty = true;
-			boolean isKEmpty = true;
-			for (int acceptancePair = 0; acceptancePair < numAcceptancePairs && isLEmpty && isKEmpty; acceptancePair++) {
+			boolean isKNonEmpty = false;
+			for (int acceptancePair = 0; acceptancePair < numAcceptancePairs; acceptancePair++) {
 				BitSet L = dra.getAcceptanceL(acceptancePair);
 				BitSet K = dra.getAcceptanceK(acceptancePair);
 				for (int state = mec.nextSetBit(0); state != -1; state = mec.nextSetBit(state + 1)) {
 					int draState = invMap[state] % draSize;
 					isLEmpty &= !L.get(draState);
-					isKEmpty &= !K.get(draState);
+					isKNonEmpty |= K.get(draState);
 				}
 				// Stop as soon as we find the first acceptance pair that is satisfied
-				if (isLEmpty && !isKEmpty) {
+				if (isLEmpty && isKNonEmpty) {
 					result.or(mec);
 					break;
 				}