sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet. 

Former-commit-id: dc60f568bf
main
dehnert 11 years ago
parent
26e9eac934
commit
6f2916d557
12 changed files with 206 additions and 459 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 266
      src/adapters/ExplicitModelAdapter.h
  2. 6
      src/storage/BitVector.cpp
  3. 6
      src/storage/BitVector.h
  4. 45
      src/storage/BitVectorHashMap.cpp
  5. 25
      src/storage/BitVectorHashMap.h
  6. 211
      src/storage/LabeledValues.h
  7. 10
      src/storage/expressions/ExprtkExpressionEvaluator.cpp
  8. 17
      src/storage/expressions/ExprtkExpressionEvaluator.h
  9. 4
      src/storage/expressions/Variable.cpp
  10. 8
      src/storage/expressions/Variable.h
  11. 37
      src/utility/PrismUtility.h
  12. 28
      src/utility/constants.h

266
src/adapters/ExplicitModelAdapter.h
View File

@ -13,7 +13,7 @@
#include "src/storage/prism/Program.h" #include "src/storage/prism/Program.h"
#include "src/storage/expressions/SimpleValuation.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/storage/BitVectorHashMap.h"
#include "src/utility/PrismUtility.h" #include "src/utility/PrismUtility.h"
#include "src/models/AbstractModel.h" #include "src/models/AbstractModel.h"
@ -58,37 +58,56 @@ namespace storm {
// A structure storing information about the used variables of the program. // A structure storing information about the used variables of the program.
struct VariableInformation { 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); auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
if (booleanIndex != booleanVariableToIndexMap.end()) { if (booleanIndex != booleanVariableToIndexMap.end()) {
return std::get<2>(booleanVariables[booleanIndex]);
return booleanVariables[booleanIndex].bitOffset;
} }
auto const& integerIndex = integerVariableToIndexMap.find(variable); auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) { 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."); 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); auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) { 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."); 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; std::map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
std::vector<BooleanVariableInformation> booleanVariables;
// 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;
// The list of integer variables.
std::map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap; 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. // A structure holding the individual components of a model.
@ -174,17 +193,12 @@ namespace storm {
} }
private: 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) { 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) { 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. * @params update The update to apply.
* @return The resulting state. * @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. * @param update The update to apply.
* @return The resulting state. * @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; return newState;
} }
@ -244,11 +268,11 @@ namespace storm {
uint32_t newIndex = stateInformation.reachableStates.size(); uint32_t newIndex = stateInformation.reachableStates.size();
// Check, if the state was already registered. // 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) { 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; return actualIndexBucketPair.first;
@ -270,7 +294,7 @@ namespace storm {
* @param actionIndex The index of the action label to select. * @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing. * @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>>>())); 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. // 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. // 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) { for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex); storm::prism::Command const& command = module.getCommand(commandIndex);
if (command.getGuardExpression().evaluateAsBool(state)) {
if (evaluator.asBool(command.getGuardExpression())) {
commands.push_back(command); commands.push_back(command);
} }
} }
@ -311,11 +335,9 @@ namespace storm {
return result; 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; std::vector<Choice<ValueType>> result;
StateType const* currentState = stateInformation.reachableStates[stateIndex];
// Iterate over all modules. // Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i); storm::prism::Module const& module = program.getModule(i);
@ -328,7 +350,7 @@ namespace storm {
if (command.isLabeled()) continue; if (command.isLabeled()) continue;
// Skip the command, if it is not enabled. // Skip the command, if it is not enabled.
if (!command.getGuardExpression().evaluateAsBool(currentState)) {
if (!evaluator.asBool(command.getGuardExpression())) {
continue; continue;
} }
@ -336,25 +358,17 @@ namespace storm {
Choice<ValueType>& choice = result.back(); Choice<ValueType>& choice = result.back();
choice.addChoiceLabel(command.getGlobalIndex()); choice.addChoiceLabel(command.getGlobalIndex());
double probabilitySum = 0;
// Iterate over all updates of the current command. // Iterate over all updates of the current command.
double probabilitySum = 0;
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(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. // 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. // Check that the resulting distribution is in fact a distribution.
@ -365,12 +379,11 @@ namespace storm {
return result; 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; std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getActionIndices()) { 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. // Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) { if (optionalActiveCommandLists) {
@ -385,9 +398,9 @@ namespace storm {
// As long as there is one feasible combination of commands, keep on expanding it. // As long as there is one feasible combination of commands, keep on expanding it.
bool done = false; bool done = false;
while (!done) { 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 // 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. // 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); storm::prism::Update const& update = command.getUpdate(j);
for (auto const& stateProbabilityPair : *currentTargetStates) { 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 there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) { if (i < iteratorList.size() - 1) {
for (auto const& stateProbabilityPair : *currentTargetStates) {
delete stateProbabilityPair.first;
}
delete currentTargetStates; delete currentTargetStates;
currentTargetStates = newTargetStates; 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; double probabilitySum = 0;
for (auto const& stateProbabilityPair : *newTargetStates) { 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. // 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. // We need to initialize the values of the variables to their initial value.
for (auto const& booleanVariable : variableInformation.booleanVariables) { 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) { 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. // 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. // Now explore the current state until there is no more reachable state.
uint_fast64_t currentRow = 0; uint_fast64_t currentRow = 0;
storm::expressions::ExprTkEvaluator evaluator(program.getManager());
storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager());
while (!stateQueue.empty()) { while (!stateQueue.empty()) {
// Get the current state and unpack it. // 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. // 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(); uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
@ -556,7 +530,7 @@ namespace storm {
if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
// Insert empty choice labeling for added self-loop transitions. // Insert empty choice labeling for added self-loop transitions.
choiceLabels.push_back(boost::container::flat_set<uint_fast64_t>()); 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; ++currentRow;
} else { } else {
LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); 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. // or compose them to one choice.
if (deterministicModel) { if (deterministicModel) {
Choice<ValueType> globalChoice; 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. // Combine all the choices and scale them with the total number of choices of the current state.
for (auto const& choice : allUnlabeledChoices) { for (auto const& choice : allUnlabeledChoices) {
@ -578,8 +551,8 @@ namespace storm {
// Now add all rewards that match this choice. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { 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. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { 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. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { 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. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { 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()) { for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset); variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
++bitOffset; ++bitOffset;
booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
} }
for (auto const& integerVariable : program.getGlobalIntegerVariables()) { for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); 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))); 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); variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
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& module : program.getModules()) {
for (auto const& booleanVariable : module.getBooleanVariables()) { for (auto const& booleanVariable : module.getBooleanVariables()) {
variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset); variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
++bitOffset; ++bitOffset;
booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
} }
for (auto const& integerVariable : module.getIntegerVariables()) { for (auto const& integerVariable : module.getIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); 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))); 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); variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
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); modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);
// Finally, construct the state rewards. // 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; return modelComponents;
} }
@ -762,6 +730,8 @@ namespace storm {
* @return The state labeling of the given program. * @return The state labeling of the given program.
*/ */
static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { 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(); std::vector<storm::prism::Label> const& labels = program.getLabels();
storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1); 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 (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
for (auto const& label : labels) { for (auto const& label : labels) {
unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator);
// Add label to state, if the corresponding expression is true. // 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); result.addAtomicPropositionToState(label.getName(), index);
} }
} }
@ -795,14 +767,18 @@ namespace storm {
* @param stateInformation Information about the state space. * @param stateInformation Information about the state space.
* @return A vector containing the state rewards for 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()); std::vector<ValueType> result(stateInformation.reachableStates.size());
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
result[index] = ValueType(0); result[index] = ValueType(0);
for (auto const& reward : rewards) { 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. // 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()));
} }
} }
} }

