diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 465a9b960..5b62364b4 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -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);
}
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index 137674607..61d2e18fa 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -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
diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index 4f1ab9174..1726847ab 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -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;
diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h
index c4b564fab..3b0c7aa70 100644
--- a/src/storage/BitVectorHashMap.h
+++ b/src/storage/BitVectorHashMap.h
@@ -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;
};
+
}
}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index a863d8e93..be76720fe 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -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);