Skip to content

Commit a7583ed

Browse files
maxkurze1maxkurze1
committed
moving label-evalution and -caching to new class
1 parent 7c57555 commit a7583ed

7 files changed

Lines changed: 279 additions & 230 deletions

File tree

‎prism/src/parser/ast/LabelList.java‎

Lines changed: 0 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -89,50 +89,6 @@ public void findCycles() throws PrismLangException
8989
}
9090
}
9191

92-
/**
93-
* Evaluates all label with the given state. <br>
94-
*
95-
* @param currentState The state to evaluate the labels in.
96-
* @return A map of the values.
97-
* @throws PrismLangException In case an evaluation fails.
98-
*/
99-
public Map<String, Boolean> getLabelValues(State currentState) throws PrismLangException
100-
{
101-
Map<String, Boolean> labelValues = new HashMap<>(labels.size());
102-
103-
for (String label : names) {
104-
evaluateLabel(label, labelValues, currentState);
105-
}
106-
107-
return labelValues;
108-
}
109-
110-
/**
111-
* Helper function to recursively evaluate label values. The value will be stored inside the given map.
112-
*
113-
* @param name The name of the label.
114-
* @param labelValues The already known values of all labels.
115-
*/
116-
private void evaluateLabel(String name, Map<String, Boolean> labelValues, State state) throws PrismLangException
117-
{
118-
// check if value is already known
119-
if (labelValues.containsKey(name)) {
120-
return;
121-
}
122-
// get expression
123-
Expression label = labels.get(names.indexOf(name));
124-
// check if all the (other) label dependencies are evaluated
125-
for (String dependency : label.getAllLabels()){
126-
if (!labelValues.containsKey(dependency)){
127-
// evaluate other label first
128-
evaluateLabel(dependency, labelValues, state);
129-
}
130-
}
131-
// all dependencies are fulfilled
132-
labelValues.put(name, label.evaluateBoolean(null, labelValues, state));
133-
}
134-
135-
13692
// Set methods
13793
public void addLabel(ExpressionIdent n, Expression l)
13894
{

‎prism/src/simulator/LabelEvaluater.java‎

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
package simulator;
2+
3+
4+
import parser.State;
5+
import parser.ast.Expression;
6+
import parser.ast.LabelList;
7+
import prism.PrismException;
8+
import prism.PrismLangException;
9+
10+
import java.util.BitSet;
11+
import java.util.HashMap;
12+
import java.util.List;
13+
import java.util.Map;
14+
15+
/**
16+
* This class will evaluate labels. Therefore, it's wrapped around a {@link LabelList}.
17+
* <br>
18+
* It also caches the results.
19+
*/
20+
public class LabelEvaluater
21+
{
22+
/** Map of each evaluated state and a bitset containing the label-values ordered as in labelList */
23+
Map<State, BitSet> stateValues = new HashMap<>();
24+
/** The labelList that will be evaluated */
25+
LabelList labelList;
26+
27+
/**
28+
* Creates new object that will evaluate and cache the given {@link LabelList}.
29+
*/
30+
public LabelEvaluater(LabelList labelList)
31+
{
32+
this.labelList = labelList;
33+
}
34+
35+
/**
36+
* Returns the value of a specific label in a specific state.
37+
* @param state The state to evaluate in.
38+
* @param label The label that will be evaluated.
39+
* @return The value of the Label.
40+
* @throws PrismLangException In case a label couldn't be evaluated.
41+
*/
42+
public boolean getLabelValue(State state, String label) throws PrismLangException
43+
{
44+
return getStateValues(state).get(labelList.getLabelIndex(label));
45+
}
46+
47+
/**
48+
* This method provides all label values concerning a given state. <br>
49+
* It will evaluate all the Labels if necessary.
50+
* @param state The state to evaluate in.
51+
* @return Returns a {@link Map} containing all label-values for the given state, indexed by their name.
52+
* @throws PrismLangException In case a label couldn't be evaluated.
53+
*/
54+
public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
55+
{
56+
// convert BitSet to Map to provide intuitiv interface
57+
BitSet value = getStateValues(state);
58+
Map<String, Boolean> labelValueMap = new HashMap<>();
59+
for (int i = 0, numLabels = labelList.size(); i < numLabels; i++){
60+
labelValueMap.put(labelList.getLabelName(i), value.get(i));
61+
}
62+
return labelValueMap;
63+
}
64+
65+
/**
66+
* This method provides all values of a certain label. They will be ordered by the given statesList. <br>
67+
* States will be evaluated if necessary.
68+
* @param label The name of the label.
69+
* @param statesList The states to evaluate against in correct order.
70+
* @return All values of the label.
71+
* @throws PrismException In case a label evaluation fails.
72+
*/
73+
public BitSet getLabel(String label, List<State> statesList) throws PrismException
74+
{
75+
int statesNum = statesList.size();
76+
int labelIndex = labelList.getLabelIndex(label);
77+
BitSet labelValues = new BitSet();
78+
for (int i = statesNum-1; i >= 0; i--) {
79+
State state = statesList.get(i);
80+
BitSet valuesOfState = getStateValues(state);
81+
labelValues.set(i, valuesOfState.get(labelIndex));
82+
}
83+
return labelValues;
84+
}
85+
86+
/**
87+
* This method provides all label values of a certain state as a {@link BitSet}.
88+
* The labels are indexed in the same order as inside the {@link LabelEvaluater#labelList}
89+
* @param state The state to evaluate in.
90+
* @return Always returns a BitSet with the label values.
91+
* @throws PrismLangException In case a label evaluation fails.
92+
*/
93+
protected BitSet getStateValues(State state) throws PrismLangException
94+
{
95+
BitSet values = stateValues.get(state);
96+
if (values == null) {
97+
values = evaluateState(state);
98+
stateValues.put(state, values);
99+
}
100+
return values;
101+
}
102+
103+
/**
104+
* Evaluates all label with the given state. <br>
105+
*
106+
* @param state The state to evaluate the labels in.
107+
* @return A {@link BitSet} of all label values in this state.
108+
* @throws PrismLangException In case a label evaluation fails.
109+
*/
110+
private BitSet evaluateState(State state) throws PrismLangException
111+
{
112+
int numLabels = labelList.size();
113+
Map<String, Boolean> labelValues = new HashMap<>(numLabels);
114+
BitSet values = new BitSet();
115+
for (int labelIndex = numLabels; labelIndex >= 0; labelIndex--) {
116+
boolean labelValue = evaluateLabel(labelList.getLabelName(labelIndex), labelValues, state);
117+
values.set(labelIndex, labelValue);
118+
}
119+
stateValues.put(state, values);
120+
return values;
121+
}
122+
123+
/**
124+
* Helper function to recursively evaluate label values. The value will be stored inside the given map.
125+
*
126+
* @param name The name of the label.
127+
* @param labelValues The already known values of all labels.
128+
*/
129+
private boolean evaluateLabel(String name, Map<String, Boolean> labelValues, State state) throws PrismLangException
130+
{
131+
// check if value is already known
132+
if (labelValues.containsKey(name)) {
133+
return labelValues.get(name);
134+
}
135+
// get expression
136+
Expression label = labelList.getLabel(labelList.getLabelIndex(name));
137+
// check if all the (other) label dependencies are evaluated
138+
for (String dependency : label.getAllLabels()){
139+
// evaluate other label first
140+
evaluateLabel(dependency, labelValues, state);
141+
}
142+
// all dependencies are fulfilled
143+
boolean labelValue = label.evaluateBoolean(null, labelValues, state);
144+
labelValues.put(name, labelValue);
145+
return labelValue;
146+
}
147+
}

‎prism/src/simulator/LabelsCache.java‎

Lines changed: 0 additions & 73 deletions
This file was deleted.

‎prism/src/simulator/ModulesFileModelGenerator.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
4949
protected boolean transitionListBuilt;
5050

5151
// label value cache
52-
protected LabelsCache labelsCache;
52+
protected LabelEvaluater labelsCache;
5353

5454
/**
5555
* Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance.
@@ -107,7 +107,7 @@ private void initialise() throws PrismException
107107
labelNames = labelList.getLabelNames();
108108

109109
// create label-cache
110-
labelsCache = new LabelsCache(labelList);
110+
labelsCache = new LabelEvaluater(labelList);
111111

112112
// Create data structures for exploring model
113113
updater = new Updater(modulesFile, varList, parent);

‎prism/src/simulator/ModulesFileModelGeneratorSymbolic.java‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,9 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
6666
boolean symbolic = false;
6767
protected ModelBuilder modelBuilder;
6868
protected FunctionFactory functionFactory;
69+
70+
// label value cache
71+
protected LabelEvaluater labelsCache;
6972

7073
/**
7174
* Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance.
@@ -122,7 +125,10 @@ private void initialise() throws PrismException
122125
varList = modulesFile.createVarList();
123126
labelList = modulesFile.getLabelList();
124127
labelNames = labelList.getLabelNames();
125-
128+
129+
// create label-cache
130+
labelsCache = new LabelEvaluater(labelList);
131+
126132
// Create data structures for exploring model
127133
//updater = new Updater(modulesFile, varList, parent);
128134
//transitionList = new TransitionList();
@@ -445,7 +451,7 @@ public State computeTransitionTarget(int index, int offset) throws PrismExceptio
445451
@Override
446452
public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
447453
{
448-
return labelList.getLabelValues(state);
454+
return labelsCache.getLabelValues(state);
449455
}
450456

451457
// Methods for RewardGenerator interface

0 commit comments

Comments
 (0)