From 1243b9300c6c2b20905c95a89954d1e555160bc5 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 27 Aug 2020 06:25:25 +0200 Subject: [PATCH] (LTL) SparseDtmcModelChecker: Implement LTL model checking Conflicts: src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h --- .../prctl/SparseDtmcPrctlModelChecker.cpp | 131 ++++++++++++++---- .../prctl/SparseDtmcPrctlModelChecker.h | 15 +- 2 files changed, 112 insertions(+), 34 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 30858ae3a..859de2fb2 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -18,10 +18,17 @@ #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" + +#include "storm/automata/AcceptanceCondition.h" +#include "storm/automata/DeterministicAutomaton.h" +#include "storm/automata/LTL2DeterministicAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/DebugSettings.h" #include "storm/exceptions/InvalidStateException.h" @@ -33,11 +40,11 @@ namespace storm { SparseDtmcPrctlModelChecker::SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } - + template bool SparseDtmcPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { + if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true).setHOAPathFormulasAllowed(true))) { return true; } else if (checkTask.isOnlyInitialStatesRelevantSet() && formula.isInFragment(storm::logic::quantiles())) { if (requiresSingleInitialState) { @@ -47,7 +54,7 @@ namespace storm { } return false; } - + template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { bool requiresSingleInitialState = false; @@ -57,7 +64,7 @@ namespace storm { return false; } } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); @@ -84,7 +91,7 @@ namespace storm { return result; } } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); @@ -93,7 +100,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities(env, this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); @@ -104,7 +111,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); @@ -113,7 +120,77 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); 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_LOG_INFO("Obtaining HOA automaton..."); + storm::automata::DeterministicAutomaton::ptr da = pathFormula.readAutomaton(); + const storm::automata::APSet& apSet = da->getAPSet(); + + STORM_LOG_INFO("Deterministic automaton from HOA file has " + << da->getNumberOfStates() << " states, " + << da->getAPSet().size() << " atomic propositions and " + << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); + + std::map apSets; + for (std::string const& ap : apSet.getAPs()) { + std::shared_ptr expression = pathFormula.getAPMapping().at(ap); + STORM_LOG_INFO("Computing satisfaction set for atomic proposition \"" << ap << "\" <=> " << *expression << "..."); + std::unique_ptr resultPointer = this->check(*expression); + ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); + storm::storage::BitVector bitVector = result.getTruthValuesVector(); + STORM_LOG_INFO("Atomic proposition \"" << ap << "\" is satisfied by " << bitVector.getNumberOfSetBits() << " states."); + apSets[ap] = std::move(bitVector); + } + + const SparseDtmcModelType& dtmc = this->getModel(); + storm::solver::SolveGoal goal(dtmc, checkTask); + + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + 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(); + + std::vector extracted; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); + + STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); + + std::map apSets; + + for (auto& p : extracted) { + STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + + std::unique_ptr subResultPointer = this->check(env, *p.second); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto sat = subResult.getTruthValuesVector(); + + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + + apSets[p.first] = std::move(sat); + } + + STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula); + STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); + + std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula); + + STORM_LOG_INFO("Deterministic automaton for LTL formula has " + << da->getNumberOfStates() << " states, " + << da->getAPSet().size() << " atomic propositions and " + << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); + + const SparseDtmcModelType& dtmc = this->getModel(); + storm::solver::SolveGoal goal(dtmc, checkTask); + + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + 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(); @@ -134,7 +211,7 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); @@ -142,7 +219,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -152,7 +229,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -161,7 +238,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityTimes(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); @@ -171,18 +248,18 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { - + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); - + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); @@ -191,7 +268,7 @@ namespace storm { auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); @@ -206,28 +283,28 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); - + std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - - + + template<> std::unique_ptr SparseDtmcPrctlModelChecker>::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Quantiles for parametric models are not implemented."); } - + template std::unique_ptr SparseDtmcPrctlModelChecker::checkQuantileFormula(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for the initial states of a model."); @@ -236,19 +313,19 @@ namespace storm { helper::rewardbounded::QuantileHelper qHelper(this->getModel(), checkTask.getFormula()); auto res = qHelper.computeQuantile(env); - + if (res.size() == 1 && res.front().size() == 1) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, std::move(res.front().front()))); } else { return std::unique_ptr(new ExplicitParetoCurveCheckResult(initialState, std::move(res))); } } - + template std::unique_ptr SparseDtmcPrctlModelChecker::computeSteadyStateDistribution(Environment const& env) { // Initialize helper storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); - + // Compute result std::vector result; auto const& initialStates = this->getModel().getInitialStates(); @@ -265,7 +342,7 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - + template class SparseDtmcPrctlModelChecker>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 93ae8dbfb..572ecc57e 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -9,21 +9,21 @@ namespace storm { namespace modelchecker { - + template class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker { public: typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; - + explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model); - + /*! * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state */ static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); - + // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; @@ -32,6 +32,7 @@ namespace storm { virtual std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; @@ -41,15 +42,15 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; - + /*! * Computes the long run average (or: steady state) distribution over all states * Assumes a uniform distribution over initial states. */ std::unique_ptr computeSteadyStateDistribution(Environment const& env); - + }; - + } // namespace modelchecker } // namespace storm