From ca354cffe4e771da62777e6a102b3e45eeb20770 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Mar 2016 13:12:24 +0100 Subject: [PATCH] moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker Former-commit-id: 704dde9ec5bfb6c7af4a368d39fcd475108528f7 --- src/builder/ExplicitPrismModelBuilder.cpp | 52 +---- src/cli/entrypoints.h | 16 +- .../reachability/SparseLearningModelChecker.h | 0 .../SparseMdpLearningModelChecker.cpp | 28 +++ .../SparseMdpLearningModelChecker.h | 29 +++ src/utility/prism.cpp | 66 +++++- src/utility/prism.h | 190 +----------------- src/utility/storm.h | 1 + 8 files changed, 141 insertions(+), 241 deletions(-) delete mode 100644 src/modelchecker/reachability/SparseLearningModelChecker.h create mode 100644 src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp create mode 100644 src/modelchecker/reachability/SparseMdpLearningModelChecker.h diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ef53b9e43..94b1e0f46 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -182,57 +182,7 @@ namespace storm { } template - ExplicitPrismModelBuilder::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) { - this->program = program.defineUndefinedConstants(options.constantDefinitions.get()); - } else { - this->program = program; - } - - // 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 && this->program.hasUndefinedConstants()) { - std::vector> undefinedConstants = this->program.getUndefinedConstants(); - std::stringstream stream; - bool printComma = false; - for (auto const& constant : undefinedConstants) { - if (printComma) { - stream << ", "; - } else { - printComma = true; - } - stream << constant.get().getName() << " (" << constant.get().getType() << ")"; - } - stream << "."; - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); - } else if (std::is_same::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."); - } - - // 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) { - 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 constantsSubstitution = this->program.getConstantsSubstitution(); - - for (auto const& expression : options.expressionLabels.get()) { - std::stringstream stream; - stream << expression.substitute(constantsSubstitution); - std::string name = stream.str(); - 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. - this->program = this->program.substituteConstants(); + ExplicitPrismModelBuilder::ExplicitPrismModelBuilder(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) { // Create the variable information for the transformed program. this->variableInformation = VariableInformation(this->program); diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index a467825e9..ba863af43 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -58,12 +58,12 @@ namespace storm { void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidSettingsException, "Currently learning-based verification is only available for DTMCs and MDPs."); + STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently learning-based verification is only available for DTMCs and MDPs."); std::cout << std::endl << "Model checking property: " << *formula << " ..."; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - storm::modelchecker::SparseLearningModelChecker checker(program); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::SparseMdpLearningModelChecker checker(program); std::unique_ptr result; - if (checker.canHandle(formula)) { + if (checker.canHandle(task)) { std::unique_ptr result = checker.check(task); } else { std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl; @@ -71,13 +71,19 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); std::cout << *result << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } } } + +#ifdef STORM_HAVE_CARL + template<> + void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Learning-based verification does currently not support parametric models."); + } +#endif template void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { diff --git a/src/modelchecker/reachability/SparseLearningModelChecker.h b/src/modelchecker/reachability/SparseLearningModelChecker.h deleted file mode 100644 index e69de29bb..000000000 diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp new file mode 100644 index 000000000..0316d6bc4 --- /dev/null +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp @@ -0,0 +1,28 @@ +#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h" + +#include "src/logic/FragmentSpecification.h" + +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +namespace storm { + namespace modelchecker { + template + SparseMdpLearningModelChecker::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(program) { + // Intentionally left empty. + } + + template + bool SparseMdpLearningModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); + storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true); + return formula.isInFragment(fragment); + } + + template + std::unique_ptr SparseMdpLearningModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + return nullptr; + } + + template class SparseMdpLearningModelChecker; + } +} \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h new file mode 100644 index 000000000..d398c6be3 --- /dev/null +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h @@ -0,0 +1,29 @@ +#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ +#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ + +#include "src/modelchecker/AbstractModelChecker.h" + +#include "src/storage/prism/Program.h" + +#include "src/utility/constants.h" + +namespace storm { + namespace modelchecker { + + template + class SparseMdpLearningModelChecker : public AbstractModelChecker { + public: + SparseMdpLearningModelChecker(storm::prism::Program const& program); + + virtual bool canHandle(CheckTask const& checkTask) const override; + + virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; + + private: + // The program that defines the model to check. + storm::prism::Program program; + }; + } +} + +#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPLEARNINGMODELCHECKER_H_ */ \ No newline at end of file diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp index 5901d3434..822e01fdc 100644 --- a/src/utility/prism.cpp +++ b/src/utility/prism.cpp @@ -1,13 +1,72 @@ #include "src/utility/prism.h" + +#include "src/adapters/CarlAdapter.h" + #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/prism/Program.h" +#include "src/utility/macros.h" + #include "src/exceptions/InvalidArgumentException.h" -#include "macros.h" namespace storm { namespace utility { 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; + } + + // 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()) { + std::vector> undefinedConstants = result.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + } else if (std::is_same::value && !result.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."); + } + + // 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; + } + std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map constantDefinitions; std::set definedConstants; @@ -64,6 +123,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 preprocessProgram(storm::prism::Program const& program, boost::optional> const& constantDefinitions, boost::optional> const& restrictedLabelSet, boost::optional> const& expressionLabels); + } } } \ No newline at end of file diff --git a/src/utility/prism.h b/src/utility/prism.h index f894b464f..c6a8918b9 100644 --- a/src/utility/prism.h +++ b/src/utility/prism.h @@ -1,13 +1,11 @@ #ifndef STORM_UTILITY_PRISM_H_ #define STORM_UTILITY_PRISM_H_ -#include #include -#include -#include - -#include "src/utility/OsDetection.h" +#include +#include +#include namespace storm { namespace expressions { @@ -21,185 +19,9 @@ namespace storm { namespace utility { namespace prism { - // A structure holding information about a particular choice. - template> - struct Choice { - public: - Choice(uint_fast64_t actionIndex = 0, bool createChoiceLabels = false) : distribution(), actionIndex(actionIndex), choiceLabels(nullptr) { - if (createChoiceLabels) { - choiceLabels = std::shared_ptr>(new boost::container::flat_set()); - } - } - - Choice(Choice const& other) = default; - Choice& operator=(Choice const& other) = default; -#ifndef WINDOWS - Choice(Choice&& other) = default; - Choice& operator=(Choice&& other) = default; -#endif - - /*! - * Returns an iterator to the first element of this choice. - * - * @return An iterator to the first element of this choice. - */ - typename std::map::iterator begin() { - return distribution.begin(); - } - - /*! - * Returns an iterator to the first element of this choice. - * - * @return An iterator to the first element of this choice. - */ - typename std::map::const_iterator begin() const { - return distribution.cbegin(); - } - - /*! - * Returns an iterator that points past the elements of this choice. - * - * @return An iterator that points past the elements of this choice. - */ - typename std::map::iterator end() { - return distribution.end(); - } - - /*! - * Returns an iterator that points past the elements of this choice. - * - * @return An iterator that points past the elements of this choice. - */ - typename std::map::const_iterator end() const { - return distribution.cend(); - } - - /*! - * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to - * distribution.end(). - * - * @param value The value to find. - * @return An iterator to the element with the given key, if there is one. - */ - typename std::map::iterator find(uint_fast64_t value) { - return distribution.find(value); - } - - /*! - * Inserts the contents of this object to the given output stream. - * - * @param out The stream in which to insert the contents. - */ - friend std::ostream& operator<<(std::ostream& out, Choice const& choice) { - out << "<"; - for (auto const& stateProbabilityPair : choice.distribution) { - out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; - } - out << ">"; - return out; - } - - /*! - * 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) { - choiceLabels->insert(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(boost::container::flat_set const& labelSet) { - for (uint_fast64_t label : labelSet) { - addChoiceLabel(label); - } - } - - /*! - * Retrieves the set of labels associated with this choice. - * - * @return The set of labels associated with this choice. - */ - boost::container::flat_set const& getChoiceLabels() const { - return *choiceLabels; - } - - /*! - * Retrieves the index of the action of this choice. - * - * @return The index of the action of this choice. - */ - uint_fast64_t getActionIndex() const { - return actionIndex; - } - - /*! - * Retrieves the total mass of this choice. - * - * @return The total mass. - */ - ValueType getTotalMass() const { - return totalMass; - } - - /*! - * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, - * yet. - * - * @param state The state for which to add the entry. - * @return A reference to the entry that is associated with the given state. - */ - ValueType& getOrAddEntry(uint_fast64_t state) { - auto stateProbabilityPair = distribution.find(state); - - if (stateProbabilityPair == distribution.end()) { - distribution[state] = ValueType(); - } - return distribution.at(state); - } - - /*! - * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, - * yet. - * - * @param state The state for which to add the entry. - * @return A reference to the entry that is associated with the given state. - */ - ValueType const& getOrAddEntry(uint_fast64_t state) const { - auto stateProbabilityPair = distribution.find(state); - - if (stateProbabilityPair == distribution.end()) { - distribution[state] = ValueType(); - } - return distribution.at(state); - } - - void addProbability(KeyType state, ValueType value) { - totalMass += value; - distribution[state] += value; - } - - std::size_t size() const { - return distribution.size(); - } - - private: - // The distribution that is associated with the choice. - std::map distribution; - - // The total probability mass (or rates) of this choice. - ValueType totalMass; - - // The index of the action name. - uint_fast64_t actionIndex; - - // The labels that are associated with this choice. - std::shared_ptr> choiceLabels; - }; + + 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); std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString); diff --git a/src/utility/storm.h b/src/utility/storm.h index c7afeb523..aca1a1cac 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -57,6 +57,7 @@ #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" +#include "src/modelchecker/reachability/SparseMdpLearningModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"