From 34e48473b32f938a49c1e7b9945e1927004a5d43 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 16 May 2017 11:28:36 +0200 Subject: [PATCH 01/28] Updated changelog --- CHANGELOG.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b13f803b..efb029b07 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,18 @@ The releases of major and minor versions contain an overview of changes since th Version 1.0.x ------------------- +### Version 1.0.2 (2017/5) + +- Fix for nested formulae +- JANI: Explicit engine supports custom model compositions. +- Storm now overwrites files if asked to write files to a specific location +- Changes in build process to accomodate for changes in carl. Also, more robust against issues with carl +- Wellformedness constraints on PMCs: + * include constraints from rewards + * are in smtlib2 +- USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set. + Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction + ### Version 1.0.1 (2017/4) - Multi-objective model checking support now fully included From 9276cc355af2193d074a50b595c769cbc5bc6c12 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Jun 2017 16:17:45 +0200 Subject: [PATCH 02/28] Fixed issues in export of parametric result file --- src/storm/analysis/GraphConditions.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 4f47f15a7..9d915e73e 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -50,25 +50,34 @@ namespace storm { for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { + // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { - if (transition.getValue().denominatorAsNumber() > 0) { + if (transition.getValue().denominator().constantPart() > 0) { + // Assert: nom <= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + // Assert: nom >= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); - } else if (transition.getValue().denominatorAsNumber() < 0) { + } else if (transition.getValue().denominator().constantPart() < 0) { + // Assert nom >= denom wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + // Assert: nom <= 0 wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_ASSERT(false, "Denominator must not equal 0."); } } else { + // Assert: denom != 0 wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); - wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + // Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0 + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); + // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); } } STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); if(!storm::utility::isConstant(sum)) { + // Assert: sum == 1 wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ); } From 3ffaa77193881d7499e0e84c09b515c0522a77da Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Jun 2017 14:27:16 +0200 Subject: [PATCH 03/28] first version of state filters in filter expressions --- src/storm/cli/cli.cpp | 76 ++++++++++++++++++----- src/storm/logic/Formula.cpp | 4 ++ src/storm/logic/Formula.h | 4 +- src/storm/parser/FormulaParserGrammar.cpp | 8 +-- src/storm/parser/FormulaParserGrammar.h | 4 +- src/storm/storage/jani/Property.cpp | 13 ++-- src/storm/storage/jani/Property.h | 17 ++++- 7 files changed, 94 insertions(+), 32 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 0f53aa2d3..fad3709af 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -353,15 +353,27 @@ namespace storm { return input; } + std::vector> createFormulasToRespect(std::vector const& properties) { + std::vector> result = storm::api::extractFormulasFromProperties(properties); + + for (auto const& property : properties) { + if (!property.getFilter().getStatesFormula()->isInitialFormula()) { + result.push_back(property.getFilter().getStatesFormula()); + } + } + + return result; + } + template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties)); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties)); } template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + return storm::api::buildSparseModel(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); } template @@ -379,6 +391,9 @@ namespace storm { std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { storm::utility::Stopwatch modelBuildingWatch(true); + + // Make sure that states in filter are built as label. ALso for bisimulation. + std::shared_ptr result; if (input.model) { if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { @@ -622,11 +637,11 @@ namespace storm { }; template - void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { for (auto const& property : properties) { printModelCheckingProperty(property); storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula()); + std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); watch.stop(); printInitialStatesResult(result, property, &watch); postprocessingCallback(result); @@ -636,7 +651,8 @@ namespace storm { template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); }); } @@ -645,7 +661,8 @@ namespace storm { void verifyWithExplorationEngine(SymbolicInput const& input) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); }); } @@ -654,9 +671,18 @@ namespace storm { void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { auto sparseModel = model->as>(); verifyProperties(input.properties, - [&sparseModel] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + [&sparseModel] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique(sparseModel->getInitialStates()); + } else { + filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); + } + result->filter(filter->asQualitativeCheckResult()); return result; }, [&sparseModel] (std::unique_ptr const& result) { @@ -670,20 +696,42 @@ namespace storm { template void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); + } + + result->filter(filter->asQualitativeCheckResult()); return result; }); } template void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); + } + + result->filter(filter->asQualitativeCheckResult()); return result; }); } diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 9038a2307..3f871908e 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -175,6 +175,10 @@ namespace storm { return std::shared_ptr(new BooleanLiteralFormula(true)); } + bool Formula::isInitialFormula() const { + return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init"; + } + PathFormula& Formula::asPathFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 2ad5e9477..a76dd0ef7 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -93,10 +93,12 @@ namespace storm { bool isInFragment(FragmentSpecification const& fragment) const; FormulaInformation info() const; - + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0; static std::shared_ptr getTrueFormula(); + + bool isInitialFormula() const; PathFormula& asPathFormula(); PathFormula const& asPathFormula() const; diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index bee6b5117..78102f859 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -128,7 +128,7 @@ namespace storm { #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)]; + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -332,8 +332,8 @@ namespace storm { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } - storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula) { - storm::jani::FilterExpression filterExpression(formula, filterType); + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { + storm::jani::FilterExpression filterExpression(formula, filterType, states); ++propertyCount; if (propertyName) { @@ -343,7 +343,7 @@ namespace storm { } } - storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula) { + storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula) { ++propertyCount; if (propertyName) { return storm::jani::Property(propertyName.get(), formula); diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 79b272246..7ae6740b8 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -223,8 +223,8 @@ namespace storm { std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiObjectiveFormula(std::vector> const& subformulas); - storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula); - storm::jani::Property createPropertyWithDefaultFilterType(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); + storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); // An error handler function. phoenix::function handler; diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index e46d2ee50..73c6d0dec 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -5,19 +5,17 @@ namespace storm { std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { - return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; } Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)) - { - + : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + // Intentionally left empty. } Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) - : name(name), comment(comment), filterExpression(fe) - { - + : name(name), comment(comment), filterExpression(fe) { + // Intentionally left empty. } std::string const& Property::getName() const { @@ -48,6 +46,5 @@ namespace storm { return os << "(" << p.getName() << ") : " << p.getFilter(); } - } } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 52db07fef..74aceab5c 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -2,6 +2,10 @@ #include "storm/modelchecker/results/FilterType.h" #include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace jani { @@ -30,28 +34,35 @@ namespace storm { public: FilterExpression() = default; - explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {} + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr const& statesFormula = std::make_shared("init")) : formula(formula), ft(ft), statesFormula(statesFormula) { + STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula."); + } std::shared_ptr const& getFormula() const { return formula; } + std::shared_ptr const& getStatesFormula() const { + return statesFormula; + } + storm::modelchecker::FilterType getFilterType() const { return ft; } FilterExpression substitute(std::map const& substitution) const { - return FilterExpression(formula->substitute(substitution), ft); + return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution)); } FilterExpression substituteLabels(std::map const& labelSubstitution) const { - return FilterExpression(formula->substitute(labelSubstitution), ft); + return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution)); } private: // For now, we assume that the states are always the initial states. std::shared_ptr formula; storm::modelchecker::FilterType ft; + std::shared_ptr statesFormula; }; From bc373475ff34eb755931453f9b4fed82b5204a77 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Jun 2017 14:31:26 +0200 Subject: [PATCH 04/28] respecting state filters in bisimulation --- src/storm/cli/cli.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index fad3709af..8fea01e61 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -391,9 +391,6 @@ namespace storm { std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { storm::utility::Stopwatch modelBuildingWatch(true); - - // Make sure that states in filter are built as label. ALso for bisimulation. - std::shared_ptr result; if (input.model) { if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { @@ -432,7 +429,7 @@ namespace storm { } STORM_LOG_INFO("Performing bisimulation minimization..."); - return storm::api::performBisimulationMinimization(model, storm::api::extractFormulasFromProperties(input.properties), bisimType); + return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); } template From 9b90e0c784a711dd11c945ba19294e2a4824efe0 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 29 Jun 2017 10:30:17 +0200 Subject: [PATCH 05/28] typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index efb029b07..e701cd146 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,7 +13,7 @@ Version 1.0.x - Fix for nested formulae - JANI: Explicit engine supports custom model compositions. - Storm now overwrites files if asked to write files to a specific location -- Changes in build process to accomodate for changes in carl. Also, more robust against issues with carl +- Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl - Wellformedness constraints on PMCs: * include constraints from rewards * are in smtlib2 From d5902ac6946c422671646aadc789bb2acd1d567b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 29 Jun 2017 11:25:44 +0200 Subject: [PATCH 06/28] Started on changelog for next version --- CHANGELOG.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b13f803b..3208b8b8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,12 +2,16 @@ Changelog ============== This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. -The releases of major and minor versions contain an overview of changes since the last major/minor update. +The releases of major and minor versions contain an overview of changes since the last major/minor update. Version 1.0.x ------------------- +### Version 1.0.2 + +- Several improvements and fixes in building process + ### Version 1.0.1 (2017/4) - Multi-objective model checking support now fully included From 6151dc0e9643661f58bddec009d24f393bcb4b19 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Jun 2017 11:42:49 +0200 Subject: [PATCH 07/28] Enabled Long Run Average Rewards for MAs (LP based) --- .../SparseMarkovAutomatonCslModelChecker.cpp | 10 +++- .../SparseMarkovAutomatonCslModelChecker.h | 1 + .../helper/SparseMarkovAutomatonCslHelper.cpp | 58 ++++++++++++++++--- .../helper/SparseMarkovAutomatonCslHelper.h | 11 +++- 4 files changed, 69 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 7f555e6d2..e1570cebc 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -106,7 +106,15 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long run average rewards in non-closed Markov automaton."); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 971c7b383..94db9727d 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -25,6 +25,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 50e26ddae..15166122d 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -214,8 +214,9 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - + // If there are no goal states, we avoid the computation and directly return zero. if (psiStates.empty()) { return std::vector(numberOfStates, storm::utility::zero()); @@ -226,6 +227,36 @@ namespace storm { return std::vector(numberOfStates, storm::utility::one()); } + // Otherwise, reduce the long run average probabilities to long run average rewards. + // Every Markovian goal state s gets 1/E(s) reward for its (unique) action. + std::vector totalActionRewards(transitionMatrix.getRowCount(), storm::utility::zero()); + storm::storage::BitVector markovianGoalStates = markovianStates & psiStates; + for (auto const& state : markovianGoalStates) { + totalActionRewards[transitionMatrix.getRowGroupIndices()[state]] = storm::utility::one() / exitRateVector[state]; + } + return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalActionRewards, minMaxLinearEquationSolverFactory); + + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + // Obtain the total action reward vector where the state rewards are scaled accordingly + std::vector stateRewardWeights(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + for (auto const markovianState : markovianStates) { + stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; + } + std::vector totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights); + RewardModelType scaledRewardModel(boost::none, std::move(totalRewardVector)); + + return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalRewardVector, minMaxLinearEquationSolverFactory); + } + + template + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + // Start by decomposing the Markov automaton into its MECs. storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); @@ -251,7 +282,7 @@ namespace storm { } // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, mec)); + lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, totalActionRewards, mec)); } // For fast transition rewriting, we build some auxiliary data structures. @@ -381,7 +412,7 @@ namespace storm { } template - ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec) { std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); @@ -402,6 +433,9 @@ namespace storm { // Now, based on the type of the state, create a suitable constraint. if (markovianStates.get(state)) { + STORM_LOG_ASSERT(stateChoicesPair.second.size() == 1, "Markovian state " << state << " is not deterministic: It has " << stateChoicesPair.second.size() << " choices."); + uint_fast64_t choice = *stateChoicesPair.second.begin(); + storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { @@ -409,7 +443,7 @@ namespace storm { } constraint = constraint + solver->getManager().rational(storm::utility::one() / exitRateVector[state]) * k; - storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getManager().rational(storm::utility::one() / exitRateVector[state]) : solver->getManager().rational(storm::utility::zero()); + storm::expressions::Expression rightHandSide = solver->getManager().rational(totalActionRewards[choice]); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -426,7 +460,7 @@ namespace storm { constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getManager().rational(element.getValue()); } - storm::expressions::Expression rightHandSide = solver->getManager().rational(storm::utility::zero()); + storm::expressions::Expression rightHandSide = solver->getManager().rational(totalActionRewards[choice]); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -451,11 +485,15 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -464,12 +502,16 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 20d6c9598..613f81d91 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -31,6 +31,12 @@ namespace storm { template static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template + static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template + static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -49,12 +55,13 @@ namespace storm { * @param markovianStates A bit vector storing all markovian states. * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are * assumed to be zero. - * @param goalStates A bit vector indicating which states are to be considered as goal states. + * @param totalActionRewards A vector indicating the total rewards obtained for each action * @param mec The maximal end component to consider for computing the long-run average. * @return The long-run average of being in a goal state for the given MEC. */ template - static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); + }; } From b8844d5ad1c9979873deb7d47cf57bc25b6c9068 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Jun 2017 11:57:22 +0200 Subject: [PATCH 08/28] updated changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e701cd146..5acbcc582 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,6 +19,7 @@ Version 1.0.x * are in smtlib2 - USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set. Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction +- Parametric model checking is now handled in a separated library/executable called storm-pars ### Version 1.0.1 (2017/4) From 75e4c229cb0934f6da8902e6f219a3c605a1754b Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Jun 2017 13:54:16 +0200 Subject: [PATCH 09/28] minor fix for Long run average rewards for Markov automata --- .../modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e1570cebc..c444c72a5 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -34,7 +34,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true))) { + if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 15166122d..d48c38a6c 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -247,7 +247,6 @@ namespace storm { stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; } std::vector totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights); - RewardModelType scaledRewardModel(boost::none, std::move(totalRewardVector)); return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalRewardVector, minMaxLinearEquationSolverFactory); } From ae470851f41b08a810e3a991c9a6f8d785924277 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Jun 2017 13:59:43 +0200 Subject: [PATCH 10/28] Do not segfault when a property could not be verified --- src/storm/cli/cli.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index b28f068c3..6d938735c 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -655,7 +655,9 @@ namespace storm { verifyProperties(input.properties, [&sparseModel] (std::shared_ptr const& formula) { std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + if (result) { + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + } return result; }); } @@ -665,7 +667,9 @@ namespace storm { verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + if (result) { + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + } return result; }); } @@ -675,7 +679,9 @@ namespace storm { verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + if (result) { + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + } return result; }); } From bec6b664d91e2d9042fb5c5b77733c0292540c35 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 29 Jun 2017 16:50:33 +0200 Subject: [PATCH 11/28] actually check carl version, error if outdated --- resources/3rdparty/CMakeLists.txt | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 4148df10a..3a7a44240 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -199,6 +199,9 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) ############################################################# set(STORM_HAVE_CARL OFF) +set(CARL_MINYEAR 17) +set(CARL_MINMONTH 06) +set(CARL_MINPATCH 0) if(USE_CARL) if (NOT STORM_FORCE_SHIPPED_CARL) find_package(carl QUIET) @@ -212,6 +215,18 @@ if(USE_CARL) else() message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?") endif() + if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR}) + if(${carl_MINORMONTHVERSION} LESS ${CARL_MINMONTH}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + elseif(${carl_MINORMONTHVERSION} EQUAL ${CARL_MINMONTH}) + if(${carl_MAINTENANCEVERSION} LESS ${CARL_MINPATCH}) + message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + endif() + endif() + endif() + set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) message(STATUS "Storm - Use system version of carl.") From 4cafe33415df7bbe64c6c2711e4ce84a4f08b6ca Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 30 Jun 2017 18:27:04 +0200 Subject: [PATCH 12/28] Changed unique_ptr to shared_ptr for RegionModelCheckers --- src/storm-pars/api/region.h | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 043f461b0..a8cc6bbe2 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -78,7 +78,7 @@ namespace storm { } template - std::unique_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -93,22 +93,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ConstantType>>(); + checker = std::make_shared, ConstantType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::shared_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); @@ -123,22 +123,22 @@ namespace storm { } // Obtain the region model checker - std::unique_ptr> result; + std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) { - result = std::make_unique, ImpreciseType, PreciseType>>(); + checker = std::make_shared, ImpreciseType, PreciseType>>(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - result->specify(consideredModel, task); + checker->specify(consideredModel, task); - return result; + return checker; } template - std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { + std::shared_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { switch (engine) { case storm::modelchecker::RegionCheckEngine::ParameterLifting: return initializeParameterLiftingRegionModelChecker(model, task); From 6bd8c8f9b5a195ae7db6db6a28e061f6e537754d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 30 Jun 2017 18:27:27 +0200 Subject: [PATCH 13/28] Fixed some typos --- src/storm-dft/CMakeLists.txt | 2 +- src/storm/analysis/GraphConditions.cpp | 1 + src/storm/analysis/GraphConditions.h | 6 +++--- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 3951551ae..9ec70aed2 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -8,7 +8,7 @@ file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp) file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) -# Create storm-pgcl. +# Create storm-dft. add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) # Remove define symbol for shared libstorm. diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 9d915e73e..812429dec 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -72,6 +72,7 @@ namespace storm { wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } + // Assert: transition > 0 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); } } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 87b95a78c..c6043fd5a 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -35,7 +35,7 @@ namespace storm { void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * Constructs a constraint collector for the given DTMC. The constraints are built and ready for * retrieval after the construction. * * @param dtmc The DTMC for which to create the constraints. @@ -47,14 +47,14 @@ namespace storm { * * @return The set of wellformed-ness constraints. */ - std::unordered_set::val> const& getWellformedConstraints() const; + std::unordered_set::val> const& getWellformedConstraints() const; /*! * Returns the set of graph-preserving constraints. * * @return The set of graph-preserving constraints. */ - std::unordered_set::val> const& getGraphPreservingConstraints() const; + std::unordered_set::val> const& getGraphPreservingConstraints() const; /*! * Constructs the constraints for the given DTMC. From bff745656c14e041d8183c40e0d73759a8c064ef Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 30 Jun 2017 19:01:04 +0200 Subject: [PATCH 14/28] Fixed some matrix builder bugs related to 0x0 matrices --- src/storm/storage/SparseMatrix.cpp | 32 ++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 99a716415..1a005d2d0 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -104,17 +104,25 @@ namespace storm { } template - SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& 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() { + SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& 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), currentRowGroup() { + + lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1; + lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); + highestColumn = matrix.getColumnCount() == 0 ? 0 : matrix.getColumnCount() - 1; // 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.get().pop_back(); - currentRowGroup = rowGroupIndices.get().size() - 1; + if (!rowGroupIndices->empty()) { + rowGroupIndices.get().pop_back(); + } + currentRowGroup = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; } // Likewise, we need to 'open' the row indications again. - rowIndications.pop_back(); + if (!rowIndications.empty()) { + rowIndications.pop_back(); + } } template @@ -191,7 +199,10 @@ namespace storm { template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { - uint_fast64_t rowCount = lastRow + 1; + + bool hasEntries = currentEntryCount != 0; + + uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0; if (initialRowCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); rowCount = std::max(rowCount, initialRowCount); @@ -203,12 +214,17 @@ namespace storm { rowIndications.push_back(currentEntryCount); } + // If there are no rows, we need to erase the start index of the current (non-existing) row. + if (rowCount == 0) { + rowIndications.pop_back(); + } + // We put a sentinel element at the last position of the row indices array. This eases iteration work, // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. rowIndications.push_back(currentEntryCount); - - uint_fast64_t columnCount = highestColumn + 1; + assert(rowCount == rowIndications.size() - 1); + uint_fast64_t columnCount = hasEntries ? highestColumn + 1 : 0; if (initialColumnCountSet && forceInitialDimensions) { STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << "."); columnCount = std::max(columnCount, initialColumnCount); @@ -300,7 +316,7 @@ namespace storm { } highestColumn = maxColumn; - lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); + lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues[columnsAndValues.size() - 1].getColumn(); } template From 19925ac74d6b2dfe2e49cba85a2433442f48e3e2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 30 Jun 2017 19:05:02 +0200 Subject: [PATCH 15/28] implemented value iteration based Long run average rewards for Markov automata by Butkova et al. (TACAS 2017) --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 212 ++++++++++++++---- .../helper/SparseMarkovAutomatonCslHelper.h | 27 ++- .../models/sparse/StandardRewardModel.cpp | 28 +++ src/storm/models/sparse/StandardRewardModel.h | 14 ++ 4 files changed, 231 insertions(+), 50 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index d48c38a6c..411c0fecd 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -213,7 +213,7 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); @@ -228,32 +228,18 @@ namespace storm { } // Otherwise, reduce the long run average probabilities to long run average rewards. - // Every Markovian goal state s gets 1/E(s) reward for its (unique) action. - std::vector totalActionRewards(transitionMatrix.getRowCount(), storm::utility::zero()); - storm::storage::BitVector markovianGoalStates = markovianStates & psiStates; - for (auto const& state : markovianGoalStates) { - totalActionRewards[transitionMatrix.getRowGroupIndices()[state]] = storm::utility::one() / exitRateVector[state]; - } - return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalActionRewards, minMaxLinearEquationSolverFactory); + // Every Markovian goal state gets reward one. + std::vector stateRewards(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::utility::vector::setVectorValues(stateRewards, markovianStates & psiStates, storm::utility::one()); + storm::models::sparse::StandardRewardModel rewardModel(std::move(stateRewards)); + + return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, rewardModel, minMaxLinearEquationSolverFactory, useLpBasedTechnique); } template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { - // Obtain the total action reward vector where the state rewards are scaled accordingly - std::vector stateRewardWeights(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - for (auto const markovianState : markovianStates) { - stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; - } - std::vector totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights); - - return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, totalRewardVector, minMaxLinearEquationSolverFactory); - } - - template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Start by decomposing the Markov automaton into its MECs. @@ -281,7 +267,7 @@ namespace storm { } // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, totalActionRewards, mec)); + lraValuesForEndComponents.push_back(computeLraForMaximalEndComponent(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec, minMaxLinearEquationSolverFactory, useLpBasedTechnique)); } // For fast transition rewriting, we build some auxiliary data structures. @@ -410,8 +396,31 @@ namespace storm { return SparseMdpPrctlHelper::computeReachabilityRewards(dir, transitionMatrix, backwardTransitions, rewardModel, psiStates, false, false, minMaxLinearEquationSolverFactory).values; } - template - ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec) { + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { + + // If the mec only consists of a single state, we compute the LRA value directly + if (++mec.begin() == mec.end()) { + uint_fast64_t state = mec.begin()->first; + STORM_LOG_THROW(markovianStates.get(state), storm::exceptions::InvalidOperationException, "Markov Automaton has Zeno behavior. Computation of Long Run Average values not supported."); + ValueType result = rewardModel.hasStateRewards() ? rewardModel.getStateReward(state) : storm::utility::zero(); + if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { + STORM_LOG_ASSERT(mec.begin()->second.size() == 1, "Markovian state has nondeterministic behavior."); + uint_fast64_t choice = *mec.begin()->second.begin(); + result += exitRateVector[state] * rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero()); + } + return result; + } + + if (useLpBasedTechnique) { + return computeLraForMaximalEndComponentLP(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec); + } else { + return computeLraForMaximalEndComponentVI(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec, minMaxLinearEquationSolverFactory); + } + } + + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); @@ -442,7 +451,8 @@ namespace storm { } constraint = constraint + solver->getManager().rational(storm::utility::one() / exitRateVector[state]) * k; - storm::expressions::Expression rightHandSide = solver->getManager().rational(totalActionRewards[choice]); + + storm::expressions::Expression rightHandSide = solver->getManager().rational(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, (ValueType) (storm::utility::one() / exitRateVector[state]))); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -458,8 +468,8 @@ namespace storm { for (auto element : transitionMatrix.getRow(choice)) { constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getManager().rational(element.getValue()); } - - storm::expressions::Expression rightHandSide = solver->getManager().rational(totalActionRewards[choice]); + + storm::expressions::Expression rightHandSide = solver->getManager().rational(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero())); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -473,8 +483,128 @@ namespace storm { solver->optimize(); return storm::utility::convertNumber(solver->getContinuousValue(k)); } - + template + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + // Initialize data about the mec + + storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false); + storm::storage::BitVector mecChoices(transitionMatrix.getRowCount(), false); + for (auto const& stateChoicesPair : mec) { + mecStates.set(stateChoicesPair.first); + for (auto const& choice : stateChoicesPair.second) { + mecChoices.set(choice); + } + } + storm::storage::BitVector markovianMecStates = mecStates & markovianStates; + storm::storage::BitVector probabilisticMecStates = mecStates & ~markovianStates; + storm::storage::BitVector probabilisticMecChoices = transitionMatrix.getRowFilter(probabilisticMecStates) & mecChoices; + STORM_LOG_THROW(!markovianMecStates.empty(), storm::exceptions::InvalidOperationException, "Markov Automaton has Zeno behavior. Computation of Long Run Average values not supported."); + + // Get the uniformization rate + + ValueType uniformizationRate = storm::utility::vector::max_if(exitRateVector, markovianMecStates); + // To ensure that the model is aperiodic, we need to make sure that every Markovian state gets a self loop. + // Hence, we increase the uniformization rate a little. + uniformizationRate += storm::utility::one(); // Todo: try other values such as *=1.01 + + // Get the transitions of the submodel, that is + // * a matrix aMarkovian with all (uniformized) transitions from Markovian mec states to all Markovian mec states. + // * a matrix aMarkovianToProbabilistic with all (uniformized) transitions from Markovian mec states to all probabilistic mec states. + // * a matrix aProbabilistic with all transitions from probabilistic mec states to other probabilistic mec states. + // * a matrix aProbabilisticToMarkovian with all transitions from probabilistic mec states to all Markovian mec states. + typename storm::storage::SparseMatrix aMarkovian = transitionMatrix.getSubmatrix(true, markovianMecStates, markovianMecStates, true); + typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianMecStates, probabilisticMecStates); + typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, probabilisticMecStates); + typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, markovianMecStates); + // The matrices with transitions from Markovian states need to be uniformized. + uint_fast64_t subState = 0; + for (auto state : markovianMecStates) { + ValueType uniformizationFactor = exitRateVector[state] / uniformizationRate; + for (auto& entry : aMarkovianToProbabilistic.getRow(subState)) { + entry.setValue(entry.getValue() * uniformizationFactor); + } + for (auto& entry : aMarkovian.getRow(subState)) { + if (entry.getColumn() == subState) { + entry.setValue(storm::utility::one() - uniformizationFactor * (storm::utility::one() - entry.getValue())); + } else { + entry.setValue(entry.getValue() * uniformizationFactor); + } + } + ++subState; + } + + // Compute the rewards obtained in a single uniformization step + + std::vector markovianChoiceRewards; + markovianChoiceRewards.reserve(aMarkovian.getRowCount()); + for (auto const& state : markovianMecStates) { + ValueType stateRewardScalingFactor = storm::utility::one() / uniformizationRate; + ValueType actionRewardScalingFactor = exitRateVector[state] / uniformizationRate; + assert(transitionMatrix.getRowGroupSize(state) == 1); + uint_fast64_t choice = transitionMatrix.getRowGroupIndices()[state]; + markovianChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, stateRewardScalingFactor, actionRewardScalingFactor)); + } + + std::vector probabilisticChoiceRewards; + probabilisticChoiceRewards.reserve(aProbabilistic.getRowCount()); + for (auto const& state : probabilisticMecStates) { + uint_fast64_t groupStart = transitionMatrix.getRowGroupIndices()[state]; + uint_fast64_t groupEnd = transitionMatrix.getRowGroupIndices()[state + 1]; + for (uint_fast64_t choice = probabilisticMecChoices.getNextSetIndex(groupStart); choice < groupEnd; choice = probabilisticMecChoices.getNextSetIndex(choice + 1)) { + probabilisticChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero())); + } + } + + // start the iterations + + ValueType precision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()) / uniformizationRate; + std::vector v(aMarkovian.getRowCount(), storm::utility::zero()); + std::vector vOld = v; + std::vector w = v; + std::vector x(aProbabilistic.getRowGroupCount(), storm::utility::zero()); + std::vector xPrime = x; + std::vector b = probabilisticChoiceRewards; + auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); + solver->setCachingEnabled(true); + + while (true) { + + // Compute the expected total rewards for the probabilistic states + solver->solveEquations(dir, x, b); + + // now compute the values for the markovian states + for (uint_fast64_t row = 0; row < aMarkovian.getRowCount(); ++row) { + v[row] = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); + } + + // Check for convergence + auto vIt = v.begin(); + auto vEndIt = v.end(); + auto vOldIt = vOld.begin(); + ValueType maxDiff = *vIt - *vOldIt; + ValueType minDiff = maxDiff; + for (++vIt, ++vOldIt; vIt != vEndIt; ++vIt, ++vOldIt) { + ValueType diff = *vIt - *vOldIt; + maxDiff = std::max(maxDiff, diff); + minDiff = std::min(minDiff, diff); + } + if (maxDiff - minDiff < precision) { + break; + } + + // update the rhs of the MinMax equation system + ValueType referenceValue = v.front(); + storm::utility::vector::applyPointwise(v, w, [&referenceValue] (ValueType const& v_i) -> ValueType { return v_i - referenceValue; }); + aProbabilisticToMarkovian.multiplyWithVector(w, b); + storm::utility::vector::addVectors(b, probabilisticChoiceRewards, b); + + vOld = v; + } + return v.front() * uniformizationRate; + + } template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -482,35 +612,39 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); + + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); - template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); + + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); + + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 613f81d91..8faddede5 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -29,13 +29,10 @@ namespace storm { template - static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); template - static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - - template - static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); template static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -44,24 +41,32 @@ namespace storm { template ::SupportsExponential, int>::type = 0> static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template ::SupportsExponential, int>::type = 0> - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template ::SupportsExponential, int>::type = 0> + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. * + * Implementations are based on Linear Programming (LP) and Value Iteration (VI). + * * @param dir Sets whether the long-run average is to be minimized or maximized. * @param transitionMatrix The transition matrix of the underlying Markov automaton. * @param markovianStates A bit vector storing all markovian states. * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are * assumed to be zero. - * @param totalActionRewards A vector indicating the total rewards obtained for each action + * @param rewardModel The considered reward model + * @param actionRewards The action rewards (earned instantaneously). * @param mec The maximal end component to consider for computing the long-run average. + * @param minMaxLinearEquationSolverFactory The factory for creating MinMaxLinearEquationSolvers (if needed by the performed method * @return The long-run average of being in a goal state for the given MEC. */ - template - static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, std::vector const& totalActionRewards, storm::storage::MaximalEndComponent const& mec); - + template + static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique = false); + template + static ValueType computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec); + template + static ValueType computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + }; } diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index bffd8a7e9..721608047 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -139,6 +139,30 @@ namespace storm { return StandardRewardModel(std::move(newStateRewardVector), std::move(newStateActionRewardVector), std::move(newTransitionRewardMatrix)); } + template + template + ValueType StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, MatrixValueType const& stateRewardWeight, MatrixValueType const& actionRewardWeight) const { + ValueType result = this->hasStateRewards() ? (this->hasStateActionRewards() ? (ValueType) (this->getStateReward(stateIndex) * stateRewardWeight + this->getStateActionReward(choiceIndex) * actionRewardWeight) + : (ValueType) (this->getStateReward(stateIndex) * stateRewardWeight)) + : (this->hasStateActionRewards() ? (ValueType) (this->getStateActionReward(choiceIndex) * actionRewardWeight) + : storm::utility::zero()); + if (this->hasTransitionRewards()) { + auto rewMatrixEntryIt = this->getTransitionRewardMatrix().begin(choiceIndex); + for (auto const& transitionEntry : transitionMatrix.getRow(choiceIndex)) { + assert(rewMatrixEntryIt != this->getTransitionRewardMatrix().end(choiceIndex)); + if (transitionEntry.getColumn() < rewMatrixEntryIt->getColumn()) { + continue; + } else { + // We assume that the transition reward matrix is a submatrix of the given transition matrix. Hence, the following must hold + assert(transitionEntry.getColumn() == rewMatrixEntryIt->getColumn()); + result += actionRewardWeight * rewMatrixEntryIt->getValue() * storm::utility::convertNumber(transitionEntry.getValue()); + ++rewMatrixEntryIt; + } + } + } + return result; + } + template template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards) { @@ -362,6 +386,8 @@ namespace storm { template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -385,6 +411,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); @@ -398,6 +425,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; + template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 2a3033ea7..c58f38312 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -4,6 +4,7 @@ #include #include "storm/storage/SparseMatrix.h" +#include "storm/utility/constants.h" #include "storm/utility/OsDetection.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -161,6 +162,19 @@ namespace storm { * @return The transition reward matrix if there is one. */ boost::optional> const& getOptionalTransitionRewardMatrix() const; + + /*! + * Retrieves the total reward for the given state action pair (including (scaled) state rewards, action rewards and transition rewards + * + * @param stateIndex The index of the considered state + * @param choiceIndex The index of the considered choice + * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix. + * @param stateRewardWeight The weight that is used to scale the state reward + * @param actionRewardWeight The weight that is used to scale the action based rewards (includes action and transition rewards). + * @return + */ + template + ValueType getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, MatrixValueType const& stateRewardWeight = storm::utility::one(), MatrixValueType const& actionRewardWeight = storm::utility::one()) const; /*! * Creates a new reward model by restricting the actions of the action-based rewards. From 49713eea72db74aa7a095a844441235c46ba16cb Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Jul 2017 17:03:51 +0200 Subject: [PATCH 16/28] Added new MinMaxMethod: 'acyclic' which potentially increases performance on acyclic mdps --- .../modules/MinMaxEquationSolverSettings.cpp | 4 +- .../solver/MinMaxLinearEquationSolver.cpp | 4 +- src/storm/solver/SolverSelectionOptions.cpp | 3 +- src/storm/solver/SolverSelectionOptions.h | 2 +- .../StandardMinMaxLinearEquationSolver.cpp | 111 ++++++++++++++++++ .../StandardMinMaxLinearEquationSolver.h | 8 +- 6 files changed, 125 insertions(+), 7 deletions(-) diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index c13bb492d..c140e7520 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -19,7 +19,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "acyclic"}; this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); @@ -36,6 +36,8 @@ namespace storm { return storm::solver::MinMaxMethod::ValueIteration; } else if (minMaxEquationSolvingTechnique == "policy-iteration" || minMaxEquationSolvingTechnique == "pi") { return storm::solver::MinMaxMethod::PolicyIteration; + } else if (minMaxEquationSolvingTechnique == "acyclic") { + return storm::solver::MinMaxMethod::Acyclic; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 5f1e0c176..4bdb08f3e 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -170,7 +170,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { result = std::make_unique>(std::forward(matrix), std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(std::forward(matrix)); @@ -187,7 +187,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; auto method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available."); + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic, storm::exceptions::InvalidSettingsException, "For this data type only value iteration, policy iteration, and acyclic value iteration are available."); return std::make_unique>(std::forward(matrix), std::make_unique>()); } #endif diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index fe42f299a..2a39108ea 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -10,7 +10,8 @@ namespace storm { return "value"; case MinMaxMethod::Topological: return "topological"; - + case MinMaxMethod::Acyclic: + return "acyclic"; } return "invalid"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 32af0a4eb..94584c7c3 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -6,7 +6,7 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological) + ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological, Acyclic) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 0a93a70f4..627dcd131 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -29,6 +29,7 @@ namespace storm { switch (method) { case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; + case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -91,6 +92,8 @@ namespace storm { return solveEquationsValueIteration(dir, x, b); case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: return solveEquationsPolicyIteration(dir, x, b); + case StandardMinMaxLinearEquationSolverSettings::SolutionMethod::Acyclic: + return solveEquationsAcyclic(dir, x, b); default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method"); } @@ -293,6 +296,113 @@ namespace storm { return status == Status::Converged || status == Status::TerminatedEarly; } + template + bool StandardMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + uint64_t numGroups = this->A.getRowGroupCount(); + + // Allocate memory for the scheduler (if required) + if (this->isTrackSchedulerSet()) { + if (this->schedulerChoices) { + this->schedulerChoices->resize(numGroups); + } else { + this->schedulerChoices = std::vector(numGroups); + } + } + + // We now compute a topological sort of the row groups. + // If caching is enabled, it might be possible to obtain this sort from the cache. + if (this->isCachingEnabled()) { + if (rowGroupOrdering) { + for (auto const& group : *rowGroupOrdering) { + computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); + } + return true; + } else { + rowGroupOrdering = std::make_unique>(); + rowGroupOrdering->reserve(numGroups); + } + } + + auto transposedMatrix = this->A.transpose(true); + + // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. + storm::storage::BitVector processedGroups(numGroups, false); + // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. + // A group can be processed if all successors have already been processed. + // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. + // This is due to the observation that groups with higher indices usually need to be processed earlier. + storm::storage::BitVector candidates(numGroups, true); + uint64_t candidate = numGroups - 1; + for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { + candidates.set(numGroups - candidate - 1, false); + + // Check if the candidate row group has an unprocessed successor + bool hasUnprocessedSuccessor = false; + for (auto const& entry : this->A.getRowGroup(candidate)) { + if (!processedGroups.get(entry.getColumn())) { + hasUnprocessedSuccessor = true; + break; + } + } + + uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; + + if (!hasUnprocessedSuccessor) { + // This candidate can be processed. + processedGroups.set(candidate); + computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); + if (this->isCachingEnabled()) { + rowGroupOrdering->push_back(candidate); + } + + // Add new candidates + for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { + uint64_t predecessor = predecessorEntry.getColumn(); + if (!candidates.get(numGroups - predecessor - 1)) { + candidates.set(numGroups - predecessor - 1, true); + nextCandidate = std::max(nextCandidate, predecessor); + ++numCandidates; + } + } + } + candidate = nextCandidate; + } + + assert(candidates.empty()); + STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); + return true; + } + + template + void StandardMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { + uint64_t row = this->A.getRowGroupIndices()[group]; + uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1]; + assert(row != groupEnd); + + auto bIt = b.begin() + row; + ValueType& xi = x[group]; + xi = this->A.multiplyRowWithVector(row, x) + *bIt; + uint64_t optimalRow = row; + + for (++row, ++bIt; row < groupEnd; ++row, ++bIt) { + ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt; + if (minimize(dir)) { + if (choiceVal < xi) { + xi = choiceVal; + optimalRow = row; + } + } else { + if (choiceVal > xi) { + xi = choiceVal; + optimalRow = row; + } + } + } + if (choice != nullptr) { + *choice = optimalRow - this->A.getRowGroupIndices()[group]; + } + } + template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if(!linEqSolverA) { @@ -356,6 +466,7 @@ namespace storm { linEqSolverA.reset(); auxiliaryRowVector.reset(); auxiliaryRowGroupVector.reset(); + rowGroupOrdering.reset(); MinMaxLinearEquationSolver::clearCache(); } diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index f7e1e40c6..050ce0bde 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -12,7 +12,7 @@ namespace storm { StandardMinMaxLinearEquationSolverSettings(); enum class SolutionMethod { - ValueIteration, PolicyIteration + ValueIteration, PolicyIteration, Acyclic }; void setSolutionMethod(SolutionMethod const& solutionMethod); @@ -51,9 +51,12 @@ namespace storm { private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; + void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice = nullptr) const; + enum class Status { Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress }; @@ -62,7 +65,8 @@ namespace storm { mutable std::unique_ptr> linEqSolverA; mutable std::unique_ptr> auxiliaryRowVector; // A.rowCount() entries mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries - + mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries + Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; void reportStatus(Status status, uint64_t iterations) const; From 8da6a6e30e5fb80e899803e58cb7119f64bd7f2a Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Jul 2017 17:04:35 +0200 Subject: [PATCH 17/28] reduced memory consumption of VI based LRA computation --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 25 ++++++++----------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 411c0fecd..f692944eb 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -561,10 +561,8 @@ namespace storm { ValueType precision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()) / uniformizationRate; std::vector v(aMarkovian.getRowCount(), storm::utility::zero()); - std::vector vOld = v; std::vector w = v; std::vector x(aProbabilistic.getRowGroupCount(), storm::utility::zero()); - std::vector xPrime = x; std::vector b = probabilisticChoiceRewards; auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); solver->setCachingEnabled(true); @@ -574,22 +572,22 @@ namespace storm { // Compute the expected total rewards for the probabilistic states solver->solveEquations(dir, x, b); - // now compute the values for the markovian states - for (uint_fast64_t row = 0; row < aMarkovian.getRowCount(); ++row) { - v[row] = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); - } - - // Check for convergence + // now compute the values for the markovian states. We also keep track of the maximal and minimal difference between two values (for convergence checking) auto vIt = v.begin(); - auto vEndIt = v.end(); - auto vOldIt = vOld.begin(); - ValueType maxDiff = *vIt - *vOldIt; + uint_fast64_t row = 0; + ValueType newValue = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); + ValueType maxDiff = newValue - *vIt; ValueType minDiff = maxDiff; - for (++vIt, ++vOldIt; vIt != vEndIt; ++vIt, ++vOldIt) { - ValueType diff = *vIt - *vOldIt; + *vIt = newValue; + for (++vIt, ++row; row < aMarkovian.getRowCount(); ++vIt, ++row) { + newValue = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); + ValueType diff = newValue - *vIt; maxDiff = std::max(maxDiff, diff); minDiff = std::min(minDiff, diff); + *vIt = newValue; } + + // Check for convergence if (maxDiff - minDiff < precision) { break; } @@ -600,7 +598,6 @@ namespace storm { aProbabilisticToMarkovian.multiplyWithVector(w, b); storm::utility::vector::addVectors(b, probabilisticChoiceRewards, b); - vOld = v; } return v.front() * uniformizationRate; From 1c9d8886761db451939b42bc8fa0832fb329e313 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Jul 2017 17:10:33 +0200 Subject: [PATCH 18/28] uint_fast64_t -> uint64_t --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 78 +++++++++---------- .../helper/SparseMarkovAutomatonCslHelper.h | 4 +- 2 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index f692944eb..bc83d20f9 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -32,7 +32,7 @@ namespace storm { namespace helper { template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. @@ -46,7 +46,7 @@ namespace storm { // The matrices with transitions from Markovian states need to be digitized. // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. - uint_fast64_t rowIndex = 0; + uint64_t rowIndex = 0; for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovian.getRow(rowIndex)) { ValueType eTerm = std::exp(-exitRates[state] * delta); @@ -96,7 +96,7 @@ namespace storm { // and 1_G being the characteristic vector for all goal states. // * perform one timed-step using v_MS := A_MSwG * v_MS + A_MStoPS * v_PS + (A * 1_G)|MS std::vector markovianNonGoalValuesSwap(markovianNonGoalValues); - for (uint_fast64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { + for (uint64_t currentStep = 0; currentStep < numberOfSteps; ++currentStep) { // Start by (re-)computing bProbabilistic = bProbabilisticFixed + aProbabilisticToMarkovian * vMarkovian. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); @@ -119,14 +119,14 @@ namespace storm { } template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type."); } template ::SupportsExponential, int>::type> std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); // 'Unpack' the bounds to make them more easily accessible. double lowerBound = boundsPair.first; @@ -140,7 +140,7 @@ namespace storm { ValueType delta = (2 * storm::settings::getModule().getPrecision()) / (upperBound * maxExitRate * maxExitRate); // (2) Compute the number of steps we need to make for the interval. - uint_fast64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); + uint64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [" << lowerBound << ", " << upperBound << "]." << std::endl); // (3) Compute the non-goal states and initialize two vectors @@ -165,7 +165,7 @@ namespace storm { storm::utility::vector::setVectorValues(vAllMarkovian, ~psiStates % markovianStates, vMarkovian); // Compute the number of steps to reach the target interval. - numberOfSteps = static_cast(std::ceil(lowerBound / delta)); + numberOfSteps = static_cast(std::ceil(lowerBound / delta)); STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl); // Compute the bounded reachability for interval [0, b-a]. @@ -215,7 +215,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); // If there are no goal states, we avoid the computation and directly return zero. if (psiStates.empty()) { @@ -240,27 +240,27 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique) { - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Start by decomposing the Markov automaton into its MECs. storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); // Get some data members for convenience. - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now start with compute the long-run average for all end components in isolation. std::vector lraValuesForEndComponents; // While doing so, we already gather some information for the following steps. - std::vector stateToMecIndexMap(numberOfStates); + std::vector stateToMecIndexMap(numberOfStates); storm::storage::BitVector statesInMecs(numberOfStates); - for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { + for (uint64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; // Gather information for later use. for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; + uint64_t state = stateChoicesPair.first; statesInMecs.set(state); stateToMecIndexMap[state] = currentMecIndex; @@ -272,10 +272,10 @@ namespace storm { // For fast transition rewriting, we build some auxiliary data structures. storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; - uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); - uint_fast64_t lastStateNotInMecs = 0; - uint_fast64_t numberOfStatesNotInMecs = 0; - std::vector statesNotInMecsBeforeIndex; + uint64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); + uint64_t lastStateNotInMecs = 0; + uint64_t numberOfStatesNotInMecs = 0; + std::vector statesNotInMecsBeforeIndex; statesNotInMecsBeforeIndex.reserve(numberOfStates); for (auto state : statesNotContainedInAnyMec) { while (lastStateNotInMecs <= state) { @@ -290,11 +290,11 @@ namespace storm { typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). - uint_fast64_t currentChoice = 0; + uint64_t currentChoice = 0; for (auto state : statesNotContainedInAnyMec) { sspMatrixBuilder.newRowGroup(currentChoice); - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { + for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); b.push_back(storm::utility::zero()); @@ -310,7 +310,7 @@ namespace storm { } // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { + for (uint64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); } @@ -319,15 +319,15 @@ namespace storm { } // Now we are ready to construct the choices for the auxiliary states. - for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { + for (uint64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex]; sspMatrixBuilder.newRowGroup(currentChoice); for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; - boost::container::flat_set const& choicesInMec = stateChoicesPair.second; + uint64_t state = stateChoicesPair.first; + boost::container::flat_set const& choicesInMec = stateChoicesPair.second; - for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. @@ -346,7 +346,7 @@ namespace storm { } // Now insert all (cumulative) probability values that target an MEC. - for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { + for (uint64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); } @@ -401,12 +401,12 @@ namespace storm { // If the mec only consists of a single state, we compute the LRA value directly if (++mec.begin() == mec.end()) { - uint_fast64_t state = mec.begin()->first; + uint64_t state = mec.begin()->first; STORM_LOG_THROW(markovianStates.get(state), storm::exceptions::InvalidOperationException, "Markov Automaton has Zeno behavior. Computation of Long Run Average values not supported."); ValueType result = rewardModel.hasStateRewards() ? rewardModel.getStateReward(state) : storm::utility::zero(); if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { STORM_LOG_ASSERT(mec.begin()->second.size() == 1, "Markovian state has nondeterministic behavior."); - uint_fast64_t choice = *mec.begin()->second.begin(); + uint64_t choice = *mec.begin()->second.begin(); result += exitRateVector[state] * rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero()); } return result; @@ -426,7 +426,7 @@ namespace storm { solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. - std::map stateToVariableMap; + std::map stateToVariableMap; for (auto const& stateChoicesPair : mec) { std::string variableName = "x" + std::to_string(stateChoicesPair.first); stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); @@ -435,14 +435,14 @@ namespace storm { solver->update(); // Now we encode the problem as constraints. - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& stateChoicesPair : mec) { - uint_fast64_t state = stateChoicesPair.first; + uint64_t state = stateChoicesPair.first; // Now, based on the type of the state, create a suitable constraint. if (markovianStates.get(state)) { STORM_LOG_ASSERT(stateChoicesPair.second.size() == 1, "Markovian state " << state << " is not deterministic: It has " << stateChoicesPair.second.size() << " choices."); - uint_fast64_t choice = *stateChoicesPair.second.begin(); + uint64_t choice = *stateChoicesPair.second.begin(); storm::expressions::Expression constraint = stateToVariableMap.at(state); @@ -519,7 +519,7 @@ namespace storm { typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, probabilisticMecStates); typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(false, probabilisticMecChoices, markovianMecStates); // The matrices with transitions from Markovian states need to be uniformized. - uint_fast64_t subState = 0; + uint64_t subState = 0; for (auto state : markovianMecStates) { ValueType uniformizationFactor = exitRateVector[state] / uniformizationRate; for (auto& entry : aMarkovianToProbabilistic.getRow(subState)) { @@ -543,16 +543,16 @@ namespace storm { ValueType stateRewardScalingFactor = storm::utility::one() / uniformizationRate; ValueType actionRewardScalingFactor = exitRateVector[state] / uniformizationRate; assert(transitionMatrix.getRowGroupSize(state) == 1); - uint_fast64_t choice = transitionMatrix.getRowGroupIndices()[state]; + uint64_t choice = transitionMatrix.getRowGroupIndices()[state]; markovianChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, stateRewardScalingFactor, actionRewardScalingFactor)); } std::vector probabilisticChoiceRewards; probabilisticChoiceRewards.reserve(aProbabilistic.getRowCount()); for (auto const& state : probabilisticMecStates) { - uint_fast64_t groupStart = transitionMatrix.getRowGroupIndices()[state]; - uint_fast64_t groupEnd = transitionMatrix.getRowGroupIndices()[state + 1]; - for (uint_fast64_t choice = probabilisticMecChoices.getNextSetIndex(groupStart); choice < groupEnd; choice = probabilisticMecChoices.getNextSetIndex(choice + 1)) { + uint64_t groupStart = transitionMatrix.getRowGroupIndices()[state]; + uint64_t groupEnd = transitionMatrix.getRowGroupIndices()[state + 1]; + for (uint64_t choice = probabilisticMecChoices.getNextSetIndex(groupStart); choice < groupEnd; choice = probabilisticMecChoices.getNextSetIndex(choice + 1)) { probabilisticChoiceRewards.push_back(rewardModel.getTotalStateActionReward(state, choice, transitionMatrix, storm::utility::zero())); } } @@ -574,7 +574,7 @@ namespace storm { // now compute the values for the markovian states. We also keep track of the maximal and minimal difference between two values (for convergence checking) auto vIt = v.begin(); - uint_fast64_t row = 0; + uint64_t row = 0; ValueType newValue = markovianChoiceRewards[row] + aMarkovianToProbabilistic.multiplyRowWithVector(row, x) + aMarkovian.multiplyRowWithVector(row, w); ValueType maxDiff = newValue - *vIt; ValueType minDiff = maxDiff; @@ -615,7 +615,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); @@ -635,7 +635,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useLpBasedTechnique); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 8faddede5..f41c8e287 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -39,10 +39,10 @@ namespace storm { private: template ::SupportsExponential, int>::type = 0> - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the long-run average value for the given maximal end component of a Markov automaton. From 3de51e28e5ac20f01396a5ec35735d9a3dbfb158 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 3 Jul 2017 22:53:47 +0200 Subject: [PATCH 19/28] towards reward-bounded properties --- src/storm-dft-cli/storm-dyftee.cpp | 2 +- ...SparseDtmcParameterLiftingModelChecker.cpp | 2 +- .../SparseMdpParameterLiftingModelChecker.cpp | 2 +- .../SparseParametricDtmcSimplifier.cpp | 2 +- .../SparseParametricMdpSimplifier.cpp | 2 +- .../SparseParametricModelSimplifier.cpp | 6 ++-- src/storm/logic/BoundedUntilFormula.cpp | 14 +++----- src/storm/logic/BoundedUntilFormula.h | 9 +++-- src/storm/logic/FragmentChecker.cpp | 8 +++-- src/storm/logic/FragmentSpecification.cpp | 12 ++++++- src/storm/logic/FragmentSpecification.h | 4 +++ src/storm/logic/TimeBoundType.h | 35 +++++++++++++++++-- .../logic/VariableSubstitutionVisitor.cpp | 2 +- .../csl/HybridCtmcCslModelChecker.cpp | 2 +- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../SparseMultiObjectivePreprocessor.cpp | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 4 +-- src/storm/parser/JaniParser.cpp | 22 ++++++++++-- src/storm/storage/jani/JSONExporter.cpp | 9 +++-- 20 files changed, 102 insertions(+), 41 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 5bb379962..b2dc40006 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -185,7 +185,7 @@ int main(const int argc, const char** argv) { storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); auto evtlFormula = std::make_shared(targetExpression); - auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundType::Time); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); auto tbUntil = std::make_shared(tbFormula); auto evFormula = std::make_shared(evtlFormula, storm::logic::FormulaContext::Time); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 5f32c8386..155b13dec 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -75,7 +75,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 6169d22bf..65e16d628 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { // get the step bound STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + STORM_LOG_THROW(checkTask.getFormula().getTimeBoundReference().isStepBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); if (checkTask.getFormula().isUpperBoundStrict()) { diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index ed05131e4..826e141ff 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -111,7 +111,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index 1862936f4..97f93cf03 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -135,7 +135,7 @@ namespace storm { // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); - auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); return true; diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 343fc06e3..1679bdcca 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -78,21 +78,21 @@ namespace storm { template bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } template bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { // If this method was not overriden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); return false; } diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 10cd7f33e..66b5a29fa 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -10,7 +10,7 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundType(timeBoundType), lowerBound(lowerBound), upperBound(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReference), lowerBound(lowerBound), upperBound(upperBound) { STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } @@ -26,17 +26,11 @@ namespace storm { return visitor.visit(*this, data); } - TimeBoundType const& BoundedUntilFormula::getTimeBoundType() const { - return timeBoundType; + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const { + return timeBoundReference; } - bool BoundedUntilFormula::isStepBounded() const { - return timeBoundType == TimeBoundType::Steps; - } - - bool BoundedUntilFormula::isTimeBounded() const { - return timeBoundType == TimeBoundType::Time; - } + bool BoundedUntilFormula::isLowerBoundStrict() const { return lowerBound.get().isStrict(); diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 5dc2a3889..754d94cdf 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -12,7 +12,7 @@ namespace storm { namespace logic { class BoundedUntilFormula : public BinaryPathFormula { public: - BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundType const& timeBoundType = TimeBoundType::Time); + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); virtual bool isBoundedUntilFormula() const override; @@ -20,9 +20,8 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; - TimeBoundType const& getTimeBoundType() const; - bool isStepBounded() const; - bool isTimeBounded() const; + TimeBoundReference const& getTimeBoundReference() const; + bool isLowerBoundStrict() const; bool hasLowerBound() const; @@ -49,7 +48,7 @@ namespace storm { private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundType timeBoundType; + TimeBoundReference timeBoundReference; boost::optional lowerBound; boost::optional upperBound; }; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index c47b8ea5d..ee0967d22 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -58,10 +58,14 @@ namespace storm { result = result && !f.getLeftSubformula().isPathFormula(); result = result && !f.getRightSubformula().isPathFormula(); } - if (f.isStepBounded()) { + auto tbr = f.getTimeBoundReference(); + if (tbr.isStepBound()) { result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); - } else { + } else if(tbr.isTimeBound()) { result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + } else { + assert(tbr.isRewardBound()); + result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); } result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 0d4771552..19c4116aa 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -141,6 +141,7 @@ namespace storm { onlyEventuallyFormuluasInConditionalFormulas = true; stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; + rewardBoundedUntilFormulas = false; varianceAsMeasureType = false; qualitativeOperatorResults = true; @@ -423,7 +424,16 @@ namespace storm { this->timeBoundedUntilFormulas = newValue; return *this; } - + + bool FragmentSpecification::areRewardBoundedUntilFormulasAllowed() const { + return this->rewardBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setRewardBoundedUntilFormulasAllowed(bool newValue) { + this->rewardBoundedUntilFormulas = newValue; + return *this; + } + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 587d49bf3..619394189 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -102,6 +102,9 @@ namespace storm { bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); + + bool areRewardBoundedUntilFormulasAllowed() const; + FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); @@ -162,6 +165,7 @@ namespace storm { bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; + bool rewardBoundedUntilFormulas; bool varianceAsMeasureType; bool quantitativeOperatorResults; bool qualitativeOperatorResults; diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index aef71b040..2488baaaf 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -2,11 +2,42 @@ namespace storm { namespace logic { - + enum class TimeBoundType { Steps, - Time + Time, + Reward }; + + class TimeBoundReference { + TimeBoundType type; + std::string rewardName; + + public: + explicit TimeBoundReference(TimeBoundType t) : type(t) { + // For rewards, use the other constructor. + assert(t != TimeBoundType::Reward); + } + + explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) { + assert(rewardName != ""); // Empty reward name is reserved. + } + + + bool isStepBound() const { + return type == TimeBoundType::Steps; + } + + bool isTimeBound() const { + return type == TimeBoundType::Time; + } + + bool isRewardBound() const { + return type == TimeBoundType::Reward; + } + }; + + } } diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 96ede4769..8c0945adb 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -47,7 +47,7 @@ namespace storm { upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); } - return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundType())); + return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundReference())); } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 16574947f..ba7a727c4 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -83,7 +83,7 @@ namespace storm { SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 5de82a7d1..facfd3da2 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -60,7 +60,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index c444c72a5..2f90c23d5 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -54,7 +54,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - STORM_LOG_THROW(!pathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); + STORM_LOG_THROW(!pathFormula.getTimeBoundReference().isStepBound(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on MAs are not supported."); double lowerBound = 0; double upperBound = 0; if (pathFormula.hasLowerBound()) { diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index b2da20897..485bc41bf 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -266,7 +266,7 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); if (formula.hasLowerBound()) { STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index bee6b5117..95cb3f860 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -257,7 +257,7 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -273,7 +273,7 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundType::Time)); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index ecb3ed0ff..28ac7ae7c 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -297,7 +297,7 @@ namespace storm { } } } else if (propertyStructure.count("reward-instants") > 0) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant Reward for reward constraints not supported currently."); } //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); @@ -353,7 +353,7 @@ namespace storm { upperBound--; } STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); - return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); } else if (propertyStructure.count("time-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); @@ -364,10 +364,26 @@ namespace storm { double upperBound = pi.upperBound.evaluateAsDouble(); STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); - return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); } else if (propertyStructure.count("reward-bounds") > 0 ) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants); + STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); + std::string rewardName = rewExpr.getVariables().begin()->getName(); + STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm"); + return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName)); + } if (args[0]->isTrueFormula()) { return std::make_shared(args[1], formulaContext); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 65cab6fb1..5fde8267a 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -194,11 +194,14 @@ namespace storm { upperExclusive = f.isUpperBoundStrict(); } modernjson::json propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); - - if(f.isStepBounded()) { + + auto tbr = f.getTimeBoundReference(); + if(tbr.isStepBound()) { opDecl["step-bounds"] = propertyInterval; - } else { + } else if(tbr.isRewardBound()) { opDecl["time-bounds"] = propertyInterval; + } else { + opDecl["reward-bounds"] = propertyInterval; } return opDecl; } From 322808db5b938ebdd896a8bb13cbd7fe5e9f10c6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 4 Jul 2017 10:47:44 +0200 Subject: [PATCH 20/28] getting reward name from reward bounded until formula. --- src/storm/logic/TimeBoundType.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 2488baaaf..7200cc89d 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -36,6 +36,11 @@ namespace storm { bool isRewardBound() const { return type == TimeBoundType::Reward; } + + std::string const& getRewardName() const { + assert(isRewardBound()); + return rewardName; + } }; From d0551c1d593a9f4756d75c507c858f8cead9dd76 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 4 Jul 2017 10:48:26 +0200 Subject: [PATCH 21/28] getting time/step/reward bounds as rational number --- src/storm/logic/BoundedUntilFormula.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 66b5a29fa..b954d4720 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -1,5 +1,6 @@ #include "storm/logic/BoundedUntilFormula.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -80,6 +81,22 @@ namespace storm { return bound; } + template <> + storm::RationalNumber BoundedUntilFormula::getLowerBound() const { + checkNoVariablesInBound(this->getLowerBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + storm::RationalNumber BoundedUntilFormula::getUpperBound() const { + checkNoVariablesInBound(this->getUpperBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + template <> uint64_t BoundedUntilFormula::getLowerBound() const { checkNoVariablesInBound(this->getLowerBound()); From 6471bfdcea68e60831008fbd1f806358e4a328c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 4 Jul 2017 11:17:01 +0200 Subject: [PATCH 22/28] made cli output respect filters --- src/storm/cli/cli.cpp | 8 +++++--- src/storm/modelchecker/results/CheckResult.cpp | 18 ++++++++++++++++++ src/storm/modelchecker/results/CheckResult.h | 10 +++------- 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 8fea01e61..10f992d96 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -615,9 +615,11 @@ namespace storm { } template - void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { + void printResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { if (result) { - STORM_PRINT_AND_LOG("Result (initial states): "); + std::stringstream ss; + ss << "'" << *property.getFilter().getStatesFormula() << "'"; + STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): "); printFilteredResult(result, property.getFilter().getFilterType()); if (watch) { STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); @@ -640,8 +642,8 @@ namespace storm { storm::utility::Stopwatch watch(true); std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); watch.stop(); - printInitialStatesResult(result, property, &watch); postprocessingCallback(result); + printResult(result, property, &watch); } } diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index bdcf68c8f..9155057d3 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -113,6 +113,15 @@ namespace storm { return dynamic_cast(*this); } + template + QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { + return static_cast &>(*this); + } + + template + QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { + return static_cast const&>(*this); + } template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult() { @@ -155,6 +164,9 @@ namespace storm { } // Explicitly instantiate the template functions. + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); @@ -184,9 +196,15 @@ namespace storm { #ifdef STORM_HAVE_CARL + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; + template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); + template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; + template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index 2cff249c9..43954a220 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -66,14 +66,10 @@ namespace storm { QualitativeCheckResult const& asQualitativeCheckResult() const; template - QuantitativeCheckResult& asQuantitativeCheckResult() { - return static_cast &>(*this); - } + QuantitativeCheckResult& asQuantitativeCheckResult(); + template - QuantitativeCheckResult const& asQuantitativeCheckResult() const { - return static_cast const&>(*this); - } - + QuantitativeCheckResult const& asQuantitativeCheckResult() const; ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; From 980f1864afed4db4ec9c6a398f156b6c0562f7e8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 16:54:08 +0200 Subject: [PATCH 23/28] test cases --- src/test/storm/parser/FormulaParserTest.cpp | 29 +++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 012555e8b..6269a082c 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -71,6 +71,35 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) { EXPECT_FALSE(formula->asProbabilityOperatorFormula().hasOptimalityType()); } +TEST(FormulaParserTest, UntilOperatorTest) { + // API does not allow direct test of until, so we have to pack it in a probability operator. + storm::parser::FormulaParser formulaParser; + + std::string input = "P<0.9 [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested1 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested1.isUntilFormula()); + EXPECT_FALSE(nested1.isBoundedUntilFormula()); + + input = "P<0.9 [\"a\" U<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested2 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested2.isBoundedUntilFormula()); + EXPECT_TRUE(nested2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(3, nested2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested3 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested3.isBoundedUntilFormula()); + EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); // This will fail, as we have not finished the parser. + //EXPECT_EQ("rewardname", nested3.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_EQ(3, nested3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + // TODO: Extend as soon as it does not crash anymore. +} + + TEST(FormulaParserTest, RewardOperatorTest) { storm::parser::FormulaParser formulaParser; From 9af46452bca1f8e647b3ca36ef79dd8f41e9fc13 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 16:54:26 +0200 Subject: [PATCH 24/28] first attempt for a parser --- src/storm/parser/FormulaParserGrammar.cpp | 10 +++++++--- src/storm/parser/FormulaParserGrammar.h | 8 ++++---- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 95cb3f860..6141cacac 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -77,7 +77,8 @@ namespace storm { conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); - timeBound = (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_1, qi::_2)] | ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; + timeBound = (-rewardModelName >> (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] + | (-rewardModelName >> ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; timeBound.name("time bound"); pathFormula = conditionalFormula(qi::_r1); @@ -212,13 +213,16 @@ namespace storm { return static_cast(manager); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const { + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. + storm::logic::TimeBound lower(false, lowerBound); storm::logic::TimeBound upper(false, upperBound); return std::make_pair(lower, upper); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const { + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { return std::make_pair(boost::none, storm::logic::TimeBound(strict, bound)); } else { diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 79b272246..10c124785 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -198,10 +198,10 @@ namespace storm { void addConstant(std::string const& name, bool integer); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); - std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; - - // Methods that actually create the expression objects. + std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; + std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; + + // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const; std::shared_ptr createTotalRewardFormula() const; From 95831c1058ca5701a7c90b8fa2fb954a84a75f6a Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 4 Jul 2017 20:30:45 +0200 Subject: [PATCH 25/28] make formula grammar compile again --- src/storm/parser/FormulaParserGrammar.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 6141cacac..45f6fc62e 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -77,8 +77,10 @@ namespace storm { conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); - timeBound = (-rewardModelName >> (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] - | (-rewardModelName >> ((qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; + timeBound = ((-rewardModelName >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")) + [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] + | (-rewardModelName >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser) + [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; timeBound.name("time bound"); pathFormula = conditionalFormula(qi::_r1); From 6a46d0abd5f83242c7a105e3ea0994cde135667e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 23:34:46 +0200 Subject: [PATCH 26/28] formula parser extended with reward bounded rewards --- src/storm/parser/FormulaParserGrammar.cpp | 27 +++++++++++++++-------- src/storm/parser/FormulaParserGrammar.h | 12 +++++----- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 45f6fc62e..45fa27c16 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -215,20 +215,20 @@ namespace storm { return static_cast(manager); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { + std::tuple, boost::optional, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { // As soon as it somehow does not break everything anymore, I will change return types here. storm::logic::TimeBound lower(false, lowerBound); storm::logic::TimeBound upper(false, upperBound); - return std::make_pair(lower, upper); + return std::make_tuple(lower, upper, rewardName); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { + std::tuple, boost::optional, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { - return std::make_pair(boost::none, storm::logic::TimeBound(strict, bound)); + return std::make_tuple(boost::none, storm::logic::TimeBound(strict, bound), rewardName); } else { - return std::make_pair(storm::logic::TimeBound(strict, bound), boost::none); + return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, rewardName); } } @@ -261,9 +261,13 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -277,9 +281,14 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } + } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 10c124785..31f766789 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -181,7 +181,7 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional, boost::optional>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; @@ -197,9 +197,9 @@ namespace storm { bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, bool integer); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); - - std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; + + std::tuple, boost::optional, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; + std::tuple, boost::optional, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; @@ -209,10 +209,10 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; From 4a43d7ab0d6f1142aff39fcc66edfb49b2e77f17 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 5 Jul 2017 15:29:09 +0200 Subject: [PATCH 27/28] towards compiling storm with the latest carl version --- .../expressions/ToRationalNumberVisitor.cpp | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 9a82be279..042485104 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -1,6 +1,6 @@ #include "storm/storage/expressions/ToRationalNumberVisitor.h" -#include "storm/utility/macros.h" + #include "storm/utility/constants.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" @@ -128,22 +128,12 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) { - (void)expression; -#ifdef STORM_HAVE_CARL - return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); -#endif + return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); } template boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) { - (void)expression; -#ifdef STORM_HAVE_CARL return expression.getValue(); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); -#endif } template @@ -151,8 +141,8 @@ namespace storm { valueMapping[variable] = value; } -#ifdef STORM_HAVE_CARL + template class ToRationalNumberVisitor; -#endif + } } From c46ce03e6092c765f4653235b08d0526d95f7370 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 5 Jul 2017 18:08:15 +0200 Subject: [PATCH 28/28] make storm compile with latest version of carl --- resources/3rdparty/sylvan/src/storm_wrapper.cpp | 6 +++--- src/storm/storage/expressions/ToRationalNumberVisitor.cpp | 2 +- src/storm/utility/constants.cpp | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index b042227fd..ae9a91bb9 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -201,8 +201,8 @@ storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - - uint64_t exponentAsInteger = carl::toInt(srn_b); + + carl::uint exponentAsInteger = carl::toInt(srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(carl::pow(srn_a, exponentAsInteger)); return (storm_rational_number_ptr)result_srn; } @@ -515,7 +515,7 @@ storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - uint64_t exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); + carl::uint exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); return (storm_rational_function_ptr)result_srf; } diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 042485104..f7aa3236d 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -75,7 +75,7 @@ namespace storm { break; case BinaryNumericalFunctionExpression::OperatorType::Power: STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); - uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); + uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); return result; break; diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 35d79c13f..67ac0a6b8 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -256,7 +256,7 @@ namespace storm { template<> uint_fast64_t convertNumber(ClnRationalNumber const& number) { - return carl::toInt(number); + return carl::toInt(number); } template<> @@ -386,7 +386,7 @@ namespace storm { template<> uint_fast64_t convertNumber(GmpRationalNumber const& number){ - return carl::toInt(number); + return carl::toInt(number); } template<> @@ -549,8 +549,8 @@ namespace storm { #endif template<> - uint_fast64_t convertNumber(RationalFunction const& func) { - return carl::toInt(convertNumber(func)); + carl::uint convertNumber(RationalFunction const& func) { + return carl::toInt(convertNumber(func)); } template<>