Skip to content

Commit

Permalink
Update some VarList methods to respect current evaluation mode.
Browse files Browse the repository at this point in the history
Notably these methods are used to handle models with initial states.
  • Loading branch information
davexparker committed Mar 6, 2024
1 parent bd9b0aa commit 95bdff3
Showing 1 changed file with 21 additions and 15 deletions.
36 changes: 21 additions & 15 deletions prism/src/parser/VarList.java
Original file line number Diff line number Diff line change
Expand Up @@ -298,21 +298,27 @@ public int getTotalNumBits()
}

/**
* Get the value (as an Object) for the ith variable, from its encoding as an integer.
* Get the value (as an Object) for the ith variable, from its encoding as an integer.
* In case of any problems, this will return null.
*/
public Object decodeFromInt(int i, int val)
{
Type type = getType(i);
// Integer type
if (type instanceof TypeInt) {
return val + getLow(i);
}
// Boolean type
else if (type instanceof TypeBool) {
return val != 0;
try {
Type type = getType(i);
// Integer type
if (type instanceof TypeInt) {
return type.castValueTo(val + getLow(i), ec.getEvaluationMode());
}
// Boolean type
else if (type instanceof TypeBool) {
return val != 0;
}
// Unknown
return null;
} catch (PrismLangException e) {
// In case of any error return null
return null;
}
// Anything else
return null;
}

/**
Expand Down Expand Up @@ -411,10 +417,10 @@ public List<Values> getAllValues(List<String> vars) throws PrismLangException
vals = allValues.get(j);
for (k = lo + 1; k < hi + 1; k++) {
valsNew = new Values(vals);
valsNew.setValue(var, k);
valsNew.setValue(var, getType(i).castValueTo(k, ec.getEvaluationMode()));
allValues.add(valsNew);
}
vals.addValue(var, lo);
vals.addValue(var, getType(i).castValueTo(lo, ec.getEvaluationMode()));
}
} else {
throw new PrismLangException("Cannot determine all values for a variable of type " + getType(i));
Expand Down Expand Up @@ -453,10 +459,10 @@ public List<State> getAllStates() throws PrismLangException
state = allStates.get(j);
for (int k = lo + 1; k < hi + 1; k++) {
stateNew = new State(state);
stateNew.setValue(i, k);
stateNew.setValue(i, getType(i).castValueTo(k, ec.getEvaluationMode()));
allStates.add(stateNew);
}
state.setValue(i, lo);
state.setValue(i, getType(i).castValueTo(lo, ec.getEvaluationMode()));
}
} else {
throw new PrismLangException("Cannot determine all values for a variable of type " + getType(i));
Expand Down

0 comments on commit 95bdff3

Please sign in to comment.