diff --git a/prism/src/explicit/SCCComputer.java b/prism/src/explicit/SCCComputer.java index 458c4a80..7fa1c058 100644 --- a/prism/src/explicit/SCCComputer.java +++ b/prism/src/explicit/SCCComputer.java @@ -77,4 +77,9 @@ public abstract class SCCComputer * Get the list of computed BSCCs. */ public abstract List getBSCCs(); + + /** + * Get the states not in any BSCC. + */ + public abstract BitSet getNotInBSCCs(); } diff --git a/prism/src/explicit/SCCComputerTarjan.java b/prism/src/explicit/SCCComputerTarjan.java index 3f48a35f..4da2ac93 100644 --- a/prism/src/explicit/SCCComputerTarjan.java +++ b/prism/src/explicit/SCCComputerTarjan.java @@ -44,6 +44,10 @@ public class SCCComputerTarjan extends SCCComputer private int numNodes; /* Computed list of SCCs */ private List sccs = new ArrayList(); + /* Computed list of BSCCs */ + private List bsccs = new ArrayList(); + /* States not in any BSCC */ + private BitSet notInBSCCs; /* Next index to give to a node */ private int index = 0; @@ -79,7 +83,23 @@ public class SCCComputerTarjan extends SCCComputer @Override public void computeBSCCs() { - throw new UnsupportedOperationException(); + computeSCCs(); + notInBSCCs = new BitSet(); + int n = sccs.size(); + for (int i = 0; i < n; i++) { + BitSet scc = sccs.get(i); + boolean bottom = true; + for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) { + if (!model.allSuccessorsInSet(s, scc)) { + bottom = false; + break; + } + } + if (bottom) + bsccs.add(scc); + else + notInBSCCs.or(scc); + } } @Override @@ -91,9 +111,15 @@ public class SCCComputerTarjan extends SCCComputer @Override public List getBSCCs() { - return null; + return bsccs; } + @Override + public BitSet getNotInBSCCs() + { + return notInBSCCs; + } + // SCC Computation /**