Some tidying/fixing in EC generation, including proper support in the explicit engine version for finding ECs that intersect with "accept".

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

prism/src/explicit/ECComputer.java

@@ -65,10 +65,23 @@ public abstract class ECComputer extends PrismComponent
 	 * Compute states of all maximal end components (MECs) in the submodel obtained
 	 * by restricting this one to the set of states {@code restrict}, and store them.
 	 * They can be retrieved using {@link #getMECStates()}.
+	 * If {@code restrict} is null, we look at the whole model, not a submodel.
 	 * @param restrict BitSet for the set of states to restrict to.
 	 */
 	public abstract void computeMECStates(BitSet restrict) throws PrismException;
 
+	/**
+	 * Compute states of all accepting maximal end components (MECs) in the submodel obtained
+	 * by restricting this one to the set of states {@code restrict}, and store them,
+	 * where acceptance is defined as those which intersect with {@code accept}.
+	 * They can be retrieved using {@link #getMECStates()}.
+	 * If {@code restrict} is null, we look at the whole model, not a submodel.
+	 * If {@code accept} is null, the acceptance condition is trivially satisfied.
+	 * @param restrict BitSet for the set of states to restrict to
+	 * @param accept BitSet for the set of accepting states
+	 */
+	public abstract void computeMECStates(BitSet restrict, BitSet accept) throws PrismException;
+	
 	/**
 	 * Get the list of states for computed MECs.
 	 */

prism/src/explicit/ECComputerDefault.java

@@ -74,6 +74,12 @@ public class ECComputerDefault extends ECComputer
 		mecs = findEndComponents(restrict, null);
 	}
 
+	@Override
+	public void computeMECStates(BitSet restrict, BitSet accept) throws PrismException
+	{
+		mecs = findEndComponents(restrict, accept);
+	}
+
 	@Override
 	public List<BitSet> getMECStates()
 	{
@@ -81,8 +87,6 @@ public class ECComputerDefault extends ECComputer
 	}
 
 	// Computation
-
-	// TODO: handle 'accept'
 	
 	/**
 	 * Find all accepting maximal end components (MECs) in the submodel obtained
@@ -106,7 +110,7 @@ public class ECComputerDefault extends ECComputer
 		if (restrict.cardinality() == 0)
 			return L;
 		L.add(restrict);
-		
+		// Find MECs
 		boolean changed = true;
 		while (changed) {
 			changed = false;
@@ -116,7 +120,17 @@ public class ECComputerDefault extends ECComputer
 			L = replaceEWithSCCs(L, E, sccs);
 			changed = canLBeChanged(L, E);
 		}
-
+		// Filter and return those that contain a state in accept
+		if (accept != null) {
+			int i = 0;
+			while (i < L.size()) {
+				if (!L.get(i).intersects(accept)) {
+					L.remove(i);
+				} else {
+					i++;
+				}
+			}
+		}
 		return L;
 	}
 

prism/src/explicit/LTLModelChecker.java

@@ -624,16 +624,13 @@ public class LTLModelChecker extends PrismComponent
 			// Skip pairs with empty !L_i
 			if (statesLi_not.cardinality() == 0)
 				continue;
-			// Compute maximum end components (MECs) in !L_i
+			// Compute accepting maximum end components (MECs) in !L_i
 			ECComputer ecComputer = ECComputer.createECComputer(this, model);
-			ecComputer.computeMECStates(statesLi_not);
+			ecComputer.computeMECStates(statesLi_not, acceptance.get(i).getK());
 			List<BitSet> mecs = ecComputer.getMECStates();
-			// Check with MECs contain a K_i state
-			BitSet bitsetKi = acceptance.get(i).getK();
+			// Union MEC states
 			for (BitSet mec : mecs) {
-				if (mec.intersects(bitsetKi)) {
-					allAcceptingStates.or(mec);
-				}
+				allAcceptingStates.or(mec);
 			}
 		}
 

prism/src/prism/ECComputer.java

@@ -100,16 +100,19 @@ public abstract class ECComputer extends PrismComponent
 	 * by restricting this one to the set of states {@code restrict}, and store them.
 	 * They can be retrieved using {@link #getMECStates()}.
 	 * You will need to to deref these afterwards.
+	 * If {@code restrict} is null, we look at the whole model, not a submodel.
 	 * @param restrict BDD for the set of states to restrict to
 	 */
 	public abstract void computeMECStates(JDDNode restrict) throws PrismException;
 
 	/**
-	 * Compute states of all maximal end components (MECs) in the submodel obtained
+	 * Compute states of all accepting maximal end components (MECs) in the submodel obtained
 	 * by restricting this one to the set of states {@code restrict}, and store them,
 	 * where acceptance is defined as those which intersect with {@code accept}.
 	 * They can be retrieved using {@link #getMECStates()}.
 	 * You will need to to deref these afterwards.
+	 * If {@code restrict} is null, we look at the whole model, not a submodel.
+	 * If {@code accept} is null, the acceptance condition is trivially satisfied.
 	 * @param restrict BDD for the set of states to restrict to
 	 * @param accept BDD for the set of accepting states
 	 */