6
src/storage/BitVector.cpp
View File

@ -131,7 +131,7 @@ namespace storm {
return *this; 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 the lengths of the vectors do not match, they are considered unequal.
if (this->bitCount != other.bitCount) return false; if (this->bitCount != other.bitCount) return false;
@ -146,7 +146,7 @@ namespace storm {
return true; return true;
} }
bool BitVector::operator!=(BitVector const& other) {
bool BitVector::operator!=(BitVector const& other) const {
return !(*this == other); return !(*this == other);
} }
@ -648,7 +648,7 @@ namespace storm {
} }
namespace std { 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()); return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end());
} }
} }

6
src/storage/BitVector.h
View File

@ -138,7 +138,7 @@ namespace storm {
* @param other The bitvector with which to compare the current one. * @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. * @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. * 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. * @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. * @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. * 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 { namespace std {
template <> template <>
struct hash<storm::storage::BitVector> { struct hash<storm::storage::BitVector> {
std::size_t operator()(storm::storage::BitVector const& bv);
std::size_t operator()(storm::storage::BitVector const& bv) const;
}; };
} }

45
src/storage/BitVectorHashMap.cpp
View File

@ -21,7 +21,7 @@ namespace storm {
} }
template<class ValueType, class Hash1, class Hash2> 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); return occupied.get(bucket);
} }
@ -66,37 +66,48 @@ namespace storm {
this->increaseSize(); 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 initialHash = hasher1(key) % *currentSizeIterator;
uint_fast64_t bucket = initialHash; uint_fast64_t bucket = initialHash;
while (isBucketOccupied(bucket)) { while (isBucketOccupied(bucket)) {
if (buckets.matches(bucket * bucketSize, key)) { if (buckets.matches(bucket * bucketSize, key)) {
return std::make_pair(values[bucket], bucket);
return std::make_pair(true, bucket);
} }
bucket += hasher2(key); bucket += hasher2(key);
bucket %= *currentSizeIterator; 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> 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<uint_fast64_t>;
template class BitVectorHashMap<uint32_t>;
} }
} }

25
src/storage/BitVectorHashMap.h
View File

@ -50,12 +50,20 @@ namespace storm {
std::pair<ValueType, std::size_t> findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value); 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. * @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. * 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. * @param bucket The bucket to check.
* @return True iff the bucket is occupied. * @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. * Increases the size of the hash map and performs the necessary rehashing of all entries.

