Align explicit SCComputer with symbolic one - it should not include trivial SCCs in the set computed; these should be stored separately.

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

prism/src/explicit/SCCComputer.java

@@ -71,21 +71,29 @@ public abstract class SCCComputer extends PrismComponent
 	}
 
 	/**
-	 * Compute strongly connected components (SCCs) and store them.
-	 * They can be retrieved using {@link #getSCCs()}.
+	 * Compute (non-trivial) strongly connected components (SCCs) and store them.
+	 * They should be retrieved using {@link #getSCCs()}.
+	 * States in trivial SCCs (those comprising a single state without a self-loop) are also stored.
+	 * They should be retrieved using {@link #getNotInSCCs()}.
 	 */
 	public abstract void computeSCCs();
 
 	/**
-	 * Compute bottom strongly connected components (BSCCs) and store them.
-	 * They can be retrieved using {@link #getBSCCs()} and {@link #getNotInBSCCs()}.
+	 * Get the list of computed (non-trivial) SCCs.
 	 */
-	public abstract void computeBSCCs();
+	public abstract List<BitSet> getSCCs();
 
 	/**
-	 * Get the list of computed SCCs.
+	 * Get the states not in any (non-trivial) SCC.
+	 * In other words, this is all states in trivial SCCs (those comprising a single state without a self-loop).
 	 */
-	public abstract List<BitSet> getSCCs();
+	public abstract BitSet getNotInSCCs();
+
+	/**
+	 * Compute bottom strongly connected components (BSCCs) and store them.
+	 * They can be retrieved using {@link #getBSCCs()} and {@link #getNotInBSCCs()}.
+	 */
+	public abstract void computeBSCCs();
 
 	/**
 	 * Get the list of computed BSCCs.

prism/src/explicit/SCCComputerTarjan.java

@@ -47,6 +47,8 @@ public class SCCComputerTarjan extends SCCComputer
 	private int numNodes;
 	/* Computed list of SCCs */
 	private List<BitSet> sccs = new ArrayList<BitSet>();
+	/* States not in non-trivial SCCs */
+	private BitSet notInSCCs;
 	/* Computed list of BSCCs */
 	private List<BitSet> bsccs = new ArrayList<BitSet>();
 	/* States not in any BSCC */
@@ -82,6 +84,18 @@ public class SCCComputerTarjan extends SCCComputer
 	public void computeSCCs()
 	{
 		tarjan();
+		// Now remove trivial SCCs
+		notInSCCs = new BitSet();
+		for (int i = 0; i < sccs.size(); i++) {
+			BitSet scc = sccs.get(i);
+			if (scc.cardinality() == 1) {
+				int s = scc.nextSetBit(0);
+				if (!model.someSuccessorsInSet(s, scc)) {
+					sccs.remove(i);
+					notInSCCs.set(s);
+				}
+			}
+		}
 	}
 
 	@Override
@@ -112,6 +126,12 @@ public class SCCComputerTarjan extends SCCComputer
 		return sccs;
 	}
 
+	@Override
+	public BitSet getNotInSCCs()
+	{
+		return notInSCCs;
+	}
+	
 	@Override
 	public List<BitSet> getBSCCs()
 	{

prism/src/explicit/SubNondetModel.java

@@ -220,13 +220,27 @@ public class SubNondetModel implements NondetModel
 	@Override
 	public boolean allSuccessorsInSet(int s, BitSet set)
 	{
-		throw new UnsupportedOperationException();
+		Iterator<Integer> successors = getSuccessorsIterator(s);
+		while (successors.hasNext()) {
+			Integer successor = successors.next();
+			if (set.get(successor)) {
+				return true;
+			}
+		}
+		return false;
 	}
 
 	@Override
 	public boolean someSuccessorsInSet(int s, BitSet set)
 	{
-		throw new UnsupportedOperationException();
+		Iterator<Integer> successors = getSuccessorsIterator(s);
+		while (successors.hasNext()) {
+			Integer successor = successors.next();
+			if (set.get(successor)) {
+				return true;
+			}
+		}
+		return false;
 	}
 
 	@Override
@@ -383,7 +397,6 @@ public class SubNondetModel implements NondetModel
 				return false;
 			}
 		}
-
 		return true;
 	}
 
@@ -397,7 +410,6 @@ public class SubNondetModel implements NondetModel
 				return true;
 			}
 		}
-
 		return false;
 	}