From be834a8aff7bbda6b391b2e841d41673d04c4c87 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 13 Jun 2015 00:38:01 +0000
Subject: [PATCH] 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       | 22 ++++++++++++++-------
 prism/src/explicit/SCCComputerTarjan.java | 20 +++++++++++++++++++
 prism/src/explicit/SubNondetModel.java    | 24 +++++++++++++++++------
 3 files changed, 53 insertions(+), 13 deletions(-)

diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java
index 2222cb1f..cc1d4f56 100644
--- a/prism/src/explicit/SCCComputer.java
+++ b/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.
diff --git a/prism/src/explicit/SCCComputerTarjan.java b/prism/src/explicit/SCCComputerTarjan.java
index 9120e8b8..874535bc 100644
--- a/prism/src/explicit/SCCComputerTarjan.java
+++ b/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()
 	{
diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java
index 282a29f9..bd2d34d3 100644
--- a/prism/src/explicit/SubNondetModel.java
+++ b/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
@@ -376,28 +390,26 @@ public class SubNondetModel implements NondetModel
 	@Override
 	public boolean allSuccessorsInSet(int s, int i, BitSet set)
 	{
-		Iterator<Integer> successors = getSuccessorsIterator(s,i);
+		Iterator<Integer> successors = getSuccessorsIterator(s, i);
 		while (successors.hasNext()) {
 			Integer successor = successors.next();
 			if (!set.get(successor)) {
 				return false;
 			}
 		}
-
 		return true;
 	}
 
 	@Override
 	public boolean someSuccessorsInSet(int s, int i, BitSet set)
 	{
-		Iterator<Integer> successors = getSuccessorsIterator(s,i);
+		Iterator<Integer> successors = getSuccessorsIterator(s, i);
 		while (successors.hasNext()) {
 			Integer successor = successors.next();
 			if (set.get(successor)) {
 				return true;
 			}
 		}
-
 		return false;
 	}