From 7e7d6defa0948b221fcfbe6f350ea8b9718c3a88 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 30 Aug 2021 12:41:16 +0200 Subject: [PATCH] Merge pull request #137 from tquatmann/ltl LTL Model Checking Also includes a reset of src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h since there have been to many changes to fix them individually. Will follow up with a commit to introduce shield and smg formula parsing Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.h src/storm/logic/FragmentChecker.cpp src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/logic/ToPrefixStringVisitor.cpp src/storm/logic/ToPrefixStringVisitor.h src/storm/modelchecker/AbstractModelChecker.cpp src/storm/modelchecker/AbstractModelChecker.h src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp src/storm/storage/MaximalEndComponent.cpp src/storm/storage/Scheduler.cpp src/storm/storage/Scheduler.h src/storm/storage/jani/JSONExporter.cpp src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp --- .../parser/FormulaParserGrammar.cpp | 2 -- .../parser/FormulaParserGrammar.h | 4 --- src/storm/logic/Formula.h | 3 ++ src/storm/logic/FragmentSpecification.cpp | 29 +++++++++++++++ src/storm/logic/FragmentSpecification.h | 5 ++- .../LiftableTransitionRewardsVisitor.cpp | 1 - src/storm/logic/ToPrefixStringVisitor.cpp | 4 --- .../prctl/SparseDtmcPrctlModelChecker.cpp | 28 +++++++++++++++ .../prctl/SparseMdpPrctlModelChecker.cpp | 1 + src/storm/storage/Scheduler.cpp | 35 ++++++++++++++++++- src/storm/storage/Scheduler.h | 1 - src/storm/storage/jani/JSONExporter.cpp | 2 +- 12 files changed, 98 insertions(+), 17 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 1d5360a90..aa07a7961 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -176,8 +176,6 @@ namespace storm { formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); - - constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 63ba71f3e..fca3b3a1c 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -10,7 +10,6 @@ #include "storm/storage/jani/Property.h" #include "storm/logic/Formulas.h" #include "storm-parsers/parser/ExpressionParser.h" -#include "storm-parsers/parser/ConstantDataType.h" #include "storm/modelchecker/results/FilterType.h" @@ -243,9 +242,6 @@ namespace storm { storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; - std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); - std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); - bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 29eba01ff..0c83e718c 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -149,6 +149,9 @@ namespace storm { HOAPathFormula& asHOAPathFormula(); HOAPathFormula const& asHOAPathFormula() const; + HOAPathFormula& asHOAPathFormula(); + HOAPathFormula const& asHOAPathFormula() const; + BoundedUntilFormula& asBoundedUntilFormula(); BoundedUntilFormula const& asBoundedUntilFormula() const; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 2272ef61f..b75dca240 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -114,6 +114,35 @@ namespace storm { return rpatl; } + FragmentSpecification prctl() { + FragmentSpecification prctl = pctl(); + + prctl.setRewardOperatorsAllowed(true); + prctl.setCumulativeRewardFormulasAllowed(true); + prctl.setInstantaneousFormulasAllowed(true); + prctl.setReachabilityRewardFormulasAllowed(true); + prctl.setLongRunAverageOperatorsAllowed(true); + prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); + prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); + + return prctl; + } + + FragmentSpecification prctlstar() { + FragmentSpecification prctlstar = pctlstar(); + + prctlstar.setRewardOperatorsAllowed(true); + prctlstar.setCumulativeRewardFormulasAllowed(true); + prctlstar.setInstantaneousFormulasAllowed(true); + prctlstar.setReachabilityRewardFormulasAllowed(true); + prctlstar.setLongRunAverageOperatorsAllowed(true); + prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true); + prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true); + + return prctlstar; + + } + FragmentSpecification csl() { FragmentSpecification csl = pctl(); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 18b8a8686..0bbe0fb17 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -249,6 +249,8 @@ namespace storm { // Flat PCTL. FragmentSpecification flatPctl(); + // rPATL for SMGs + FragmentSpecification rpatl(); // PCTL* FragmentSpecification pctlstar(); @@ -258,9 +260,6 @@ namespace storm { // PCTL* + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctlstar(); - // rPATL for SMGs - FragmentSpecification rpatl(); - // Regular CSL. FragmentSpecification csl(); diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index 7c3b1da97..2ead1325b 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -30,7 +30,6 @@ namespace storm { return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this, data)); } - boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return true; } diff --git a/src/storm/logic/ToPrefixStringVisitor.cpp b/src/storm/logic/ToPrefixStringVisitor.cpp index af6e3f31c..300a53d97 100644 --- a/src/storm/logic/ToPrefixStringVisitor.cpp +++ b/src/storm/logic/ToPrefixStringVisitor.cpp @@ -59,10 +59,6 @@ namespace storm { return result; } - boost::any ToPrefixStringVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); - } - boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 838caf03d..645564aa6 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -141,8 +141,36 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); + + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 6551b61fe..a48995526 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -28,6 +28,7 @@ #include "storm/shields/ShieldHandling.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/storage/expressions/Expressions.h" diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 3d2c5a697..6405528a0 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -224,6 +224,18 @@ namespace storm { continue; } + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; + } else { + out << std::setw(widthOfStates) << ""; + out << " "; + } + // Print the memory state info + if (!isMemorylessScheduler()) { + out << "m="<< memoryState << std::setw(8) << ""; + } + // Print choice info SchedulerChoice const& choice = schedulerChoices[memoryState][state]; if (choice.isDefined()) { @@ -282,7 +294,28 @@ namespace storm { } } - stateString << std::endl; + // Print memory updates + if(!isMemorylessScheduler()) { + out << std::setw(widthOfStates) << ""; + // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state. + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + bool firstUpdate = true; + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + if (firstUpdate) { + firstUpdate = false; + } else { + out << ", "; + } + out << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + } + + } + + } + + out << std::endl; } stateString << stateString.str(); diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 1a8322e81..96819be58 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -139,7 +139,6 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; - /*! * Prints the scheduler in json format to the given output stream. */ diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 5706618c6..bf5895d5e 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -711,7 +711,7 @@ namespace storm { return opDecl; } } - + boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = operatorTypeToJaniString(expression.getOperator());