unittests for labels inside labels and guards

Author: maxkurze1

prism/src/simulator/LabelEvaluator.java

@@ -34,26 +34,25 @@ public class LabelEvaluator
 	public LabelEvaluator(LabelList labelList) throws PrismLangException
 	{
 		this.labelList = labelList;
-		this.evaluationOrder = fixEvaluationOrder(labelList);
+		this.evaluationOrder = fixEvaluationOrder(labelList.getLabelDependencies());
 	}
 
 	/**
 	 * Fix an order on the labels such that l1 < l2 if l2 depends on l1.
 	 *
-	 * @param labels a {@link LabelList} of labels to be evaluated
+	 * @param deps an adjacency matrix with adj[i][j] iff i->j
 	 * @return an int array of the label indices in ascending order
-	 * @throws PrismLangException In case a label dependencies could not be computed.
 	 */
-	private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException
+	public int[] fixEvaluationOrder(boolean[][] deps)
 	{
-		boolean[][] deps = labels.getLabelDependencies();
-		assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce";
+		assert deps.length == 0 || deps.length == deps[0].length : "dependency matrix must be square";
+		assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cycle";
 
-		int numLabels = labels.size();
+		int numLabels = deps.length;
 		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);
+		for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) {
+			last = traverseDfs(deps, l, order, last, done);
 		}
 		return order;
 	}
@@ -113,7 +112,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.
@@ -133,7 +132,7 @@ public BitSet getLabel(String label, List<State> statesList) throws PrismExcepti
 
 	/**
 	 * This method provides all label values of a certain state as a {@link BitSet}.
-	 * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}
+	 * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}.
 	 *
 	 * @param state The state to evaluate in.
 	 * @return Always returns a BitSet with the label values.
@@ -150,7 +149,7 @@ protected BitSet getStateValues(State state) throws PrismLangException
 	}
 
 	/**
-	 * Evaluates all label with the given state. <br>
+	 * Evaluates all label with the given state.
 	 *
 	 * @param state The state to evaluate the labels in.
 	 * @return A {@link BitSet} of all label values in this state.
@@ -173,7 +172,7 @@ private BitSet evaluateState(State state) throws PrismLangException
 	 * Convert the label values for a state to a predicate on the label names.
 	 *
 	 * @param values the label values for some state
-	 * @return a Predicate evaluating to {@code true} for a label name if the Bit at the corresponding index in {@code values} is set
+	 * @return a Predicate evaluating to {@code true} for a label name iff the Bit at the corresponding index in {@code values} is set
 	 */
 	public Predicate<String> asPredicate(BitSet values)
 	{

prism/unit-tests/parser/ast/LabelEvaluatorTest.java

@@ -0,0 +1,133 @@
+package parser.ast;
+
+import org.junit.jupiter.api.Test;
+import parser.State;
+import prism.PrismLangException;
+import simulator.LabelEvaluator;
+
+import java.util.Arrays;
+import java.util.List;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+import static parser.ast.LabelTest.createLabelListWithDependencyChain;
+import static parser.ast.LabelTest.createLabelListWithoutCycle;
+
+public class LabelEvaluatorTest
+{
+	@Test
+	public void testGetLabelValues() throws PrismLangException
+	{
+		/*
+		creating LabelList with
+
+		label "l2" = d<=3;
+		label "l1" = "l2" | d=5;
+
+		and checking for [0..5] of int d
+		 */
+		LabelList ll = createLabelListWithoutCycle();
+		LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
+
+		// loop through all states and check label values
+		for (int i = 0; i <= 5; i++) {
+			// create the new state with 1 variable
+			State state = new State(1);
+			// set d to [0..5]
+			state.setValue(0, i); // index of d is 0
+
+			// expected labelValues
+			boolean l2 = i <= 3;
+			boolean l1 = l2 || i == 5;
+
+			// compare
+			Predicate<String> actualValues = labelEvaluator.getLabelValues(state);
+			assertEquals(l1, actualValues.test("l1"));
+			assertEquals(l2, actualValues.test("l2"));
+		}
+	}
+
+	@Test
+	public void testLabelChainEvaluation() throws PrismLangException
+	{
+		LabelList ll = createLabelListWithDependencyChain();
+		LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
+
+		State state = new State(0);
+		assertTrue(labelEvaluator.getLabelValue(state, "l1"));
+		assertTrue(labelEvaluator.getLabelValue(state, "l2"));
+		assertTrue(labelEvaluator.getLabelValue(state, "l3"));
+	}
+
+	@Test
+	public void testLabelDFS_chain() throws PrismLangException
+	{
+		/*
+		 * label "l0" = "l2"
+		 * label "l2" = "l4"
+		 * label "l4" = "l3"
+		 * label "l3" = "l1"
+		 */
+		boolean[][] dependencies = new boolean[5][5];
+		dependencies[0][2] = true;
+		dependencies[2][4] = true;
+		dependencies[4][3] = true;
+		dependencies[3][1] = true;
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertTrue(order.indexOf(2) < order.indexOf(0));
+		assertTrue(order.indexOf(4) < order.indexOf(2));
+		assertTrue(order.indexOf(3) < order.indexOf(4));
+		assertTrue(order.indexOf(1) < order.indexOf(3));
+	}
+
+	@Test
+	public void testLabelDFS_unrelatedLabels() throws PrismLangException
+	{
+		// all false -- no dependencies
+		boolean[][] dependencies = new boolean[5][5];
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertEquals(5, order.size());
+	}
+
+	@Test
+	public void testLabelDFS_multipleCorrelationComponents() throws PrismLangException
+	{
+		/*
+		 * label "l0" = "l1" & "l3"
+		 * label "l3" = "l1"
+		 *
+		 * label "l4" = "l2" & "l5"
+		 * label "l2" = "l6"
+		 */
+		boolean[][] dependencies = new boolean[7][7];
+		dependencies[0][1] = dependencies[0][3] = true;
+		dependencies[3][1] = true;
+		dependencies[4][2] = dependencies[4][5] = true;
+		dependencies[2][6] = true;
+
+		List<Integer> order = getEvaluationOrder(dependencies);
+
+		assertTrue(order.indexOf(1) < order.indexOf(0));
+		assertTrue(order.indexOf(3) < order.indexOf(0));
+
+		assertTrue(order.indexOf(1) < order.indexOf(3));
+
+		assertTrue(order.indexOf(2) < order.indexOf(4));
+		assertTrue(order.indexOf(5) < order.indexOf(4));
+
+		assertTrue(order.indexOf(6) < order.indexOf(2));
+	}
+
+	private List<Integer> getEvaluationOrder(boolean[][] deps) throws PrismLangException
+	{
+		LabelEvaluator labelEvaluator = new LabelEvaluator(new LabelList());
+		return Arrays.stream(labelEvaluator.fixEvaluationOrder(deps)).boxed().collect(Collectors.toList());
+	}
+
+}