Browse Source

Bug fix in explicit.SCCComputerTarjan (from Joachim Klein).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10088 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
commit
5173aab053
  1. 6
      prism/src/explicit/SCCComputerTarjan.java

6
prism/src/explicit/SCCComputerTarjan.java

@ -86,12 +86,12 @@ public class SCCComputerTarjan extends SCCComputer
tarjan();
// Now remove trivial SCCs
notInSCCs = new BitSet();
for (int i = 0; i < sccs.size(); i++) {
BitSet scc = sccs.get(i);
for (Iterator<BitSet> it = sccs.iterator(); it.hasNext(); ) {
BitSet scc = it.next();
if (scc.cardinality() == 1) {
int s = scc.nextSetBit(0);
if (!model.someSuccessorsInSet(s, scc)) {
sccs.remove(i);
it.remove(); // remove this SCC from sccs list
notInSCCs.set(s);
}
}

Loading…
Cancel
Save