new label evaluation ordering algorithm

Author: maxkurze1

prism/src/simulator/LabelEvaluator.java

@@ -1,17 +1,18 @@
 package simulator;
 
 
-import common.iterable.IterableArray;
-import common.iterable.Range;
-import common.iterable.Reducible;
 import parser.State;
 import parser.ast.Expression;
 import parser.ast.LabelList;
 import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismUtils;
 
-import java.util.*;
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.NoSuchElementException;
 import java.util.function.Predicate;
 
 /**
@@ -41,34 +42,48 @@ public LabelEvaluator(LabelList labelList) throws PrismLangException
      *
      * @param labels a {@link LabelList} of labels to be evaluated
      * @return an int array of the label indices in ascending order
-     * @throws PrismLangException In case a label depencies could not be computed.
+     * @throws PrismLangException In case a label dependencies could not be computed.
      */
     private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException
     {
         boolean[][] deps = labels.getLabelDependencies();
         assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce";
 
         int numLabels = labels.size();
-        Integer[] order = new Range(numLabels).collect(new Integer[numLabels]);
-        Arrays.sort(order, new Comparator<Integer>()
-        {
-            @Override
-            public int compare(Integer row, Integer col)
-            {
-                int i = row;
-                int j = col;
-                if (deps[i][j]) { // i depends on j
-                    return +1;
-                }
-                if (deps[j][i]) { // j depends on i
-                    return -1;
+        BitSet done = new BitSet(numLabels);
+        int[] order = new int[numLabels];
+        for (int l = done.nextClearBit(0); l < numLabels; l = done.nextClearBit(l)) {
+            traverseDfs(deps, l, order, -1, done);
+        }
+        return order;
+    }
+
+    /**
+     * Do a depth-first search in a graph given by an adjacency matrix starting at a given node.
+     *
+     * @param adj   an adjacency matrix with adj[i][j] iff i->j
+     * @param start a start node
+     * @param trace an int array to record the trace, will be modified
+     * @param last  index of last element of the trace
+     * @param done  a {@link BitSet} of already visited nodes, will be modified
+     * @return the index of the last element of the extended trace, i.e., of the start node
+     */
+    private int traverseDfs(boolean[][] adj, int start, int[] trace, int last, BitSet done)
+    {
+        if (!done.get(start)) {
+            boolean[] isSuccessor = adj[start];
+            for (int node = isSuccessor.length - 1; node >= 0; node--) {
+                if (isSuccessor[node]) {
+                    last = traverseDfs(adj, node, trace, last, done);
                 }
-                return Integer.compare(i, j);
             }
-        });
-        return Reducible.unboxInt(new IterableArray.Of<>(order)).collect(new int[numLabels]);
+            trace[++last] = start;
+            done.set(start);
+        }
+        return last;
     }
 
+
     /**
      * Returns the value of a specific label in a specific state.
      *
@@ -99,7 +114,7 @@ public Predicate<String> getLabelValues(State state) throws PrismLangException
      * This method provides all values of a certain label. They will be ordered by the given statesList. <br>
      * States will be evaluated if necessary.
      *
-     * @param label The name of the label.
+     * @param label      The name of the label.
      * @param statesList The states to evaluate against in correct order.
      * @return All values of the label.
      * @throws PrismException In case a label evaluation fails.
@@ -109,7 +124,7 @@ public BitSet getLabel(String label, List<State> statesList) throws PrismExcepti
         int statesNum = statesList.size();
         int labelIndex = labelList.getLabelIndex(label);
         BitSet labelValues = new BitSet();
-        for (int i = statesNum-1; i >= 0; i--) {
+        for (int i = statesNum - 1; i >= 0; i--) {
             State state = statesList.get(i);
             BitSet valuesOfState = getStateValues(state);
             labelValues.set(i, valuesOfState.get(labelIndex));
@@ -163,7 +178,8 @@ private BitSet evaluateState(State state) throws PrismLangException
      */
     public Predicate<String> asPredicate(BitSet values)
     {
-        return new Predicate<String>() {
+        return new Predicate<String>()
+        {
             @Override
             public boolean test(String name)
             {