EC generation: comments and refactoring.

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

prism/src/explicit/ECComputer.java

@@ -62,11 +62,12 @@ 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.
+	 * 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()}.
-	 * @param states BitSet for the set of containing states
+	 * @param restrict BitSet for the set of states to restrict to.
 	 */
-	public abstract void computeMECStates(BitSet states) throws PrismException;
+	public abstract void computeMECStates(BitSet restrict) throws PrismException;
 
 	/**
 	 * Get the list of states for computed MECs.

prism/src/explicit/ECComputerDefault.java

@@ -65,16 +65,13 @@ public class ECComputerDefault extends ECComputer
 	@Override
 	public void computeMECStates() throws PrismException
 	{
-		// Look within set of all reachable states
-		BitSet reach = new BitSet();
-		reach.set(0, model.getNumStates());
-		computeMECStates(reach);
+		mecs = findEndComponents(null, null);
 	}
 
 	@Override
-	public void computeMECStates(BitSet states) throws PrismException
+	public void computeMECStates(BitSet restrict) throws PrismException
 	{
-		mecs = findEndComponents(states, null); //TODO
+		mecs = findEndComponents(restrict, null);
 	}
 
 	@Override
@@ -85,21 +82,30 @@ public class ECComputerDefault extends ECComputer
 
 	// Computation
 
+	// TODO: handle 'accept'
+	
 	/**
-	 * 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
+	 * Find all accepting maximal end components (MECs) in the submodel obtained
+	 * by restricting this one to the set of states {@code restrict},
+	 * where acceptance is defined as those which intersect with {@code accept}.
+	 * 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
 	 * @return a list of BitSets representing the MECs
 	 */
-	private List<BitSet> findEndComponents(BitSet states, BitSet filter) throws PrismException
+	private List<BitSet> findEndComponents(BitSet restrict, BitSet accept) throws PrismException
 	{
+		// If restrict is null, look within set of all reachable states
+		if (restrict == null) {
+			restrict = new BitSet();
+			restrict.set(0, model.getNumStates());
+		}
 		// Initialise L with set of all states to look in (if non-empty)
 		List<BitSet> L = new ArrayList<BitSet>();
-		if (states.cardinality() == 0)
+		if (restrict.cardinality() == 0)
 			return L;
-		L.add(states);
+		L.add(restrict);
 		
 		boolean changed = true;
 		while (changed) {

prism/src/prism/ECComputer.java

@@ -96,22 +96,24 @@ 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.
+	 * 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()}.
 	 * You will need to to deref these afterwards.
-	 * @param states BDD of the set of containing states
+	 * @param restrict BDD for the set of states to restrict to
 	 */
-	public abstract void computeMECStates(JDDNode states) throws PrismException;
+	public abstract void computeMECStates(JDDNode restrict) throws PrismException;
 
 	/**
-	 * Compute states of all accepting maximal end components (MECs) contained within {@code states}, and store them,
-	 * where acceptance is defined as those which intersect with {@code filter}.
+	 * 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,
+	 * 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.
-	 * @param states BDD of the set of containing states
-	 * @param filter BDD for the set of accepting states
+	 * @param restrict BDD for the set of states to restrict to
+	 * @param accept BDD for the set of accepting states
 	 */
-	public abstract void computeMECStates(JDDNode states, JDDNode filter) throws PrismException;
+	public abstract void computeMECStates(JDDNode restrict, JDDNode accept) throws PrismException;
 
 	/**
 	 * Get the list of states for computed MECs.

prism/src/prism/ECComputerDefault.java

@@ -56,40 +56,45 @@ public class ECComputerDefault extends ECComputer
 	@Override
 	public void computeMECStates() throws PrismException
 	{
-		mecs = findEndComponents(reach, null);
+		mecs = findEndComponents(null, null);
 	}
 
 	@Override
-	public void computeMECStates(JDDNode states) throws PrismException
+	public void computeMECStates(JDDNode restrict) throws PrismException
 	{
-		mecs = findEndComponents(states, null);
+		mecs = findEndComponents(restrict, null);
 	}
 
 	@Override
-	public void computeMECStates(JDDNode states, JDDNode filter) throws PrismException
+	public void computeMECStates(JDDNode restrict, JDDNode accept) throws PrismException
 	{
-		mecs = findEndComponents(states, filter);
+		mecs = findEndComponents(restrict, accept);
 	}
 
 	// Computation
 
 	/**
-	 * 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 BDD of the set of containing states
-	 * @param filter BDD for the set of accepting states
+	 * Find all accepting maximal end components (MECs) in the submodel obtained
+	 * by restricting this one to the set of states {@code restrict},
+	 * where acceptance is defined as those which intersect with {@code accept}.
+	 * 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
 	 * @return a list of (referenced) BDDs representing the MECs
 	 */
-	private List<JDDNode> findEndComponents(JDDNode states, JDDNode filter) throws PrismException
+	private List<JDDNode> findEndComponents(JDDNode restrict, JDDNode accept) throws PrismException
 	{
 		Vector<JDDNode> mecs = new Vector<JDDNode>();
 		SCCComputer sccComputer;
 
 		// Initial set of candidates for MECs just contains the whole set we are searching
+		// (which, if null, is all states)
+		if (restrict == null)
+			restrict = reach;
 		Stack<JDDNode> candidates = new Stack<JDDNode>();
-		JDD.Ref(states);
-		candidates.push(states);
+		JDD.Ref(restrict);
+		candidates.push(restrict);
 
 		// Go through each candidate set
 		while (!candidates.isEmpty()) {
@@ -118,8 +123,8 @@ public class ECComputerDefault extends ECComputer
 
 			// Find the maximal SCCs in (stableSet, stableSetTrans)
 			sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars);
-			if (filter != null)
-				sccComputer.computeSCCs(filter);
+			if (accept != null)
+				sccComputer.computeSCCs(accept);
 			else
 				sccComputer.computeSCCs();
 			JDD.Deref(stableSet);