Skip to content

Commit 73c9b65

Browse files
maxkurze1maxkurze1
committed
tests for label DFS
1 parent 9fb0ebb commit 73c9b65

3 files changed

Lines changed: 184 additions & 78 deletions

File tree

‎prism/src/simulator/LabelEvaluator.java‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -34,22 +34,21 @@ public class LabelEvaluator
3434
public LabelEvaluator(LabelList labelList) throws PrismLangException
3535
{
3636
this.labelList = labelList;
37-
this.evaluationOrder = fixEvaluationOrder(labelList);
37+
this.evaluationOrder = fixEvaluationOrder(labelList.getLabelDependencies());
3838
}
3939

4040
/**
4141
* Fix an order on the labels such that l1 < l2 if l2 depends on l1.
4242
*
43-
* @param labels a {@link LabelList} of labels to be evaluated
43+
* @param deps an adjacency matrix with adj[i][j] iff i->j
4444
* @return an int array of the label indices in ascending order
45-
* @throws PrismLangException In case a label dependencies could not be computed.
4645
*/
47-
private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException
46+
public int[] fixEvaluationOrder(boolean[][] deps)
4847
{
49-
boolean[][] deps = labels.getLabelDependencies();
48+
assert deps.length == 0 || deps.length == deps[0].length : "dependency matrix must be square";
5049
assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cycle";
5150

52-
int numLabels = labels.size();
51+
int numLabels = deps.length;
5352
BitSet done = new BitSet(numLabels);
5453
int[] order = new int[numLabels];
5554
for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) {

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

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
package parser.ast;
2+
3+
import org.junit.jupiter.api.Test;
4+
import parser.State;
5+
import prism.PrismLangException;
6+
import simulator.LabelEvaluator;
7+
8+
import java.util.Arrays;
9+
import java.util.List;
10+
import java.util.function.Predicate;
11+
import java.util.stream.Collectors;
12+
13+
import static org.junit.jupiter.api.Assertions.assertEquals;
14+
import static org.junit.jupiter.api.Assertions.assertTrue;
15+
import static parser.ast.LabelTest.createLabelListWithDependencyChain;
16+
import static parser.ast.LabelTest.createLabelListWithoutCycle;
17+
18+
public class LabelEvaluatorTest
19+
{
20+
@Test
21+
public void testGetLabelValues() throws PrismLangException
22+
{
23+
/*
24+
creating LabelList with
25+
26+
label "l2" = d<=3;
27+
label "l1" = "l2" | d=5;
28+
29+
and checking for [0..5] of int d
30+
*/
31+
LabelList ll = createLabelListWithoutCycle();
32+
LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
33+
34+
// loop through all states and check label values
35+
for (int i = 0; i <= 5; i++) {
36+
// create the new state with 1 variable
37+
State state = new State(1);
38+
// set d to [0..5]
39+
state.setValue(0, i); // index of d is 0
40+
41+
// expected labelValues
42+
boolean l2 = i <= 3;
43+
boolean l1 = l2 || i == 5;
44+
45+
// compare
46+
Predicate<String> actualValues = labelEvaluator.getLabelValues(state);
47+
assertEquals(l1, actualValues.test("l1"));
48+
assertEquals(l2, actualValues.test("l2"));
49+
}
50+
}
51+
52+
@Test
53+
public void testLabelChainEvaluation() throws PrismLangException
54+
{
55+
LabelList ll = createLabelListWithDependencyChain();
56+
LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
57+
58+
State state = new State(0);
59+
assertTrue(labelEvaluator.getLabelValue(state, "l1"));
60+
assertTrue(labelEvaluator.getLabelValue(state, "l2"));
61+
assertTrue(labelEvaluator.getLabelValue(state, "l3"));
62+
}
63+
64+
@Test
65+
public void testLabelDFS_chain() throws PrismLangException
66+
{
67+
/*
68+
* label "l0" = "l2"
69+
* label "l2" = "l4"
70+
* label "l4" = "l3"
71+
* label "l3" = "l1"
72+
*/
73+
boolean[][] dependencies = new boolean[5][5];
74+
dependencies[0][2] = true;
75+
dependencies[2][4] = true;
76+
dependencies[4][3] = true;
77+
dependencies[3][1] = true;
78+
79+
List<Integer> order = getEvaluationOrder(dependencies);
80+
81+
assertTrue(order.indexOf(2) < order.indexOf(0));
82+
assertTrue(order.indexOf(4) < order.indexOf(2));
83+
assertTrue(order.indexOf(3) < order.indexOf(4));
84+
assertTrue(order.indexOf(1) < order.indexOf(3));
85+
}
86+
87+
@Test
88+
public void testLabelDFS_unrelatedLabels() throws PrismLangException
89+
{
90+
// all false -- no dependencies
91+
boolean[][] dependencies = new boolean[5][5];
92+
93+
List<Integer> order = getEvaluationOrder(dependencies);
94+
95+
assertEquals(5, order.size());
96+
}
97+
98+
@Test
99+
public void testLabelDFS_multipleCorrelationComponents() throws PrismLangException
100+
{
101+
/*
102+
* label "l0" = "l1" & "l3"
103+
* label "l3" = "l1"
104+
*
105+
* label "l4" = "l2" & "l5"
106+
* label "l2" = "l6"
107+
*/
108+
boolean[][] dependencies = new boolean[7][7];
109+
dependencies[0][1] = dependencies[0][3] = true;
110+
dependencies[3][1] = true;
111+
dependencies[4][2] = dependencies[4][5] = true;
112+
dependencies[2][6] = true;
113+
114+
List<Integer> order = getEvaluationOrder(dependencies);
115+
116+
assertTrue(order.indexOf(1) < order.indexOf(0));
117+
assertTrue(order.indexOf(3) < order.indexOf(0));
118+
119+
assertTrue(order.indexOf(1) < order.indexOf(3));
120+
121+
assertTrue(order.indexOf(2) < order.indexOf(4));
122+
assertTrue(order.indexOf(5) < order.indexOf(4));
123+
124+
assertTrue(order.indexOf(6) < order.indexOf(2));
125+
}
126+
127+
private List<Integer> getEvaluationOrder(boolean[][] deps) throws PrismLangException
128+
{
129+
LabelEvaluator labelEvaluator = new LabelEvaluator(new LabelList());
130+
return Arrays.stream(labelEvaluator.fixEvaluationOrder(deps)).boxed().collect(Collectors.toList());
131+
}
132+
133+
}

‎prism/unit-tests/parser/ast/LabelTest.java‎

Lines changed: 46 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -2,18 +2,12 @@
22

33
import org.junit.jupiter.api.Nested;
44
import org.junit.jupiter.api.Test;
5-
import parser.State;
65
import parser.type.TypeBool;
76
import parser.type.TypeInt;
87
import prism.PrismLangException;
9-
import simulator.LabelEvaluator;
10-
11-
import java.util.function.Predicate;
128

139
import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
14-
import static org.junit.jupiter.api.Assertions.assertEquals;
1510
import static org.junit.jupiter.api.Assertions.assertThrows;
16-
import static org.junit.jupiter.api.Assertions.assertTrue;
1711

1812
public class LabelTest
1913
{
@@ -49,58 +43,20 @@ public void testFindCycles_noCycle()
4943
}
5044
}
5145