211
src/storage/LabeledValues.h
View File

@ -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 */

10
src/storage/expressions/ExprtkExpressionEvaluator.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
symbolTable.add_constants(); symbolTable.add_constants();
} }
bool ExprtkExpressionEvaluator::asBool(Expression const& expression) {
bool ExprtkExpressionEvaluator::asBool(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) { if (expressionPair == this->compiledExpressions.end()) {
@ -27,7 +27,7 @@ namespace storm {
return expressionPair->second.value() == ValueType(1); 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(); BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) { if (expressionPair == this->compiledExpressions.end()) {
@ -37,7 +37,7 @@ namespace storm {
return static_cast<int_fast64_t>(expressionPair->second.value()); 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(); BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) { if (expressionPair == this->compiledExpressions.end()) {
@ -47,11 +47,11 @@ namespace storm {
return static_cast<double>(expressionPair->second.value()); 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()); std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression, CompiledExpressionType());
CompiledExpressionType& compiledExpression = result.first->second; CompiledExpressionType& compiledExpression = result.first->second;
compiledExpression.register_symbol_table(symbolTable); compiledExpression.register_symbol_table(symbolTable);
bool parsingOk = parser.compile(stringTranslator.toString(expression), compiledExpression);
bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
return compiledExpression; return compiledExpression;
} }

17
src/storage/expressions/ExprtkExpressionEvaluator.h
View File

@ -21,9 +21,9 @@ namespace storm {
*/ */
ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager); 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 setBooleanValue(storm::expressions::Variable const& variable, bool value);
void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t 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. * @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. // The expression manager that is used by this evaluator.
std::shared_ptr<storm::expressions::ExpressionManager const> manager; std::shared_ptr<storm::expressions::ExpressionManager const> manager;
// The parser used. // The parser used.
exprtk::parser<ValueType> parser;
mutable exprtk::parser<ValueType> parser;
// The symbol table used. // The symbol table used.
exprtk::symbol_table<ValueType> symbolTable;
mutable exprtk::symbol_table<ValueType> symbolTable;
// The actual data that is fed into the expression. // The actual data that is fed into the expression.
std::vector<ValueType> booleanValues; std::vector<ValueType> booleanValues;
@ -56,10 +56,7 @@ namespace storm {
std::vector<ValueType> rationalValues; std::vector<ValueType> rationalValues;
// A mapping of expressions to their compiled counterpart. // 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;
}; };
} }
} }

4
src/storage/expressions/Variable.cpp
View File

@ -11,6 +11,10 @@ namespace storm {
return manager == other.manager && index == other.index; return manager == other.manager && index == other.index;
} }
bool Variable::operator!=(Variable const& other) const {
return !(*this == other);
}
bool Variable::operator<(Variable const& other) const { bool Variable::operator<(Variable const& other) const {
return this->getIndex() < other.getIndex(); return this->getIndex() < other.getIndex();
} }

8
src/storage/expressions/Variable.h
View File

@ -41,6 +41,14 @@ namespace storm {
*/ */
bool operator==(Variable const& other) const; 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. * Checks whether the variable appears earlier in the total ordering of variables.
* *

37
src/utility/PrismUtility.h
View File

@ -1,7 +1,6 @@
#ifndef STORM_UTILITY_PRISMUTILITY #ifndef STORM_UTILITY_PRISMUTILITY
#define STORM_UTILITY_PRISMUTILITY #define STORM_UTILITY_PRISMUTILITY
#include "src/storage/LabeledValues.h"
#include "src/storage/prism/Program.h" #include "src/storage/prism/Program.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
@ -10,7 +9,7 @@ namespace storm {
namespace utility { namespace utility {
namespace prism { namespace prism {
// A structure holding information about a particular choice. // 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 { struct Choice {
public: public:
Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() { Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() {
@ -148,6 +147,10 @@ namespace storm {
return distribution.at(state); return distribution.at(state);
} }
void addProbability(KeyType state, ValueType value) {
distribution[state] += value;
}
private: private:
// The distribution that is associated with the choice. // The distribution that is associated with the choice.
std::map<KeyType, ValueType, Compare> distribution; std::map<KeyType, ValueType, Compare> distribution;
@ -159,36 +162,6 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> choiceLabels; 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) { 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::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
std::set<storm::expressions::Variable> definedConstants; std::set<storm::expressions::Variable> definedConstants;

28
src/utility/constants.h
View File

@ -20,7 +20,6 @@
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/storage/LabeledValues.h"
namespace storm { namespace storm {
@ -73,15 +72,6 @@ inline double constantZero() {
return 0.0; 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 */ /*! @endcond */
/*! /*!
@ -131,15 +121,6 @@ inline double constantOne() {
return 1.0; 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 */ /*! @endcond */
/*! /*!
@ -191,15 +172,6 @@ inline double constantInfinity() {
return std::numeric_limits<double>::infinity(); 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 */ /*! @endcond */

Write Preview
Loading…
Cancel
Save