From 7884fc37edff6267ba4401599b9e4aff5157c4d7 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 1 Oct 2015 15:14:24 +0200 Subject: [PATCH] explicit model builder supports non-default reward models Former-commit-id: 97aabc54bbac6a648905c595b87e4fc5a2c4f825 --- src/builder/ExplicitPrismModelBuilder.cpp | 107 +++++++++++----------- src/builder/ExplicitPrismModelBuilder.h | 9 +- src/utility/storm.h | 4 +- 3 files changed, 61 insertions(+), 59 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index cfc7d8577..465a9b960 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -63,23 +63,23 @@ namespace storm { storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; }; - template - ExplicitPrismModelBuilder::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { + template + ExplicitPrismModelBuilder::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { + template + ExplicitPrismModelBuilder::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::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 + ExplicitPrismModelBuilder::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) { // Intentionally left empty. } - template - uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { + template + uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { auto const& booleanIndex = booleanVariableToIndexMap.find(variable); if (booleanIndex != booleanVariableToIndexMap.end()) { return booleanVariables[booleanIndex->second].bitOffset; @@ -91,8 +91,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); } - template - uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { + template + uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { auto const& integerIndex = integerVariableToIndexMap.find(variable); if (integerIndex != integerVariableToIndexMap.end()) { return integerVariables[integerIndex->second].bitWidth; @@ -100,23 +100,23 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); } - template - ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + template + ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); } - template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -130,8 +130,8 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + template + void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { if (formula.isAtomicExpressionFormula()) { terminalStates = formula.asAtomicExpressionFormula().getExpression(); } else if (formula.isAtomicLabelFormula()) { @@ -160,8 +160,8 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { + template + void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. if (terminalStates) { terminalStates.reset(); @@ -200,8 +200,8 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { + template + void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); // If there is at least one constant that is defined, and the constant definition map does not yet exist, @@ -216,8 +216,8 @@ namespace storm { } } - template - std::shared_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, Options const& options) { + template + std::shared_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, Options const& options) { // Start by defining the undefined constants in the model. storm::prism::Program preparedProgram; if (options.constantDefinitions) { @@ -299,16 +299,16 @@ namespace storm { ModelComponents modelComponents = buildModelComponents(preparedProgram, selectedRewardModels, options); - std::shared_ptr> result; + std::shared_ptr> result; switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMC: - result = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::MDP: - result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -318,8 +318,8 @@ namespace storm { return result; } - template - void ExplicitPrismModelBuilder::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator) { + template + void ExplicitPrismModelBuilder::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator) { for (auto const& booleanVariable : variableInformation.booleanVariables) { evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset)); } @@ -328,13 +328,13 @@ namespace storm { } } - template - typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { + template + typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { return applyUpdate(variableInformation, state, state, update, evaluator); } - template - typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { + template + typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { CompressedState newState(state); auto assignmentIt = update.getAssignments().begin(); @@ -367,8 +367,8 @@ namespace storm { return newState; } - template - IndexType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue& stateQueue) { + template + IndexType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue& stateQueue) { uint32_t newIndex = stateInformation.reachableStates.size(); // Check, if the state was already registered. @@ -382,8 +382,8 @@ namespace storm { return actualIndexBucketPair.first; } - template - boost::optional>>> ExplicitPrismModelBuilder::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) { + template + boost::optional>>> ExplicitPrismModelBuilder::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) { boost::optional>>> result((std::vector>>())); // Iterate over all modules. @@ -425,8 +425,8 @@ namespace storm { return result; } - template - std::vector> ExplicitPrismModelBuilder::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { + template + std::vector> ExplicitPrismModelBuilder::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { std::vector> result; // Iterate over all modules. @@ -476,8 +476,8 @@ namespace storm { return result; } - template - std::vector> ExplicitPrismModelBuilder::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { + template + std::vector> ExplicitPrismModelBuilder::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { std::vector> result; for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { @@ -571,8 +571,8 @@ namespace storm { return result; } - template - boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { + template + boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { // Create choice labels, if requested, boost::optional>> choiceLabels; if (commandLabels) { @@ -890,8 +890,8 @@ namespace storm { return choiceLabels; } - template - typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options) { + template + typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options) { ModelComponents modelComponents; uint_fast64_t bitOffset = 0; @@ -936,7 +936,7 @@ namespace storm { // Prepare the transition matrix builder and the reward model builders. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - std::vector> rewardModelBuilders; + std::vector> rewardModelBuilders; for (auto const& rewardModel : selectedRewardModels) { rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards()); } @@ -987,8 +987,8 @@ namespace storm { return modelComponents; } - template - storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { + template + storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { storm::expressions::ExpressionEvaluator evaluator(program.getManager()); std::vector const& labels = program.getLabels(); @@ -1019,10 +1019,11 @@ namespace storm { } // Explicitly instantiate the class. - template class ExplicitPrismModelBuilder; + template class ExplicitPrismModelBuilder, uint32_t>; #ifdef STORM_HAVE_CARL - template class ExplicitPrismModelBuilder; + template class ExplicitPrismModelBuilder, uint32_t>; + template class ExplicitPrismModelBuilder, uint32_t>; #endif } } \ No newline at end of file diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 1356394d8..137674607 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -9,6 +9,7 @@ #include #include #include +#include #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" @@ -35,7 +36,7 @@ namespace storm { // Forward-declare classes. template struct RewardModelBuilder; - template + template, typename IndexType = uint32_t> class ExplicitPrismModelBuilder { public: typedef storm::storage::BitVector CompressedState; @@ -118,7 +119,7 @@ namespace storm { storm::models::sparse::StateLabeling stateLabeling; // The reward models associated with the model. - std::unordered_map> rewardModels; + std::unordered_map> rewardModels; // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; @@ -212,7 +213,7 @@ namespace storm { * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - static std::shared_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); + static std::shared_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); private: static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); @@ -289,7 +290,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>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); + static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); /*! * Explores the state space of the given program and returns the components of the model as a result. diff --git a/src/utility/storm.h b/src/utility/storm.h index 49518170b..a863d8e93 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -93,8 +93,8 @@ namespace storm { // Customize and perform model-building. if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { - typename storm::builder::ExplicitPrismModelBuilder::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formulas); + typename storm::builder::ExplicitPrismModelBuilder>::Options options; + options = typename storm::builder::ExplicitPrismModelBuilder>::Options(formulas); options.addConstantDefinitionsFromString(program, constants); // Generate command labels if we are going to build a counterexample later.