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

added the feature to build information about the state space that can be retrieved after building the model to the explicit model builder 

Former-commit-id: 72b9b18e4e
tempestpy_adaptions
dehnert 9 years ago
parent
44a9636f69
commit
5c838e2006
5 changed files with 208 additions and 45 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 100
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 62
      src/builder/ExplicitPrismModelBuilder.h
  3. 42
      src/storage/BitVectorHashMap.cpp
  4. 47
      src/storage/BitVectorHashMap.h
  5. 2
      src/utility/storm.h

100
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -7,6 +7,8 @@
#include "src/models/sparse/Mdp.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/utility/prism.h"
@ -15,6 +17,7 @@
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace builder {
@ -64,7 +67,12 @@ namespace storm {
};
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
// Intentionally left empty.
}
@ -78,6 +86,11 @@ namespace storm {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
@ -106,17 +119,17 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@ -216,6 +229,12 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getStateInformation() const {
STORM_LOG_THROW(static_cast<bool>(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
return stateInformation.get();
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
// Start by defining the undefined constants in the model.
@ -327,6 +346,18 @@ namespace storm {
evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation) {
storm::expressions::SimpleValuation result(variableInformation.manager.getSharedPointer());
for (auto const& booleanVariable : variableInformation.booleanVariables) {
result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
}
for (auto const& integerVariable : variableInformation.integerVariables) {
result.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
@ -368,15 +399,15 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename IndexType>
IndexType ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
uint32_t newIndex = stateInformation.reachableStates.size();
IndexType ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
uint32_t newIndex = internalStateInformation.reachableStates.size();
// Check, if the state was already registered.
std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
std::pair<uint32_t, std::size_t> actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
if (actualIndexBucketPair.first == newIndex) {
stateQueue.push(state);
stateInformation.reachableStates.push_back(state);
internalStateInformation.reachableStates.push_back(state);
}
return actualIndexBucketPair.first;
@ -426,7 +457,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
@ -460,7 +491,7 @@ namespace storm {
// 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);
uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), internalStateInformation, stateQueue);
// Update the choice by adding the probability/target state to it.
ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
@ -477,7 +508,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
@ -539,7 +570,7 @@ namespace storm {
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue);
uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, internalStateInformation, stateQueue);
choice.addProbability(actualIndex, stateProbabilityPair.second);
probabilitySum += stateProbabilityPair.second;
}
@ -572,7 +603,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename IndexType>
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
// Create choice labels, if requested,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabels;
if (commandLabels) {
@ -584,7 +615,7 @@ namespace storm {
// Initialize a queue and insert the initial state.
std::queue<storm::storage::BitVector> stateQueue;
CompressedState initialState(stateInformation.bitsPerState);
CompressedState initialState(internalStateInformation.bitsPerState);
// We need to initialize the values of the variables to their initial value.
for (auto const& booleanVariable : variableInformation.booleanVariables) {
@ -605,8 +636,8 @@ namespace storm {
}
// Insert the initial state in the global state to index mapping and state queue.
uint32_t stateIndex = getOrAddStateIndex(initialState, stateInformation, stateQueue);
stateInformation.initialStateIndices.push_back(stateIndex);
uint32_t stateIndex = getOrAddStateIndex(initialState, internalStateInformation, stateQueue);
internalStateInformation.initialStateIndices.push_back(stateIndex);
// Now explore the current state until there is no more reachable state.
uint_fast64_t currentRow = 0;
@ -619,7 +650,7 @@ namespace storm {
// Get the current state and unpack it.
storm::storage::BitVector currentState = stateQueue.front();
stateQueue.pop();
IndexType stateIndex = stateInformation.stateStorage.getValue(currentState);
IndexType stateIndex = internalStateInformation.stateStorage.getValue(currentState);
STORM_LOG_TRACE("Exploring state with id " << stateIndex << ".");
unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
@ -630,8 +661,8 @@ namespace storm {
// Nothing to do in this case.
} else {
// Retrieve all choices for the current state.
allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
}
uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
@ -895,7 +926,7 @@ namespace storm {
ModelComponents modelComponents;
uint_fast64_t bitOffset = 0;
VariableInformation variableInformation;
VariableInformation variableInformation(program.getManager());
for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
++bitOffset;
@ -927,7 +958,7 @@ namespace storm {
// Create the structure for storing the reachable state space.
uint64_t bitsPerState = ((bitOffset / 64) + 1) * 64;
StateInformation stateInformation(bitsPerState);
InternalStateInformation internalStateInformation(bitsPerState);
// Determine whether we have to combine different choices to one or whether this model can have more than
// one choice per state.
@ -972,7 +1003,7 @@ namespace storm {
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
}
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, internalStateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
// Now finalize all reward models.
@ -981,26 +1012,37 @@ namespace storm {
modelComponents.rewardModels.emplace(rewardModelIt->get().getName(), builderIt->build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
}
// Finally, build the state labeling.
modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);
// Build the state labeling.
modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, internalStateInformation);
// Finally -- if requested -- build the state information that can be retrieved from the outside.
if (options.buildStateInformation) {
stateInformation = StateInformation(internalStateInformation.reachableStates.size());
for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) {
stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation);
}
for (auto const& el : stateInformation.get().valuations) {
std::cout << "state: " << el << std::endl;
}
}
return modelComponents;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation) {
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
std::vector<storm::prism::Label> const& labels = program.getLabels();
storm::models::sparse::StateLabeling result(stateInformation.reachableStates.size());
storm::models::sparse::StateLabeling result(internalStateInformation.reachableStates.size());
// Initialize labeling.
for (auto const& label : labels) {
result.addLabel(label.getName());
}
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
unpackStateIntoEvaluator(stateInformation.reachableStates[index], variableInformation, evaluator);
for (uint_fast64_t index = 0; index < internalStateInformation.reachableStates.size(); index++) {
unpackStateIntoEvaluator(internalStateInformation.reachableStates[index], variableInformation, evaluator);
for (auto const& label : labels) {
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.getStatePredicateExpression())) {
@ -1011,7 +1053,7 @@ namespace storm {
// Also label the initial state with the special label "init".
result.addLabel("init");
for (auto index : stateInformation.initialStateIndices) {
for (auto index : internalStateInformation.initialStateIndices) {
result.addLabelToState("init", index);
}

62
src/builder/ExplicitPrismModelBuilder.h
View File

@ -41,9 +41,9 @@ namespace storm {
public:
typedef storm::storage::BitVector CompressedState;
// A structure holding information about the reachable state space.
struct StateInformation {
StateInformation(uint64_t bitsPerState);
// A structure holding information about the reachable state space while building it.
struct InternalStateInformation {
InternalStateInformation(uint64_t bitsPerState);
// This member stores all the states and maps them to their unique indices.
storm::storage::BitVectorHashMap<IndexType> stateStorage;
@ -58,8 +58,21 @@ namespace storm {
std::vector<storm::storage::BitVector> reachableStates;
};
// A structure holding information about the reachable state space that can be retrieved from the outside.
struct StateInformation {
/*!
* Constructs a state information object for the given number of states.
*/
StateInformation(uint_fast64_t numberOfStates);
// A mapping from state indices to their variable valuations.
std::vector<storm::expressions::SimpleValuation> valuations;
};
// A structure storing information about the used variables of the program.
struct VariableInformation {
VariableInformation(storm::expressions::ExpressionManager const& manager);
struct BooleanVariableInformation {
BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
@ -106,6 +119,8 @@ namespace storm {
// The known integer variables.
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
std::vector<IntegerVariableInformation> integerVariables;
storm::expressions::ExpressionManager const& manager;
};
// A structure holding the individual components of a model.
@ -179,6 +194,11 @@ namespace storm {
// A flag that indicates whether or not all reward models are to be build.
bool buildAllRewardModels;
// A flag that indicates whether or not to store the state information after successfully building the
// model. If it is to be preserved, it can be retrieved via the appropriate methods after a successfull
// call to <code>translateProgram</code>.
bool buildStateInformation;
// A list of reward models to be build in case not all reward models are to be build.
std::set<std::string> rewardModelsToBuild;
@ -213,11 +233,21 @@ namespace storm {
* @param rewardModel The reward model that is to be built.
* @return The explicit model that was given by the probabilistic program.
*/
static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translateProgram(storm::prism::Program program, Options const& options = Options());
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translateProgram(storm::prism::Program program, Options const& options = Options());
/*!
* If requested in the options, information about the variable valuations in the reachable states can be
* retrieved via this function.
*
* @return A structure that stores information about all reachable states.
*/
StateInformation const& getStateInformation() const;
private:
static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
static storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation);
/*!
* Applies an update to the given state and returns the resulting new state object. This methods does not
* modify the given state but returns a new one.
@ -247,10 +277,10 @@ namespace storm {
* used after invoking this method.
*
* @param state A pointer to a state for which to retrieve the index. This must not be used after the call.
* @param stateInformation The information about the already explored part of the reachable state space.
* @param internalStateInformation The information about the already explored part of the reachable state space.
* @return A pair indicating whether the state was already discovered before and the state id of the state.
*/
static IndexType getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue<storm::storage::BitVector>& stateQueue);
static IndexType getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue);
/*!
* Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
@ -270,9 +300,9 @@ namespace storm {
*/
static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex);
static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
/*!
* Builds the transition matrix and the transition reward matrix based for the given program.
*
@ -280,7 +310,7 @@ namespace storm {
* @param variableInformation A structure containing information about the variables in the program.
* @param transitionRewards A list of transition rewards that are to be considered in the transition reward
* matrix.
* @param stateInformation A structure containing information about the states of the program.
* @param internalStateInformation A structure containing information about the states of the program.
* @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not.
* @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this
* function.
@ -290,7 +320,7 @@ namespace storm {
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
/*!
* Explores the state space of the given program and returns the components of the model as a result.
@ -300,17 +330,21 @@ namespace storm {
* @param options A set of options used to customize the building process.
* @return A structure containing the components of the resulting model.
*/
static ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options);
ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options);
/*!
* Builds the state labeling for the given program.
*
* @param program The program for which to build the state labeling.
* @param variableInformation Information about the variables in the program.
* @param stateInformation Information about the state space of the program.
* @param internalStateInformation Information about the state space of the program.
* @return The state labeling of the given program.
*/
static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation);
static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation);
// This member holds information about reachable states that can be retrieved from the outside after a
// successful build.
boost::optional<StateInformation> stateInformation;
};
} // namespace adapters

42
src/storage/BitVectorHashMap.cpp
View File

@ -9,6 +9,38 @@ namespace storm {
template<class ValueType, class Hash1, class Hash2>
const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191};
template<class ValueType, class Hash1, class Hash2>
BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {
// Intentionally left empty.
}
template<class ValueType, class Hash1, class Hash2>
bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) {
return &map == &other.map && *indexIt == *other.indexIt;
}
template<class ValueType, class Hash1, class Hash2>
bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) {
return !(*this == other);
}
template<class ValueType, class Hash1, class Hash2>
typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++(int) {
++indexIt;
return *this;
}
template<class ValueType, class Hash1, class Hash2>
typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++() {
++indexIt;
return *this;
}
template<class ValueType, class Hash1, class Hash2>
std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const {
return map.getBucketAndValue(*indexIt);
}
template<class ValueType, class Hash1, class Hash2>
BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64.");
@ -136,6 +168,16 @@ namespace storm {
return values[flagBucketPair.second];
}
template<class ValueType, class Hash1, class Hash2>
typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::begin() const {
return const_iterator(*this, occupied.begin());
}
template<class ValueType, class Hash1, class Hash2>
typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::end() const {
return const_iterator(*this, occupied.end());
}
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;

47
src/storage/BitVectorHashMap.h
View File

@ -8,7 +8,7 @@
namespace storm {
namespace storage {
/*!
* This class represents a hash-map whose keys are bit vectors. The value type is arbitrary. Currently, only
* queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of
@ -17,6 +17,36 @@ namespace storm {
template<class ValueType, class Hash1 = std::hash<storm::storage::BitVector>, class Hash2 = storm::storage::NonZeroBitVectorHash>
class BitVectorHashMap {
public:
class BitVectorHashMapIterator {
public:
/*! Creates an iterator that points to the bucket with the given index in the given map.
*
* @param map The map of the iterator.
* @param indexIt An iterator to the index of the bucket the iterator points to.
*/
BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt);
// Methods to compare two iterators.
bool operator==(BitVectorHashMapIterator const& other);
bool operator!=(BitVectorHashMapIterator const& other);
// Methods to move iterator forward.
BitVectorHashMapIterator& operator++(int);
BitVectorHashMapIterator& operator++();
// Method to retrieve the currently pointed-to bit vector and its mapped-to value.
std::pair<storm::storage::BitVector, ValueType> operator*() const;
private:
// The map this iterator refers to.
BitVectorHashMap const& map;
// An iterator to the bucket this iterator points to.
BitVector::const_iterator indexIt;
};
typedef BitVectorHashMapIterator const_iterator;
/*!
* Creates a new hash map with the given bucket size and initial size.
*
@ -65,6 +95,20 @@ namespace storm {
*/
ValueType getValue(storm::storage::BitVector const& key) const;
/*!
* Retrieves an iterator to the elements of the map.
*
* @return The iterator.
*/
const_iterator begin() const;
/*!
* Retrieves an iterator that points one past the elements of the map.
*
* @return The iterator.
*/
const_iterator end() const;
/*!
* Retrieves the size of the map in terms of the number of key-value pairs it stores.
*
@ -157,6 +201,7 @@ namespace storm {
// A static table that produces the next possible size of the hash table.
static const std::vector<std::size_t> sizes;
};
}
}

2
src/utility/storm.h
View File

@ -102,7 +102,7 @@ namespace storm {
options.buildCommandLabels = true;
}
result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
result = storm::builder::ExplicitPrismModelBuilder<ValueType>().translateProgram(program, options);
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);

Write Preview
Loading…
Cancel
Save