52-
@Nested
53-
class LabelEvaluterTest
46+
/**
47+
* <p>
48+
* Helper method that will create a {@link LabelList} with the following Labels:
49+
* </p>
50+
* <ul>
51+
* <li>label "l2" = d<=3;</li>
52+
* <li>label "l1" = "l2" | d=5;</li>
53+
* </ul>
54+
* </p>
55+
* Note: d is the only variable (index 0) and has {@link TypeInt}
56+
* <p>
57+
*/
58+
protected static LabelList createLabelListWithoutCycle()
5459
{
55-
@Test
56-
public void testGetLabelValues() throws PrismLangException
57-
{
58-
/*
59-
d is part of the state and will go from [0..5]
60-
61-
label "l1" = "l2" | d=5
62-
label "l2" = d<=3
63-
*/
64-
LabelList ll = createLabelListWithoutCycle();
65-
LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
66-
67-
// loop through all states and check label values
68-
for (int i = 0; i <= 5; i++) {
69-
// create the new state with 1 variable
70-
State state = new State(1);
71-
// set d to [0..5]
72-
state.setValue(0, i); // index of d is 0
73-
74-
// expected labelValues
75-
boolean l2 = i <= 3;
76-
boolean l1 = l2 || i == 5;
77-
78-
// compare
79-
Predicate<String> actualValues = labelEvaluator.getLabelValues(state);
80-
assertEquals(l1, actualValues.test("l1"));
81-
assertEquals(l2, actualValues.test("l2"));
82-
}
83-
}
84-
85-
@Test
86-
public void testLabelChainEvaluation() throws PrismLangException
87-
{
88-
LabelList ll = createLabelListWithDependencyChain();
89-
LabelEvaluator labelEvaluator = new LabelEvaluator(ll);
90-
91-
State state = new State(0);
92-
assertTrue(labelEvaluator.getLabelValue(state, "l1"));
93-
assertTrue(labelEvaluator.getLabelValue(state, "l2"));
94-
assertTrue(labelEvaluator.getLabelValue(state, "l3"));
95-
}
96-
}
97-
98-
private LabelList createLabelListWithoutCycle()
99-
{
100-
/*
101-
label "l1" = "l2" | d=5
102-
label "l2" = d<=3
103-
*/
10460
LabelList ll = new LabelList();
10561
ExpressionVar dVar = new ExpressionVar("d", TypeInt.getInstance());
10662
dVar.setIndex(0); // index of d is 0
@@ -112,38 +68,56 @@ private LabelList createLabelListWithoutCycle()
11268
return ll;
11369
}
11470

