diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 090994bb9..07620491b 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -13,7 +13,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/SimpleValuation.h"
-#include "storm/storage/expressions/ExprTkEvaluator.h"
+#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
#include "src/storage/BitVectorHashMap.h"
#include "src/utility/PrismUtility.h"
#include "src/models/AbstractModel.h"
@@ -58,37 +58,56 @@ namespace storm {
// A structure storing information about the used variables of the program.
struct VariableInformation {
- uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) {
+ struct BooleanVariableInformation {
+ BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
+ // Intentionally left empty.
+ }
+
+ storm::expressions::Variable variable;
+ bool initialValue;
+ uint_fast64_t bitOffset;
+ };
+
+ struct IntegerVariableInformation {
+ IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
+ // Intentionally left empty.
+ }
+
+ storm::expressions::Variable variable;
+ int_fast64_t initialValue;
+ int_fast64_t lowerBound;
+ int_fast64_t upperBound;
+ uint_fast64_t bitOffset;
+ uint_fast64_t bitWidth;
+ };
+
+ uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const {
auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
if (booleanIndex != booleanVariableToIndexMap.end()) {
- return std::get<2>(booleanVariables[booleanIndex]);
+ return booleanVariables[booleanIndex].bitOffset;
}
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
- return std::get<4>(integerVariables[integerIndex]);
+ return integerVariables[integerIndex].bitOffset;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
}
- uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) {
+ uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const {
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
- return std::get<5>(integerVariables[integerIndex]);
+ return integerVariables[integerIndex].bitWidth;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
}
+ // The list of boolean variables.
std::map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
-
- // The list of boolean variables. Along with the variable we store its initial value and bit offset in
- // the state.
- std::vector<std::tuple<storm::expressions::Variable, bool, uint_fast64_t>> booleanVariables;
+ std::vector<BooleanVariableInformation> booleanVariables;
+ // The list of integer variables.
std::map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
-
- // The list of integer variables. Along with the variable, we store its initial value, lower and upper
- // bound, the bit offset in the state and the bit width.
- std::vector<std::tuple<storm::expressions::Variable, int_fast64_t, int_fast64_t, int_fast64_t, uint_fast64_t, uint_fast64_t>> integerVariables;
+ std::vector<IntegerVariableInformation> integerVariables;
};
// A structure holding the individual components of a model.
@@ -174,17 +193,12 @@ namespace storm {
}
private:
- void unpackState(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprTkEvaluator& evaluator) {
+ static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator) {
for (auto const& booleanVariable : variableInformation.booleanVariables) {
- if (currentState.get(std::get<2>(booleanVariable))) {
- evaluator.setBoolean(std::get<0>(booleanVariable), true);
- } else {
- evaluator.setBooleanValue(std::get<0>(booleanVariable), false);
- }
+ evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
}
for (auto const& integerVariable : variableInformation.integerVariables) {
- int_fast64_t value = currentState.getAsInt(std::get<4>(integerVariable), std::get<5>(integerVariable));
- evaluator.setIntegerValue(std::get<0>(integerVariable), value);
+ evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
}
@@ -196,8 +210,8 @@ namespace storm {
* @params update The update to apply.
* @return The resulting state.
*/
- static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::prism::Update const& update) {
- return applyUpdate(variableInformation, state, state, update);
+ static StateType applyUpdate(VariableInformation const& variableInformation, StateType const& state, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator) {
+ return applyUpdate(variableInformation, state, state, update, evaluator);
}
/*!
@@ -210,23 +224,33 @@ namespace storm {
* @param update The update to apply.
* @return The resulting state.
*/
- static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) {
- StateType* newState = new StateType(*state);
-
- int_fast64_t newValue = 0;
- for (auto const& assignment : update.getAssignments()) {
- if (assignment.getExpression().hasBooleanType()) {
- newState->setBooleanValue(assignment.getVariable(), assignment.getExpression().evaluateAsBool(baseState));
- } else if (assignment.getExpression().hasIntegerType()) {
- newValue = assignment.getExpression().evaluateAsInt(baseState);
- auto const& boundsPair = variableInformation.variableToBoundsMap.find(assignment.getVariableName());
- STORM_LOG_THROW(boundsPair->second.first <= newValue && newValue <= boundsPair->second.second, storm::exceptions::InvalidArgumentException, "Invalid value " << newValue << " for variable '" << assignment.getVariableName() << "'.");
- newState->setIntegerValue(assignment.getVariable(), newValue);
- } else {
- STORM_LOG_ASSERT(false, "Invalid type '" << assignment.getExpression().getType() << "' of assignment.");
+ static StateType applyUpdate(VariableInformation const& variableInformation, StateType const& state, StateType const& baseState, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator) {
+ StateType newState(state);
+
+ auto assignmentIt = update.getAssignments().begin();
+ auto assignmentIte = update.getAssignments().end();
+
+ // Iterate over all boolean assignments and carry them out.
+ auto boolIt = variableInformation.booleanVariables.begin();
+ for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
+ while (assignmentIt->getVariable() != boolIt->variable) {
+ ++boolIt;
}
+ newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression()));
}
+ // Iterate over all integer assignments and carry them out.
+ auto integerIt = variableInformation.integerVariables.begin();
+ for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
+ while (assignmentIt->getVariable() != integerIt->variable) {
+ ++integerIt;
+ }
+ newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, evaluator.asInt(assignmentIt->getExpression()) - integerIt->lowerBound);
+ }
+
+ // Check that we processed all assignments.
+ STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
+
return newState;
}
@@ -244,11 +268,11 @@ namespace storm {
uint32_t newIndex = stateInformation.reachableStates.size();
// Check, if the state was already registered.
- std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAdd(state, newIndex);
+ std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAddAndGetBucket(state, newIndex);
if (actualIndexBucketPair.first == newIndex) {
- stateQueue.insert(actualIndexBucketPair.second);
- reachableStates.push_back(actualIndexBucketPair.second);
+ stateQueue.push(actualIndexBucketPair.second);
+ stateInformation.reachableStates.push_back(actualIndexBucketPair.second);
}
return actualIndexBucketPair.first;
@@ -270,7 +294,7 @@ namespace storm {
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
- static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) {
+ static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExprtkExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
// Iterate over all modules.
@@ -295,7 +319,7 @@ namespace storm {
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
- if (command.getGuardExpression().evaluateAsBool(state)) {
+ if (evaluator.asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
@@ -311,10 +335,8 @@ namespace storm {
return result;
}
- static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
+ static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<std::size_t>& stateQueue) {
std::vector<Choice<ValueType>> result;
-
- StateType const* currentState = stateInformation.reachableStates[stateIndex];
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
@@ -328,7 +350,7 @@ namespace storm {
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
- if (!command.getGuardExpression().evaluateAsBool(currentState)) {
+ if (!evaluator.asBool(command.getGuardExpression())) {
continue;
}
@@ -336,25 +358,17 @@ namespace storm {
Choice<ValueType>& choice = result.back();
choice.addChoiceLabel(command.getGlobalIndex());
- double probabilitySum = 0;
// Iterate over all updates of the current command.
+ double probabilitySum = 0;
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(k);
- // Obtain target state index.
- std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation);
-
- // If the state has not been discovered yet, add it to the queue of states to be explored.
- if (!flagTargetStateIndexPair.first) {
- stateQueue.push(flagTargetStateIndexPair.second);
- }
+ // Obtain target state index and add it to the list of known states. If it has not yet been
+ // seen, we also add it to the set of states that have yet to be explored.
+ uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), stateInformation, stateQueue);
// Update the choice by adding the probability/target state to it.
- double probabilityToAdd = update.getLikelihoodExpression().evaluateAsDouble(currentState);
- probabilitySum += probabilityToAdd;
- boost::container::flat_set<uint_fast64_t> labels;
- labels.insert(update.getGlobalIndex());
- addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, labels);
+ choice.addProbability(stateIndex, evaluator.asDouble(update.getLikelihoodExpression()));
}
// Check that the resulting distribution is in fact a distribution.
@@ -365,12 +379,11 @@ namespace storm {
return result;
}
- static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
+ static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<std::size_t>& stateQueue) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getActionIndices()) {
- StateType const* currentState = stateInformation.reachableStates[stateIndex];
- boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, currentState, actionIndex);
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
@@ -385,9 +398,9 @@ namespace storm {
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
- std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>* currentTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
- std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>* newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
- (*currentTargetStates)[new StateType(*currentState)] = storm::storage::LabeledValues<double>(1.0);
+ std::unordered_map<StateType, ValueType>* currentTargetStates = new std::unordered_map<StateType, ValueType>();
+ std::unordered_map<StateType, ValueType>* newTargetStates = new std::unordered_map<StateType, ValueType>();
+ currentTargetStates->emplace(currentState, storm::utility::one<ValueType>());
// FIXME: This does not check whether a global variable is written multiple times. While the
// behaviour for this is undefined anyway, a warning should be issued in that case.
@@ -398,40 +411,17 @@ namespace storm {
storm::prism::Update const& update = command.getUpdate(j);
for (auto const& stateProbabilityPair : *currentTargetStates) {
- StateType* newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update);
-
- storm::storage::LabeledValues<double> newProbability;
-
- double updateProbability = update.getLikelihoodExpression().evaluateAsDouble(currentState);
- for (auto const& valueLabelSetPair : stateProbabilityPair.second) {
- // Copy the label set, so we can modify it.
- boost::container::flat_set<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
- newLabelSet.insert(update.getGlobalIndex());
-
- newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet);
- }
-
- auto existingStateProbabilityPair = newTargetStates->find(newTargetState);
- if (existingStateProbabilityPair == newTargetStates->end()) {
- (*newTargetStates)[newTargetState] = newProbability;
- } else {
- existingStateProbabilityPair->second += newProbability;
-
- // If the state was already seen in one of the other updates, we need to delete this copy.
- delete newTargetState;
- }
+ // Compute the new state under the current update and add it to the set of new target states.
+ StateType newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update, evaluator);
+ newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asDouble(update.getLikelihoodExpression()));
}
}
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
- for (auto const& stateProbabilityPair : *currentTargetStates) {
- delete stateProbabilityPair.first;
- }
-
delete currentTargetStates;
currentTargetStates = newTargetStates;
- newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
+ newTargetStates = new std::unordered_map<StateType, ValueType>();
}
}
@@ -450,17 +440,8 @@ namespace storm {
double probabilitySum = 0;
for (auto const& stateProbabilityPair : *newTargetStates) {
- std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation);
-
- // If the state has not been discovered yet, add it to the queue of states to be explored.
- if (!flagTargetStateIndexPair.first) {
- stateQueue.push(flagTargetStateIndexPair.second);
- }
-
- for (auto const& probabilityLabelPair : stateProbabilityPair.second) {
- addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second);
- probabilitySum += probabilityLabelPair.first;
- }
+ uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue);
+ choice.addProbability(actualIndex, stateProbabilityPair.second);
}
// Check that the resulting distribution is in fact a distribution.
@@ -518,18 +499,10 @@ namespace storm {
// We need to initialize the values of the variables to their initial value.
for (auto const& booleanVariable : variableInformation.booleanVariables) {
- initialState.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable));
+ initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
}
for (auto const& integerVariable : variableInformation.integerVariables) {
- initialState.set(std::get<4>(integerVariable), std::get<5>(integerVariable), std::get<1>(integerVariable) - std::get<2>(integerVariable));
- }
- for (auto const& module : program.getModules()) {
- for (auto const& booleanVariable : module.getBooleanVariables()) {
- initialState.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable));
- }
- for (auto const& integerVariable : module.getIntegerVariables()) {
- initialState.set(std::get<4>(integerVariable), std::get<5>(integerVariable), std::get<1>(integerVariable) - std::get<2>(integerVariable));
- }
+ initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
}
// Insert the initial state in the global state to index mapping and state queue.
@@ -537,16 +510,17 @@ namespace storm {
// Now explore the current state until there is no more reachable state.
uint_fast64_t currentRow = 0;
- storm::expressions::ExprTkEvaluator evaluator(program.getManager());
+ storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager());
while (!stateQueue.empty()) {
// Get the current state and unpack it.
- std::size_t currentStateIndex = stateQueue.front();
- storm::storage::BitVector currentState = stateInformation.stateToIndexMap.getBucket(currentStateIndex);
- unpackState(currentState, variableInformation, evaluator);
+ std::size_t currentStateBucket = stateQueue.front();
+ std::pair<storm::storage::BitVector, uint32_t> stateValuePair = stateInformation.stateToIndexMap.getBucketAndValue(currentStateBucket);
+ storm::storage::BitVector const& currentState = stateValuePair.first;
+ unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
// Retrieve all choices for the current state.
- std::vector<Choice<ValueType>> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue);
- std::vector<Choice<ValueType>> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue);
+ std::vector<Choice<ValueType>> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue);
+ std::vector<Choice<ValueType>> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue);
uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
@@ -556,7 +530,7 @@ namespace storm {
if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
// Insert empty choice labeling for added self-loop transitions.
choiceLabels.push_back(boost::container::flat_set<uint_fast64_t>());
- transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne<ValueType>());
+ transitionMatrixBuilder.addNextValue(currentRow, stateValuePair.second, storm::utility::one<ValueType>());
++currentRow;
} else {
LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
@@ -567,8 +541,7 @@ namespace storm {
// or compose them to one choice.
if (deterministicModel) {
Choice<ValueType> globalChoice;
- std::map<uint_fast64_t, ValueType> stateToRewardMap;
- boost::container::flat_set<uint_fast64_t> allChoiceLabels;
+ std::map<uint32_t, ValueType> stateToRewardMap;
// Combine all the choices and scale them with the total number of choices of the current state.
for (auto const& choice : allUnlabeledChoices) {
@@ -578,8 +551,8 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
- if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
- stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
+ if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) {
+ stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression()));
}
}
}
@@ -591,8 +564,8 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
- if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
- stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
+ if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) {
+ stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression()));
}
}
}
@@ -629,8 +602,8 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
- if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
- stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
+ if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) {
+ stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression()));
}
}
@@ -656,8 +629,8 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
- if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
- stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
+ if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) {
+ stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression()));
}
}
@@ -696,7 +669,7 @@ namespace storm {
for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
++bitOffset;
- booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
+ variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
}
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
@@ -704,13 +677,13 @@ namespace storm {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound)));
variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
bitOffset += bitwidth;
- integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
+ variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
}
for (auto const& module : program.getModules()) {
for (auto const& booleanVariable : module.getBooleanVariables()) {
variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
++bitOffset;
- booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
+ variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
}
for (auto const& integerVariable : module.getIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
@@ -718,7 +691,7 @@ namespace storm {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound)));
variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
bitOffset += bitwidth;
- integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
+ variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
}
}
@@ -743,12 +716,7 @@ namespace storm {
modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);
// Finally, construct the state rewards.
- modelComponents.stateRewards = buildStateRewards(rewardModel.getStateRewards(), stateInformation);
-
- // After everything has been created, we can delete the states.
- for (auto state : stateInformation.reachableStates) {
- delete state;
- }
+ modelComponents.stateRewards = buildStateRewards(program, variableInformation, rewardModel.getStateRewards(), stateInformation);
return modelComponents;
}
@@ -762,6 +730,8 @@ namespace storm {
* @return The state labeling of the given program.
*/
static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
+ storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager());
+
std::vector<storm::prism::Label> const& labels = program.getLabels();
storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1);
@@ -772,8 +742,10 @@ namespace storm {
}
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
for (auto const& label : labels) {
+ unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator);
+
// Add label to state, if the corresponding expression is true.
- if (label.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
+ if (evaluator.asBool(label.getStatePredicateExpression())) {
result.addAtomicPropositionToState(label.getName(), index);
}
}
@@ -795,14 +767,18 @@ namespace storm {
* @param stateInformation Information about the state space.
* @return A vector containing the state rewards for the state space.
*/
- static std::vector<ValueType> buildStateRewards(std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) {
+ static std::vector<ValueType> buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) {
+ storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager());
+
std::vector<ValueType> result(stateInformation.reachableStates.size());
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
result[index] = ValueType(0);
for (auto const& reward : rewards) {
+ unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator);
+
// Add this reward to the state if the state is included in the state reward.
- if (reward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
- result[index] += ValueType(reward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates[index]));
+ if (evaluator.asBool(reward.getStatePredicateExpression())) {
+ result[index] += ValueType(evaluator.asDouble(reward.getRewardValueExpression()));
}
}
}
diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp
index f6598a7a2..9c458ea7b 100644
--- a/src/storage/BitVector.cpp
+++ b/src/storage/BitVector.cpp
@@ -131,7 +131,7 @@ namespace storm {
return *this;
}
- bool BitVector::operator==(BitVector const& other) {
+ bool BitVector::operator==(BitVector const& other) const {
// If the lengths of the vectors do not match, they are considered unequal.
if (this->bitCount != other.bitCount) return false;
@@ -146,7 +146,7 @@ namespace storm {
return true;
}
- bool BitVector::operator!=(BitVector const& other) {
+ bool BitVector::operator!=(BitVector const& other) const {
return !(*this == other);
}
@@ -648,7 +648,7 @@ namespace storm {
}
namespace std {
- std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bv) {
+ std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bv) const {
return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end());
}
}
\ No newline at end of file
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index f5b0f6de9..0312f39f9 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -138,7 +138,7 @@ namespace storm {
* @param other The bitvector with which to compare the current one.
* @return True iff the other bit vector is semantically the same as the current one.
*/
- bool operator==(BitVector const& other);
+ bool operator==(BitVector const& other) const;
/*!
* Compares the given bit vector with the current one.
@@ -146,7 +146,7 @@ namespace storm {
* @param other The bitvector with which to compare the current one.
* @return True iff the other bit vector is semantically not the same as the current one.
*/
- bool operator!=(BitVector const& other);
+ bool operator!=(BitVector const& other) const;
/*!
* Assigns the contents of the given bit vector to the current bit vector via a deep copy.
@@ -494,7 +494,7 @@ namespace storm {
namespace std {
template <>
struct hash<storm::storage::BitVector> {
- std::size_t operator()(storm::storage::BitVector const& bv);
+ std::size_t operator()(storm::storage::BitVector const& bv) const;
};
}
diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index 1bb77bc6b..d02ce69a2 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -21,7 +21,7 @@ namespace storm {
}
template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::isBucketOccupied(uint_fast64_t bucket) {
+ bool BitVectorHashMap<ValueType, Hash1, Hash2>::isBucketOccupied(uint_fast64_t bucket) const {
return occupied.get(bucket);
}
@@ -66,37 +66,48 @@ namespace storm {
this->increaseSize();
}
+ std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
+ if (flagBucketPair.first) {
+ return std::make_pair(values[flagBucketPair.second], flagBucketPair.second);
+ } else {
+ // Insert the new bits into the bucket.
+ buckets.set(flagBucketPair.second * bucketSize, key);
+ occupied.set(flagBucketPair.second);
+ values[flagBucketPair.second] = value;
+ ++numberOfElements;
+ return std::make_pair(value, flagBucketPair.second);
+ }
+ }
+
+ template<class ValueType, class Hash1, class Hash2>
+ ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const {
+ std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
+ STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key.");
+ return flagBucketPair.second;
+ }
+
+ template<class ValueType, class Hash1, class Hash2>
+ std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucket(storm::storage::BitVector const& key) const {
uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator;
uint_fast64_t bucket = initialHash;
while (isBucketOccupied(bucket)) {
if (buckets.matches(bucket * bucketSize, key)) {
- return std::make_pair(values[bucket], bucket);
+ return std::make_pair(true, bucket);
}
bucket += hasher2(key);
bucket %= *currentSizeIterator;
-
- // If we arrived at the original position, this means that we have visited all possible locations, but
- // could not find a suitable position. This implies that we have to enlarge the map in order to resolve
- // the issue.
- if (bucket == initialHash) {
- this->increaseSize();
- }
}
-
- // Insert the new bits into the bucket.
- buckets.set(bucket * bucketSize, key);
- occupied.set(bucket);
- values[bucket] = value;
- ++numberOfElements;
- return std::make_pair(value, bucket);
+
+ return std::make_pair(false, bucket);
}
template<class ValueType, class Hash1, class Hash2>
- storm::storage::BitVector BitVectorHashMap<ValueType, Hash1, Hash2>::getBucket(std::size_t bucket) const {
- return buckets.get(bucket * bucketSize, bucketSize);
+ std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::getBucketAndValue(std::size_t bucket) const {
+ return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);
}
template class BitVectorHashMap<uint_fast64_t>;
+ template class BitVectorHashMap<uint32_t>;
}
}
diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h
index bea8fcbbc..9d6ea299f 100644
--- a/src/storage/BitVectorHashMap.h
+++ b/src/storage/BitVectorHashMap.h
@@ -50,12 +50,20 @@ namespace storm {
std::pair<ValueType, std::size_t> findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value);
/*!
- * Retrieves the key stored in the given bucket (if any).
+ * Retrieves the key stored in the given bucket (if any) and the value it is mapped to.
*
* @param bucket The index of the bucket.
- * @return The content of the named bucket.
+ * @return The content and value of the named bucket.
*/
- storm::storage::BitVector getBucket(std::size_t bucket) const;
+ std::pair<storm::storage::BitVector, ValueType> getBucketAndValue(std::size_t bucket) const;
+
+ /*!
+ * Retrieves the value associated with the given key (if any). If the key does not exist, the behaviour is
+ * undefined.
+ *
+ * @return The value associated with the given key (if any).
+ */
+ ValueType getValue(storm::storage::BitVector const& key) const;
/*!
* Retrieves the size of the map in terms of the number of key-value pairs it stores.
@@ -78,7 +86,16 @@ namespace storm {
* @param bucket The bucket to check.
* @return True iff the bucket is occupied.
*/
- bool isBucketOccupied(uint_fast64_t bucket);
+ bool isBucketOccupied(uint_fast64_t bucket) const;
+
+ /*!
+ * Searches for the bucket into which the given key can be inserted.
+ *
+ * @param key The key to search for.
+ * @return A pair whose first component indicates whether the key is already contained in the map and whose
+ * second component indicates in which bucket the key is stored/is supposed to be stored.
+ */
+ std::pair<bool, std::size_t> findBucket(storm::storage::BitVector const& key) const;
/*!
* Increases the size of the hash map and performs the necessary rehashing of all entries.
diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h
deleted file mode 100644
index 58f58f68b..000000000
--- a/src/storage/LabeledValues.h
+++ /dev/null
@@ -1,211 +0,0 @@
-/*
- * LabeledValues.h
- *
- * Created on: 26.09.2013
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_STORAGE_LABELEDVALUES_H
-#define STORM_STORAGE_LABELEDVALUES_H
-
-#include <list>
-#include <boost/container/flat_set.hpp>
-
-namespace storm {
- namespace utility {
- template<class ValueType>
- static ValueType constantZero();
- }
-
- namespace storage {
- // This class provides the functionality to store a list of values, each of which is labeled with possibly several
- // labels.
- template<class ValueType>
- class LabeledValues {
- public:
- /*!
- * Default-constructs an empty object.
- */
- explicit LabeledValues() : valueLabelList() {
- // Intentionally left empty.
- }
-
- /*!
- * Constructs an object that stores the single probability value without any label.
- *
- * @param value The probability to sto
- */
- explicit LabeledValues(ValueType value) : valueLabelList() {
- addValue(value);
- }
-
- /*!
- * Adds an (unlabeled) value to the list of labeled values.
- *
- * @param value The value to add.
- * @return A reference to the list of labels that is associated with the given value.
- */
- boost::container::flat_set<uint_fast64_t>& addValue(ValueType value) {
- valueLabelList.emplace_back(value, boost::container::flat_set<uint_fast64_t>());
- return valueLabelList.back().second;
- }
-
- /*!
- * Adds a labeled value to the list of labeled values.
- *
- * @param value The value to add.
- * @param labels The labels to associate with this value.
- * @return A reference to the list of labels that is associated with the given value.
- */
- boost::container::flat_set<uint_fast64_t>& addValue(ValueType value, boost::container::flat_set<uint_fast64_t> const& labels) {
- valueLabelList.emplace_back(value, labels);
- return valueLabelList.back().second;
- }
-
- /*!
- * Returns an iterator pointing to the first labeled probability.
- *
- * @return An iterator pointing to the first labeled probability.
- */
- typename std::list<std::pair<ValueType, boost::container::flat_set<uint_fast64_t>>>::iterator begin() {
- return valueLabelList.begin();
- }
-
- /*!
- * Returns an iterator pointing past the last labeled probability.
- *
- * @return An iterator pointing past the last labeled probability.
- */
- typename std::list<std::pair<ValueType, boost::container::flat_set<uint_fast64_t>>>::const_iterator end() {
- return valueLabelList.end();
- }
-
- /*!
- * Returns a const iterator pointing to the first labeled probability.
- *
- * @return A const iterator pointing to the first labeled probability.
- */
- typename std::list<std::pair<ValueType, boost::container::flat_set<uint_fast64_t>>>::const_iterator begin() const {
- return valueLabelList.begin();
- }
-
- /*!
- * Returns a const iterator pointing past the last labeled probability.
- *
- * @return A const iterator pointing past the last labeled probability.
- */
- typename std::list<std::pair<ValueType, boost::container::flat_set<uint_fast64_t>>>::const_iterator end() const {
- return valueLabelList.end();
- }
-
- /*!
- * Inserts the contents of this object to the given output stream.
- *
- * @param out The stream in which to insert the contents.
- */
- friend std::ostream& operator<<(std::ostream& out, LabeledValues const& labeledValues) {
- out << "[";
- for (auto const& element : labeledValues) {
- out << element.first << " (";
- for (auto const& label : element.second) {
- out << label << ", ";
- }
- out << ") ";
- }
- out << "]";
- return out;
- }
-
- /*!
- * Adds all labeled values of the given object to the current one.
- *
- * @param labeledValues The labeled values to add to the object.
- */
- LabeledValues<ValueType>& operator+=(LabeledValues<ValueType> const& labeledValues) {
- for (auto const& valueLabelListPair : labeledValues) {
- this->valueLabelList.push_back(valueLabelListPair);
- }
- return *this;
- }
-
- /*!
- * Divides the values by the given value.
- *
- * @param value The value by which to divide.
- * @return A collection of labeled values that have the same labels as the current object, but whose values
- * are divided by the given one.
- */
- LabeledValues<ValueType> operator/(ValueType value) const {
- LabeledValues<ValueType> result;
- for (auto const& valueLabelListPair : valueLabelList) {
- result.addValue(valueLabelListPair.first / value, valueLabelListPair.second);
- }
- return result;
- }
-
- /*!
- * Divides the values by the given unsigned integer value.
- *
- * @param value The unsigned integer value by which to divide.
- * @return A collection of labeled values that have the same labels as the current object, but whose values
- * are divided by the given one.
- */
- LabeledValues<ValueType> operator/(uint_fast64_t value) const {
- LabeledValues<ValueType> result;
- for (auto const& valueLabelListPair : valueLabelList) {
- result.addValue(valueLabelListPair.first / value, valueLabelListPair.second);
- }
- return result;
- }
-
- /*!
- * Converts the object into the value type by returning the sum.
- *
- * @return The sum of the values.
- */
- operator ValueType() const {
- return this->getSum();
- }
-
- /*!
- * Retrieves the number of separate entries in this object.
- *
- * @return The number of separate entries in this object.
- */
- size_t size() const {
- return this->valueLabelList.size();
- }
-
- private:
- // The actual storage used to store the list of values and the associated labels.
- std::list<std::pair<ValueType, boost::container::flat_set<uint_fast64_t>>> valueLabelList;
-
- /*!
- * Returns the sum of the values.
- *
- * @return The sum of the values.
- */
- ValueType getSum() const {
- ValueType sum = storm::utility::constantZero<ValueType>();
- for (auto const& valueLabelListPair : *this) {
- sum += valueLabelListPair.first;
- }
- return sum;
- }
- };
-
- /*!
- * Computes the hash value of a given labeled probabilities object.
- *
- * @param labeledProbabilities The labeled probabilities object for which to compute the hash value.
- * @return A hash value for the labeled probabilities object.
- */
- template<typename ValueType>
- std::size_t hash_value(LabeledValues<ValueType> const& labeledValues) {
- return labeledValues.size();
- }
-
- }
-}
-
-#endif /* STORM_STORAGE_LABELEDVALUES_H */
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
index 7c11c4fc5..83b3e725d 100644
--- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -17,7 +17,7 @@ namespace storm {
symbolTable.add_constants();
}
- bool ExprtkExpressionEvaluator::asBool(Expression const& expression) {
+ bool ExprtkExpressionEvaluator::asBool(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@@ -27,7 +27,7 @@ namespace storm {
return expressionPair->second.value() == ValueType(1);
}
- int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) {
+ int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@@ -37,7 +37,7 @@ namespace storm {
return static_cast<int_fast64_t>(expressionPair->second.value());
}
- double ExprtkExpressionEvaluator::asDouble(Expression const& expression) {
+ double ExprtkExpressionEvaluator::asDouble(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@@ -47,11 +47,11 @@ namespace storm {
return static_cast<double>(expressionPair->second.value());
}
- ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) {
+ ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) const {
std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression, CompiledExpressionType());
CompiledExpressionType& compiledExpression = result.first->second;
compiledExpression.register_symbol_table(symbolTable);
- bool parsingOk = parser.compile(stringTranslator.toString(expression), compiledExpression);
+ bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
return compiledExpression;
}
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h
index 8aa771130..41cc313c3 100644
--- a/src/storage/expressions/ExprtkExpressionEvaluator.h
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.h
@@ -21,9 +21,9 @@ namespace storm {
*/
ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
- bool asBool(Expression const& expression);
- int_fast64_t asInt(Expression const& expression);
- double asDouble(Expression const& expression);
+ bool asBool(Expression const& expression) const;
+ int_fast64_t asInt(Expression const& expression) const;
+ double asDouble(Expression const& expression) const;
void setBooleanValue(storm::expressions::Variable const& variable, bool value);
void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value);
@@ -39,16 +39,16 @@ namespace storm {
*
* @param expression The expression that is to be compiled.
*/
- CompiledExpressionType& getCompiledExpression(BaseExpression const* expression);
+ CompiledExpressionType& getCompiledExpression(BaseExpression const* expression) const;
// The expression manager that is used by this evaluator.
std::shared_ptr<storm::expressions::ExpressionManager const> manager;
// The parser used.
- exprtk::parser<ValueType> parser;
+ mutable exprtk::parser<ValueType> parser;
// The symbol table used.
- exprtk::symbol_table<ValueType> symbolTable;
+ mutable exprtk::symbol_table<ValueType> symbolTable;
// The actual data that is fed into the expression.
std::vector<ValueType> booleanValues;
@@ -56,10 +56,7 @@ namespace storm {
std::vector<ValueType> rationalValues;
// A mapping of expressions to their compiled counterpart.
- CacheType compiledExpressions;
-
- // A translator that can be used for transforming an expression into the correct string format.
- ToExprtkStringVisitor stringTranslator;
+ mutable CacheType compiledExpressions;
};
}
}
diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp
index a5f425215..64c7174ca 100644
--- a/src/storage/expressions/Variable.cpp
+++ b/src/storage/expressions/Variable.cpp
@@ -10,6 +10,10 @@ namespace storm {
bool Variable::operator==(Variable const& other) const {
return manager == other.manager && index == other.index;
}
+
+ bool Variable::operator!=(Variable const& other) const {
+ return !(*this == other);
+ }
bool Variable::operator<(Variable const& other) const {
return this->getIndex() < other.getIndex();
diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h
index c3a18eab0..f3a271760 100644
--- a/src/storage/expressions/Variable.h
+++ b/src/storage/expressions/Variable.h
@@ -41,6 +41,14 @@ namespace storm {
*/
bool operator==(Variable const& other) const;
+ /*!
+ * Checks the two variables for inequality.
+ *
+ * @param other The variable to compare with.
+ * @return True iff the two variables are different.
+ */
+ bool operator!=(Variable const& other) const;
+
/*!
* Checks whether the variable appears earlier in the total ordering of variables.
*
diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h
index e54932538..b3a78c364 100644
--- a/src/utility/PrismUtility.h
+++ b/src/utility/PrismUtility.h
@@ -1,7 +1,6 @@
#ifndef STORM_UTILITY_PRISMUTILITY
#define STORM_UTILITY_PRISMUTILITY
-#include "src/storage/LabeledValues.h"
#include "src/storage/prism/Program.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -10,7 +9,7 @@ namespace storm {
namespace utility {
namespace prism {
// A structure holding information about a particular choice.
- template<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
+ template<typename ValueType, typename KeyType=uint32_t, typename Compare=std::less<uint32_t>>
struct Choice {
public:
Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() {
@@ -148,6 +147,10 @@ namespace storm {
return distribution.at(state);
}
+ void addProbability(KeyType state, ValueType value) {
+ distribution[state] += value;
+ }
+
private:
// The distribution that is associated with the choice.
std::map<KeyType, ValueType, Compare> distribution;
@@ -159,36 +162,6 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> choiceLabels;
};
- /*!
- * Adds the target state and probability to the given choice and ignores the labels. This function overloads with
- * other functions to ensure the proper treatment of labels.
- *
- * @param choice The choice to which to add the target state and probability.
- * @param state The target state of the probability.
- * @param probability The probability to reach the target state in one step.
- * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this
- * is ignored by this particular function but not by the overloaded functions.
- */
- template<typename ValueType>
- void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
- choice.getOrAddEntry(state) += probability;
- }
-
- /*!
- * Adds the target state and probability to the given choice and labels it accordingly. This function overloads
- * with other functions to ensure the proper treatment of labels.
- *
- * @param choice The choice to which to add the target state and probability.
- * @param state The target state of the probability.
- * @param probability The probability to reach the target state in one step.
- * @param labels A set of labels that is supposed to be associated with this state and probability.
- */
- template<typename ValueType>
- void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
- auto& labeledEntry = choice.getOrAddEntry(state);
- labeledEntry.addValue(probability, labels);
- }
-
static std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
std::set<storm::expressions::Variable> definedConstants;
diff --git a/src/utility/constants.h b/src/utility/constants.h
index a857e40ba..c956eecb9 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -20,7 +20,6 @@
#include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/BitVector.h"
-#include "src/storage/LabeledValues.h"
namespace storm {
@@ -73,15 +72,6 @@ inline double constantZero() {
return 0.0;
}
-/*!
- * Template specialization for LabeledValues.
- * @return A LabeledValues object that represents a value of 0.
- */
-template<>
-inline storm::storage::LabeledValues<double> constantZero() {
- return storm::storage::LabeledValues<double>(0.0);
-}
-
/*! @endcond */
/*!
@@ -131,15 +121,6 @@ inline double constantOne() {
return 1.0;
}
-/*!
- * Template specialization for LabeledValues.
- * @return A LabeledValues object that represents a value of 1.
- */
-template<>
-inline storm::storage::LabeledValues<double> constantOne() {
- return storm::storage::LabeledValues<double>(1.0);
-}
-
/*! @endcond */
/*!
@@ -191,15 +172,6 @@ inline double constantInfinity() {
return std::numeric_limits<double>::infinity();
}
-/*!
- * Template specialization for LabeledValues.
- * @return Value Infinity, fit to the type LabeledValues.
- */
-template<>
-inline storm::storage::LabeledValues<double> constantInfinity() {
- return storm::storage::LabeledValues<double>(std::numeric_limits<double>::infinity());
-}
-
/*! @endcond */