Skip to content

Commit 2311a0f

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

7 files changed

Lines changed: 274 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: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
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+
if (!stateValues.containsKey(state)){
45+
evaluateState(state);
46+
}
47+
return stateValues.get(state).get(labelList.getLabelIndex(label));
48+
}
49+
50+
/**
51+
* This method provides all label values concerning a given state. <br>
52+
* It will evaluate all the Labels if necessary.
53+
* @param state The state to evaluate in.
54+
* @return Returns a {@link Map} containing all label-values for the given state, indexed by their name.
55+
* @throws PrismLangException In case a label couldn't be evaluated.
56+
*/
57+
public Map<String, Boolean> getLabelValues(State state) throws PrismLangException
58+
{
59+
// evaluate labels if necessary
60+
if (!stateValues.containsKey(state)){
61+
evaluateState(state);
62+
}
63+
// convert BitSet to Map to provide intuitiv interface
64+
BitSet value = stateValues.get(state);
65+
int numLabels = labelList.size();
66+
Map<String, Boolean> labelValueMap = new HashMap<>();
67+
for (int i = 0; i < numLabels; i++){
68+
labelValueMap.put(labelList.getLabelName(i), value.get(i));
69+
}
70+
return labelValueMap;
71+
}
72+
73+
/**
74+
* This method provides all values of a certain label. They will be ordered by the given statesList. <br>
75+
* States will be evaluated if necessary.
76+
* @param label The name of the label.
77+
* @param statesList The states to evaluate against in correct order.
78+
* @return All values of the label.
79+
* @throws PrismException
80+
*/
81+
public BitSet getLabel(String label, List<State> statesList) throws PrismException
82+
{
83+
int statesNum = statesList.size();
84+
int labelIndex = labelList.getLabelIndex(label);
85+
BitSet labelValues = new BitSet(statesNum);
86+
for (int i = 0; i < statesNum; i++) {
87+
State state = statesList.get(i);
88+
if (!stateValues.containsKey(state)){
89+
evaluateState(state);
90+
}
91+
BitSet valuesOfState = stateValues.get(state);
92+
labelValues.set(i, valuesOfState.get(labelIndex));
93+
}
94+
return labelValues;
95+
}
96+
97+
/**
98+
* Evaluates all label with the given state. <br>
99+
*
100+
* @param state The state to evaluate the labels in.
101+
* @return A map of the values.
102+
* @throws PrismLangException In case an evaluation fails.
103+
*/
104+
private void evaluateState(State state) throws PrismLangException
105+
{
106+
int numLabels = labelList.size();
107+
Map<String, Boolean> labelValues = new HashMap<>(numLabels);
108+
BitSet values = new BitSet(numLabels);
109+
for (int labelIndex = 0; labelIndex < numLabels; labelIndex++) {
110+
boolean labelValue = evaluateLabel(labelList.getLabelName(labelIndex), labelValues, state);
111+
values.set(labelIndex, labelValue);
112+
}
113+
stateValues.put(state, values);
114+
}
115+
116+
/**
117+
* Helper function to recursively evaluate label values. The value will be stored inside the given map.
118+
*
119+
* @param name The name of the label.
120+
* @param labelValues The already known values of all labels.
121+
*/
122+
private boolean evaluateLabel(String name, Map<String, Boolean> labelValues, State state) throws PrismLangException
123+
{
124+
// check if value is already known
125+
if (labelValues.containsKey(name)) {
126+
return labelValues.get(name);
127+
}
128+
// get expression
129+
Expression label = labelList.getLabel(labelList.getLabelIndex(name));
130+
// check if all the (other) label dependencies are evaluated
131+
for (String dependency : label.getAllLabels()){
132+
if (!labelValues.containsKey(dependency)){
133+
// evaluate other label first
134+
evaluateLabel(dependency, labelValues, state);
135+
}
136+
}
137+
// all dependencies are fulfilled
138+
boolean labelValue = label.evaluateBoolean(null, labelValues, state);
139+
labelValues.put(name, labelValue);
140+
return labelValue;
141+
}
142+
}

‎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)