diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5b06a498d..7587a3f22 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -11,6 +11,7 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp)
+file(GLOB_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp)
file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp)
@@ -57,6 +58,7 @@ set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI})
source_group(main FILES ${STORM_MAIN_FILE})
source_group(adapters FILES ${STORM_ADAPTERS_FILES})
source_group(builder FILES ${STORM_BUILDER_FILES})
+source_group(generator FILES ${STORM_GENERATOR_FILES})
source_group(cli FILES ${STORM_CLI_FILES})
source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES})
source_group(logic FILES ${STORM_LOGIC_FILES})
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index d7c2f6293..ef53b9e43 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -11,7 +11,11 @@
#include "src/settings/modules/GeneralSettings.h"
+#include "src/generator/PrismNextStateGenerator.h"
+#include "src/generator/PrismStateLabelingGenerator.h"
+
#include "src/utility/prism.h"
+#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/utility/ConstantsComparator.h"
#include "src/exceptions/WrongFormatException.h"
@@ -21,13 +25,14 @@
namespace storm {
namespace builder {
+
/*!
* A structure that is used to keep track of a reward model currently being built.
*/
template <typename ValueType>
struct RewardModelBuilder {
public:
- RewardModelBuilder(bool deterministicModel, bool hasStateRewards, bool hasStateActionRewards, bool hasTransitionRewards) : hasStateRewards(hasStateRewards), hasStateActionRewards(hasStateActionRewards), hasTransitionRewards(hasTransitionRewards), stateRewardVector(), stateActionRewardVector(), transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0) {
+ RewardModelBuilder(bool deterministicModel, bool hasStateRewards, bool hasStateActionRewards, bool hasTransitionRewards) : hasStateRewards(hasStateRewards), hasStateActionRewards(hasStateActionRewards), hasTransitionRewards(hasTransitionRewards), stateRewardVector(), stateActionRewardVector() {
// Intentionally left empty.
}
@@ -37,19 +42,14 @@ namespace storm {
stateRewardVector.resize(rowGroupCount);
optionalStateRewardVector = std::move(stateRewardVector);
}
-
+
boost::optional<std::vector<ValueType>> optionalStateActionRewardVector;
if (hasStateActionRewards) {
stateActionRewardVector.resize(rowCount);
optionalStateActionRewardVector = std::move(stateActionRewardVector);
}
- boost::optional<storm::storage::SparseMatrix<ValueType>> optionalTransitionRewardMatrix;
- if (hasTransitionRewards) {
- optionalTransitionRewardMatrix = transitionRewardMatrixBuilder.build(rowCount, columnCount, rowGroupCount);
- }
-
- return storm::models::sparse::StandardRewardModel<ValueType>(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix));
+ return storm::models::sparse::StandardRewardModel<ValueType>(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector));
}
bool hasStateRewards;
@@ -61,75 +61,40 @@ namespace storm {
// The state-action reward vector.
std::vector<ValueType> stateActionRewardVector;
-
- // A builder that is used for constructing the transition reward matrix.
- storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder;
};
- template <typename ValueType, typename RewardModelType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::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() {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation() : stateStorage(64, 10), initialStateIndices(), bitsPerState(64), numberOfStates() {
// Intentionally left empty.
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() {
// Intentionally left empty.
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::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) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
// Intentionally left empty.
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// 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);
- if (booleanIndex != booleanVariableToIndexMap.end()) {
- return booleanVariables[booleanIndex->second].bitOffset;
- }
- auto const& integerIndex = integerVariableToIndexMap.find(variable);
- if (integerIndex != integerVariableToIndexMap.end()) {
- return integerVariables[integerIndex->second].bitOffset;
- }
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
- auto const& integerIndex = integerVariableToIndexMap.find(variable);
- if (integerIndex != integerVariableToIndexMap.end()) {
- return integerVariables[integerIndex->second].bitWidth;
- }
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
- // Intentionally left empty.
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- 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), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), 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<const storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -143,8 +108,8 @@ namespace storm {
}
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
if (formula.isAtomicExpressionFormula()) {
terminalStates = formula.asAtomicExpressionFormula().getExpression();
} else if (formula.isAtomicLabelFormula()) {
@@ -172,9 +137,9 @@ namespace storm {
}
}
}
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
+
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::preserveFormula(storm::logic::Formula const& formula) {
// If we already had terminal states, we need to erase them.
if (terminalStates) {
terminalStates.reset();
@@ -211,40 +176,23 @@ namespace storm {
}
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
}
- 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>
- storm::prism::Program const& ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getTranslatedProgram() const {
- return preparedProgram.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) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(program), options(options) {
// Start by defining the undefined constants in the model.
if (options.constantDefinitions) {
- preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
+ this->program = program.defineUndefinedConstants(options.constantDefinitions.get());
} else {
- preparedProgram = program;
+ this->program = program;
}
-
+
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
-#ifdef STORM_HAVE_CARL
- // If the program either has undefined constants or we are building a parametric model, but the parameters
- // not only appear in the probabilities, we re
- if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
-#else
- if (preparedProgram->hasUndefinedConstants()) {
-#endif
- std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
+ if (!std::is_same<ValueType, storm::RationalFunction>::value && this->program.hasUndefinedConstants()) {
+ std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = this->program.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@@ -257,59 +205,78 @@ namespace storm {
}
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
-#ifdef STORM_HAVE_CARL
- } else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram->hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+ } else if (std::is_same<ValueType, storm::RationalFunction>::value && !this->program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
-#endif
}
-
+
// If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
if (options.labelsToBuild) {
if (!options.buildAllLabels) {
- preparedProgram->filterLabels(options.labelsToBuild.get());
+ this->program.filterLabels(options.labelsToBuild.get());
}
}
// If we need to build labels for expressions that may appear in some formula, we need to add appropriate
// labels to the program.
if (options.expressionLabels) {
- std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
-
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = this->program.getConstantsSubstitution();
+
for (auto const& expression : options.expressionLabels.get()) {
std::stringstream stream;
stream << expression.substitute(constantsSubstitution);
std::string name = stream.str();
- if (!preparedProgram->hasLabel(name)) {
- preparedProgram->addLabel(name, expression);
+ if (!this->program.hasLabel(name)) {
+ this->program.addLabel(name, expression);
}
}
}
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
- preparedProgram = preparedProgram->substituteConstants();
+ this->program = this->program.substituteConstants();
+
+ // Create the variable information for the transformed program.
+ this->variableInformation = VariableInformation(this->program);
+
+ // Create the internal state storage.
+ this->internalStateInformation = InternalStateInformation(variableInformation.getTotalBitOffset(true));
+ }
+
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::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 StateType>
+ storm::prism::Program const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getTranslatedProgram() const {
+ return program;
+ }
+
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::translate() {
+ STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl);
+ STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder);
- STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl);
-
// Select the appropriate reward models (after the constants have been substituted).
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
-
+
// First, we make sure that all selected reward models actually exist.
for (auto const& rewardModelName : options.rewardModelsToBuild) {
- STORM_LOG_THROW(rewardModelName.empty() || preparedProgram->hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
+ STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
}
-
- for (auto const& rewardModel : preparedProgram->getRewardModels()) {
+
+ for (auto const& rewardModel : program.getRewardModels()) {
if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
selectedRewardModels.push_back(rewardModel);
}
}
// If no reward model was selected until now and a referenced reward model appears to be unique, we build
// the only existing reward model (given that no explicit name was given for the referenced reward model).
- if (selectedRewardModels.empty() && preparedProgram->getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
- selectedRewardModels.push_back(preparedProgram->getRewardModel(0));
+ if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
+ selectedRewardModels.push_back(program.getRewardModel(0));
}
-
- ModelComponents modelComponents = buildModelComponents(*preparedProgram, selectedRewardModels, options);
+
+ ModelComponents modelComponents = buildModelComponents(selectedRewardModels);
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> result;
switch (program.getModelType()) {
@@ -330,19 +297,9 @@ namespace storm {
return result;
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
- for (auto const& booleanVariable : variableInformation.booleanVariables) {
- evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
- }
- for (auto const& integerVariable : variableInformation.integerVariables) {
- 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());
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState) {
+ storm::expressions::SimpleValuation result(program.getManager().getSharedPointer());
for (auto const& booleanVariable : variableInformation.booleanVariables) {
result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
}
@@ -352,620 +309,192 @@ namespace storm {
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) {
- return applyUpdate(variableInformation, state, state, update, evaluator);
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
- CompressedState 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;
- }
- int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
- STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
- newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
- STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
- }
-
- // Check that we processed all assignments.
- STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
-
- return newState;
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- IndexType ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
- uint32_t newIndex = internalStateInformation.reachableStates.size();
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
+ uint32_t newIndex = internalStateInformation.numberOfStates;
// Check, if the state was already registered.
std::pair<uint32_t, std::size_t> actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
if (actualIndexBucketPair.first == newIndex) {
- stateQueue.push(state);
- internalStateInformation.reachableStates.push_back(state);
- }
-
- return actualIndexBucketPair.first;
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex) {
- boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
-
- // Iterate over all modules.
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::prism::Module const& module = program.getModule(i);
-
- // If the module has no command labeled with the given action, we can skip this module.
- if (!module.hasActionIndex(actionIndex)) {
- continue;
- }
-
- std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
-
- // If the module contains the action, but there is no command in the module that is labeled with
- // this action, we don't have any feasible command combinations.
- if (commandIndices.empty()) {
- return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
- }
-
- std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
-
- // Look up commands by their indices and add them if the guard evaluates to true in the given state.
- for (uint_fast64_t commandIndex : commandIndices) {
- storm::prism::Command const& command = module.getCommand(commandIndex);
- if (evaluator.asBool(command.getGuardExpression())) {
- commands.push_back(command);
- }
- }
-
- // If there was no enabled command although the module has some command with the required action label,
- // we must not return anything.
- if (commands.size() == 0) {
- return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
- }
-
- result.get().push_back(std::move(commands));
- }
-
- return result;
- }
-
- template <typename ValueType, typename RewardModelType, typename IndexType>
- 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.
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::prism::Module const& module = program.getModule(i);
-
- // Iterate over all commands.
- for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
- storm::prism::Command const& command = module.getCommand(j);
-
- // Only consider unlabeled commands.
- if (command.isLabeled()) continue;
-
- // Skip the command, if it is not enabled.
- if (!evaluator.asBool(command.getGuardExpression())) {
- continue;
- }
-
- result.push_back(Choice<ValueType>(0, choiceLabeling));
- Choice<ValueType>& choice = result.back();
-
- // Remember the command labels only if we were asked to.
- if (choiceLabeling) {
- choice.addChoiceLabel(command.getGlobalIndex());
- }
-
- // Iterate over all updates of the current command.
- ValueType probabilitySum = storm::utility::zero<ValueType>();
- for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
- storm::prism::Update const& update = command.getUpdate(k);
-
- // 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), internalStateInformation, stateQueue);
-
- // Update the choice by adding the probability/target state to it.
- ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
- choice.addProbability(stateIndex, probability);
- probabilitySum += probability;
- }
+ if (options.explorationOrder == ExplorationOrder::Dfs) {
+ statesToExplore.push_front(state);
- // Check that the resulting distribution is in fact a distribution.
- STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+ // Reserve one slot for the new state in the remapping.
+ stateRemapping.get().push_back(storm::utility::zero<StateType>());
+ } else if (options.explorationOrder == ExplorationOrder::Bfs) {
+ statesToExplore.push_back(state);
+ } else {
+ STORM_LOG_ASSERT(false, "Invalid exploration order.");
}
+ ++internalStateInformation.numberOfStates;
}
- return result;
+ return actualIndexBucketPair.first;
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- 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()) {
- boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex);
-
- // Only process this action label, if there is at least one feasible solution.
- if (optionalActiveCommandLists) {
- std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get();
- std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size());
-
- // Initialize the list of iterators.
- for (size_t i = 0; i < activeCommandList.size(); ++i) {
- iteratorList[i] = activeCommandList[i].cbegin();
- }
-
- // As long as there is one feasible combination of commands, keep on expanding it.
- bool done = false;
- while (!done) {
- std::unordered_map<CompressedState, ValueType>* currentTargetStates = new std::unordered_map<CompressedState, ValueType>();
- std::unordered_map<CompressedState, ValueType>* newTargetStates = new std::unordered_map<CompressedState, ValueType>();
- currentTargetStates->emplace(currentState, storm::utility::one<ValueType>());
-
- for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
- storm::prism::Command const& command = *iteratorList[i];
-
- for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
- storm::prism::Update const& update = command.getUpdate(j);
-
- for (auto const& stateProbabilityPair : *currentTargetStates) {
- // Compute the new state under the current update and add it to the set of new target states.
- CompressedState newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update, evaluator);
- newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
- }
- }
-
- // If there is one more command to come, shift the target states one time step back.
- if (i < iteratorList.size() - 1) {
- delete currentTargetStates;
- currentTargetStates = newTargetStates;
- newTargetStates = new std::unordered_map<CompressedState, ValueType>();
- }
- }
-
- // At this point, we applied all commands of the current command combination and newTargetStates
- // contains all target states and their respective probabilities. That means we are now ready to
- // add the choice to the list of transitions.
- result.push_back(Choice<ValueType>(actionIndex, choiceLabeling));
-
- // Now create the actual distribution.
- Choice<ValueType>& choice = result.back();
-
- // Remember the command labels only if we were asked to.
- if (choiceLabeling) {
- // Add the labels of all commands to this choice.
- for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
- choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex());
- }
- }
-
- ValueType probabilitySum = storm::utility::zero<ValueType>();
- for (auto const& stateProbabilityPair : *newTargetStates) {
- uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, internalStateInformation, stateQueue);
- choice.addProbability(actualIndex, stateProbabilityPair.second);
- probabilitySum += stateProbabilityPair.second;
- }
-
- // Check that the resulting distribution is in fact a distribution.
- STORM_LOG_THROW(!discreteTimeModel || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
-
- // Dispose of the temporary maps.
- delete currentTargetStates;
- delete newTargetStates;
-
- // Now, check whether there is one more command combination to consider.
- bool movedIterator = false;
- for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
- ++iteratorList[j];
- if (iteratorList[j] != activeCommandList[j].end()) {
- movedIterator = true;
- } else {
- // Reset the iterator to the beginning of the list.
- iteratorList[j] = activeCommandList[j].begin();
- }
- }
-
- done = !movedIterator;
- }
- }
- }
-
- return result;
- }
-
- 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, 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) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, 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) {
+ if (options.buildCommandLabels) {
choiceLabels = std::vector<boost::container::flat_set<uint_fast64_t>>();
}
-
- // A comparator that can be used to check whether we actually have distributions.
- storm::utility::ConstantsComparator<ValueType> comparator;
-
- // Initialize a queue and insert the initial state.
- std::queue<storm::storage::BitVector> stateQueue;
- CompressedState initialState(internalStateInformation.bitsPerState);
-
- // We need to initialize the values of the variables to their initial value.
- for (auto const& booleanVariable : variableInformation.booleanVariables) {
- initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
+
+ // Create a generator that is able to expand states.
+ storm::generator::PrismNextStateGenerator<ValueType, StateType> generator(program, variableInformation, options.buildCommandLabels);
+ if (terminalExpression) {
+ generator.setTerminalExpression(terminalExpression.get());
}
- for (auto const& integerVariable : variableInformation.integerVariables) {
- initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
+ for (auto const& rewardModel : selectedRewardModels) {
+ generator.addRewardModel(rewardModel.get());
}
+
+ // Create a callback for the next-state generator to enable it to request the index of states.
+ std::function<StateType (CompressedState const&)> stateToIdCallback = std::bind(&ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex, this, std::placeholders::_1);
- // At this point, we determine whether there are reward models with state-action rewards, because we might
- // want to know that quickly later on.
- bool hasStateActionRewards = false;
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt) {
- if (rewardModelIt->get().hasStateActionRewards()) {
- hasStateActionRewards = true;
- break;
- }
+ // If the exploration order is something different from breadth-first, we need to keep track of the remapping
+ // from state ids to row groups. For this, we actually store the reversed mapping of row groups to state-ids
+ // and later reverse it.
+ if (options.explorationOrder != ExplorationOrder::Bfs) {
+ stateRemapping = std::vector<uint_fast64_t>();
}
- // Insert the initial state in the global state to index mapping and state queue.
- uint32_t stateIndex = getOrAddStateIndex(initialState, internalStateInformation, stateQueue);
- internalStateInformation.initialStateIndices.push_back(stateIndex);
+ // Let the generator create all initial states.
+ this->internalStateInformation.initialStateIndices = generator.getInitialStates(stateToIdCallback);
// Now explore the current state until there is no more reachable state.
+ uint_fast64_t currentRowGroup = 0;
uint_fast64_t currentRow = 0;
-
- // The evaluator used to determine the truth value of guards and predicates in the *current* state.
- storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
-
- // Perform a BFS through the model.
- while (!stateQueue.empty()) {
- // Get the current state and unpack it.
- storm::storage::BitVector currentState = stateQueue.front();
- stateQueue.pop();
- IndexType stateIndex = internalStateInformation.stateStorage.getValue(currentState);
- STORM_LOG_TRACE("Exploring state with id " << stateIndex << ".");
- unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
-
- // If a terminal expression was given, we check whether the current state needs to be explored further.
- std::vector<Choice<ValueType>> allUnlabeledChoices;
- std::vector<Choice<ValueType>> allLabeledChoices;
- bool deadlockOnPurpose = false;
- if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
- //std::cout << unpackStateIntoValuation(currentState, variableInformation).toString(true) << std::endl;
- //allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
- //allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
- // Nothing to do in this case.
- deadlockOnPurpose = true;
- } else {
- // Retrieve all choices for the current state.
- allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
- allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
+ // Perform a search through the model.
+ while (!statesToExplore.empty()) {
+ // Get the first state in the queue.
+ CompressedState currentState = statesToExplore.front();
+ StateType currentIndex = internalStateInformation.stateStorage.getValue(currentState);
+ statesToExplore.pop_front();
+
+ // If the exploration order differs from breadth-first, we remember that this row group was actually
+ // filled with the transitions of a different state.
+ if (options.explorationOrder != ExplorationOrder::Bfs) {
+ stateRemapping.get()[currentIndex] = currentRowGroup;
}
- uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
+ STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
+
+ storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(currentState, stateToIdCallback);
- // If the current state does not have a single choice, we equip it with a self-loop if that was
- // requested and issue an error otherwise.
- if (totalNumberOfChoices == 0) {
- if (!storm::settings::generalSettings().isDontFixDeadlocksSet() || deadlockOnPurpose) {
- if (commandLabels) {
+ // If there is no behavior, we might have to introduce a self-loop.
+ if (behavior.empty()) {
+ if (!storm::settings::generalSettings().isDontFixDeadlocksSet() || !behavior.wasExpanded()) {
+ if (options.buildCommandLabels) {
// Insert empty choice labeling for added self-loop transitions.
choiceLabels.get().push_back(boost::container::flat_set<uint_fast64_t>());
}
- if (!deterministicModel) {
+ if (!generator.isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
- transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one<ValueType>());
+ transitionMatrixBuilder.addNextValue(currentRow, currentIndex, storm::utility::one<ValueType>());
auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
+ for (auto const& rewardModel : selectedRewardModels) {
+ if (rewardModel.get().hasStateRewards()) {
builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
}
- if (rewardModelIt->get().hasStateActionRewards()) {
+ if (rewardModel.get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
}
+ ++builderIt;
}
++currentRow;
+ ++currentRowGroup;
} else {
- std::cout << unpackStateIntoValuation(currentState, variableInformation).toString(true) << std::endl;
+ std::cout << unpackStateIntoValuation(currentState).toString(true) << std::endl;
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
"Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
-
- }
- } else if (totalNumberOfChoices == 1) {
- if (!deterministicModel) {
- transitionMatrixBuilder.newRowGroup(currentRow);
}
-
- bool labeledChoice = allUnlabeledChoices.empty() ? true : false;
- Choice<ValueType> const& globalChoice = labeledChoice ? allLabeledChoices.front() : allUnlabeledChoices.front();
-
+ } else {
+ // Add the state rewards to the corresponding reward models.
auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
- builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
- for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
- if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
- }
- }
- }
-
- if (rewardModelIt->get().hasStateActionRewards()) {
- builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
- for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
- if ((labeledChoice && stateActionReward.isLabeled() && stateActionReward.getActionIndex() == globalChoice.getActionIndex()) || (!labeledChoice && !stateActionReward.isLabeled())) {
- if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
- }
- }
- }
+ auto stateRewardIt = behavior.getStateRewards().begin();
+ for (auto const& rewardModel : selectedRewardModels) {
+ if (rewardModel.get().hasStateRewards()) {
+ builderIt->stateRewardVector.push_back(*stateRewardIt);
}
+ ++stateRewardIt;
+ ++builderIt;
}
- for (auto const& stateProbabilityPair : globalChoice) {
- transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
- }
-
- if (commandLabels) {
- // Now add the resulting distribution as the only choice of the current state.
- choiceLabels.get().push_back(globalChoice.getChoiceLabels());
+ // If the model is nondeterministic, we need to open a row group.
+ if (!generator.isDeterministicModel()) {
+ transitionMatrixBuilder.newRowGroup(currentRow);
}
- ++currentRow;
- } else {
- // Then, based on whether the model is deterministic or not, either add the choices individually
- // or compose them to one choice.
- if (deterministicModel) {
- Choice<ValueType> globalChoice;
-
- // We need to prepare the entries of those vectors that are going to be used.
- auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
- builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
- for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
- if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
- }
- }
- }
-
- if (rewardModelIt->get().hasStateActionRewards()) {
- builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
- }
- }
-
- // If there is one state-action reward model, we need to scale the rewards according to the
- // multiple choices.
- ValueType totalExitMass = storm::utility::zero<ValueType>();
- if (hasStateActionRewards) {
- if (discreteTimeModel) {
- totalExitMass = static_cast<ValueType>(totalNumberOfChoices);
- } else {
- // In the CTMC, we need to compute the exit rate of the state here, sin
- for (auto const& choice : allUnlabeledChoices) {
- totalExitMass += choice.getTotalMass();
- }
- for (auto const& choice : allLabeledChoices) {
- totalExitMass += choice.getTotalMass();
- }
- }
+ // Now add all choices.
+ for (auto const& choice : behavior) {
+ // Add command labels if requested.
+ if (options.buildCommandLabels) {
+ choiceLabels.get().push_back(choice.getChoiceLabels());
}
- // Combine all the choices and scale them with the total number of choices of the current state.
- for (auto const& choice : allUnlabeledChoices) {
- if (commandLabels) {
- globalChoice.addChoiceLabels(choice.getChoiceLabels());
- }
-
- auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateActionRewards()) {
- for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
- if (!stateActionReward.isLabeled()) {
- if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitMass;
- }
- }
- }
- }
- }
-
- for (auto const& stateProbabilityPair : choice) {
- if (discreteTimeModel) {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
- } else {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
- }
- }
- }
- for (auto const& choice : allLabeledChoices) {
- if (commandLabels) {
- globalChoice.addChoiceLabels(choice.getChoiceLabels());
- }
-
- auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateActionRewards()) {
- for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
- if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) {
- if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitMass;
- }
- }
- }
- }
- }
-
- for (auto const& stateProbabilityPair : choice) {
- if (discreteTimeModel) {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
- } else {
- globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
- }
- }
- }
-
-
- if (commandLabels) {
- // Now add the resulting distribution as the only choice of the current state.
- choiceLabels.get().push_back(globalChoice.getChoiceLabels());
- }
-
- for (auto const& stateProbabilityPair : globalChoice) {
+ // Add the probabilistic behavior to the matrix.
+ for (auto const& stateProbabilityPair : choice) {
transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
}
- ++currentRow;
- } else {
- // If the model is nondeterministic, we add all choices individually.
- transitionMatrixBuilder.newRowGroup(currentRow);
-
+ // Add the rewards to the reward models.
auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
- builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
-
- for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
- if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
- }
- }
+ auto choiceRewardIt = choice.getChoiceRewards().begin();
+ for (auto const& rewardModel : selectedRewardModels) {
+ if (rewardModel.get().hasStateActionRewards()) {
+ builderIt->stateActionRewardVector.push_back(*choiceRewardIt);
}
+ ++choiceRewardIt;
+ ++builderIt;
}
-
- // First, process all unlabeled choices.
- for (auto const& choice : allUnlabeledChoices) {
- std::map<uint_fast64_t, ValueType> stateToRewardMap;
- if (commandLabels) {
- choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels()));
- }
-
- auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateActionRewards()) {
- builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
- for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
- if (!stateActionReward.isLabeled()) {
- if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
- }
- }
- }
- }
- }
-
- for (auto const& stateProbabilityPair : choice) {
- transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
- }
-
- ++currentRow;
- }
-
- // Then, process all labeled choices.
- for (auto const& choice : allLabeledChoices) {
- std::map<uint_fast64_t, ValueType> stateToRewardMap;
- if (commandLabels) {
- choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels()));
- }
-
- auto builderIt = rewardModelBuilders.begin();
- for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateActionRewards()) {
- builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
- for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
- if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) {
- if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
- }
- }
- }
- }
- }
-
- for (auto const& stateProbabilityPair : choice) {
- transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
- }
-
- ++currentRow;
- }
+ ++currentRow;
}
+ ++currentRowGroup;
}
}
+
+ // If the exploration order was not breadth-first, we need to fix the entries in the matrix according to
+ // (reversed) mapping of row groups to indices.
+ if (options.explorationOrder != ExplorationOrder::Bfs) {
+ STORM_LOG_ASSERT(stateRemapping, "Unable to fix columns without mapping.");
+ std::vector<uint_fast64_t> const& remapping = stateRemapping.get();
+
+ // We need to fix the following entities:
+ // (a) the transition matrix
+ // (b) the initial states
+ // (c) the hash map storing the mapping states -> ids
+
+ // Fix (a).
+ transitionMatrixBuilder.replaceColumns(remapping, 0);
+
+ // Fix (b).
+ std::vector<StateType> newInitialStateIndices(this->internalStateInformation.initialStateIndices.size());
+ std::transform(this->internalStateInformation.initialStateIndices.begin(), this->internalStateInformation.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
+ std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end());
+ this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices);
+
+ // Fix (c).
+ this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } );
+ }
return choiceLabels;
}
- template <typename ValueType, typename RewardModelType, typename IndexType>
- typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options) {
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildModelComponents(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels) {
ModelComponents modelComponents;
-
- uint_fast64_t bitOffset = 0;
- VariableInformation variableInformation(program.getManager());
- for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
- variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
- ++bitOffset;
- variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
- }
- for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
- int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
- int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
- uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
- variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
- bitOffset += bitwidth;
- variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
- }
- for (auto const& module : program.getModules()) {
- for (auto const& booleanVariable : module.getBooleanVariables()) {
- variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset);
- ++bitOffset;
- variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1;
- }
- for (auto const& integerVariable : module.getIntegerVariables()) {
- int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
- int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
- uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
- variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
- bitOffset += bitwidth;
- variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
- }
- }
-
- // Create the structure for storing the reachable state space.
- uint64_t bitsPerState = ((bitOffset / 64) + 1) * 64;
- 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.
- bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;
- bool discreteTimeModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP;
+ bool deterministicModel = program.isDeterministicModel();
// Prepare the transition matrix builder and the reward model builders.
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
@@ -1005,7 +534,7 @@ namespace storm {
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
}
- modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, internalStateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
+ modelComponents.choiceLabeling = buildMatrices(selectedRewardModels, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
// Now finalize all reward models.
@@ -1015,48 +544,23 @@ namespace storm {
}
// Build the state labeling.
- modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, internalStateInformation);
+ modelComponents.stateLabeling = buildStateLabeling();
// Finally -- if requested -- build the state information that can be retrieved from the outside.
if (options.buildStateInformation) {
- stateInformation = StateInformation(internalStateInformation.reachableStates.size());
+ stateInformation = StateInformation(internalStateInformation.numberOfStates);
for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) {
- stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation);
+ stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first);
}
}
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, InternalStateInformation const& internalStateInformation) {
- storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
-
- std::vector<storm::prism::Label> const& labels = program.getLabels();
-
- 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 < 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())) {
- result.addLabelToState(label.getName(), index);
- }
- }
- }
-
- // Also label the initial state with the special label "init".
- result.addLabel("init");
- for (auto index : internalStateInformation.initialStateIndices) {
- result.addLabelToState("init", index);
- }
-
- return result;
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
+ storm::generator::PrismStateLabelingGenerator<ValueType, StateType> generator(program, variableInformation);
+ return generator.generate(internalStateInformation.stateStorage, internalStateInformation.initialStateIndices);
}
// Explicitly instantiate the class.
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index ccb0622e7..ab2eb9815 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -1,10 +1,10 @@
-#ifndef STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H
-#define STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H
+#ifndef STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H
+#define STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H
#include <memory>
#include <utility>
#include <vector>
-#include <queue>
+#include <deque>
#include <cstdint>
#include <boost/functional/hash.hpp>
#include <boost/container/flat_set.hpp>
@@ -22,9 +22,13 @@
#include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.h"
-#include "src/utility/constants.h"
#include "src/utility/prism.h"
+#include "src/builder/ExplorationOrder.h"
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/VariableInformation.h"
+
namespace storm {
namespace utility {
template<typename ValueType> class ConstantsComparator;
@@ -33,30 +37,33 @@ namespace storm {
namespace builder {
using namespace storm::utility::prism;
+ using namespace storm::generator;
// Forward-declare classes.
template <typename ValueType> struct RewardModelBuilder;
- template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
+ template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitPrismModelBuilder {
public:
- typedef storm::storage::BitVector CompressedState;
-
// A structure holding information about the reachable state space while building it.
struct InternalStateInformation {
+ // Builds an empty state information.
+ InternalStateInformation();
+
+ // Creates a state information structure for storing states of the given bit width.
InternalStateInformation(uint64_t bitsPerState);
// This member stores all the states and maps them to their unique indices.
- storm::storage::BitVectorHashMap<IndexType> stateStorage;
+ storm::storage::BitVectorHashMap<StateType> stateStorage;
// A list of initial states in terms of their global indices.
- std::vector<IndexType> initialStateIndices;
+ std::vector<StateType> initialStateIndices;
// The number of bits of each state.
uint64_t bitsPerState;
- // A list of reachable states as indices in the stateToIndexMap.
- std::vector<storm::storage::BitVector> reachableStates;
+ // The number of states that were found in the exploration so far.
+ uint_fast64_t numberOfStates;
};
// A structure holding information about the reachable state space that can be retrieved from the outside.
@@ -74,60 +81,6 @@ namespace storm {
}
};
- // 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);
-
- // The boolean variable.
- storm::expressions::Variable variable;
-
- // Its initial value.
- bool initialValue;
-
- // Its bit offset in the compressed state.
- 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);
-
- // The integer variable.
- storm::expressions::Variable variable;
-
- // Its initial value.
- int_fast64_t initialValue;
-
- // The lower bound of its range.
- int_fast64_t lowerBound;
-
- // The upper bound of its range.
- int_fast64_t upperBound;
-
- // Its bit offset in the compressed state.
- uint_fast64_t bitOffset;
-
- // Its bit width in the compressed state.
- uint_fast64_t bitWidth;
- };
-
- // Provide methods to access the bit offset and width of variables in the compressed state.
- uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
- uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
-
- // The known boolean variables.
- boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
- std::vector<BooleanVariableInformation> booleanVariables;
-
- // 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.
struct ModelComponents {
ModelComponents();
@@ -151,6 +104,11 @@ namespace storm {
*/
Options();
+ /*!
+ * Copies the given set of options.
+ */
+ Options(Options const& other) = default;
+
/*! Creates an object representing the suggested building options assuming that the given formula is the
* only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
*
@@ -193,6 +151,9 @@ namespace storm {
*/
void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
+ // The order in which to explore the model.
+ ExplorationOrder explorationOrder;
+
// A flag that indicates whether or not command labels are to be built.
bool buildCommandLabels;
@@ -228,6 +189,13 @@ namespace storm {
boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
};
+ /*!
+ * Creates a builder for the given program.
+ *
+ * @param program The program to build.
+ */
+ ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options());
+
/*!
* Convert the program given at construction time to an abstract model. The type of the model is the one
* specified in the program. The given reward model name selects the rewards that the model will contain.
@@ -238,7 +206,7 @@ namespace storm {
* @param rewardModel The reward model that is to be built.
* @return The explicit model that was given by the probabilistic program.
*/
- 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>> translate();
/*!
* If requested in the options, information about the variable valuations in the reachable states can be
@@ -249,39 +217,14 @@ namespace storm {
StateInformation const& getStateInformation() const;
/*!
- * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
- * that this function may only be called after a succesful translation.
+ * Retrieves the program that was actually translated (i.e. including constant substitutions etc.).
*
* @return The translated program.
*/
storm::prism::Program const& getTranslatedProgram() 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.
- *
- * @params state The state to which to apply the update.
- * @params update The update to apply.
- * @return The resulting state.
- */
- static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
-
- /*!
- * Applies an update to the given state and returns the resulting new state object. The update is evaluated
- * over the variable values of the given base state. This methods does not modify the given state but
- * returns a new one.
- *
- * @param state The state to which to apply the update.
- * @param baseState The state used for evaluating the update.
- * @param update The update to apply.
- * @return The resulting state.
- */
- static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
+ storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState);
/*!
* Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
@@ -293,29 +236,8 @@ namespace storm {
* @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, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue);
+ StateType getOrAddStateIndex(CompressedState const& state);
- /*!
- * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
- * modules.
- *
- * This function will iterate over all modules and retrieve all commands that are labeled with the given
- * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
- * the inner lists contain all commands of exactly one module. If a module does not have *any* (including
- * disabled) commands, there will not be a list of commands of that module in the result. If, however, the
- * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
- * is no legal transition possible.
- *
- * @param The program in which to search for active commands.
- * @param state The current state.
- * @param actionIndex The index of the action label to select.
- * @return A list of lists of active commands or nothing.
- */
- static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex);
-
- 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, 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.
*
@@ -333,7 +255,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, 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);
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, 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.
@@ -343,7 +265,7 @@ namespace storm {
* @param options A set of options used to customize the building process.
* @return A structure containing the components of the resulting model.
*/
- ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options);
+ ModelComponents buildModelComponents(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels);
/*!
* Builds the state labeling for the given program.
@@ -353,17 +275,34 @@ namespace storm {
* @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, InternalStateInformation const& internalStateInformation);
+ storm::models::sparse::StateLabeling buildStateLabeling();
+
+ // The program to translate. The necessary transformations are performed upon construction of the builder.
+ storm::prism::Program program;
+
+ // The options to be used for translating the program.
+ Options options;
+
+ // The variable information.
+ VariableInformation variableInformation;
+
+ // Internal information about the states that were explored.
+ InternalStateInformation internalStateInformation;
// This member holds information about reachable states that can be retrieved from the outside after a
// successful build.
boost::optional<StateInformation> stateInformation;
- // This member holds the program that was most recently translated (if any).
- boost::optional<storm::prism::Program> preparedProgram;
+ // A set of states that still need to be explored.
+ std::deque<CompressedState> statesToExplore;
+
+ // An optional mapping from state indices to the row groups in which they actually reside. This needs to be
+ // built in case the exploration order is not BFS.
+ boost::optional<std::vector<uint_fast64_t>> stateRemapping;
+
};
} // namespace adapters
} // namespace storm
-#endif /* STORM_ADAPTERS_EXPLICITPRISMMODELBUILDER_H */
+#endif /* STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H */
diff --git a/src/builder/ExplorationOrder.cpp b/src/builder/ExplorationOrder.cpp
new file mode 100644
index 000000000..fb0b82766
--- /dev/null
+++ b/src/builder/ExplorationOrder.cpp
@@ -0,0 +1,22 @@
+#include "src/builder/ExplorationOrder.h"
+
+namespace storm {
+ namespace builder {
+
+ std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order) {
+ switch (order) {
+ case ExplorationOrder::Dfs:
+ out << "depth-first";
+ break;
+ case ExplorationOrder::Bfs:
+ out << "breadth-first";
+ break;
+ default:
+ out << "undefined";
+ break;
+ }
+ return out;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/builder/ExplorationOrder.h b/src/builder/ExplorationOrder.h
new file mode 100644
index 000000000..94c6363b3
--- /dev/null
+++ b/src/builder/ExplorationOrder.h
@@ -0,0 +1,17 @@
+#ifndef STORM_BUILDER_EXPLORATIONORDER_H_
+#define STORM_BUILDER_EXPLORATIONORDER_H_
+
+#include <ostream>
+
+namespace storm {
+ namespace builder {
+
+ // An enum that contains all currently supported exploration orders.
+ enum class ExplorationOrder { Dfs, Bfs };
+
+ std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order);
+
+ }
+}
+
+#endif /* STORM_BUILDER_EXPLORATIONORDER_H_ */
\ No newline at end of file
diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp
new file mode 100644
index 000000000..9202f2c5e
--- /dev/null
+++ b/src/generator/Choice.cpp
@@ -0,0 +1,105 @@
+#include "src/generator/Choice.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+#include "src/utility/constants.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType>
+ Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceRewards() {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType, typename StateType>
+ typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::begin() {
+ return distribution.begin();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::begin() const {
+ return distribution.cbegin();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::end() {
+ return distribution.end();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::end() const {
+ return distribution.cend();
+ }
+
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::addChoiceLabel(uint_fast64_t label) {
+ if (!choiceLabels) {
+ choiceLabels = LabelSet();
+ }
+ choiceLabels->insert(label);
+ }
+
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::addChoiceLabels(LabelSet const& labelSet) {
+ if (!choiceLabels) {
+ choiceLabels = LabelSet();
+ }
+ choiceLabels->insert(labelSet.begin(), labelSet.end());
+ }
+
+ template<typename ValueType, typename StateType>
+ boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getChoiceLabels() const {
+ return *choiceLabels;
+ }
+
+ template<typename ValueType, typename StateType>
+ uint_fast64_t Choice<ValueType, StateType>::getActionIndex() const {
+ return actionIndex;
+ }
+
+ template<typename ValueType, typename StateType>
+ ValueType Choice<ValueType, StateType>::getTotalMass() const {
+ return totalMass;
+ }
+
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
+ totalMass += value;
+ distribution.addProbability(state, value);
+ }
+
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) {
+ choiceRewards.push_back(value);
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<ValueType> const& Choice<ValueType, StateType>::getChoiceRewards() const {
+ return choiceRewards;
+ }
+
+ template<typename ValueType, typename StateType>
+ bool Choice<ValueType, StateType>::isMarkovian() const {
+ return markovian;
+ }
+
+ template<typename ValueType, typename StateType>
+ std::size_t Choice<ValueType, StateType>::size() const {
+ return distribution.size();
+ }
+
+ template<typename ValueType, typename StateType>
+ std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) {
+ out << "<";
+ for (auto const& stateProbabilityPair : choice) {
+ out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
+ }
+ out << ">";
+ return out;
+ }
+
+ template class Choice<double>;
+ template class Choice<storm::RationalFunction>;
+ }
+}
\ No newline at end of file
diff --git a/src/generator/Choice.h b/src/generator/Choice.h
new file mode 100644
index 000000000..76b6c8d16
--- /dev/null
+++ b/src/generator/Choice.h
@@ -0,0 +1,150 @@
+#ifndef STORM_GENERATOR_CHOICE_H_
+#define STORM_GENERATOR_CHOICE_H_
+
+#include <cstdint>
+#include <functional>
+
+#include <boost/optional.hpp>
+#include <boost/container/flat_set.hpp>
+
+#include "src/storage/Distribution.h"
+
+namespace storm {
+ namespace generator {
+
+ // A structure holding information about a particular choice.
+ template<typename ValueType, typename StateType=uint32_t>
+ struct Choice {
+ public:
+ typedef boost::container::flat_set<uint_fast64_t> LabelSet;
+
+ Choice(uint_fast64_t actionIndex = 0, bool markovian = false);
+
+ Choice(Choice const& other) = default;
+ Choice& operator=(Choice const& other) = default;
+ Choice(Choice&& other) = default;
+ Choice& operator=(Choice&& other) = default;
+
+ /*!
+ * Returns an iterator to the distribution associated with this choice.
+ *
+ * @return An iterator to the first element of the distribution.
+ */
+ typename storm::storage::Distribution<ValueType, StateType>::iterator begin();
+
+ /*!
+ * Returns an iterator to the distribution associated with this choice.
+ *
+ * @return An iterator to the first element of the distribution.
+ */
+ typename storm::storage::Distribution<ValueType, StateType>::const_iterator begin() const;
+
+ /*!
+ * Returns an iterator past the end of the distribution associated with this choice.
+ *
+ * @return An iterator past the end of the distribution.
+ */
+ typename storm::storage::Distribution<ValueType, StateType>::iterator end();
+
+ /*!
+ * Returns an iterator past the end of the distribution associated with this choice.
+ *
+ * @return An iterator past the end of the distribution.
+ */
+ typename storm::storage::Distribution<ValueType, StateType>::const_iterator end() const;
+
+ /*!
+ * Inserts the contents of this object to the given output stream.
+ *
+ * @param out The stream in which to insert the contents.
+ */
+ template<typename ValueTypePrime, typename StateTypePrime>
+ friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice);
+
+ /*!
+ * Adds the given label to the labels associated with this choice.
+ *
+ * @param label The label to associate with this choice.
+ */
+ void addChoiceLabel(uint_fast64_t label);
+
+ /*!
+ * Adds the given label set to the labels associated with this choice.
+ *
+ * @param labelSet The label set to associate with this choice.
+ */
+ void addChoiceLabels(LabelSet const& labelSet);
+
+ /*!
+ * Retrieves the set of labels associated with this choice.
+ *
+ * @return The set of labels associated with this choice.
+ */
+ LabelSet const& getChoiceLabels() const;
+
+ /*!
+ * Retrieves the index of the action of this choice.
+ *
+ * @return The index of the action of this choice.
+ */
+ uint_fast64_t getActionIndex() const;
+
+ /*!
+ * Retrieves the total mass of this choice.
+ *
+ * @return The total mass.
+ */
+ ValueType getTotalMass() const;
+
+ /*!
+ * Adds the given probability value to the given state in the underlying distribution.
+ */
+ void addProbability(StateType const& state, ValueType const& value);
+
+ /*!
+ * Adds the given value to the reward associated with this choice.
+ */
+ void addChoiceReward(ValueType const& value);
+
+ /*!
+ * Retrieves the rewards for this choice under selected reward models.
+ */
+ std::vector<ValueType> const& getChoiceRewards() const;
+
+ /*!
+ * Retrieves whether the choice is Markovian.
+ */
+ bool isMarkovian() const;
+
+ /*!
+ * Retrieves the size of the distribution associated with this choice.
+ */
+ std::size_t size() const;
+
+ private:
+ // A flag indicating whether this choice is Markovian or not.
+ bool markovian;
+
+ // The action index associated with this choice.
+ uint_fast64_t actionIndex;
+
+ // The distribution that is associated with the choice.
+ storm::storage::Distribution<ValueType, StateType> distribution;
+
+ // The total probability mass (or rates) of this choice.
+ ValueType totalMass;
+
+ // The reward values associated with this choice.
+ std::vector<ValueType> choiceRewards;
+
+ // The labels that are associated with this choice.
+ boost::optional<LabelSet> choiceLabels;
+ };
+
+ template<typename ValueType, typename StateType>
+ std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice);
+
+ }
+}
+
+#endif /* STORM_GENERATOR_CHOICE_H_ */
\ No newline at end of file
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
new file mode 100644
index 000000000..c63504ebb
--- /dev/null
+++ b/src/generator/CompressedState.cpp
@@ -0,0 +1,23 @@
+#include "src/generator/CompressedState.h"
+
+#include "src/generator/VariableInformation.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType>
+ void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
+ for (auto const& booleanVariable : variableInformation.booleanVariables) {
+ evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
+ }
+ for (auto const& integerVariable : variableInformation.integerVariables) {
+ evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
+ }
+
+ }
+
+ template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
+ template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
+ }
+}
\ No newline at end of file
diff --git a/src/generator/CompressedState.h b/src/generator/CompressedState.h
new file mode 100644
index 000000000..52f0b4a62
--- /dev/null
+++ b/src/generator/CompressedState.h
@@ -0,0 +1,30 @@
+#ifndef STORM_GENERATOR_COMPRESSEDSTATE_H_
+#define STORM_GENERATOR_COMPRESSEDSTATE_H_
+
+#include "src/storage/BitVector.h"
+
+namespace storm {
+ namespace expressions {
+ template<typename ValueType> class ExpressionEvaluator;
+ }
+
+ namespace generator {
+
+ typedef storm::storage::BitVector CompressedState;
+
+ class VariableInformation;
+
+ /*!
+ * Unpacks the compressed state into the evaluator.
+ *
+ * @param state The state to unpack.
+ * @param variableInformation The information about how the variables are packed with the state.
+ * @param evaluator The evaluator into which to load the state.
+ */
+ template<typename ValueType>
+ void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
+ }
+}
+
+#endif /* STORM_GENERATOR_COMPRESSEDSTATE_H_ */
+
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
new file mode 100644
index 000000000..779a49ef3
--- /dev/null
+++ b/src/generator/NextStateGenerator.h
@@ -0,0 +1,24 @@
+#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_
+
+#include <vector>
+#include <cstdint>
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/StateBehavior.h"
+
+namespace storm {
+ namespace generator {
+ template<typename ValueType, typename StateType = uint32_t>
+ class NextStateGenerator {
+ public:
+ typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
+
+ virtual bool isDeterministicModel() const = 0;
+ virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
+ virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) = 0;
+ };
+ }
+}
+
+#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
new file mode 100644
index 000000000..fac3be0f5
--- /dev/null
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -0,0 +1,404 @@
+#include "src/generator/PrismNextStateGenerator.h"
+
+#include <boost/container/flat_map.hpp>
+
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType>
+ PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType, typename StateType>
+ void PrismNextStateGenerator<ValueType, StateType>::addRewardModel(storm::prism::RewardModel const& rewardModel) {
+ selectedRewardModels.push_back(rewardModel);
+ hasStateActionRewards |= rewardModel.hasStateActionRewards();
+ }
+
+ template<typename ValueType, typename StateType>
+ void PrismNextStateGenerator<ValueType, StateType>::setTerminalExpression(storm::expressions::Expression const& terminalExpression) {
+ this->terminalExpression = terminalExpression;
+ }
+
+ template<typename ValueType, typename StateType>
+ bool PrismNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
+ return program.isDeterministicModel();
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
+ // FIXME: This only works for models with exactly one initial state. We should make this more general.
+ CompressedState initialState(variableInformation.getTotalBitOffset());
+
+ // We need to initialize the values of the variables to their initial value.
+ for (auto const& booleanVariable : variableInformation.booleanVariables) {
+ initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
+ }
+ for (auto const& integerVariable : variableInformation.integerVariables) {
+ initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
+ }
+
+ // Register initial state and return it.
+ StateType id = stateToIdCallback(initialState);
+ return {id};
+ }
+
+ template<typename ValueType, typename StateType>
+ StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) {
+ // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
+ unpackStateIntoEvaluator(state, variableInformation, evaluator);
+
+ // Prepare the result, in case we return early.
+ StateBehavior<ValueType, StateType> result;
+
+ // First, construct the state rewards, as we may return early if there are no choices later and we already
+ // need the state rewards then.
+ for (auto const& rewardModel : selectedRewardModels) {
+ ValueType stateRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateRewards()) {
+ for (auto const& stateReward : rewardModel.get().getStateRewards()) {
+ if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
+ stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
+ }
+ }
+ }
+ result.addStateReward(stateRewardValue);
+ }
+
+ // If a terminal expression was set and we must not expand this state, return now.
+ if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
+ return result;
+ }
+
+ // Get all choices for the state.
+ std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(state, stateToIdCallback);
+ std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(state, stateToIdCallback);
+ for (auto& choice : allLabeledChoices) {
+ allChoices.push_back(std::move(choice));
+ }
+
+ std::size_t totalNumberOfChoices = allChoices.size();
+
+ // If there is not a single choice, we return immediately, because the state has no behavior (other than
+ // the state reward).
+ if (totalNumberOfChoices == 0) {
+ return result;
+ }
+
+ // If the model is a deterministic model, we need to fuse the choices into one.
+ if (program.isDeterministicModel() && totalNumberOfChoices > 1) {
+ Choice<ValueType> globalChoice;
+
+ // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
+ // this is equal to the number of choices, which is why we initialize it like this here.
+ ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
+
+ // Iterate over all choices and combine the probabilities/rates into one choice.
+ for (auto const& choice : allChoices) {
+ for (auto const& stateProbabilityPair : choice) {
+ if (program.isDiscreteTimeModel()) {
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
+ } else {
+ globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
+ }
+ }
+
+ if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
+ totalExitRate += choice.getTotalMass();
+ }
+
+ if (buildChoiceLabeling) {
+ globalChoice.addChoiceLabels(choice.getChoiceLabels());
+ }
+ }
+
+ // Now construct the state-action reward for all selected reward models.
+ for (auto const& rewardModel : selectedRewardModels) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+ for (auto const& choice : allChoices) {
+ if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
+ }
+ }
+
+ }
+ }
+ globalChoice.addChoiceReward(stateActionRewardValue);
+ }
+
+ // Move the newly fused choice in place.
+ allChoices.clear();
+ allChoices.push_back(std::move(globalChoice));
+ }
+
+ // Move all remaining choices in place.
+ for (auto& choice : allChoices) {
+ result.addChoice(std::move(choice));
+ }
+
+ result.setExpanded();
+ return result;
+ }
+
+ template<typename ValueType, typename StateType>
+ CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
+ CompressedState 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;
+ }
+ int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
+ STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
+ newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+ STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
+ }
+
+ // Check that we processed all assignments.
+ STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
+
+ return newState;
+ }
+
+ template<typename ValueType, typename StateType>
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
+
+ // Iterate over all modules.
+ for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+ storm::prism::Module const& module = program.getModule(i);
+
+ // If the module has no command labeled with the given action, we can skip this module.
+ if (!module.hasActionIndex(actionIndex)) {
+ continue;
+ }
+
+ std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
+
+ // If the module contains the action, but there is no command in the module that is labeled with
+ // this action, we don't have any feasible command combinations.
+ if (commandIndices.empty()) {
+ return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
+ }
+
+ std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
+
+ // Look up commands by their indices and add them if the guard evaluates to true in the given state.
+ for (uint_fast64_t commandIndex : commandIndices) {
+ storm::prism::Command const& command = module.getCommand(commandIndex);
+ if (evaluator.asBool(command.getGuardExpression())) {
+ commands.push_back(command);
+ }
+ }
+
+ // If there was no enabled command although the module has some command with the required action label,
+ // we must not return anything.
+ if (commands.size() == 0) {
+ return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
+ }
+
+ result.get().push_back(std::move(commands));
+ }
+
+ return result;
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+ std::vector<Choice<ValueType>> result;
+
+ // Iterate over all modules.
+ for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+ storm::prism::Module const& module = program.getModule(i);
+
+ // Iterate over all commands.
+ for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+ storm::prism::Command const& command = module.getCommand(j);
+
+ // Only consider unlabeled commands.
+ if (command.isLabeled()) continue;
+
+ // Skip the command, if it is not enabled.
+ if (!evaluator.asBool(command.getGuardExpression())) {
+ continue;
+ }
+
+ result.push_back(Choice<ValueType>(command.getActionIndex()));
+ Choice<ValueType>& choice = result.back();
+
+ // Remember the command labels only if we were asked to.
+ if (buildChoiceLabeling) {
+ choice.addChoiceLabel(command.getGlobalIndex());
+ }
+
+ // Iterate over all updates of the current command.
+ ValueType probabilitySum = storm::utility::zero<ValueType>();
+ for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
+ storm::prism::Update const& update = command.getUpdate(k);
+
+ // 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.
+ StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
+
+ // Update the choice by adding the probability/target state to it.
+ ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
+ choice.addProbability(stateIndex, probability);
+ probabilitySum += probability;
+ }
+
+ // Create the state-action reward for the newly created choice.
+ for (auto const& rewardModel : selectedRewardModels) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+ if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+ }
+ }
+ }
+ choice.addChoiceReward(stateActionRewardValue);
+ }
+
+ // Check that the resulting distribution is in fact a distribution.
+ STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+ }
+ }
+
+ return result;
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+ std::vector<Choice<ValueType>> result;
+
+ for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
+
+ // Only process this action label, if there is at least one feasible solution.
+ if (optionalActiveCommandLists) {
+ std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get();
+ std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size());
+
+ // Initialize the list of iterators.
+ for (size_t i = 0; i < activeCommandList.size(); ++i) {
+ iteratorList[i] = activeCommandList[i].cbegin();
+ }
+
+ // As long as there is one feasible combination of commands, keep on expanding it.
+ bool done = false;
+ while (!done) {
+ boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+ boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+
+ currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+
+ for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+ storm::prism::Command const& command = *iteratorList[i];
+
+ for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
+ storm::prism::Update const& update = command.getUpdate(j);
+
+ for (auto const& stateProbabilityPair : *currentTargetStates) {
+ // Compute the new state under the current update and add it to the set of new target states.
+ CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+ newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
+ }
+ }
+
+ // If there is one more command to come, shift the target states one time step back.
+ if (i < iteratorList.size() - 1) {
+ delete currentTargetStates;
+ currentTargetStates = newTargetStates;
+ newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+ }
+ }
+
+ // At this point, we applied all commands of the current command combination and newTargetStates
+ // contains all target states and their respective probabilities. That means we are now ready to
+ // add the choice to the list of transitions.
+ result.push_back(Choice<ValueType>(actionIndex));
+
+ // Now create the actual distribution.
+ Choice<ValueType>& choice = result.back();
+
+ // Remember the command labels only if we were asked to.
+ if (buildChoiceLabeling) {
+ // Add the labels of all commands to this choice.
+ for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+ choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex());
+ }
+ }
+
+ // Add the probabilities/rates to the newly created choice.
+ ValueType probabilitySum = storm::utility::zero<ValueType>();
+ for (auto const& stateProbabilityPair : *newTargetStates) {
+ StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
+ choice.addProbability(actualIndex, stateProbabilityPair.second);
+ probabilitySum += stateProbabilityPair.second;
+ }
+
+ // Check that the resulting distribution is in fact a distribution.
+ STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+
+ // Create the state-action reward for the newly created choice.
+ for (auto const& rewardModel : selectedRewardModels) {
+ ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
+ if (rewardModel.get().hasStateActionRewards()) {
+ for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
+ if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
+ stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+ }
+ }
+ }
+ choice.addChoiceReward(stateActionRewardValue);
+ }
+
+ // Dispose of the temporary maps.
+ delete currentTargetStates;
+ delete newTargetStates;
+
+ // Now, check whether there is one more command combination to consider.
+ bool movedIterator = false;
+ for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
+ ++iteratorList[j];
+ if (iteratorList[j] != activeCommandList[j].end()) {
+ movedIterator = true;
+ } else {
+ // Reset the iterator to the beginning of the list.
+ iteratorList[j] = activeCommandList[j].begin();
+ }
+ }
+
+ done = !movedIterator;
+ }
+ }
+ }
+
+ return result;
+ }
+
+ template class PrismNextStateGenerator<double>;
+ template class PrismNextStateGenerator<storm::RationalFunction>;
+ }
+}
\ No newline at end of file
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
new file mode 100644
index 000000000..d8eddc0ac
--- /dev/null
+++ b/src/generator/PrismNextStateGenerator.h
@@ -0,0 +1,108 @@
+#ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
+
+#include "src/generator/NextStateGenerator.h"
+#include "src/generator/VariableInformation.h"
+
+#include "src/storage/prism/Program.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+#include "src/utility/ConstantsComparator.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType = uint32_t>
+ class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
+ public:
+ typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+
+ PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling);
+
+ /*!
+ * Adds a reward model to the list of selected reward models ()
+ */
+ void addRewardModel(storm::prism::RewardModel const& rewardModel);
+
+ /*!
+ * Sets an expression such that if it evaluates to true in a state, prevents the exploration.
+ */
+ void setTerminalExpression(storm::expressions::Expression const& terminalExpression);
+
+ virtual bool isDeterministicModel() const override;
+ virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
+ virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) override;
+
+ private:
+ /*!
+ * Applies an update to the state currently loaded into the evaluator and applies the resulting values to
+ * the given compressed state.
+ * @params state The state to which to apply the new values.
+ * @params update The update to apply.
+ * @return The resulting state.
+ */
+ CompressedState applyUpdate(CompressedState const& state, storm::prism::Update const& update);
+
+ /*!
+ * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
+ * modules.
+ *
+ * This function will iterate over all modules and retrieve all commands that are labeled with the given
+ * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
+ * the inner lists contain all commands of exactly one module. If a module does not have *any* (including
+ * disabled) commands, there will not be a list of commands of that module in the result. If, however, the
+ * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
+ * is no legal transition possible.
+ *
+ * @param The program in which to search for active commands.
+ * @param state The current state.
+ * @param actionIndex The index of the action label to select.
+ * @return A list of lists of active commands or nothing.
+ */
+ boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex);
+
+ /*!
+ * Retrieves all unlabeled choices possible from the given state.
+ *
+ * @param state The state for which to retrieve the unlabeled choices.
+ * @return The unlabeled choices of the state.
+ */
+ std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+
+ /*!
+ * Retrieves all labeled choices possible from the given state.
+ *
+ * @param state The state for which to retrieve the unlabeled choices.
+ * @return The labeled choices of the state.
+ */
+ std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+
+ // The program used for the generation of next states.
+ storm::prism::Program const& program;
+
+ // The reward models that need to be considered.
+ std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
+
+ // A flag that stores whether at least one of the selected reward models has state-action rewards.
+ bool hasStateActionRewards;
+
+ // A flag that stores whether or not to build the choice labeling.
+ bool buildChoiceLabeling;
+
+ // An optional expression that governs which states must not be explored.
+ boost::optional<storm::expressions::Expression> terminalExpression;
+
+ // Information about how the variables are packed.
+ VariableInformation const& variableInformation;
+
+ // An evaluator used to evaluate expressions.
+ storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+
+ // A comparator used to compare constants.
+ storm::utility::ConstantsComparator<ValueType> comparator;
+ };
+
+ }
+}
+
+#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/PrismStateLabelingGenerator.cpp b/src/generator/PrismStateLabelingGenerator.cpp
new file mode 100644
index 000000000..6022ce063
--- /dev/null
+++ b/src/generator/PrismStateLabelingGenerator.cpp
@@ -0,0 +1,50 @@
+#include "src/generator/PrismStateLabelingGenerator.h"
+
+#include "src/generator/CompressedState.h"
+
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType>
+ PrismStateLabelingGenerator<ValueType, StateType>::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType, typename StateType>
+ storm::models::sparse::StateLabeling PrismStateLabelingGenerator<ValueType, StateType>::generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
+ std::vector<storm::prism::Label> const& labels = program.getLabels();
+
+ storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
+ storm::models::sparse::StateLabeling result(states.size());
+
+ // Initialize labeling.
+ for (auto const& label : labels) {
+ result.addLabel(label.getName());
+ }
+ for (auto const& stateIndexPair : states) {
+ unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator);
+
+ for (auto const& label : labels) {
+ // Add label to state, if the corresponding expression is true.
+ if (evaluator.asBool(label.getStatePredicateExpression())) {
+ result.addLabelToState(label.getName(), stateIndexPair.second);
+ }
+ }
+ }
+
+ // Also label the initial state with the special label "init".
+ result.addLabel("init");
+ for (auto index : initialStateIndices) {
+ result.addLabelToState("init", index);
+ }
+
+ return result;
+ }
+
+ template class PrismStateLabelingGenerator<double, uint32_t>;
+ template class PrismStateLabelingGenerator<storm::RationalFunction, uint32_t>;
+
+ }
+}
\ No newline at end of file
diff --git a/src/generator/PrismStateLabelingGenerator.h b/src/generator/PrismStateLabelingGenerator.h
new file mode 100644
index 000000000..9859453ba
--- /dev/null
+++ b/src/generator/PrismStateLabelingGenerator.h
@@ -0,0 +1,31 @@
+#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_
+
+#include "src/generator/StateLabelingGenerator.h"
+
+#include "src/generator/VariableInformation.h"
+
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType = uint32_t>
+ class PrismStateLabelingGenerator : public StateLabelingGenerator<StateType> {
+ public:
+ PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation);
+
+ virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
+
+ private:
+ // The program for which to generate the labels.
+ storm::prism::Program const& program;
+
+ // Information about how the variables are packed.
+ VariableInformation const& variableInformation;
+ };
+
+ }
+}
+
+#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp
new file mode 100644
index 000000000..e14417779
--- /dev/null
+++ b/src/generator/StateBehavior.cpp
@@ -0,0 +1,57 @@
+#include "src/generator/StateBehavior.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType>
+ StateBehavior<ValueType, StateType>::StateBehavior() : expanded(false) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType, typename StateType>
+ void StateBehavior<ValueType, StateType>::addChoice(Choice<ValueType, StateType>&& choice) {
+ choices.push_back(std::move(choice));
+ }
+
+ template<typename ValueType, typename StateType>
+ void StateBehavior<ValueType, StateType>::addStateReward(ValueType const& stateReward) {
+ stateRewards.push_back(stateReward);
+ }
+
+ template<typename ValueType, typename StateType>
+ void StateBehavior<ValueType, StateType>::setExpanded(bool newValue) {
+ this->expanded = newValue;
+ }
+
+ template<typename ValueType, typename StateType>
+ bool StateBehavior<ValueType, StateType>::wasExpanded() const {
+ return expanded;
+ }
+
+ template<typename ValueType, typename StateType>
+ bool StateBehavior<ValueType, StateType>::empty() const {
+ return choices.empty();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::begin() const {
+ return choices.begin();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::end() const {
+ return choices.end();
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<ValueType> const& StateBehavior<ValueType, StateType>::getStateRewards() const {
+ return stateRewards;
+ }
+
+ template class StateBehavior<double>;
+ template class StateBehavior<storm::RationalFunction>;
+
+ }
+}
\ No newline at end of file
diff --git a/src/generator/StateBehavior.h b/src/generator/StateBehavior.h
new file mode 100644
index 000000000..393c3280c
--- /dev/null
+++ b/src/generator/StateBehavior.h
@@ -0,0 +1,73 @@
+#ifndef STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
+#define STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
+
+#include <cstdint>
+
+#include "src/generator/Choice.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename ValueType, typename StateType = uint32_t>
+ class StateBehavior {
+ public:
+ /*!
+ * Creates an empty behavior, i.e. the state was not yet expanded.
+ */
+ StateBehavior();
+
+ /*!
+ * Adds the given choice to the behavior of the state.
+ */
+ void addChoice(Choice<ValueType, StateType>&& choice);
+
+ /*!
+ * Adds the given state reward to the behavior of the state.
+ */
+ void addStateReward(ValueType const& stateReward);
+
+ /*!
+ * Sets whether the state was expanded.
+ */
+ void setExpanded(bool newValue = true);
+
+ /*!
+ * Retrieves whether the state was expanded.
+ */
+ bool wasExpanded() const;
+
+ /*!
+ * Retrieves whether the behavior is empty in the sense that there are no available choices.
+ */
+ bool empty() const;
+
+ /*!
+ * Retrieves an iterator to the choices available in the behavior.
+ */
+ typename std::vector<Choice<ValueType, StateType>>::const_iterator begin() const;
+
+ /*!
+ * Retrieves an iterator past the choices available in the behavior.
+ */
+ typename std::vector<Choice<ValueType, StateType>>::const_iterator end() const;
+
+ /*!
+ * Retrieves the list of state rewards under selected reward models.
+ */
+ std::vector<ValueType> const& getStateRewards() const;
+
+ private:
+ // The choices available in the state.
+ std::vector<Choice<ValueType, StateType>> choices;
+
+ // The state rewards (under the different, selected reward models) of the state.
+ std::vector<ValueType> stateRewards;
+
+ // A flag indicating whether the state was actually expanded.
+ bool expanded;
+ };
+
+ }
+}
+
+#endif /* STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ */
diff --git a/src/generator/StateLabelingGenerator.h b/src/generator/StateLabelingGenerator.h
new file mode 100644
index 000000000..17401c703
--- /dev/null
+++ b/src/generator/StateLabelingGenerator.h
@@ -0,0 +1,20 @@
+#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_
+#define STORM_GENERATOR_STATELABELINGGENERATOR_H_
+
+#include "src/models/sparse/StateLabeling.h"
+
+#include "src/storage/BitVectorHashMap.h"
+
+namespace storm {
+ namespace generator {
+
+ template<typename StateType = uint32_t>
+ class StateLabelingGenerator {
+ public:
+ virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0;
+ };
+
+ }
+}
+
+#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */
\ No newline at end of file
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
new file mode 100644
index 000000000..a5be93a6e
--- /dev/null
+++ b/src/generator/VariableInformation.cpp
@@ -0,0 +1,77 @@
+#include "src/generator/VariableInformation.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace generator {
+
+ BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
+ // Intentionally left empty.
+ }
+
+ 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.
+ }
+
+ VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
+ for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
+ booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset);
+ ++totalBitOffset;
+ booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1;
+ }
+ for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
+ int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
+ int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
+ uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+ integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth);
+ totalBitOffset += bitwidth;
+ integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1;
+ }
+ for (auto const& module : program.getModules()) {
+ for (auto const& booleanVariable : module.getBooleanVariables()) {
+ booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset);
+ ++totalBitOffset;
+ booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1;
+ }
+ for (auto const& integerVariable : module.getIntegerVariables()) {
+ int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
+ int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
+ uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
+ integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth);
+ totalBitOffset += bitwidth;
+ integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1;
+ }
+ }
+ }
+
+ uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {
+ uint_fast64_t result = totalBitOffset;
+ if (roundTo64Bit) {
+ result = ((result >> 6) + 1) << 6;
+ }
+ return result;
+ }
+
+ uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
+ auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
+ if (booleanIndex != booleanVariableToIndexMap.end()) {
+ return booleanVariables[booleanIndex->second].bitOffset;
+ }
+ auto const& integerIndex = integerVariableToIndexMap.find(variable);
+ if (integerIndex != integerVariableToIndexMap.end()) {
+ return integerVariables[integerIndex->second].bitOffset;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
+ }
+
+ uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
+ auto const& integerIndex = integerVariableToIndexMap.find(variable);
+ if (integerIndex != integerVariableToIndexMap.end()) {
+ return integerVariables[integerIndex->second].bitWidth;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
new file mode 100644
index 000000000..8c2841dfd
--- /dev/null
+++ b/src/generator/VariableInformation.h
@@ -0,0 +1,75 @@
+#ifndef STORM_GENERATOR_VARIABLEINFORMATION_H_
+#define STORM_GENERATOR_VARIABLEINFORMATION_H_
+
+#include <vector>
+#include <boost/container/flat_map.hpp>
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/prism/Program.h"
+
+namespace storm {
+ namespace generator {
+
+ // A structure storing information about the boolean variables of the program.
+ struct BooleanVariableInformation {
+ BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
+
+ // The boolean variable.
+ storm::expressions::Variable variable;
+
+ // Its initial value.
+ bool initialValue;
+
+ // Its bit offset in the compressed state.
+ uint_fast64_t bitOffset;
+ };
+
+ // A structure storing information about the integer variables of the program.
+ 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);
+
+ // The integer variable.
+ storm::expressions::Variable variable;
+
+ // Its initial value.
+ int_fast64_t initialValue;
+
+ // The lower bound of its range.
+ int_fast64_t lowerBound;
+
+ // The upper bound of its range.
+ int_fast64_t upperBound;
+
+ // Its bit offset in the compressed state.
+ uint_fast64_t bitOffset;
+
+ // Its bit width in the compressed state.
+ uint_fast64_t bitWidth;
+ };
+
+ // A structure storing information about the used variables of the program.
+ struct VariableInformation {
+ VariableInformation() = default;
+ VariableInformation(storm::prism::Program const& program);
+ uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
+
+ // Provide methods to access the bit offset and width of variables in the compressed state.
+ uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
+ uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
+
+ // The total bit offset over all variables.
+ uint_fast64_t totalBitOffset;
+
+ // The known boolean variables.
+ boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
+ std::vector<BooleanVariableInformation> booleanVariables;
+
+ // The known integer variables.
+ boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
+ std::vector<IntegerVariableInformation> integerVariables;
+ };
+
+ }
+}
+
+#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 5043c8296..a4724da46 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -354,7 +354,7 @@ namespace storm {
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
-
+
// Compute the total state reward vector.
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 9040f3cf4..b2a153f99 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -11,7 +11,7 @@ namespace storm {
namespace parser {
storm::prism::Program PrismParser::parse(std::string const& filename) {
// Open file and initialize result.
- std::ifstream inputFileStream(filename, std::ios::in);
+ std::ifstream inputFileStream(filename);
STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
storm::prism::Program result;
@@ -35,7 +35,7 @@ namespace storm {
PositionIteratorType first(input.begin());
PositionIteratorType iter = first;
PositionIteratorType last(input.end());
- assert(first != last);
+ STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser.");
// Create empty result;
storm::prism::Program result;
diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h
index 235ddd765..6e1b4aa02 100644
--- a/src/settings/ArgumentValidators.h
+++ b/src/settings/ArgumentValidators.h
@@ -18,6 +18,7 @@
#include "src/exceptions/IllegalArgumentValueException.h"
#include "src/exceptions/IllegalFunctionCallException.h"
+#include <sys/stat.h>
namespace storm {
namespace settings {
@@ -97,11 +98,16 @@ namespace storm {
*/
static std::function<bool (std::string const&)> existingReadableFileValidator() {
return [] (std::string const fileName) -> bool {
- std::ifstream targetFile(fileName);
- bool isFileGood = targetFile.good();
-
- STORM_LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable.");
- return isFileGood;
+ // First check existence as ifstream::good apparently als returns true for directories.
+ struct stat info;
+ stat(fileName.c_str(), &info);
+ STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << fileName << "'.");
+
+ // Now that we know it's a file, we can check its readability.
+ std::ifstream istream(fileName);
+ STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << fileName << "'.");
+
+ return true;
};
}
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 122cb23ad..85dc49c2d 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -32,6 +32,8 @@ namespace storm {
const std::string GeneralSettings::explicitOptionShortName = "exp";
const std::string GeneralSettings::symbolicOptionName = "symbolic";
const std::string GeneralSettings::symbolicOptionShortName = "s";
+ const std::string GeneralSettings::explorationOrderOptionName = "explorder";
+ const std::string GeneralSettings::explorationOrderOptionShortName = "eo";
const std::string GeneralSettings::propertyOptionName = "prop";
const std::string GeneralSettings::propertyOptionShortName = "prop";
const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
@@ -83,6 +85,11 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+
+ std::vector<std::string> explorationOrders = {"dfs", "bfs"};
+ this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
+
this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the formulas to be checked on the model.").setShortName(propertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
@@ -186,6 +193,20 @@ namespace storm {
return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
}
+ bool GeneralSettings::isExplorationOrderSet() const {
+ return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
+ }
+
+ storm::builder::ExplorationOrder GeneralSettings::getExplorationOrder() const {
+ std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
+ if (explorationOrderAsString == "dfs") {
+ return storm::builder::ExplorationOrder::Dfs;
+ } else if (explorationOrderAsString == "bfs") {
+ return storm::builder::ExplorationOrder::Bfs;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'.");
+ }
+
bool GeneralSettings::isPropertySet() const {
return this->getOption(propertyOptionName).getHasOptionBeenSet();
}
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index f2cbdca47..4eb493e4d 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -4,6 +4,8 @@
#include "storm-config.h"
#include "src/settings/modules/ModuleSettings.h"
+#include "src/builder/ExplorationOrder.h"
+
namespace storm {
namespace solver {
enum class EquationSolverType;
@@ -25,7 +27,6 @@ namespace storm {
class GeneralSettings : public ModuleSettings {
public:
// An enumeration of all engines.
-
enum class Engine {
Sparse, Hybrid, Dd, Learning, AbstractionRefinement
};
@@ -138,6 +139,20 @@ namespace storm {
* @return The name of the file that contains the symbolic model specification.
*/
std::string getSymbolicModelFilename() const;
+
+ /*!
+ * Retrieves whether the model exploration order was set.
+ *
+ * @return True if the model exploration option was set.
+ */
+ bool isExplorationOrderSet() const;
+
+ /*!
+ * Retrieves the exploration order if it was set.
+ *
+ * @return The chosen exploration order.
+ */
+ storm::builder::ExplorationOrder getExplorationOrder() const;
/*!
* Retrieves whether the property option was set.
@@ -389,6 +404,8 @@ namespace storm {
static const std::string explicitOptionShortName;
static const std::string symbolicOptionName;
static const std::string symbolicOptionShortName;
+ static const std::string explorationOrderOptionName;
+ static const std::string explorationOrderOptionShortName;
static const std::string propertyOptionName;
static const std::string propertyOptionShortName;
static const std::string transitionRewardsOptionName;
diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp
index ddfcb9de9..5919b96a0 100644
--- a/src/storage/BitVector.cpp
+++ b/src/storage/BitVector.cpp
@@ -60,11 +60,11 @@ namespace storm {
return currentIndex == other.currentIndex;
}
- BitVector::BitVector() : bitCount(0), bucketVector() {
+ BitVector::BitVector() : bitCount(0), buckets(nullptr) {
// Intentionally left empty.
}
- BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length) {
+ BitVector::BitVector(uint_fast64_t length, bool init) : bitCount(length), buckets(nullptr) {
// Compute the correct number of buckets needed to store the given number of bits.
uint_fast64_t bucketCount = length >> 6;
if ((length & mod64mask) != 0) {
@@ -73,10 +73,17 @@ namespace storm {
// Initialize the storage with the required values.
if (init) {
- bucketVector = std::vector<uint64_t>(bucketCount, -1ll);
+ buckets = new uint64_t[bucketCount];
+ std::fill_n(buckets, bucketCount, -1ull);
truncateLastBucket();
} else {
- bucketVector = std::vector<uint64_t>(bucketCount, 0);
+ buckets = new uint64_t[bucketCount]();
+ }
+ }
+
+ BitVector::~BitVector() {
+ if (buckets != nullptr) {
+ delete buckets;
}
}
@@ -89,23 +96,22 @@ namespace storm {
// Intentionally left empty.
}
- BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), bucketVector(bucketCount) {
+ BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), buckets(nullptr) {
STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets.");
+ buckets = new uint64_t[bucketCount]();
}
- BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), bucketVector(other.bucketVector) {
- // Intentionally left empty.
+ BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), buckets(nullptr) {
+ buckets = new uint64_t[other.bucketCount()];
+ std::copy_n(other.buckets, other.bucketCount(), buckets);
}
- //BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
- // Intentionally left empty.
- //}
-
BitVector& BitVector::operator=(BitVector const& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
bitCount = other.bitCount;
- bucketVector = std::vector<uint64_t>(other.bucketVector);
+ buckets = new uint64_t[other.bucketCount()];
+ std::copy_n(other.buckets, other.bucketCount(), buckets);
}
return *this;
}
@@ -117,9 +123,9 @@ namespace storm {
return false;
}
- std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin();
- std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end();
- std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
+ uint64_t* first1 = this->buckets;
+ uint64_t* last1 = this->buckets + this->bucketCount();
+ uint64_t* first2 = other.buckets;
for (; first1 != last1; ++first1, ++first2) {
if (*first1 < *first2) {
@@ -130,12 +136,18 @@ namespace storm {
}
return false;
}
+
+ BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), buckets(other.buckets) {
+ other.bitCount = 0;
+ other.buckets = nullptr;
+ }
BitVector& BitVector::operator=(BitVector&& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
bitCount = other.bitCount;
- bucketVector = std::move(other.bucketVector);
+ this->buckets = other.buckets;
+ other.buckets = nullptr;
}
return *this;
@@ -146,14 +158,7 @@ namespace storm {
if (this->bitCount != other.bitCount) return false;
// If the lengths match, we compare the buckets one by one.
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
- if (*it1 != *it2) {
- return false;
- }
- }
-
- // All buckets were equal, so the bit vectors are equal.
- return true;
+ return std::equal(this->buckets, this->buckets + this->bucketCount(), other.buckets);
}
bool BitVector::operator!=(BitVector const& other) const {
@@ -166,9 +171,9 @@ namespace storm {
uint64_t mask = 1ull << (63 - (index & mod64mask));
if (value) {
- bucketVector[bucket] |= mask;
+ buckets[bucket] |= mask;
} else {
- bucketVector[bucket] &= ~mask;
+ buckets[bucket] &= ~mask;
}
}
@@ -182,7 +187,7 @@ namespace storm {
bool BitVector::operator[](uint_fast64_t index) const {
uint64_t bucket = index >> 6;
uint64_t mask = 1ull << (63 - (index & mod64mask));
- return (this->bucketVector[bucket] & mask) == mask;
+ return (this->buckets[bucket] & mask) == mask;
}
bool BitVector::get(uint_fast64_t index) const {
@@ -197,89 +202,80 @@ namespace storm {
++newBucketCount;
}
- if (newBucketCount > bucketVector.size()) {
+ if (newBucketCount > this->bucketCount()) {
+ uint64_t* newBuckets = new uint64_t[newBucketCount];
+ std::copy_n(buckets, this->bucketCount(), newBuckets);
if (init) {
- bucketVector.back() |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
- bucketVector.resize(newBucketCount, -1ull);
+ newBuckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
+ std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), -1ull);
} else {
- bucketVector.resize(newBucketCount, 0);
+ std::fill_n(newBuckets + this->bucketCount(), newBucketCount - this->bucketCount(), 0);
+ }
+ if (buckets != nullptr) {
+ delete buckets;
}
+ buckets = newBuckets;
bitCount = newLength;
} else {
// If the underlying storage does not need to grow, we have to insert the missing bits.
if (init) {
- bucketVector.back() |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
+ buckets[this->bucketCount() - 1] |= ((1ull << (64 - (bitCount & mod64mask))) - 1ull);
}
bitCount = newLength;
}
truncateLastBucket();
} else {
- bitCount = newLength;
uint_fast64_t newBucketCount = newLength >> 6;
if ((newLength & mod64mask) != 0) {
++newBucketCount;
}
- bucketVector.resize(newBucketCount);
+ // If the number of buckets needs to be reduced, we resize it now. Otherwise, we can just truncate the
+ // last bucket.
+ if (newBucketCount < this->bucketCount()) {
+ uint64_t* newBuckets = new uint64_t[newBucketCount];
+ std::copy_n(buckets, newBucketCount, newBuckets);
+ if (buckets != nullptr) {
+ delete buckets;
+ }
+ buckets = newBuckets;
+ bitCount = newLength;
+ }
+ bitCount = newLength;
truncateLastBucket();
}
}
BitVector BitVector::operator&(BitVector const& other) const {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
BitVector result(bitCount);
- std::vector<uint64_t>::iterator it = result.bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
- *it = *it1 & *it2;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a & b; });
return result;
}
BitVector& BitVector::operator&=(BitVector const& other) {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
- std::vector<uint64_t>::iterator it = bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
- *it &= *otherIt;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets, [] (uint64_t const& a, uint64_t const& b) { return a & b; });
return *this;
}
BitVector BitVector::operator|(BitVector const& other) const {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
BitVector result(bitCount);
- std::vector<uint64_t>::iterator it = result.bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
- *it = *it1 | *it2;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a | b; });
return result;
}
BitVector& BitVector::operator|=(BitVector const& other) {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
- std::vector<uint64_t>::iterator it = bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
- *it |= *otherIt;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, this->buckets, [] (uint64_t const& a, uint64_t const& b) { return a | b; });
return *this;
}
BitVector BitVector::operator^(BitVector const& other) const {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
-
BitVector result(bitCount);
- std::vector<uint64_t>::iterator it = result.bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
- *it = *it1 ^ *it2;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return a ^ b; });
result.truncateLastBucket();
return result;
}
@@ -314,19 +310,13 @@ namespace storm {
BitVector BitVector::operator~() const {
BitVector result(this->bitCount);
- std::vector<uint64_t>::iterator it = result.bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it) {
- *it = ~(*it1);
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), result.buckets, [] (uint64_t const& a) { return ~a; });
result.truncateLastBucket();
return result;
}
void BitVector::complement() {
- for (auto& element : bucketVector) {
- element = ~element;
- }
+ std::transform(this->buckets, this->buckets + this->bucketCount(), this->buckets, [] (uint64_t const& a) { return ~a; });
truncateLastBucket();
}
@@ -334,11 +324,7 @@ namespace storm {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
BitVector result(bitCount);
- std::vector<uint64_t>::iterator it = result.bucketVector.begin();
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
- *it = ~(*it1) | *it2;
- }
-
+ std::transform(this->buckets, this->buckets + this->bucketCount(), other.buckets, result.buckets, [] (uint64_t const& a, uint64_t const& b) { return (~a | b); });
result.truncateLastBucket();
return result;
}
@@ -346,7 +332,11 @@ namespace storm {
bool BitVector::isSubsetOf(BitVector const& other) const {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
+ uint64_t const* it1 = buckets;
+ uint64_t const* ite1 = buckets + bucketCount();
+ uint64_t const* it2 = other.buckets;
+
+ for (; it1 != ite1; ++it1, ++it2) {
if ((*it1 & *it2) != *it1) {
return false;
}
@@ -357,7 +347,11 @@ namespace storm {
bool BitVector::isDisjointFrom(BitVector const& other) const {
STORM_LOG_ASSERT(bitCount == other.bitCount, "Length of the bit vectors does not match.");
- for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
+ uint64_t const* it1 = buckets;
+ uint64_t const* ite1 = buckets + bucketCount();
+ uint64_t const* it2 = other.buckets;
+
+ for (; it1 != ite1; ++it1, ++it2) {
if ((*it1 & *it2) != 0) {
return false;
}
@@ -372,9 +366,9 @@ namespace storm {
// Compute the first bucket that needs to be checked and the number of buckets.
uint64_t index = bitIndex >> 6;
- std::vector<uint64_t>::const_iterator first1 = bucketVector.begin() + index;
- std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
- std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
+ uint64_t const* first1 = buckets + index;
+ uint64_t const* first2 = other.buckets;
+ uint64_t const* last2 = other.buckets + other.bucketCount();
for (; first2 != last2; ++first1, ++first2) {
if (*first1 != *first2) {
@@ -391,10 +385,10 @@ namespace storm {
// Compute the first bucket that needs to be checked and the number of buckets.
uint64_t index = bitIndex >> 6;
- std::vector<uint64_t>::iterator first1 = bucketVector.begin() + index;
- std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
- std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
-
+ uint64_t* first1 = buckets + index;
+ uint64_t const* first2 = other.buckets;
+ uint64_t const* last2 = other.buckets + other.bucketCount();
+
for (; first2 != last2; ++first1, ++first2) {
*first1 = *first2;
}
@@ -406,8 +400,8 @@ namespace storm {
STORM_LOG_ASSERT(index + numberOfBuckets <= this->bucketCount(), "Argument is out-of-range.");
storm::storage::BitVector result(numberOfBuckets, numberOfBits);
- std::copy(this->bucketVector.begin() + index, this->bucketVector.begin() + index + numberOfBuckets, result.bucketVector.begin());
-
+ std::copy(this->buckets + index, this->buckets + index + numberOfBuckets, result.buckets);
+ result.truncateLastBucket();
return result;
}
@@ -426,10 +420,10 @@ namespace storm {
if (bitIndexInBucket + numberOfBits < 64) {
// If the value stops before the end of the bucket, we need to erase some lower bits.
mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull);
- return (bucketVector[bucket] & mask) >> (64 - (bitIndexInBucket + numberOfBits));
+ return (buckets[bucket] & mask) >> (64 - (bitIndexInBucket + numberOfBits));
} else if (bitIndexInBucket + numberOfBits > 64) {
// In this case, the integer "crosses" the bucket line.
- uint64_t result = (bucketVector[bucket] & mask);
+ uint64_t result = (buckets[bucket] & mask);
++bucket;
// Compute the remaining number of bits.
@@ -441,13 +435,13 @@ namespace storm {
// Strip away everything from the second bucket that is beyond the final index and add it to the
// intermediate result.
mask = ~((1ull << (64 - numberOfBits)) - 1ull);
- uint64_t lowerBits = bucketVector[bucket] & mask;
+ uint64_t lowerBits = buckets[bucket] & mask;
result |= (lowerBits >> (64 - numberOfBits));
return result;
} else {
// In this case, it suffices to take the current mask.
- return bucketVector[bucket] & mask;
+ return buckets[bucket] & mask;
}
}
@@ -468,10 +462,10 @@ namespace storm {
if (bitIndexInBucket + numberOfBits < 64) {
// If the value stops before the end of the bucket, we need to erase some lower bits.
mask &= ~((1ull << (64 - (bitIndexInBucket + numberOfBits))) - 1ull);
- bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
+ buckets[bucket] = (buckets[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits)));
} else if (bitIndexInBucket + numberOfBits > 64) {
// Write the part of the value that falls into the first bucket.
- bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
+ buckets[bucket] = (buckets[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64)));
++bucket;
// Compute the remaining number of bits.
@@ -482,45 +476,41 @@ namespace storm {
// Put the remaining bits in their place.
mask = ((1ull << (64 - numberOfBits)) - 1ull);
- bucketVector[bucket] = (bucketVector[bucket] & mask) | value;
+ buckets[bucket] = (buckets[bucket] & mask) | value;
} else {
- bucketVector[bucket] = (bucketVector[bucket] & ~mask) | value;
+ buckets[bucket] = (buckets[bucket] & ~mask) | value;
}
}
bool BitVector::empty() const {
- for (auto& element : bucketVector) {
- if (element != 0) {
- return false;
- }
- }
- return true;
+ uint64_t* last = buckets + bucketCount();
+ uint64_t* it = std::find_if(buckets, last, [] (uint64_t const& a) { return a != 0; });
+ return it == last;
}
bool BitVector::full() const {
// Check that all buckets except the last one have all bits set.
- for (uint_fast64_t index = 0; index < bucketVector.size() - 1; ++index) {
- if (bucketVector[index] != -1ull) {
+ uint64_t* last = buckets + bucketCount() - 1;
+ for (uint64_t const* it = buckets; it < last; ++it) {
+ if (*it != -1ull) {
return false;
}
}
-
+
// Now check whether the relevant bits are set in the last bucket.
uint64_t mask = ~((1ull << (64 - (bitCount & mod64mask))) - 1ull);
- if ((bucketVector.back() & mask) != mask) {
+ if ((*last & mask) != mask) {
return false;
}
return true;
}
void BitVector::clear() {
- for (auto& element : bucketVector) {
- element = 0;
- }
+ std::fill_n(buckets, this->bucketCount(), 0);
}
uint_fast64_t BitVector::getNumberOfSetBits() const {
- return getNumberOfSetBitsBeforeIndex(bucketVector.size() << 6);
+ return getNumberOfSetBitsBeforeIndex(bitCount);
}
uint_fast64_t BitVector::getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
@@ -531,14 +521,14 @@ namespace storm {
for (uint_fast64_t i = 0; i < bucket; ++i) {
// Check if we are using g++ or clang++ and, if so, use the built-in function
#if (defined (__GNUG__) || defined(__clang__))
- result += __builtin_popcountll(bucketVector[i]);
+ result += __builtin_popcountll(buckets[i]);
#elif defined WINDOWS
#include <nmmintrin.h>
// If the target machine does not support SSE4, this will fail.
result += _mm_popcnt_u64(bucketVector[i]);
#else
uint_fast32_t cnt;
- uint_fast64_t bitset = bucketVector[i];
+ uint_fast64_t bitset = buckets[i];
for (cnt = 0; bitset; cnt++) {
bitset &= bitset - 1;
}
@@ -550,7 +540,7 @@ namespace storm {
uint64_t tmp = index & mod64mask;
if (tmp != 0) {
tmp = ~((1ll << (64 - (tmp & mod64mask))) - 1ll);
- tmp &= bucketVector[bucket];
+ tmp &= buckets[bucket];
// Check if we are using g++ or clang++ and, if so, use the built-in function
#if (defined (__GNUG__) || defined(__clang__))
result += __builtin_popcountll(tmp);
@@ -587,19 +577,19 @@ namespace storm {
}
std::size_t BitVector::getSizeInBytes() const {
- return sizeof (*this) + sizeof (uint64_t) * bucketVector.size();
+ return sizeof (*this) + sizeof (uint64_t) * bucketCount();
}
BitVector::const_iterator BitVector::begin() const {
- return const_iterator(bucketVector.data(), 0, bitCount);
+ return const_iterator(buckets, 0, bitCount);
}
BitVector::const_iterator BitVector::end() const {
- return const_iterator(bucketVector.data(), bitCount, bitCount, false);
+ return const_iterator(buckets, bitCount, bitCount, false);
}
uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const {
- return getNextSetIndex(bucketVector.data(), startingIndex, bitCount);
+ return getNextSetIndex(buckets, startingIndex, bitCount);
}
uint_fast64_t BitVector::getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) {
@@ -643,17 +633,21 @@ namespace storm {
void BitVector::truncateLastBucket() {
if ((bitCount & mod64mask) != 0) {
- bucketVector.back() &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);
+ buckets[bucketCount() - 1] &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);
}
}
size_t BitVector::bucketCount() const {
- return bucketVector.size();
+ size_t result = (bitCount >> 6);
+ if ((bitCount & mod64mask) != 0) {
+ ++result;
+ }
+ return result;
}
- std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) {
- out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") [";
- for (auto index : bitVector) {
+ std::ostream& operator<<(std::ostream& out, BitVector const& bitvector) {
+ out << "bit vector(" << bitvector.getNumberOfSetBits() << "/" << bitvector.bitCount << ") [";
+ for (auto index : bitvector) {
out << index << " ";
}
out << "]";
@@ -661,13 +655,13 @@ namespace storm {
return out;
}
- std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bv) const {
- STORM_LOG_ASSERT(bv.size() > 0, "Cannot hash bit vector of zero size.");
+ std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const {
+ STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size.");
std::size_t result = 0;
- for (uint_fast64_t index = 0; index < bv.bucketVector.size(); ++index) {
+ for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) {
result ^= result << 3;
- result ^= result >> bv.getAsInt(index << 6, 5);
+ result ^= result >> bitvector.getAsInt(index << 6, 5);
}
// Erase the last bit and add one to definitely make this hash value non-zero.
@@ -691,7 +685,7 @@ namespace storm {
namespace std {
- std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bv) const {
- return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end());
+ std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
+ return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
}
}
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index f9c088ceb..f15eef3ed 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -104,6 +104,11 @@ namespace storm {
*/
BitVector();
+ /*
+ * Deconstructs a bit vector by deleting the underlying storage.
+ */
+ ~BitVector();
+
/*!
* Constructs a bit vector which can hold the given number of bits and initializes all bits with the
* provided truth value.
@@ -141,7 +146,7 @@ namespace storm {
*
* @param other The bit vector from which to move-construct.
*/
- BitVector(BitVector&& other) = default;
+ BitVector(BitVector&& other);
/*!
* Compares the given bit vector with the current one.
@@ -494,7 +499,7 @@ namespace storm {
uint_fast64_t bitCount;
// The underlying storage of 64-bit buckets for all bits of this bit vector.
- std::vector<uint64_t> bucketVector;
+ uint64_t* buckets;
// A bit mask that can be used to reduce a modulo 64 operation to a logical "and".
static const uint_fast64_t mod64mask = (1 << 6) - 1;
diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp
index 328e601c4..c52519d7f 100644
--- a/src/storage/BitVectorHashMap.cpp
+++ b/src/storage/BitVectorHashMap.cpp
@@ -41,7 +41,7 @@ namespace storm {
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.");
@@ -234,6 +234,13 @@ namespace storm {
return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);
}
+ template<class ValueType, class Hash1, class Hash2>
+ void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
+ for (auto pos : occupied) {
+ values[pos] = remapping(values[pos]);
+ }
+ }
+
template class BitVectorHashMap<uint_fast64_t>;
template class BitVectorHashMap<uint32_t>;
}
diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h
index 3b0c7aa70..746467203 100644
--- a/src/storage/BitVectorHashMap.h
+++ b/src/storage/BitVectorHashMap.h
@@ -55,7 +55,7 @@ namespace storm {
* @param loadFactor The load factor that determines at which point the size of the underlying storage is
* increased.
*/
- BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor = 0.75);
+ BitVectorHashMap(uint64_t bucketSize = 64, uint64_t initialSize = 1000, double loadFactor = 0.75);
/*!
* Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the
@@ -123,6 +123,13 @@ namespace storm {
*/
std::size_t capacity() const;
+ /*!
+ * Performs a remapping of all values stored by applying the given remapping.
+ *
+ * @param remapping The remapping to apply.
+ */
+ void remap(std::function<ValueType(ValueType const&)> const& remapping);
+
private:
/*!
* Retrieves whether the given bucket holds a value.
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
index 50d794d01..5843e964b 100644
--- a/src/storage/Distribution.cpp
+++ b/src/storage/Distribution.cpp
@@ -14,13 +14,13 @@
namespace storm {
namespace storage {
- template<typename ValueType>
- Distribution<ValueType>::Distribution() {
+ template<typename ValueType, typename StateType>
+ Distribution<ValueType, StateType>::Distribution() {
// Intentionally left empty.
}
- template<typename ValueType>
- bool Distribution<ValueType>::equals(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ template<typename ValueType, typename StateType>
+ bool Distribution<ValueType, StateType>::equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
// We need to check equality by ourselves, because we need to account for epsilon differences.
if (this->distribution.size() != other.distribution.size()) {
return false;
@@ -42,8 +42,8 @@ namespace storm {
return true;
}
- template<typename ValueType>
- void Distribution<ValueType>::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) {
+ template<typename ValueType, typename StateType>
+ void Distribution<ValueType, StateType>::addProbability(StateType const& state, ValueType const& probability) {
auto it = this->distribution.find(state);
if (it == this->distribution.end()) {
this->distribution.emplace_hint(it, state, probability);
@@ -52,8 +52,8 @@ namespace storm {
}
}
- template<typename ValueType>
- void Distribution<ValueType>::removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
+ template<typename ValueType, typename StateType>
+ void Distribution<ValueType, StateType>::removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
auto it = this->distribution.find(state);
STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution.");
it->second -= probability;
@@ -62,34 +62,44 @@ namespace storm {
}
}
- template<typename ValueType>
- void Distribution<ValueType>::shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
+ template<typename ValueType, typename StateType>
+ void Distribution<ValueType, StateType>::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator) {
removeProbability(fromState, probability, comparator);
addProbability(toState, probability);
}
- template<typename ValueType>
- typename Distribution<ValueType>::iterator Distribution<ValueType>::begin() {
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::iterator Distribution<ValueType, StateType>::begin() {
return this->distribution.begin();
}
- template<typename ValueType>
- typename Distribution<ValueType>::const_iterator Distribution<ValueType>::begin() const {
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::begin() const {
return this->distribution.begin();
}
- template<typename ValueType>
- typename Distribution<ValueType>::iterator Distribution<ValueType>::end() {
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::cbegin() const {
+ return this->begin();
+ }
+
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::iterator Distribution<ValueType, StateType>::end() {
return this->distribution.end();
}
- template<typename ValueType>
- typename Distribution<ValueType>::const_iterator Distribution<ValueType>::end() const {
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::end() const {
return this->distribution.end();
}
+
+ template<typename ValueType, typename StateType>
+ typename Distribution<ValueType, StateType>::const_iterator Distribution<ValueType, StateType>::cend() const {
+ return this->end();
+ }
- template<typename ValueType>
- void Distribution<ValueType>::scale(storm::storage::sparse::state_type const& state) {
+ template<typename ValueType, typename StateType>
+ void Distribution<ValueType, StateType>::scale(StateType const& state) {
auto probabilityIterator = this->distribution.find(state);
if (probabilityIterator != this->distribution.end()) {
ValueType scaleValue = storm::utility::one<ValueType>() / probabilityIterator->second;
@@ -101,13 +111,13 @@ namespace storm {
}
}
- template<typename ValueType>
- std::size_t Distribution<ValueType>::size() const {
+ template<typename ValueType, typename StateType>
+ std::size_t Distribution<ValueType, StateType>::size() const {
return this->distribution.size();
}
- template<typename ValueType>
- std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution) {
+ template<typename ValueType, typename StateType>
+ std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution) {
out << "{";
for (auto const& entry : distribution) {
out << "[" << entry.second << ": " << entry.first << "], ";
@@ -117,8 +127,8 @@ namespace storm {
return out;
}
- template<typename ValueType>
- bool Distribution<ValueType>::less(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ template<typename ValueType, typename StateType>
+ bool Distribution<ValueType, StateType>::less(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
if (this->size() != other.size()) {
return this->size() < other.size();
}
diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h
index 9d3276941..ba61f0fbd 100644
--- a/src/storage/Distribution.h
+++ b/src/storage/Distribution.h
@@ -17,10 +17,10 @@ namespace storm {
namespace storage {
- template<typename ValueType>
+ template<typename ValueType, typename StateType = uint32_t>
class Distribution {
public:
- typedef boost::container::flat_map<storm::storage::sparse::state_type, ValueType> container_type;
+ typedef boost::container::flat_map<StateType, ValueType> container_type;
typedef typename container_type::iterator iterator;
typedef typename container_type::const_iterator const_iterator;
@@ -43,7 +43,7 @@ namespace storm {
* @param other The distribution with which the current distribution is to be compared.
* @return True iff the two distributions are equal.
*/
- bool equals(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
+ bool equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>()) const;
/*!
* Assigns the given state the given probability under this distribution.
@@ -51,7 +51,7 @@ namespace storm {
* @param state The state to which to assign the probability.
* @param probability The probability to assign.
*/
- void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability);
+ void addProbability(StateType const& state, ValueType const& probability);
/*!
* Removes the given probability mass of going to the given state.
@@ -61,7 +61,7 @@ namespace storm {
* @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the
* entry is removed.
*/
- void removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
+ void removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
/*!
* Removes the probability mass from one state and adds it to another.
@@ -72,8 +72,8 @@ namespace storm {
* @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the
* entry is removed.
*/
- void shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
-
+ void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator<ValueType> const& comparator = storm::utility::ConstantsComparator<ValueType>());
+
/*!
* Retrieves an iterator to the elements in this distribution.
*
@@ -88,6 +88,13 @@ namespace storm {
*/
const_iterator begin() const;
+ /*!
+ * Retrieves an iterator to the elements in this distribution.
+ *
+ * @return The iterator to the elements in this distribution.
+ */
+ const_iterator cbegin() const;
+
/*!
* Retrieves an iterator past the elements in this distribution.
*
@@ -102,6 +109,13 @@ namespace storm {
*/
const_iterator end() const;
+ /*!
+ * Retrieves an iterator past the elements in this distribution.
+ *
+ * @return The iterator past the elements in this distribution.
+ */
+ const_iterator cend() const;
+
/*!
* Scales the distribution by multiplying all the probabilities with 1/p where p is the probability of moving
* to the given state and sets the probability of moving to the given state to zero. If the probability is
@@ -109,22 +123,22 @@ namespace storm {
*
* @param state The state whose associated probability is used to scale the distribution.
*/
- void scale(storm::storage::sparse::state_type const& state);
+ void scale(StateType const& state);
/*!
* Retrieves the size of the distribution, i.e. the size of the support set.
*/
std::size_t size() const;
- bool less(Distribution<ValueType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+ bool less(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
private:
// A list of states and the probabilities that are assigned to them.
container_type distribution;
};
- template<typename ValueType>
- std::ostream& operator<<(std::ostream& out, Distribution<ValueType> const& distribution);
+ template<typename ValueType, typename StateType = uint32_t>
+ std::ostream& operator<<(std::ostream& out, Distribution<ValueType, StateType> const& distribution);
}
}
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 3dbabf854..9795dbe2d 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -80,20 +80,23 @@ namespace storm {
if (initialEntryCountSet) {
columnsAndValues.reserve(initialEntryCount);
}
- if (initialRowGroupCountSet) {
- rowGroupIndices.reserve(initialRowGroupCount + 1);
+ if (hasCustomRowGrouping) {
+ rowGroupIndices = std::vector<index_type>();
+ }
+ if (initialRowGroupCountSet && hasCustomRowGrouping) {
+ rowGroupIndices.get().reserve(initialRowGroupCount + 1);
}
rowIndications.push_back(0);
}
template<typename ValueType>
- SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(matrix.nontrivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() {
+ SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() {
// If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again.
if (hasCustomRowGrouping) {
rowGroupIndices = std::move(matrix.rowGroupIndices);
- rowGroupIndices.pop_back();
- currentRowGroup = rowGroupIndices.size() - 1;
+ rowGroupIndices.get().pop_back();
+ currentRowGroup = rowGroupIndices.get().size() - 1;
}
// Likewise, we need to 'open' the row indications again.
@@ -141,14 +144,14 @@ namespace storm {
void SparseMatrixBuilder<ValueType>::newRowGroup(index_type startingRow) {
STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
- rowGroupIndices.push_back(startingRow);
+ rowGroupIndices.get().push_back(startingRow);
++currentRowGroup;
-
+
// Close all rows from the most recent one to the starting row.
for (index_type i = lastRow + 1; i <= startingRow; ++i) {
rowIndications.push_back(currentEntryCount);
}
-
+
// Reset the most recently seen row/column to allow for proper insertion of the following elements.
lastRow = startingRow;
lastColumn = 0;
@@ -162,7 +165,7 @@ namespace storm {
rowCount = std::max(rowCount, initialRowCount);
}
rowCount = std::max(rowCount, overriddenRowCount);
-
+
// If the current row count was overridden, we may need to add empty rows.
for (index_type i = lastRow + 1; i < rowCount; ++i) {
rowIndications.push_back(currentEntryCount);
@@ -186,11 +189,7 @@ namespace storm {
}
// Check whether row groups are missing some entries.
- if (!hasCustomRowGrouping) {
- for (index_type i = 0; i <= rowCount; ++i) {
- rowGroupIndices.push_back(i);
- }
- } else {
+ if (hasCustomRowGrouping) {
uint_fast64_t rowGroupCount = currentRowGroup;
if (initialRowGroupCountSet && forceInitialDimensions) {
STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
@@ -199,11 +198,11 @@ namespace storm {
rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) {
- rowGroupIndices.push_back(rowCount);
+ rowGroupIndices.get().push_back(rowCount);
}
}
-
- return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping);
+
+ return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
}
template<typename ValueType>
@@ -216,6 +215,44 @@ namespace storm {
return lastColumn;
}
+ template<typename ValueType>
+ bool SparseMatrixBuilder<ValueType>::replaceColumns(std::vector<index_type> const& replacements, index_type offset) {
+ bool matrixChanged = false;
+
+ // Walk through all rows.
+ for (index_type row = 0; row < rowIndications.size(); ++row) {
+ bool rowChanged = false;
+ index_type rowEnd = row < rowIndications.size()-1 ? rowIndications[row+1] : columnsAndValues.size();
+
+ for (auto it = columnsAndValues.begin() + rowIndications[row], ite = columnsAndValues.begin() + rowEnd; it != ite; ++it) {
+ if (it->getColumn() >= offset && it->getColumn() != replacements[it->getColumn() - offset]) {
+ it->setColumn(replacements[it->getColumn() - offset]);
+ rowChanged = true;
+ }
+ // Update highest column in a way that only works if the highest appearing index does not become
+ // lower during performing the replacement.
+ highestColumn = std::max(highestColumn, it->getColumn());
+ }
+
+ if (rowChanged) {
+ matrixChanged = true;
+
+ // Sort the row.
+ std::sort(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
+ [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
+ return a.getColumn() < b.getColumn();
+ });
+ // Assert no equal elements
+ STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
+ [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
+ return a.getColumn() <= b.getColumn();
+ }), "Must not have different elements with the same column in a row.");
+ }
+ }
+
+ return matrixChanged;
+ }
+
template<typename ValueType>
SparseMatrix<ValueType>::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) {
// Intentionally left empty.
@@ -257,12 +294,12 @@ namespace storm {
}
template<typename ValueType>
- SparseMatrix<ValueType>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), nontrivialRowGrouping(false), rowGroupIndices() {
+ SparseMatrix<ValueType>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
// Intentionally left empty.
}
template<typename ValueType>
- SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) {
+ SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(other.rowGroupIndices) {
// Intentionally left empty.
}
@@ -274,7 +311,7 @@ namespace storm {
}
template<typename ValueType>
- SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) {
+ SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) {
// Now update the source matrix
other.rowCount = 0;
other.columnCount = 0;
@@ -282,12 +319,12 @@ namespace storm {
}
template<typename ValueType>
- SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) {
+ SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(rowGroupIndices) {
this->updateNonzeroEntryCount();
}
template<typename ValueType>
- SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, std::vector<index_type>&& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(std::move(rowGroupIndices)) {
+ SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(std::move(rowGroupIndices)) {
this->updateNonzeroEntryCount();
}
@@ -303,7 +340,7 @@ namespace storm {
columnsAndValues = other.columnsAndValues;
rowIndications = other.rowIndications;
rowGroupIndices = other.rowGroupIndices;
- nontrivialRowGrouping = other.nontrivialRowGrouping;
+ trivialRowGrouping = other.trivialRowGrouping;
}
return *this;
@@ -321,7 +358,7 @@ namespace storm {
columnsAndValues = std::move(other.columnsAndValues);
rowIndications = std::move(other.rowIndications);
rowGroupIndices = std::move(other.rowGroupIndices);
- nontrivialRowGrouping = other.nontrivialRowGrouping;
+ trivialRowGrouping = other.trivialRowGrouping;
}
return *this;
@@ -343,7 +380,11 @@ namespace storm {
if (!equalityResult) {
return false;
}
- equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices();
+ if (!this->hasTrivialRowGrouping() && !other.hasTrivialRowGrouping()) {
+ equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices();
+ } else {
+ equalityResult &= this->hasTrivialRowGrouping() && other.hasTrivialRowGrouping();
+ }
if (!equalityResult) {
return false;
}
@@ -395,8 +436,12 @@ namespace storm {
template<typename T>
uint_fast64_t SparseMatrix<T>::getRowGroupEntryCount(uint_fast64_t const group) const {
uint_fast64_t result = 0;
- for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group + 1]; ++row) {
- result += (this->rowIndications[row + 1] - this->rowIndications[row]);
+ if (!this->hasTrivialRowGrouping()) {
+ for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group + 1]; ++row) {
+ result += (this->rowIndications[row + 1] - this->rowIndications[row]);
+ }
+ } else {
+ result += (this->rowIndications[group + 1] - this->rowIndications[group]);
}
return result;
}
@@ -435,7 +480,11 @@ namespace storm {
template<typename ValueType>
typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getRowGroupCount() const {
- return rowGroupIndices.size() - 1;
+ if (!this->hasTrivialRowGrouping()) {
+ return rowGroupIndices.get().size() - 1;
+ } else {
+ return rowCount;
+ }
}
template<typename ValueType>
@@ -445,7 +494,15 @@ namespace storm {
template<typename ValueType>
std::vector<typename SparseMatrix<ValueType>::index_type> const& SparseMatrix<ValueType>::getRowGroupIndices() const {
- return rowGroupIndices;
+ // If there is no current row grouping, we need to create it.
+ if (!this->rowGroupIndices) {
+ STORM_LOG_ASSERT(trivialRowGrouping, "Only trivial row-groupings can be constructed on-the-fly.");
+ this->rowGroupIndices = std::vector<index_type>(this->getRowCount() + 1);
+ for (uint_fast64_t group = 0; group <= this->getRowCount(); ++group) {
+ this->rowGroupIndices.get()[group] = group;
+ }
+ }
+ return rowGroupIndices.get();
}
template<typename ValueType>
@@ -457,9 +514,15 @@ namespace storm {
template<typename ValueType>
void SparseMatrix<ValueType>::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) {
- for (auto rowGroup : rowGroupConstraint) {
- for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
- makeRowDirac(row, rowGroup);
+ if (!this->hasTrivialRowGrouping()) {
+ for (auto rowGroup : rowGroupConstraint) {
+ for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
+ makeRowDirac(row, rowGroup);
+ }
+ }
+ } else {
+ for (auto rowGroup : rowGroupConstraint) {
+ makeRowDirac(rowGroup, rowGroup);
}
}
}
@@ -512,9 +575,15 @@ namespace storm {
std::vector<ValueType> SparseMatrix<ValueType>::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const {
std::vector<ValueType> result;
result.reserve(rowGroupConstraint.getNumberOfSetBits());
- for (auto rowGroup : rowGroupConstraint) {
- for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
- result.push_back(getConstrainedRowSum(row, columnConstraint));
+ if (!this->hasTrivialRowGrouping()) {
+ for (auto rowGroup : rowGroupConstraint) {
+ for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
+ result.push_back(getConstrainedRowSum(row, columnConstraint));
+ }
+ }
+ } else {
+ for (auto rowGroup : rowGroupConstraint) {
+ result.push_back(getConstrainedRowSum(rowGroup, columnConstraint));
}
}
return result;
@@ -532,25 +601,30 @@ namespace storm {
*it = i;
}
auto res = getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements);
-
- // Create a new row grouping that reflects the new sizes of the row groups.
- std::vector<uint_fast64_t> newRowGroupIndices;
- newRowGroupIndices.push_back(0);
- auto selectedRowIt = rowConstraint.begin();
-
- // For this, we need to count how many rows were preserved in every group.
- for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) {
- uint_fast64_t newRowCount = 0;
- while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) {
- ++selectedRowIt;
- ++newRowCount;
- }
- if (newRowCount > 0) {
- newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
+
+ // Create a new row grouping that reflects the new sizes of the row groups if the current matrix has a
+ // non trivial row-grouping.
+ if (!this->hasTrivialRowGrouping()) {
+ std::vector<uint_fast64_t> newRowGroupIndices;
+ newRowGroupIndices.push_back(0);
+ auto selectedRowIt = rowConstraint.begin();
+
+ // For this, we need to count how many rows were preserved in every group.
+ for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) {
+ uint_fast64_t newRowCount = 0;
+ while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) {
+ ++selectedRowIt;
+ ++newRowCount;
+ }
+ if (newRowCount > 0) {
+ newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
+ }
}
+
+ res.trivialRowGrouping = false;
+ res.rowGroupIndices = newRowGroupIndices;
}
- res.rowGroupIndices = newRowGroupIndices;
return res;
}
}
@@ -597,13 +671,13 @@ namespace storm {
}
// Create and initialize resulting matrix.
- SparseMatrixBuilder<ValueType> matrixBuilder(subRows, submatrixColumnCount, subEntries, true, this->hasNontrivialRowGrouping());
+ SparseMatrixBuilder<ValueType> matrixBuilder(subRows, submatrixColumnCount, subEntries, true, !this->hasTrivialRowGrouping());
// Copy over selected entries.
rowGroupCount = 0;
index_type rowCount = 0;
for (auto index : rowGroupConstraint) {
- if (this->hasNontrivialRowGrouping()) {
+ if (!this->hasTrivialRowGrouping()) {
matrixBuilder.newRowGroup(rowCount);
}
for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) {
@@ -639,12 +713,12 @@ namespace storm {
template<typename ValueType>
SparseMatrix<ValueType> SparseMatrix<ValueType>::restrictRows(storm::storage::BitVector const& rowsToKeep) const {
// For now, we use the expensive call to submatrix.
- assert(rowsToKeep.size() == getRowCount());
- assert(rowsToKeep.getNumberOfSetBits() >= getRowGroupCount());
+ STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch.");
+ STORM_LOG_ASSERT(rowsToKeep.getNumberOfSetBits() >= this->getRowGroupCount(), "Invalid dimensions.");
SparseMatrix<ValueType> res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false));
- assert(res.getRowCount() == rowsToKeep.getNumberOfSetBits());
- assert(res.getColumnCount() == getColumnCount());
- assert(getRowGroupCount() == res.getRowGroupCount());
+ STORM_LOG_ASSERT(res.getRowCount() == rowsToKeep.getNumberOfSetBits(), "Invalid dimensions");
+ STORM_LOG_ASSERT(res.getColumnCount() == this->getColumnCount(), "Invalid dimensions");
+ STORM_LOG_ASSERT(this->getRowGroupCount() == res.getRowGroupCount(), "Invalid dimensions");
return res;
}
@@ -655,7 +729,7 @@ namespace storm {
index_type subEntries = 0;
for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
// Determine which row we need to select from the current row group.
- index_type rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+ index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
// Iterate through that row and count the number of slots we have to reserve for copying.
bool foundDiagonalElement = false;
@@ -671,12 +745,12 @@ namespace storm {
}
// Now create the matrix to be returned with the appropriate size.
- SparseMatrixBuilder<ValueType> matrixBuilder(rowGroupIndices.size() - 1, columnCount, subEntries);
+ SparseMatrixBuilder<ValueType> matrixBuilder(rowGroupIndices.get().size() - 1, columnCount, subEntries);
// Copy over the selected lines from the source matrix.
for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
// Determine which row we need to select from the current row group.
- index_type rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+ index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
// Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if
// there is no entry yet.
@@ -743,12 +817,7 @@ namespace storm {
}
}
- std::vector<index_type> rowGroupIndices(rowCount + 1);
- for (index_type i = 0; i <= rowCount; ++i) {
- rowGroupIndices[i] = i;
- }
-
- storm::storage::SparseMatrix<ValueType> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), false);
+ storm::storage::SparseMatrix<ValueType> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), boost::none);
return transposedMatrix;
}
@@ -998,50 +1067,66 @@ namespace storm {
template<typename ValueType>
typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) const {
- return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
+ return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
}
template<typename ValueType>
typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) {
- return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
+ return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
}
template<typename ValueType>
typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRow(index_type row) const {
- return getRows(row, row);
+ return getRows(row, row + 1);
}
template<typename ValueType>
typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRow(index_type row) {
- return getRows(row, row);
+ return getRows(row, row + 1);
}
template<typename ValueType>
typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) const {
- assert(rowGroup < this->getRowGroupCount());
- assert(offset < this->getRowGroupEntryCount(rowGroup));
- return getRow(rowGroupIndices[rowGroup] + offset);
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+ STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds.");
+ if (!this->hasTrivialRowGrouping()) {
+ return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+ } else {
+ return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+ }
}
-
template<typename ValueType>
typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) {
- assert(rowGroup < this->getRowGroupCount());
- assert(offset < this->getRowGroupEntryCount(rowGroup));
- return getRow(rowGroupIndices[rowGroup] + offset);
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+ STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds.");
+ if (!this->hasTrivialRowGrouping()) {
+ return getRow(this->getRowGroupIndices()[rowGroup] + offset);
+ } else {
+ STORM_LOG_ASSERT(offset == 0, "Invalid offset.");
+ return getRow(rowGroup + offset);
+ }
}
template<typename ValueType>
typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRowGroup(index_type rowGroup) const {
- assert(rowGroup < this->getRowGroupCount());
- return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+ if (!this->hasTrivialRowGrouping()) {
+ return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
+ } else {
+ return getRows(rowGroup, rowGroup + 1);
+ }
}
template<typename ValueType>
typename SparseMatrix<ValueType>::rows SparseMatrix<ValueType>::getRowGroup(index_type rowGroup) {
- assert(rowGroup < this->getRowGroupCount());
- return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
+ if (!this->hasTrivialRowGrouping()) {
+ return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
+ } else {
+ return getRows(rowGroup, rowGroup + 1);
+ }
}
template<typename ValueType>
@@ -1075,8 +1160,8 @@ namespace storm {
}
template<typename ValueType>
- bool SparseMatrix<ValueType>::hasNontrivialRowGrouping() const {
- return nontrivialRowGrouping;
+ bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
+ return trivialRowGrouping;
}
template<typename ValueType>
@@ -1105,6 +1190,9 @@ namespace storm {
// Check for matching sizes.
if (this->getRowCount() != matrix.getRowCount()) return false;
if (this->getColumnCount() != matrix.getColumnCount()) return false;
+ if (this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping()) return false;
+ if (!this->hasTrivialRowGrouping() && matrix.hasTrivialRowGrouping()) return false;
+ if (!this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping() && this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false;
if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false;
// Check the subset property for all rows individually.
@@ -1136,7 +1224,10 @@ namespace storm {
// Iterate over all row groups.
for (typename SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) {
out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl;
- for (typename SparseMatrix<ValueType>::index_type i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) {
+ typename SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group];
+ typename SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1];
+
+ for (typename SparseMatrix<ValueType>::index_type i = start; i < end; ++i) {
typename SparseMatrix<ValueType>::index_type nextIndex = matrix.rowIndications[i];
// Print the actual row.
@@ -1172,7 +1263,7 @@ namespace storm {
assert(this->getRowGroupSize(group) == 1);
for (typename SparseMatrix<ValueType>::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) {
typename SparseMatrix<ValueType>::index_type nextIndex = this->rowIndications[i];
-
+
// Print the actual row.
out << i << "\t(";
typename SparseMatrix<ValueType>::index_type currentRealIndex = 0;
@@ -1199,7 +1290,9 @@ namespace storm {
boost::hash_combine(result, this->getEntryCount());
boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end()));
boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end()));
- boost::hash_combine(result, boost::hash_range(rowGroupIndices.begin(), rowGroupIndices.end()));
+ if (!this->hasTrivialRowGrouping()) {
+ boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end()));
+ }
return result;
}
@@ -1226,7 +1319,7 @@ namespace storm {
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
-
+
// float
template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<float>::index_type, float> const& entry);
@@ -1235,7 +1328,7 @@ namespace storm {
template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const;
template bool SparseMatrix<float>::isSubmatrixOf(SparseMatrix<float> const& matrix) const;
-
+
// int
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<int>::index_type, int> const& entry);
@@ -1243,7 +1336,7 @@ namespace storm {
template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
-
+
// state_type
template class MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<storm::storage::sparse::state_type>::index_type, storm::storage::sparse::state_type> const& entry);
@@ -1251,7 +1344,7 @@ namespace storm {
template class SparseMatrix<storm::storage::sparse::state_type>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<storm::storage::sparse::state_type> const& matrix);
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
-
+
#ifdef STORM_HAVE_CARL
// Rat Function
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
@@ -1264,7 +1357,7 @@ namespace storm {
template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
-
+
// Intervals
template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
template class MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval>;
@@ -1274,7 +1367,7 @@ namespace storm {
template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<storm::Interval> const& matrix) const;
-
+
template bool SparseMatrix<storm::Interval>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
#endif
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index f9d9916c4..c5c7133c6 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -7,9 +7,11 @@
#include <vector>
#include <iterator>
+#include <boost/functional/hash.hpp>
+#include <boost/optional.hpp>
+
#include "src/utility/OsDetection.h"
#include "src/adapters/CarlAdapter.h"
-#include <boost/functional/hash.hpp>
// Forward declaration for adapter classes.
namespace storm {
@@ -217,6 +219,17 @@ namespace storm {
*/
index_type getLastColumn() const;
+ /*!
+ * Replaces all columns with id > offset according to replacements.
+ * Every state with id offset+i is replaced by the id in replacements[i].
+ * Afterwards the columns are sorted.
+ *
+ * @param replacements Mapping indicating the replacements from offset+i -> value of i.
+ * @param offset Offset to add to each id in vector index.
+ * @return True if replacement took place, False if nothing changed.
+ */
+ bool replaceColumns(std::vector<index_type> const& replacements, index_type offset);
+
private:
// A flag indicating whether a row count was set upon construction.
bool initialRowCountSet;
@@ -248,7 +261,8 @@ namespace storm {
// The number of row groups in the matrix.
index_type initialRowGroupCount;
- std::vector<index_type> rowGroupIndices;
+ // The vector that stores the row-group indices (if they are non-trivial).
+ boost::optional<std::vector<index_type>> rowGroupIndices;
// The storage for the columns and values of all entries in the matrix.
std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
@@ -436,9 +450,8 @@ namespace storm {
* @param rowIndications The row indications vector of the matrix to be constructed.
* @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
* @param rowGroupIndices The vector representing the row groups in the matrix.
- * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial.
*/
- SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool hasNontrivialRowGrouping);
+ SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices);
/*!
* Constructs a sparse matrix by moving the given contents.
@@ -447,9 +460,8 @@ namespace storm {
* @param rowIndications The row indications vector of the matrix to be constructed.
* @param columnsAndValues The vector containing the columns and values of the entries in the matrix.
* @param rowGroupIndices The vector representing the row groups in the matrix.
- * @param hasNontrivialRowGrouping If set to true, this indicates that the row grouping is non-trivial.
*/
- SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues, std::vector<index_type>&& rowGroupIndices, bool hasNontrivialRowGrouping);
+ SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& rowGroupIndices);
/*!
* Assigns the contents of the given matrix to the current one by deep-copying its contents.
@@ -793,7 +805,7 @@ namespace storm {
* Returns an object representing the consecutive rows given by the parameters.
*
* @param startRow The starting row.
- * @param endRow The ending row (which is included in the result).
+ * @param endRow The ending row (which is *not* included in the result).
* @return An object representing the consecutive rows given by the parameters.
*/
const_rows getRows(index_type startRow, index_type endRow) const;
@@ -802,7 +814,7 @@ namespace storm {
* Returns an object representing the consecutive rows given by the parameters.
*
* @param startRow The starting row.
- * @param endRow The ending row (which is included in the result).
+ * @param endRow The ending row (which is *not* included in the result).
* @return An object representing the consecutive rows given by the parameters.
*/
rows getRows(index_type startRow, index_type endRow);
@@ -902,27 +914,28 @@ namespace storm {
iterator end();
/*!
- * Retrieves whether the matrix has a (possibly) non-trivial row grouping.
+ * Retrieves whether the matrix has a trivial row grouping.
*
- * @return True iff the matrix has a (possibly) non-trivial row grouping.
+ * @return True iff the matrix has a trivial row grouping.
*/
- bool hasNontrivialRowGrouping() const;
+ bool hasTrivialRowGrouping() const;
/*!
* Returns a copy of the matrix with the chosen internal data type
*/
template<typename NewValueType>
SparseMatrix<NewValueType> toValueType() const {
- std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> new_columnsAndValues;
- std::vector<SparseMatrix::index_type> new_rowIndications(rowIndications);
- std::vector<SparseMatrix::index_type> new_rowGroupIndices(rowGroupIndices);
+ std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> newColumnsAndValues;
+ std::vector<SparseMatrix::index_type> newRowIndications(rowIndications);
+ boost::optional<std::vector<SparseMatrix::index_type>> newRowGroupIndices(rowGroupIndices);
- new_columnsAndValues.resize(columnsAndValues.size());
- for (size_t i = 0, size = columnsAndValues.size(); i < size; ++i) {
- new_columnsAndValues.at(i) = MatrixEntry<SparseMatrix::index_type, NewValueType>(columnsAndValues.at(i).getColumn(), static_cast<NewValueType>(columnsAndValues.at(i).getValue()));
- }
+ newColumnsAndValues.resize(columnsAndValues.size());
+ std::transform(columnsAndValues.begin(), columnsAndValues.end(), newColumnsAndValues.begin(),
+ [] (MatrixEntry<SparseMatrix::index_type, ValueType> const& a) {
+ return MatrixEntry<SparseMatrix::index_type, NewValueType>(a.getColumn(), static_cast<NewValueType>(a.getValue()));
+ });
- return SparseMatrix<NewValueType>(columnCount, std::move(new_rowIndications), std::move(new_columnsAndValues), std::move(new_rowGroupIndices), nontrivialRowGrouping);
+ return SparseMatrix<NewValueType>(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices));
}
private:
@@ -961,12 +974,12 @@ namespace storm {
// entry is not included anymore.
std::vector<index_type> rowIndications;
- // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one
- // row per row group.
- bool nontrivialRowGrouping;
+ // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet
+ // there may be row group indices, because they were requested from the outside.
+ bool trivialRowGrouping;
- // A vector indicating the row groups of the matrix.
- std::vector<index_type> rowGroupIndices;
+ // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly.
+ mutable boost::optional<std::vector<index_type>> rowGroupIndices;
};
diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp
index ecd98c2d9..40223da75 100644
--- a/src/storage/dd/Add.cpp
+++ b/src/storage/dd/Add.cpp
@@ -459,7 +459,7 @@ namespace storm {
rowIndications[0] = 0;
// Construct matrix and return result.
- return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false);
+ return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), boost::none);
}
template<DdType LibraryType, typename ValueType>
@@ -583,7 +583,7 @@ namespace storm {
}
rowIndications[0] = 0;
- return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true);
+ return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
}
template<DdType LibraryType, typename ValueType>
@@ -708,7 +708,7 @@ namespace storm {
}
rowIndications[0] = 0;
- return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector));
+ return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector));
}
template<DdType LibraryType, typename ValueType>
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index bf8caf4a8..999cf2f30 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -77,6 +77,14 @@ namespace storm {
return modelType;
}
+ bool Program::isDiscreteTimeModel() const {
+ return modelType == ModelType::DTMC || modelType == ModelType::MDP;
+ }
+
+ bool Program::isDeterministicModel() const {
+ return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
+ }
+
bool Program::hasUndefinedConstants() const {
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 45ac16b62..1d091c294 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -66,6 +66,18 @@ namespace storm {
* @return The type of the model.
*/
ModelType getModelType() const;
+
+ /*!
+ * Retrieves whether the model is a discrete-time model, i.e. a DTMC or an MDP.
+ *
+ * @return True iff the model is a discrete-time model.
+ */
+ bool isDiscreteTimeModel() const;
+
+ /*!
+ * Retrieves whether the model is one without nondeterministic choices, i.e. a DTMC or a CTMC.
+ */
+ bool isDeterministicModel() const;
/*!
* Retrieves whether there are undefined constants of any type in the program.
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 3f38f7bd8..30c43728c 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -84,7 +84,7 @@ namespace storm {
std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
stream << "rewards";
if (rewardModel.getName() != "") {
- std::cout << " \"" << rewardModel.getName() << "\"";
+ stream << " \"" << rewardModel.getName() << "\"";
}
stream << std::endl;
for (auto const& reward : rewardModel.getStateRewards()) {
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 2aa10d23a..7fe39b963 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -204,6 +204,10 @@ namespace storm {
template bool isZero(storm::storage::sparse::state_type const& value);
template bool isConstant(storm::storage::sparse::state_type const& value);
+ template uint32_t one();
+ template uint32_t zero();
+ template uint32_t infinity();
+
template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero();
template storm::storage::sparse::state_type infinity();
diff --git a/src/utility/storm.h b/src/utility/storm.h
index a7a717b8d..ffbc37c47 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -106,8 +106,8 @@ namespace storm {
options.buildCommandLabels = true;
}
- storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
- result.model = builder.translateProgram(program, options);
+ storm::builder::ExplicitPrismModelBuilder<ValueType> builder(program, options);
+ result.model = builder.translate();
translatedProgram = builder.getTranslatedProgram();
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index 080b6c16f..c2151c74c 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -10,27 +10,27 @@
TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@@ -41,27 +41,27 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@@ -69,32 +69,32 @@ TEST(ExplicitPrismModelBuilderTest, Ctmc) {
TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(364ul, model->getNumberOfStates());
EXPECT_EQ(654ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(1038ul, model->getNumberOfStates());
EXPECT_EQ(1282ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(4093ul, model->getNumberOfStates());
EXPECT_EQ(5585ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(37ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
\ No newline at end of file
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index b36983962..dc9512a38 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -34,7 +34,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -117,7 +117,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -179,7 +179,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<const storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -226,7 +226,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
#endif
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 1e131c335..36a139b9c 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -284,7 +284,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 725e1376d..93643fd52 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
EXPECT_EQ(4ul, model->getNumberOfStates());
EXPECT_EQ(11ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index 72788de80..0a1d8ee4c 100644
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -32,7 +32,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -108,7 +108,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -163,7 +163,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<const storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -204,7 +204,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
index 75bea3570..657d36575 100644
--- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@@ -28,7 +28,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
options.addConstantDefinitionsFromString(program, "");
options.buildCommandLabels = true;
- std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
+ std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none);
diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index 4d87796b8..2790cd86a 100644
--- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
@@ -31,7 +31,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
options.addConstantDefinitionsFromString(program, "");
options.buildCommandLabels = true;
- std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
+ std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
// boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaSMT<>(*mdp, formula02);
// EXPECT_NE(perms, boost::none);
diff --git a/test/functional/storage/BitVectorHashMapTest.cpp b/test/functional/storage/BitVectorHashMapTest.cpp
index 616941f21..1149433fd 100644
--- a/test/functional/storage/BitVectorHashMapTest.cpp
+++ b/test/functional/storage/BitVectorHashMapTest.cpp
@@ -19,25 +19,41 @@ TEST(BitVectorHashMapTest, FindOrAdd) {
ASSERT_NO_THROW(map.findOrAdd(second, 2));
EXPECT_EQ(1ul, map.findOrAdd(first, 3));
-
+ EXPECT_EQ(2ul, map.findOrAdd(second, 3));
+
storm::storage::BitVector third(64);
third.set(10);
third.set(63);
ASSERT_NO_THROW(map.findOrAdd(third, 3));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+
storm::storage::BitVector fourth(64);
fourth.set(12);
fourth.set(14);
ASSERT_NO_THROW(map.findOrAdd(fourth, 4));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+ EXPECT_EQ(4ul, map.findOrAdd(fourth, 1));
+
storm::storage::BitVector fifth(64);
fifth.set(44);
fifth.set(55);
ASSERT_NO_THROW(map.findOrAdd(fifth, 5));
+ EXPECT_EQ(1ul, map.findOrAdd(first, 2));
+ EXPECT_EQ(2ul, map.findOrAdd(second, 1));
+ EXPECT_EQ(3ul, map.findOrAdd(third, 1));
+ EXPECT_EQ(4ul, map.findOrAdd(fourth, 1));
+ EXPECT_EQ(5ul, map.findOrAdd(fifth, 1));
+
storm::storage::BitVector sixth(64);
sixth.set(45);
sixth.set(55);
diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp
index db92724fe..7266f829b 100644
--- a/test/functional/storage/BitVectorTest.cpp
+++ b/test/functional/storage/BitVectorTest.cpp
@@ -321,24 +321,6 @@ TEST(BitVectorTest, OperatorModulo) {
ASSERT_FALSE(moduloResult.get(i));
}
}
-
- storm::storage::BitVector vector3(31);
-
- for (uint_fast64_t i = 0; i < 15; ++i) {
- vector3.set(i, i % 2 == 0);
- }
-
-
-#ifndef NDEBUG
-#ifdef WINDOWS
- EXPECT_EXIT(vector1 % vector3, ::testing::ExitedWithCode(0), ".*");
-#else
- EXPECT_DEATH_IF_SUPPORTED(vector1 % vector3, "");
-#endif
-#else
- std::cerr << "WARNING: Not testing OperatorModulo size check, as assertions are disabled in release mode." << std::endl;
- SUCCEED();
-#endif
}
TEST(BitVectorTest, OperatorNot) {
diff --git a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
index 3754b03fd..fe0a199b7 100644
--- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
@@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// Build the die model without its reward model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp
index 1fe0041f7..321fc7b91 100644
--- a/test/functional/storage/SparseMatrixTest.cpp
+++ b/test/functional/storage/SparseMatrixTest.cpp
@@ -155,8 +155,8 @@ TEST(SparseMatrix, CreationWithMovingContents) {
columnsAndValues.emplace_back(1, 0.7);
columnsAndValues.emplace_back(3, 0.2);
- ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}, false));
- storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}, false);
+ ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, boost::optional<std::vector<uint_fast64_t>>({0, 1, 2, 3})));
+ storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, boost::optional<std::vector<uint_fast64_t>>({0, 1, 2, 3}));
ASSERT_EQ(3ul, matrix.getRowCount());
ASSERT_EQ(4ul, matrix.getColumnCount());
ASSERT_EQ(5ul, matrix.getEntryCount());
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index d209998d7..4c6bf0d50 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -181,7 +181,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
TEST(GraphTest, ExplicitProb01) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -202,7 +202,7 @@ TEST(GraphTest, ExplicitProb01) {
TEST(GraphTest, ExplicitProb01MinMax) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -217,7 +217,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -238,7 +238,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+ model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
index af8f5b8d2..fe2ee4a7c 100644
--- a/test/functional/utility/ModelInstantiatorTest.cpp
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -17,12 +17,12 @@
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Mdp.h"
-TEST(ModelInstantiatorTest, Brp_Prob) {
+TEST(ModelInstantiatorTest, BrpProb) {
carl::VariablePool::getInstance().clear();
- std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
- std::string const& formulaAsString = "P=? [F s=5 ]";
- std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+ std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
+ std::string formulaAsString = "P=? [F s=5 ]";
+ std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -33,7 +33,7 @@ TEST(ModelInstantiatorTest, Brp_Prob) {
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
options.addConstantDefinitionsFromString(program, constantsAsString);
options.preserveFormula(*formulas[0]);
- std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>(program, options).translate()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
EXPECT_FALSE(dtmc->hasRewardModel());
@@ -141,9 +141,9 @@ TEST(ModelInstantiatorTest, Brp_Prob) {
TEST(ModelInstantiatorTest, Brp_Rew) {
carl::VariablePool::getInstance().clear();
- std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
- std::string const& formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
- std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+ std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
+ std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
+ std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -154,7 +154,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
options.addConstantDefinitionsFromString(program, constantsAsString);
options.preserveFormula(*formulas[0]);
- std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+ std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>(program, options).translate()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
@@ -211,12 +211,12 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
}
-TEST(ModelInstantiatorTest, consensus) {
+TEST(ModelInstantiatorTest, Consensus) {
carl::VariablePool::getInstance().clear();
- std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm";
- std::string const& formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
- std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+ std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm";
+ std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
+ std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -227,7 +227,7 @@ TEST(ModelInstantiatorTest, consensus) {
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
options.addConstantDefinitionsFromString(program, constantsAsString);
options.preserveFormula(*formulas[0]);
- std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>().translateProgram(program, options)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+ std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>(program, options).translate()->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
@@ -260,7 +260,6 @@ TEST(ModelInstantiatorTest, consensus) {
std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision());
-
}
#endif
\ No newline at end of file