115-
private LabelList createLabelListWith1LabelCycle()
71+
/**
72+
* <p>
73+
* Helper method that will create a {@link LabelList} with the following Labels:
74+
* </p>
75+
* <ul>
76+
* <li>label "l1" = "l1";</li>
77+
* </ul>
78+
*/
79+
protected static LabelList createLabelListWith1LabelCycle()
11680
{
11781
LabelList ll = new LabelList();
118-
/* label "l1" = "l1" */
11982
ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l1"));
12083
return ll;
12184
}
12285

123-
private LabelList createLabelListWith2LabelCycle()
86+
/**
87+
* <p>
88+
* Helper method that will create a {@link LabelList} with the following Labels:
89+
* </p>
90+
* <ul>
91+
* <li>label "l1" = "l2";</li>
92+
* <li>label "l2" = "l1" | d=5;</li>
93+
* </ul>
94+
* </p>
95+
* Note: d is the only variable (index 0) and has {@link TypeInt}
96+
* <p>
97+
*/
98+
protected static LabelList createLabelListWith2LabelCycle()
12499
{
125100
LabelList ll = new LabelList();
126-
/*
127-
label "l1" = "l2"
128-
label "l2" = "l1" | d=5
129-
*/
130101
ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2"));
131102
ll.addLabel(new ExpressionIdent("l2"), new ExpressionBinaryOp(ExpressionBinaryOp.OR,
132103
new ExpressionLabel("l1"), new ExpressionBinaryOp(ExpressionBinaryOp.EQ,
133104
new ExpressionVar("d", TypeInt.getInstance()), new ExpressionLiteral(TypeInt.getInstance(), 5))));
134105
return ll;
135106
}
136107

137-
private LabelList createLabelListWithDependencyChain()
108+
/**
109+
* <p>
110+
* Helper method that will create a {@link LabelList} with the following Labels:
111+
* </p>
112+
* <ul>
113+
* <li>label "l1" = "l2";</li>
114+
* <li>label "l2" = "l3";</li>
115+
* <li>label "l3" = true;</li>
116+
* </ul>
117+
*/
118+
protected static LabelList createLabelListWithDependencyChain()
138119
{
139120
LabelList ll = new LabelList();
140-
/*
141-
label "l1" = "l2"
142-
label "l2" = "l3"
143-
label "l3" = true
144-
145-
"l3" must be evaluated as dependency for "l1"
146-
*/
147121
ll.addLabel(new ExpressionIdent("l1"), new ExpressionLabel("l2"));
148122
ll.addLabel(new ExpressionIdent("l2"), new ExpressionLabel("l3"));
149123
ll.addLabel(new ExpressionIdent("l3"), new ExpressionLiteral(TypeBool.getInstance(), true));

0 commit comments

Comments
 (0)