Fix evaluation order of labels instead repetitive recursion

Author: merkste

prism/src/parser/ast/LabelList.java

@@ -26,15 +26,12 @@
 
 package parser.ast;
 
-import parser.State;
 import parser.visitor.ASTVisitor;
 import prism.PrismLangException;
 import prism.PrismUtils;
 
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.List;
-import java.util.Map;
 import java.util.Vector;
 
 // class to store list of labels
@@ -67,7 +64,23 @@ public LabelList()
 	 */
 	public void findCycles() throws PrismLangException
 	{
-		// Create boolean matrix of dependencies
+		boolean[][] matrix = getLabelDependencies();
+		// Check for and report dependencies
+		int firstCycle = PrismUtils.findCycle(matrix);
+		if (firstCycle != -1) {
+			String s = "Cyclic dependency in definition of label \"" + names.get(firstCycle) + "\"";
+			throw new PrismLangException(s, labels.get(firstCycle));
+		}
+	}
+
+	/**
+	 * 	Create a boolean matrix of dependencies between labels.
+	 *
+	 * @return a matrix m such that label i depends on label j iff m[i][j]
+	 * @throws PrismLangException
+	 */
+	public boolean[][] getLabelDependencies() throws PrismLangException
+	{
 		// (matrix[i][j] is true if label i contains label j)
 		int n = size();
 		int j;
@@ -81,12 +94,7 @@ public void findCycles() throws PrismLangException
 				}
 			}
 		}
-		// Check for and report dependencies
-		int firstCycle = PrismUtils.findCycle(matrix);
-		if (firstCycle != -1) {
-			String s = "Cyclic dependency in definition of label \"" + names.get(firstCycle) + "\"";
-			throw new PrismLangException(s, labels.get(firstCycle));
-		}
+		return matrix;
 	}
 
 	// Set methods

prism/src/simulator/LabelEvaluator.java

@@ -1,16 +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.BitSet;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
+import java.util.function.Predicate;
 
 /**
  * This class will evaluate labels. Therefore, it's wrapped around a {@link LabelList}.
@@ -23,13 +25,47 @@ public class LabelEvaluator
     Map<State, BitSet> stateValues = new HashMap<>();
     /** The labelList that will be evaluated */
     LabelList labelList;
+    int[] evaluationOrder;
 
     /**
      * Creates new object that will evaluate and cache the given {@link LabelList}.
      */
-    public LabelEvaluator(LabelList labelList)
+    public LabelEvaluator(LabelList labelList) throws PrismLangException
     {
         this.labelList = labelList;
+        this.evaluationOrder = fixEvaluationOrder(labelList);
+    }
+
+    /**
+     * Fix an order on the labels such that l1 < l2 if l2 depends on l1
+     * @param labels
+     * @return an int array of the label indices in ascending order
+     * @throws PrismLangException In case a label depencies 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;
+                }
+                return Integer.compare(i, j);
+            }
+        });
+        return Reducible.unboxInt(new IterableArray.Of<>(order)).collect(new int[numLabels]);
     }
 
     /**
@@ -60,7 +96,7 @@ public Map<String, Boolean> getLabelValues(State state) throws PrismLangExceptio
             labelValueMap.put(labelList.getLabelName(i), value.get(i));
         }
         return labelValueMap;
-    }
+   }
 
     /**
      * This method provides all values of a certain label. They will be ordered by the given statesList. <br>
@@ -112,36 +148,13 @@ private BitSet evaluateState(State state) throws PrismLangException
         int numLabels = labelList.size();
         Map<String, Boolean> labelValues = new HashMap<>(numLabels);
         BitSet values = new BitSet();
-        for (int labelIndex = numLabels; labelIndex >= 0; labelIndex--) {
-            boolean labelValue = evaluateLabel(labelList.getLabelName(labelIndex), labelValues, state);
-            values.set(labelIndex, labelValue);
+        for (int i : evaluationOrder) {
+            Expression label = labelList.getLabel(i);
+            boolean labelValue = label.evaluateBoolean(null, labelValues, state);
+            labelValues.put(labelList.getLabelName(i), labelValue);
+            values.set(i, labelValue);
         }
         stateValues.put(state, values);
         return values;
     }
-
-    /**
-     * Helper function to recursively evaluate label values. The value will be stored inside the given map.
-     *
-     * @param name The name of the label.
-     * @param labelValues The already known values of all labels.
-     */
-    private boolean evaluateLabel(String name, Map<String, Boolean> labelValues, State state) throws PrismLangException
-    {
-        // check if value is already known
-        if (labelValues.containsKey(name)) {
-            return labelValues.get(name);
-        }
-        // get expression
-        Expression label = labelList.getLabel(labelList.getLabelIndex(name));
-        // check if all the (other) label dependencies are evaluated
-        for (String dependency : label.getAllLabels()){
-            // evaluate other label first
-            evaluateLabel(dependency, labelValues, state);
-        }
-        // all dependencies are fulfilled
-        boolean labelValue = label.evaluateBoolean(null, labelValues, state);
-        labelValues.put(name, labelValue);
-        return labelValue;
-    }
 }