|
22 | 22 | */ |
23 | 23 | public class LabelEvaluator |
24 | 24 | { |
25 | | - /** Map of each evaluated state and a bitset containing the label-values ordered as in labelList */ |
26 | | - Map<State, BitSet> stateValues = new HashMap<>(); |
27 | | - /** The labelList that will be evaluated */ |
28 | | - LabelList labelList; |
29 | | - int[] evaluationOrder; |
| 25 | + /** Map of each evaluated state and a bitset containing the label-values ordered as in labelList */ |
| 26 | + Map<State, BitSet> stateValues = new HashMap<>(); |
| 27 | + /** The labelList that will be evaluated */ |
| 28 | + LabelList labelList; |
| 29 | + int[] evaluationOrder; |
30 | 30 |
|
31 | | - /** |
32 | | - * Creates new object that will evaluate and cache the given {@link LabelList}. |
33 | | - */ |
34 | | - public LabelEvaluator(LabelList labelList) throws PrismLangException |
35 | | - { |
36 | | - this.labelList = labelList; |
37 | | - this.evaluationOrder = fixEvaluationOrder(labelList); |
38 | | - } |
| 31 | + /** |
| 32 | + * Creates new object that will evaluate and cache the given {@link LabelList}. |
| 33 | + */ |
| 34 | + public LabelEvaluator(LabelList labelList) throws PrismLangException |
| 35 | + { |
| 36 | + this.labelList = labelList; |
| 37 | + this.evaluationOrder = fixEvaluationOrder(labelList); |
| 38 | + } |
39 | 39 |
|
40 | | - /** |
41 | | - * Fix an order on the labels such that l1 < l2 if l2 depends on l1. |
42 | | - * |
43 | | - * @param labels a {@link LabelList} of labels to be evaluated |
44 | | - * @return an int array of the label indices in ascending order |
45 | | - * @throws PrismLangException In case a label dependencies could not be computed. |
46 | | - */ |
47 | | - private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException |
48 | | - { |
49 | | - boolean[][] deps = labels.getLabelDependencies(); |
50 | | - assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce"; |
| 40 | + /** |
| 41 | + * Fix an order on the labels such that l1 < l2 if l2 depends on l1. |
| 42 | + * |
| 43 | + * @param labels a {@link LabelList} of labels to be evaluated |
| 44 | + * @return an int array of the label indices in ascending order |
| 45 | + * @throws PrismLangException In case a label dependencies could not be computed. |
| 46 | + */ |
| 47 | + private int[] fixEvaluationOrder(LabelList labels) throws PrismLangException |
| 48 | + { |
| 49 | + boolean[][] deps = labels.getLabelDependencies(); |
| 50 | + assert PrismUtils.findCycle(deps) == -1 : "label dependencies must not contain a cylce"; |
51 | 51 |
|
52 | | - int numLabels = labels.size(); |
53 | | - BitSet done = new BitSet(numLabels); |
54 | | - int[] order = new int[numLabels]; |
55 | | - for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) { |
56 | | - last = traverseDfs(deps, l, order, last, done); |
57 | | - } |
58 | | - return order; |
59 | | - } |
| 52 | + int numLabels = labels.size(); |
| 53 | + BitSet done = new BitSet(numLabels); |
| 54 | + int[] order = new int[numLabels]; |
| 55 | + for (int l = done.nextClearBit(0), last = -1; l < numLabels; l = done.nextClearBit(l)) { |
| 56 | + last = traverseDfs(deps, l, order, last, done); |
| 57 | + } |
| 58 | + return order; |
| 59 | + } |
60 | 60 |
|
61 | | - /** |
62 | | - * Do a depth-first search in a graph given by an adjacency matrix starting at a given node. |
63 | | - * |
64 | | - * @param adj an adjacency matrix with adj[i][j] iff i->j |
65 | | - * @param start a start node |
66 | | - * @param trace an int array to record the trace, will be modified |
67 | | - * @param last index of last element of the trace |
68 | | - * @param done a {@link BitSet} of already visited nodes, will be modified |
69 | | - * @return the index of the last element of the extended trace, i.e., of the start node |
70 | | - */ |
71 | | - private int traverseDfs(boolean[][] adj, int start, int[] trace, int last, BitSet done) |
72 | | - { |
73 | | - if (!done.get(start)) { |
74 | | - boolean[] isSuccessor = adj[start]; |
75 | | - for (int node = isSuccessor.length - 1; node >= 0; node--) { |
76 | | - if (isSuccessor[node]) { |
77 | | - last = traverseDfs(adj, node, trace, last, done); |
78 | | - } |
79 | | - } |
80 | | - trace[++last] = start; |
81 | | - done.set(start); |
82 | | - } |
83 | | - return last; |
84 | | - } |
| 61 | + /** |
| 62 | + * Do a depth-first search in a graph given by an adjacency matrix starting at a given node. |
| 63 | + * |
| 64 | + * @param adj an adjacency matrix with adj[i][j] iff i->j |
| 65 | + * @param start a start node |
| 66 | + * @param trace an int array to record the trace, will be modified |
| 67 | + * @param last index of last element of the trace |
| 68 | + * @param done a {@link BitSet} of already visited nodes, will be modified |
| 69 | + * @return the index of the last element of the extended trace, i.e., of the start node |
| 70 | + */ |
| 71 | + private int traverseDfs(boolean[][] adj, int start, int[] trace, int last, BitSet done) |
| 72 | + { |
| 73 | + if (!done.get(start)) { |
| 74 | + boolean[] isSuccessor = adj[start]; |
| 75 | + for (int node = isSuccessor.length - 1; node >= 0; node--) { |
| 76 | + if (isSuccessor[node]) { |
| 77 | + last = traverseDfs(adj, node, trace, last, done); |
| 78 | + } |
| 79 | + } |
| 80 | + trace[++last] = start; |
| 81 | + done.set(start); |
| 82 | + } |
| 83 | + return last; |
| 84 | + } |
85 | 85 |
|
86 | 86 |
|
87 | | - /** |
88 | | - * Returns the value of a specific label in a specific state. |
89 | | - * |
90 | | - * @param state The state to evaluate in. |
91 | | - * @param label The label that will be evaluated. |
92 | | - * @return The value of the Label. |
93 | | - * @throws PrismLangException In case a label couldn't be evaluated. |
94 | | - */ |
95 | | - public boolean getLabelValue(State state, String label) throws PrismLangException |
96 | | - { |
97 | | - return getStateValues(state).get(labelList.getLabelIndex(label)); |
98 | | - } |
| 87 | + /** |
| 88 | + * Returns the value of a specific label in a specific state. |
| 89 | + * |
| 90 | + * @param state The state to evaluate in. |
| 91 | + * @param label The label that will be evaluated. |
| 92 | + * @return The value of the Label. |
| 93 | + * @throws PrismLangException In case a label couldn't be evaluated. |
| 94 | + */ |
| 95 | + public boolean getLabelValue(State state, String label) throws PrismLangException |
| 96 | + { |
| 97 | + return getStateValues(state).get(labelList.getLabelIndex(label)); |
| 98 | + } |
99 | 99 |
|
100 | | - /** |
101 | | - * This method provides all label values concerning a given state. <br> |
102 | | - * It will evaluate all the Labels if necessary. |
103 | | - * |
104 | | - * @param state The state to evaluate in. |
105 | | - * @return Returns a {@link Map} containing all label-values for the given state, indexed by their name. |
106 | | - * @throws PrismLangException In case a label couldn't be evaluated. |
107 | | - */ |
108 | | - public Predicate<String> getLabelValues(State state) throws PrismLangException |
109 | | - { |
110 | | - return asPredicate(getStateValues(state)); |
111 | | - } |
| 100 | + /** |
| 101 | + * This method provides all label values concerning a given state. <br> |
| 102 | + * It will evaluate all the Labels if necessary. |
| 103 | + * |
| 104 | + * @param state The state to evaluate in. |
| 105 | + * @return Returns a {@link Map} containing all label-values for the given state, indexed by their name. |
| 106 | + * @throws PrismLangException In case a label couldn't be evaluated. |
| 107 | + */ |
| 108 | + public Predicate<String> getLabelValues(State state) throws PrismLangException |
| 109 | + { |
| 110 | + return asPredicate(getStateValues(state)); |
| 111 | + } |
112 | 112 |
|
113 | | - /** |
114 | | - * This method provides all values of a certain label. They will be ordered by the given statesList. <br> |
115 | | - * States will be evaluated if necessary. |
116 | | - * |
117 | | - * @param label The name of the label. |
118 | | - * @param statesList The states to evaluate against in correct order. |
119 | | - * @return All values of the label. |
120 | | - * @throws PrismException In case a label evaluation fails. |
121 | | - */ |
122 | | - public BitSet getLabel(String label, List<State> statesList) throws PrismException |
123 | | - { |
124 | | - int statesNum = statesList.size(); |
125 | | - int labelIndex = labelList.getLabelIndex(label); |
126 | | - BitSet labelValues = new BitSet(); |
127 | | - for (int i = statesNum - 1; i >= 0; i--) { |
128 | | - State state = statesList.get(i); |
129 | | - BitSet valuesOfState = getStateValues(state); |
130 | | - labelValues.set(i, valuesOfState.get(labelIndex)); |
131 | | - } |
132 | | - return labelValues; |
133 | | - } |
| 113 | + /** |
| 114 | + * This method provides all values of a certain label. They will be ordered by the given statesList. <br> |
| 115 | + * States will be evaluated if necessary. |
| 116 | + * |
| 117 | + * @param label The name of the label. |
| 118 | + * @param statesList The states to evaluate against in correct order. |
| 119 | + * @return All values of the label. |
| 120 | + * @throws PrismException In case a label evaluation fails. |
| 121 | + */ |
| 122 | + public BitSet getLabel(String label, List<State> statesList) throws PrismException |
| 123 | + { |
| 124 | + int statesNum = statesList.size(); |
| 125 | + int labelIndex = labelList.getLabelIndex(label); |
| 126 | + BitSet labelValues = new BitSet(); |
| 127 | + for (int i = statesNum - 1; i >= 0; i--) { |
| 128 | + State state = statesList.get(i); |
| 129 | + BitSet valuesOfState = getStateValues(state); |
| 130 | + labelValues.set(i, valuesOfState.get(labelIndex)); |
| 131 | + } |
| 132 | + return labelValues; |
| 133 | + } |
134 | 134 |
|
135 | | - /** |
136 | | - * This method provides all label values of a certain state as a {@link BitSet}. |
137 | | - * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}. |
138 | | - * |
139 | | - * @param state The state to evaluate in. |
140 | | - * @return Always returns a BitSet with the label values. |
141 | | - * @throws PrismLangException In case a label evaluation fails. |
142 | | - */ |
143 | | - protected BitSet getStateValues(State state) throws PrismLangException |
144 | | - { |
145 | | - BitSet values = stateValues.get(state); |
146 | | - if (values == null) { |
147 | | - values = evaluateState(state); |
148 | | - stateValues.put(state, values); |
149 | | - } |
150 | | - return values; |
151 | | - } |
| 135 | + /** |
| 136 | + * This method provides all label values of a certain state as a {@link BitSet}. |
| 137 | + * The labels are indexed in the same order as inside the {@link LabelEvaluator#labelList}. |
| 138 | + * |
| 139 | + * @param state The state to evaluate in. |
| 140 | + * @return Always returns a BitSet with the label values. |
| 141 | + * @throws PrismLangException In case a label evaluation fails. |
| 142 | + */ |
| 143 | + protected BitSet getStateValues(State state) throws PrismLangException |
| 144 | + { |
| 145 | + BitSet values = stateValues.get(state); |
| 146 | + if (values == null) { |
| 147 | + values = evaluateState(state); |
| 148 | + stateValues.put(state, values); |
| 149 | + } |
| 150 | + return values; |
| 151 | + } |
152 | 152 |
|
153 | | - /** |
154 | | - * Evaluates all label with the given state. |
155 | | - * |
156 | | - * @param state The state to evaluate the labels in. |
157 | | - * @return A {@link BitSet} of all label values in this state. |
158 | | - * @throws PrismLangException In case a label evaluation fails. |
159 | | - */ |
160 | | - private BitSet evaluateState(State state) throws PrismLangException |
161 | | - { |
162 | | - BitSet values = new BitSet(); |
163 | | - Predicate<String> labelValues = asPredicate(values); |
164 | | - for (int i : evaluationOrder) { |
165 | | - Expression label = labelList.getLabel(i); |
166 | | - boolean labelValue = label.evaluateBoolean(null, labelValues, state); |
167 | | - values.set(i, labelValue); |
168 | | - } |
169 | | - stateValues.put(state, values); |
170 | | - return values; |
171 | | - } |
| 153 | + /** |
| 154 | + * Evaluates all label with the given state. |
| 155 | + * |
| 156 | + * @param state The state to evaluate the labels in. |
| 157 | + * @return A {@link BitSet} of all label values in this state. |
| 158 | + * @throws PrismLangException In case a label evaluation fails. |
| 159 | + */ |
| 160 | + private BitSet evaluateState(State state) throws PrismLangException |
| 161 | + { |
| 162 | + BitSet values = new BitSet(); |
| 163 | + Predicate<String> labelValues = asPredicate(values); |
| 164 | + for (int i : evaluationOrder) { |
| 165 | + Expression label = labelList.getLabel(i); |
| 166 | + boolean labelValue = label.evaluateBoolean(null, labelValues, state); |
| 167 | + values.set(i, labelValue); |
| 168 | + } |
| 169 | + stateValues.put(state, values); |
| 170 | + return values; |
| 171 | + } |
172 | 172 |
|
173 | | - /** |
174 | | - * Convert the label values for a state to a predicate on the label names. |
175 | | - * |
176 | | - * @param values the label values for some state |
177 | | - * @return a Predicate evaluating to {@code true} for a label name iff the Bit at the corresponding index in {@code values} is set |
178 | | - */ |
179 | | - public Predicate<String> asPredicate(BitSet values) |
180 | | - { |
181 | | - return new Predicate<String>() |
182 | | - { |
183 | | - @Override |
184 | | - public boolean test(String name) |
185 | | - { |
186 | | - int index = labelList.getLabelIndex(name); |
187 | | - if (index == -1) { |
188 | | - throw new NoSuchElementException("Unknown label \"" + name + "\""); |
189 | | - } |
190 | | - return values.get(index); |
191 | | - } |
192 | | - }; |
193 | | - } |
| 173 | + /** |
| 174 | + * Convert the label values for a state to a predicate on the label names. |
| 175 | + * |
| 176 | + * @param values the label values for some state |
| 177 | + * @return a Predicate evaluating to {@code true} for a label name iff the Bit at the corresponding index in {@code values} is set |
| 178 | + */ |
| 179 | + public Predicate<String> asPredicate(BitSet values) |
| 180 | + { |
| 181 | + return new Predicate<String>() |
| 182 | + { |
| 183 | + @Override |
| 184 | + public boolean test(String name) |
| 185 | + { |
| 186 | + int index = labelList.getLabelIndex(name); |
| 187 | + if (index == -1) { |
| 188 | + throw new NoSuchElementException("Unknown label \"" + name + "\""); |
| 189 | + } |
| 190 | + return values.get(index); |
| 191 | + } |
| 192 | + }; |
| 193 | + } |
194 | 194 | } |
0 commit comments