|
|
|
@ -29,8 +29,8 @@ package explicit; |
|
|
|
|
|
|
|
import java.util.ArrayList; |
|
|
|
import java.util.BitSet; |
|
|
|
import java.util.Deque; |
|
|
|
import java.util.LinkedList; |
|
|
|
import java.util.List; |
|
|
|
import java.util.function.IntPredicate; |
|
|
|
|
|
|
|
import prism.PrismComponent; |
|
|
|
@ -49,7 +49,7 @@ public class SCCComputerTarjan extends SCCComputer |
|
|
|
/* Next index to give to a node */ |
|
|
|
private int index = 0; |
|
|
|
/* Stack of nodes */ |
|
|
|
private List<Integer> stack = new LinkedList<Integer>(); |
|
|
|
private Deque<Integer> stack = new LinkedList<Integer>(); |
|
|
|
/* List of nodes in the graph. Invariant: {@code nodeList.get(i).id == i} */ |
|
|
|
private ArrayList<Node> nodeList; |
|
|
|
/* Nodes currently on the stack. */ |
|
|
|
@ -108,7 +108,7 @@ public class SCCComputerTarjan extends SCCComputer |
|
|
|
v.index = index; |
|
|
|
v.lowlink = index; |
|
|
|
index++; |
|
|
|
stack.add(0, i); |
|
|
|
stack.push(i); |
|
|
|
onStack.set(i); |
|
|
|
|
|
|
|
boolean hadSelfloop = false; |
|
|
|
@ -135,10 +135,10 @@ public class SCCComputerTarjan extends SCCComputer |
|
|
|
} |
|
|
|
if (v.lowlink == v.index) { |
|
|
|
// this is a singleton SCC if the top of the stack equals i |
|
|
|
boolean singletonSCC = (stack.get(0) == i); |
|
|
|
boolean singletonSCC = (stack.peek() == i); |
|
|
|
if (singletonSCC && filterTrivialSCCs) { |
|
|
|
if (!hadSelfloop) { // singleton SCC & no selfloop -> trivial |
|
|
|
stack.remove(0); |
|
|
|
stack.pop(); |
|
|
|
onStack.set(i, false); |
|
|
|
return; |
|
|
|
} |
|
|
|
@ -147,7 +147,7 @@ public class SCCComputerTarjan extends SCCComputer |
|
|
|
int n; |
|
|
|
consumer.notifyStartSCC(); |
|
|
|
do { |
|
|
|
n = stack.remove(0); |
|
|
|
n = stack.pop(); |
|
|
|
onStack.set(n, false); |
|
|
|
consumer.notifyStateInSCC(n); |
|
|
|
} while (n != i); |
|
|
|
|