From ddf165d4d35bfcdf10a0682dc3f0fab1915a8a87 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 8 Jun 2016 23:24:31 +0200 Subject: [PATCH] more work on tearing PRISM-specific functionality out of the explicit model builder Former-commit-id: a835c9072ed8a4822698e2946f343aeeb4060f48 --- src/builder/ExplicitModelBuilder.cpp | 177 +++++++----------- src/builder/ExplicitModelBuilder.h | 9 +- src/cli/entrypoints.h | 2 +- src/generator/NextStateGenerator.cpp | 40 +++- src/generator/NextStateGenerator.h | 49 ++++- src/generator/PrismNextStateGenerator.cpp | 77 ++++++-- src/generator/PrismNextStateGenerator.h | 15 +- .../SparseExplorationModelChecker.cpp | 4 +- .../SparseExplorationModelChecker.h | 3 - .../exploration/StateGeneration.cpp | 2 +- .../exploration/StateGeneration.h | 2 +- src/storage/BitVectorHashMap.h | 2 +- src/utility/prism.cpp | 41 ++-- src/utility/prism.h | 7 +- src/utility/storm.h | 28 +-- 15 files changed, 255 insertions(+), 203 deletions(-) diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index c6917ff54..b1d67bee2 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -30,21 +30,21 @@ namespace storm { * A structure that is used to keep track of a reward model currently being built. */ template - struct RewardModelBuilder { + class RewardModelBuilder { public: - RewardModelBuilder(std::string const& rewardModelName) : rewardModelName(rewardModelName), stateRewardVector(), stateActionRewardVector() { - // Intentionally left empty. + RewardModelBuilder(storm::generator::RewardModelInformation const& rewardModelInformation) : rewardModelName(rewardModelInformation.getName()), stateRewards(rewardModelInformation.hasStateRewards()), stateRewardVector(), stateActionRewards(rewardModelInformation.hasStateActionRewards()), stateActionRewardVector() { + STORM_LOG_THROW(!rewardModelInformation.hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "Unable to treat transition rewards."); } storm::models::sparse::StandardRewardModel build(uint_fast64_t rowCount, uint_fast64_t columnCount, uint_fast64_t rowGroupCount) { boost::optional> optionalStateRewardVector; - if (!stateRewardVector.empty()) { + if (hasStateRewards()) { stateRewardVector.resize(rowGroupCount); optionalStateRewardVector = std::move(stateRewardVector); } boost::optional> optionalStateActionRewardVector; - if (!stateActionRewardVector.empty()) { + if (hasStateActionRewards()) { stateActionRewardVector.resize(rowCount); optionalStateActionRewardVector = std::move(stateActionRewardVector); } @@ -52,7 +52,31 @@ namespace storm { return storm::models::sparse::StandardRewardModel(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector)); } + std::string const& getName() const { + return rewardModelName; + } + + void addStateReward(ValueType const& value) { + stateRewardVector.push_back(value); + } + + void addStateActionReward(ValueType const& value) { + stateActionRewardVector.push_back(value); + } + + bool hasStateRewards() const { + return stateRewards; + } + + bool hasStateActionRewards() const { + return stateActionRewards; + } + + private: std::string rewardModelName; + + bool stateRewards; + bool stateActionRewards; // The state reward vector. std::vector stateRewardVector; @@ -72,7 +96,7 @@ namespace storm { } template - ExplicitModelBuilder::ExplicitModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) { + ExplicitModelBuilder::ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options) : generator(generator), options(options), stateStorage(generator->getStateSize()) { // Intentionally left empty. } @@ -84,39 +108,18 @@ namespace storm { template std::shared_ptr> ExplicitModelBuilder::translate() { - STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl); STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); - - // First, we make sure that all selected reward models actually exist. - for (auto const& rewardModelName : options.rewardModelsToBuild) { - STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); - } - - std::vector selectedRewardModels; - if (options.buildAllRewardModels) { -// for (auto const& rewardModel : program.getRewardModels()) { -// selectedRewardModels.push_back(rewardModel); -// } - } else { - selectedRewardModels = std::vector(options.rewardModelsToBuild.begin(), options.rewardModelsToBuild.end()); - } -// // 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() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { -// selectedRewardModels.push_back(program.getRewardModel(0)); -// } - - ModelComponents modelComponents = buildModelComponents(selectedRewardModels); + ModelComponents modelComponents = buildModelComponents(); std::shared_ptr> result; - switch (program.getModelType()) { - case storm::prism::Program::ModelType::DTMC: + switch (generator->getModelType()) { + case storm::generator::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))); break; - case storm::prism::Program::ModelType::CTMC: + case storm::generator::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))); break; - case storm::prism::Program::ModelType::MDP: + case storm::generator::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))); break; default: @@ -151,22 +154,13 @@ namespace storm { } template - boost::optional>> ExplicitModelBuilder::buildMatrices(std::vector> const& selectedRewardModels, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { + boost::optional>> ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders) { // Create choice labels, if requested, boost::optional>> choiceLabels; - if (options.buildCommandLabels) { + if (generator->getOptions().isBuildChoiceLabelsSet()) { choiceLabels = std::vector>(); } - // Create a generator that is able to expand states. - storm::generator::PrismNextStateGenerator generator(program, variableInformation, options.buildCommandLabels); - if (terminalExpression) { - generator.setTerminalExpression(terminalExpression.get()); - } - 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 stateToIdCallback = std::bind(&ExplicitModelBuilder::getOrAddStateIndex, this, std::placeholders::_1); @@ -178,7 +172,7 @@ namespace storm { } // Let the generator create all initial states. - this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback); + this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); // Now explore the current state until there is no more reachable state. uint_fast64_t currentRowGroup = 0; @@ -199,62 +193,56 @@ namespace storm { STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); - generator.load(currentState); - storm::generator::StateBehavior behavior = generator.expand(stateToIdCallback); + generator->load(currentState); + storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { - if (options.buildCommandLabels) { + if (generator->getOptions().isBuildChoiceLabelsSet()) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.get().push_back(boost::container::flat_set()); } - if (!generator.isDeterministicModel()) { + if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } transitionMatrixBuilder.addNextValue(currentRow, currentIndex, storm::utility::one()); - auto builderIt = rewardModelBuilders.begin(); - for (auto const& rewardModel : selectedRewardModels) { - if (rewardModel.get().hasStateRewards()) { - builderIt->stateRewardVector.push_back(storm::utility::zero()); + for (auto& rewardModelBuilder : rewardModelBuilders) { + if (rewardModelBuilder.hasStateRewards()) { + rewardModelBuilder.addStateReward(storm::utility::zero()); } - if (rewardModel.get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.push_back(storm::utility::zero()); + if (rewardModelBuilder.hasStateActionRewards()) { + rewardModelBuilder.addStateActionReward(storm::utility::zero()); } - ++builderIt; } ++currentRow; ++currentRowGroup; } else { - std::cout << storm::generator::unpackStateIntoValuation(currentState, variableInformation, program.getManager()).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."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->toValuation(currentState).toString(true) << "). For fixing these, please provide the appropriate option."); } } else { // Add the state rewards to the corresponding reward models. - auto builderIt = rewardModelBuilders.begin(); auto stateRewardIt = behavior.getStateRewards().begin(); - for (auto const& rewardModel : selectedRewardModels) { - if (rewardModel.get().hasStateRewards()) { - builderIt->stateRewardVector.push_back(*stateRewardIt); + for (auto& rewardModelBuilder : rewardModelBuilders) { + if (rewardModelBuilder.hasStateRewards()) { + rewardModelBuilder.addStateReward(*stateRewardIt); } ++stateRewardIt; - ++builderIt; } // If the model is nondeterministic, we need to open a row group. - if (!generator.isDeterministicModel()) { + if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } // Now add all choices. for (auto const& choice : behavior) { // Add command labels if requested. - if (options.buildCommandLabels) { + if (generator->getOptions().isBuildChoiceLabelsSet()) { choiceLabels.get().push_back(choice.getChoiceLabels()); } @@ -264,14 +252,12 @@ namespace storm { } // Add the rewards to the reward models. - auto builderIt = rewardModelBuilders.begin(); auto choiceRewardIt = choice.getChoiceRewards().begin(); - for (auto const& rewardModel : selectedRewardModels) { - if (rewardModel.get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.push_back(*choiceRewardIt); + for (auto& rewardModelBuilder : rewardModelBuilders) { + if (rewardModelBuilder.hasStateActionRewards()) { + rewardModelBuilder.addStateActionReward(*choiceRewardIt); } ++choiceRewardIt; - ++builderIt; } ++currentRow; } @@ -307,58 +293,26 @@ namespace storm { } template - typename ExplicitModelBuilder::ModelComponents ExplicitModelBuilder::buildModelComponents(std::vector const& selectedRewardModels) { + typename ExplicitModelBuilder::ModelComponents ExplicitModelBuilder::buildModelComponents() { ModelComponents modelComponents; // 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.isDeterministicModel(); + bool deterministicModel = generator->isDeterministicModel(); // Prepare the transition matrix builder and the reward model builders. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); std::vector> rewardModelBuilders; - for (auto const& rewardModelName : selectedRewardModels) { - rewardModelBuilders.emplace_back(rewardModelName); - } - - // If we were asked to treat some states as terminal states, we determine an expression characterizing the - // terminal states of the model that we pass on to the matrix building routine. - boost::optional terminalExpression; - if (options.terminalStates) { - if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { - terminalExpression = boost::get(options.terminalStates.get()); - } else { - std::string const& labelName = boost::get(options.terminalStates.get()); - terminalExpression = program.getLabelExpression(labelName); - } - } - if (options.negatedTerminalStates) { - if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { - if (terminalExpression) { - terminalExpression = terminalExpression.get() || !boost::get(options.negatedTerminalStates.get()); - } else { - terminalExpression = !boost::get(options.negatedTerminalStates.get()); - } - } else { - std::string const& labelName = boost::get(options.negatedTerminalStates.get()); - if (terminalExpression) { - terminalExpression = terminalExpression.get() || !program.getLabelExpression(labelName); - } else { - terminalExpression = !program.getLabelExpression(labelName); - } - } - } - if (terminalExpression) { - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal."); + for (uint64_t i = 0; i < generator->getNumberOfRewardModels(); ++i) { + rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i)); } - modelComponents.choiceLabeling = buildMatrices(selectedRewardModels, transitionMatrixBuilder, rewardModelBuilders, terminalExpression); + modelComponents.choiceLabeling = buildMatrices(transitionMatrixBuilder, rewardModelBuilders); modelComponents.transitionMatrix = transitionMatrixBuilder.build(); // Now finalize all reward models. - auto builderIt = rewardModelBuilders.begin(); - for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { - modelComponents.rewardModels.emplace(rewardModelIt->get().getName(), builderIt->build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); + for (auto& rewardModelBuilder : rewardModelBuilders) { + modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); } // Build the state labeling. @@ -368,7 +322,7 @@ namespace storm { if (options.buildStateValuations) { stateValuations = storm::storage::sparse::StateValuations(stateStorage.getNumberOfStates()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { - stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation, program.getManager()); + stateValuations.get().valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first); } } @@ -377,8 +331,7 @@ namespace storm { template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { - storm::generator::PrismStateLabelingGenerator generator(program, variableInformation); - return generator.generate(stateStorage.stateToId, stateStorage.initialStateIndices); + return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices); } // Explicitly instantiate the class. diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h index 3d21299da..685ff8870 100644 --- a/src/builder/ExplicitModelBuilder.h +++ b/src/builder/ExplicitModelBuilder.h @@ -13,7 +13,6 @@ #include #include "src/storage/prism/Program.h" -#include "src/storage/expressions/SimpleValuation.h" #include "src/storage/expressions/ExpressionEvaluator.h" #include "src/storage/BitVectorHashMap.h" #include "src/logic/Formulas.h" @@ -88,7 +87,7 @@ namespace storm { /*! * Creates an explicit model builder that uses the provided generator.. * - * @param generator The generator to build. + * @param generator The generator to use. */ ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options = Options()); @@ -129,19 +128,17 @@ namespace storm { * * @param transitionMatrixBuilder The builder of the transition matrix. * @param rewardModelBuilders The builders for the selected reward models. - * @param terminalExpression If given, states satisfying this expression are not explored further. * @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. */ - boost::optional>> buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); + boost::optional>> buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders); /*! * Explores the state space of the given program and returns the components of the model as a result. * - * @param selectedRewardModels The reward models that are to be considered. * @return A structure containing the components of the resulting model. */ - ModelComponents buildModelComponents(std::vector const& selectedRewardModels); + ModelComponents buildModelComponents(); /*! * Builds the state labeling for the given program. diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index b8352ae49..3f97db791 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -162,7 +162,7 @@ namespace storm { modelFormulasPair.model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (!formulas.empty()) { + if (!modelFormulasPair.formulas.empty()) { if (modelFormulasPair.model->isSparseModel()) { if (storm::settings::getModule().isCounterexampleSet()) { // If we were requested to generate a counterexample, we now do so for each formula. diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index fae2fcc43..26563d408 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -34,6 +34,10 @@ namespace storm { return boost::get(labelOrExpression); } + NextStateGeneratorOptions::NextStateGeneratorOptions() : buildChoiceLabels(false) { + // Intentionally left empty. + } + NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); @@ -112,8 +116,8 @@ namespace storm { return labels; } - std::vector const& NextStateGeneratorOptions::getLabelExpressions() const { - return labelExpressions; + std::vector const& NextStateGeneratorOptions::getExpressionLabels() const { + return expressionLabels; } std::vector> const& NextStateGeneratorOptions::getTerminalStates() const { @@ -138,7 +142,7 @@ namespace storm { } NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) { - labelExpressions.emplace_back(expression); + expressionLabels.emplace_back(expression); return *this; } @@ -162,11 +166,41 @@ namespace storm { return *this; } + RewardModelInformation::RewardModelInformation(std::string const& name, bool stateRewards, bool stateActionRewards, bool transitionRewards) : name(name), stateRewards(stateRewards), stateActionRewards(stateActionRewards), transitionRewards(transitionRewards) { + // Intentionally left empty. + } + + std::string const& RewardModelInformation::getName() const { + return name; + } + + bool RewardModelInformation::hasStateRewards() const { + return stateRewards; + } + + bool RewardModelInformation::hasStateActionRewards() const { + return stateActionRewards; + } + + bool RewardModelInformation::hasTransitionRewards() const { + return transitionRewards; + } + template NextStateGenerator::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) { // Intentionally left empty. } + template + std::size_t NextStateGenerator::getNumberOfRewardModels() const { + return this->options.getRewardModelNames().size(); + } + + template + NextStateGeneratorOptions const& NextStateGenerator::getOptions() const { + return options; + } + template class NextStateGenerator; template class NextStateGenerator; diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index a4063d2aa..1b9c7a374 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -7,6 +7,7 @@ #include #include "src/storage/expressions/Expression.h" +#include "src/storage/BitVectorHashMap.h" #include "src/generator/CompressedState.h" #include "src/generator/StateBehavior.h" @@ -16,11 +17,6 @@ namespace storm { class Expression; } - namespace storage { - template - class BitVectorHashMap; - } - namespace models { namespace sparse { class StateLabeling; @@ -49,6 +45,11 @@ namespace storm { class NextStateGeneratorOptions { public: + /*! + * Creates an object representing the default options. + */ + NextStateGeneratorOptions(); + /*! * 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 preserveFormula. @@ -85,7 +86,7 @@ namespace storm { std::vector const& getRewardModelNames() const; std::set const& getLabels() const; - std::vector const& getLabelExpressions() const; + std::vector const& getExpressionLabels() const; std::vector> const& getTerminalStates() const; bool hasTerminalStates() const; void clearTerminalStates(); @@ -106,7 +107,7 @@ namespace storm { std::set labels; /// The expression that are to be used for creating the state labeling. - std::vector labelExpressions; + std::vector expressionLabels; /// If one of these labels/expressions evaluates to the given bool, the state generator can abort the exploration. std::vector> terminalStates; @@ -115,6 +116,29 @@ namespace storm { bool buildChoiceLabels; }; + enum class ModelType { + DTMC, + CTMC, + MDP, + MA + }; + + class RewardModelInformation { + public: + RewardModelInformation(std::string const& name, bool stateRewards, bool stateActionRewards, bool transitionRewards); + + std::string const& getName() const; + bool hasStateRewards() const; + bool hasStateActionRewards() const; + bool hasTransitionRewards() const; + + private: + std::string name; + bool stateRewards; + bool stateActionRewards; + bool transitionRewards; + }; + template class NextStateGenerator { public: @@ -122,6 +146,8 @@ namespace storm { NextStateGenerator(NextStateGeneratorOptions const& options); + virtual uint64_t getStateSize() const = 0; + virtual ModelType getModelType() const = 0; virtual bool isDeterministicModel() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; @@ -129,7 +155,14 @@ namespace storm { virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; virtual bool satisfies(storm::expressions::Expression const& expression) const = 0; - virtual storm::models::sparse::StateLabeling generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; + std::size_t getNumberOfRewardModels() const; + virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; + + virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const = 0; + + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; + + NextStateGeneratorOptions const& getOptions() const; protected: NextStateGeneratorOptions options; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 8286a6418..da83134ef 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -4,7 +4,7 @@ #include "src/models/sparse/StateLabeling.h" -#include "src/storage/BitVectorHashMap.h" +#include "src/storage/expressions/SimpleValuation.h" #include "src/utility/constants.h" #include "src/utility/macros.h" @@ -14,15 +14,43 @@ namespace storm { namespace generator { template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator(options), program(program), rewardModels(), variableInformation(VariableInformation(program)), evaluator(program.getManager()), state(nullptr), comparator() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator(options), program(program), rewardModels(), variableInformation(program), evaluator(program.getManager()), state(nullptr), comparator() { STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); // Extract the reward models from the program based on the names we were given. for (auto const& rewardModelName : this->options.getRewardModelNames()) { rewardModels.push_back(program.getRewardModel(rewardModelName)); } + + // If there are terminal states we need to handle, we now need to translate all labels to expressions. + if (this->options.hasTerminalStates()) { + for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { + if (expressionOrLabelAndBool.first.isExpression()) { + terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); + } else { + terminalStates.push_back(std::make_pair(program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second)); + } + } + } } - + + template + uint64_t PrismNextStateGenerator::getStateSize() const { + return variableInformation.getTotalBitOffset(true); + } + + template + ModelType PrismNextStateGenerator::getModelType() const { + switch (program.getModelType()) { + case storm::prism::Program::ModelType::DTMC: return ModelType::DTMC; + case storm::prism::Program::ModelType::CTMC: return ModelType::CTMC; + case storm::prism::Program::ModelType::MDP: return ModelType::MDP; + case storm::prism::Program::ModelType::MA: return ModelType::MA; + default: + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); + } + } + template bool PrismNextStateGenerator::isDeterministicModel() const { return program.isDeterministicModel(); @@ -83,9 +111,9 @@ namespace storm { } // If a terminal expression was set and we must not expand this state, return now. - if (this->options.hasTerminalExpression()) { - for (auto const& expression : this->options.getTerminalExpressions()) { - if (evaluator.asBool(expression) { + if (!terminalStates.empty()) { + for (auto const& expressionBool : terminalStates) { + if (evaluator.asBool(expressionBool.first) == expressionBool.second) { return result; } } @@ -423,22 +451,38 @@ namespace storm { } template - storm::models::sparse::StateLabeling PrismNextStateGenerator::generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { - std::vector const& labels = program.getLabels(); + storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { + // Gather a vector of labels and their expressions so we can iterate it over it a lot. + std::vector> labels; + for (auto const& label : this->options.getLabels()) { + labels.push_back(std::make_pair(label, program.getLabelExpression(label))); + } + + // Make the labels unique. + std::sort(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; } ); + auto it = std::unique(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first == b.first; } ); + labels.resize(std::distance(labels.begin(), it)); + for (auto const& expression : this->options.getExpressionLabels()) { + std::stringstream stream; + stream << expression; + labels.push_back(std::make_pair(stream.str(), expression)); + } + + // Prepare result. storm::models::sparse::StateLabeling result(states.size()); // Initialize labeling. for (auto const& label : labels) { - result.addLabel(label.getName()); + result.addLabel(label.first); } 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); + if (evaluator.asBool(label.second)) { + result.addLabelToState(label.first, stateIndexPair.second); } } } @@ -452,6 +496,17 @@ namespace storm { return result; } + template + RewardModelInformation PrismNextStateGenerator::getRewardModelInformation(uint64_t const& index) const { + storm::prism::RewardModel const& rewardModel = rewardModels[index].get(); + return RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards()); + } + + template + storm::expressions::SimpleValuation PrismNextStateGenerator::toValuation(CompressedState const& state) const { + return unpackStateIntoValuation(state, variableInformation, program.getManager()); + } + template class PrismNextStateGenerator; template class PrismNextStateGenerator; } diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index 27d43864a..c7fc61e16 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -19,6 +19,8 @@ namespace storm { PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); + virtual uint64_t getStateSize() const override; + virtual ModelType getModelType() const override; virtual bool isDeterministicModel() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; @@ -26,7 +28,11 @@ namespace storm { virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; virtual bool satisfies(storm::expressions::Expression const& expression) const override; - virtual storm::models::sparse::StateLabeling generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; + virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; + + virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override; + + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; private: /*! @@ -76,13 +82,16 @@ namespace storm { storm::prism::Program const& program; // The reward models that need to be considered. - std::vector> selectedRewardModels; + std::vector> rewardModels; + + // The expressions that define terminal states. + std::vector> terminalStates; // A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; // Information about how the variables are packed. - VariableInformation const& variableInformation; + VariableInformation variableInformation; // An evaluator used to evaluate expressions. storm::expressions::ExpressionEvaluator evaluator; diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp index 580097119..fe192aa9e 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -35,7 +35,7 @@ namespace storm { namespace modelchecker { template - SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().getPrecision()) { + SparseExplorationModelChecker::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions) : program(storm::utility::prism::preprocess(program, constantDefinitions.get())), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule().getPrecision()) { // Intentionally left empty. } @@ -59,7 +59,7 @@ namespace storm { explorationInformation.newRowGroup(0); std::map labelToExpressionMapping = program.getLabelToExpressionMapping(); - StateGeneration stateGeneration(program, variableInformation, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); + StateGeneration stateGeneration(program, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); // Compute and return result. diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h index aa13f379a..6c137d088 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.h +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h @@ -74,9 +74,6 @@ namespace storm { // The program that defines the model to check. storm::prism::Program program; - // The variable information. - storm::generator::VariableInformation variableInformation; - // The random number generator. mutable std::default_random_engine randomGenerator; diff --git a/src/modelchecker/exploration/StateGeneration.cpp b/src/modelchecker/exploration/StateGeneration.cpp index 71fc4d416..0765bf594 100644 --- a/src/modelchecker/exploration/StateGeneration.cpp +++ b/src/modelchecker/exploration/StateGeneration.cpp @@ -7,7 +7,7 @@ namespace storm { namespace exploration_detail { template - StateGeneration::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), stateStorage(variableInformation.getTotalBitOffset(true)), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { + StateGeneration::StateGeneration(storm::prism::Program const& program, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program), stateStorage(generator.getStateSize()), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { stateToIdCallback = [&explorationInformation, this] (storm::generator::CompressedState const& state) -> StateType { StateType newIndex = stateStorage.getNumberOfStates(); diff --git a/src/modelchecker/exploration/StateGeneration.h b/src/modelchecker/exploration/StateGeneration.h index f75211e54..7375f1867 100644 --- a/src/modelchecker/exploration/StateGeneration.h +++ b/src/modelchecker/exploration/StateGeneration.h @@ -21,7 +21,7 @@ namespace storm { template class StateGeneration { public: - StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); + StateGeneration(storm::prism::Program const& program, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); void load(storm::generator::CompressedState const& state); diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h index cda4a1fde..fc86fb14e 100644 --- a/src/storage/BitVectorHashMap.h +++ b/src/storage/BitVectorHashMap.h @@ -14,7 +14,7 @@ namespace storm { * queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of * 64. */ - template, class Hash2 = storm::storage::NonZeroBitVectorHash> + template, class Hash2 = storm::storage::NonZeroBitVectorHash> class BitVectorHashMap { public: class BitVectorHashMapIterator { diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp index 822e01fdc..617a5642b 100644 --- a/src/utility/prism.cpp +++ b/src/utility/prism.cpp @@ -14,15 +14,8 @@ namespace storm { namespace prism { template - storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional> const& constantDefinitions, boost::optional> const& restrictedLabelSet, boost::optional> const& expressionLabels) { - storm::prism::Program result; - - // Start by defining the undefined constants in the model. - if (constantDefinitions) { - result = program.defineUndefinedConstants(constantDefinitions.get()); - } else { - result = program; - } + storm::prism::Program preprocess(storm::prism::Program const& program, std::map const& constantDefinitions) { + storm::prism::Program result = program.defineUndefinedConstants(constantDefinitions); // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. if (!std::is_same::value && result.hasUndefinedConstants()) { @@ -43,30 +36,16 @@ namespace storm { 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."); } - // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. - if (restrictedLabelSet) { - result.filterLabels(restrictedLabelSet.get()); - } - - // Build new labels. - if (expressionLabels) { - std::map constantsSubstitution = result.getConstantsSubstitution(); - - for (auto const& expression : expressionLabels.get()) { - std::stringstream stream; - stream << expression.substitute(constantsSubstitution); - std::string name = stream.str(); - if (!result.hasLabel(name)) { - result.addLabel(name, expression); - } - } - } - // Now that the program is fixed, we we need to substitute all constants with their concrete value. result = result.substituteConstants(); return result; } + template + storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString) { + return preprocess(program, parseConstantDefinitionString(program, constantDefinitionString)); + } + std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map constantDefinitions; std::set definedConstants; @@ -124,9 +103,11 @@ namespace storm { return constantDefinitions; } - template storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional> const& constantDefinitions, boost::optional> const& restrictedLabelSet, boost::optional> const& expressionLabels); + template storm::prism::Program preprocess(storm::prism::Program const& program, std::map const& constantDefinitions); + template storm::prism::Program preprocess(storm::prism::Program const& program, std::map const& constantDefinitions); - template storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional> const& constantDefinitions, boost::optional> const& restrictedLabelSet, boost::optional> const& expressionLabels); + template storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); + template storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); } } diff --git a/src/utility/prism.h b/src/utility/prism.h index c6a8918b9..610f82bd0 100644 --- a/src/utility/prism.h +++ b/src/utility/prism.h @@ -20,10 +20,13 @@ namespace storm { namespace utility { namespace prism { + std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString); + template - storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional> const& constantDefinitions = boost::none, boost::optional> const& restrictedLabelSet = boost::none, boost::optional> const& expressionLabels = boost::none); + storm::prism::Program preprocess(storm::prism::Program const& program, std::map const& constantDefinitions); - std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString); + template + storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); } // namespace prism } // namespace utility diff --git a/src/utility/storm.h b/src/utility/storm.h index 964ef4f56..91047f751 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -14,12 +14,9 @@ #include "storm-config.h" - - // Headers that provide auxiliary functionality. #include "src/settings/SettingsManager.h" - #include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/modules/IOSettings.h" #include "src/settings/modules/BisimulationSettings.h" @@ -75,6 +72,9 @@ #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" +// Headers related to program preprocessing. +#include "src/utility/prism.h" + // Headers related to exception handling. #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidArgumentException.h" @@ -83,9 +83,6 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotSupportedException.h" -// Notice: The implementation for the template functions must stay in the header. -// Otherwise the linker complains. - namespace storm { template @@ -105,7 +102,9 @@ namespace storm { storm::prism::Program translatedProgram; // Get the string that assigns values to the unknown currently undefined constants in the model. - std::string constants = storm::settings::getModule().getConstantDefinitionString(); + std::string constantDefinitionString = storm::settings::getModule().getConstantDefinitionString(); + translatedProgram = storm::utility::prism::preprocess(program, constantDefinitionString); + std::map constantsSubstitution = translatedProgram.getConstantsSubstitution(); // Customize and perform model-building. if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { @@ -120,29 +119,20 @@ namespace storm { storm::builder::ExplicitModelBuilder builder(program, options); result.model = builder.translate(); - translatedProgram = builder.getTranslatedProgram(); } else if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - options.addConstantDefinitionsFromString(program, constants); + options.addConstantDefinitionsFromString(program, constantDefinitionString); storm::builder::DdPrismModelBuilder builder; result.model = builder.translateProgram(program, options); translatedProgram = builder.getTranslatedProgram(); } + // There may be constants of the model appearing in the formulas, so we replace all their occurrences // by their definitions in the translated program. - - // Start by building a mapping from constants of the (translated) model to their defining expressions. - std::map constantSubstitution; - for (auto const& constant : translatedProgram.getConstants()) { - if (constant.isDefined()) { - constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); - } - } - for (auto const& formula : formulas) { - result.formulas.emplace_back(formula->substitute(constantSubstitution)); + result.formulas.emplace_back(formula->substitute(constantsSubstitution)); } return result; }