From b30713c23d82fdf5bba2a9fe3fa7c83156b9f5fe Mon Sep 17 00:00:00 2001 From: hannah Date: Sat, 15 May 2021 22:42:31 +0200 Subject: [PATCH] Started to restructure LTL model checking algorithms Conflicts: src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp --- .../helper/SingleValueModelCheckerHelper.cpp | 10 + .../helper/SingleValueModelCheckerHelper.h | 11 + .../helper/ltl/SparseLTLHelper.cpp | 192 ++++++++++++++++++ .../modelchecker/helper/ltl/SparseLTLHelper.h | 52 +++++ .../utility/SetInformationFromCheckTask.h | 7 + .../prctl/SparseDtmcPrctlModelChecker.cpp | 28 +-- .../prctl/SparseMdpPrctlModelChecker.cpp | 21 +- .../prctl/SparseMdpPrctlModelChecker.h | 2 +- 8 files changed, 291 insertions(+), 32 deletions(-) create mode 100644 src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp create mode 100644 src/storm/modelchecker/helper/ltl/SparseLTLHelper.h diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp index 796b696f8..885411b01 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp @@ -82,6 +82,16 @@ namespace storm { bool SingleValueModelCheckerHelper::isProduceSchedulerSet() const { return _produceScheduler; } + + template + void SingleValueModelCheckerHelper::setQualitative(bool value) { + _isQualitativeSet = value; + } + + template + bool SingleValueModelCheckerHelper::isQualitativeSet() const { + return _isQualitativeSet; + } template class SingleValueModelCheckerHelper; template class SingleValueModelCheckerHelper; diff --git a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h index 2246ef793..f328d5a7f 100644 --- a/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h +++ b/src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h @@ -100,11 +100,22 @@ namespace storm { * @return whether an optimal scheduler shall be constructed during the computation */ bool isProduceSchedulerSet() const; + + /*! + * Sets whether the property needs to be checked qualitatively + */ + void setQualitative(bool value); + + /*! + * @return whether the property needs to be checked qualitatively + */ + bool isQualitativeSet() const; private: boost::optional _optimizationDirection; boost::optional> _valueThreshold; bool _produceScheduler; + bool _isQualitativeSet; }; } } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp new file mode 100644 index 000000000..7dd5e1367 --- /dev/null +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -0,0 +1,192 @@ +#include "SparseLTLHelper.h" + +#include "storm/transformer/DAProductBuilder.h" +#include "storm/automata/LTL2DeterministicAutomaton.h" + +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" + +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" + +#include "storm/storage/StronglyConnectedComponentDecomposition.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseLTLHelper::SparseLTLHelper(Model const& model, storm::storage::SparseMatrix const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix) { + // Intentionally left empty. + } + + template + std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { + STORM_LOG_THROW((!Nondeterministic) || goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); + + + const storm::automata::APSet& apSet = da.getAPSet(); + + std::vector apLabels; + for (const std::string& ap : apSet.getAPs()) { + auto it = apSatSets.find(ap); + STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula"); + + apLabels.push_back(std::move(it->second)); + } + + storm::storage::BitVector statesOfInterest; + if (goal.hasRelevantValues()) { + statesOfInterest = goal.relevantValues(); + } else { + // product from all model states + statesOfInterest = storm::storage::BitVector(this->_model.getNumberOfStates(), true); + } + + + STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); + storm::transformer::DAProductBuilder productBuilder(da, apLabels); + + auto product = productBuilder.build(this->_model, statesOfInterest); + + STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC")) +" has " << product->getProductModel().getNumberOfStates() << " states and " + << product->getProductModel().getNumberOfTransitions() << " transitions."); + + if (storm::settings::getModule().isTraceSet()) { + STORM_LOG_TRACE("Writing model to model.dot"); + std::ofstream modelDot("model.dot"); + this->_model.writeDotToStream(modelDot); + modelDot.close(); + + STORM_LOG_TRACE("Writing product model to product.dot"); + std::ofstream productDot("product.dot"); + product->getProductModel().writeDotToStream(productDot); + productDot.close(); + + STORM_LOG_TRACE("Product model mapping:"); + std::stringstream str; + product->printMapping(str); + STORM_LOG_TRACE(str.str()); + } + + + // DTMC: BCC + // MDP: computeSurelyAcceptingPmaxStates + storm::storage::BitVector accepting; + if (Nondeterministic) { + STORM_LOG_INFO("Computing accepting end components..."); + accepting = storm::modelchecker::helper::SparseMdpPrctlHelper::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); + if (accepting.empty()) { + STORM_LOG_INFO("No accepting states, skipping probability computation."); + std::vector numericResult(this->_model.getNumberOfStates(), storm::utility::zero()); + return numericResult; + } + + } else { + STORM_LOG_INFO("Computing BSCCs and checking for acceptance..."); + + storm::storage::StronglyConnectedComponentDecomposition bottomSccs(product->getProductModel().getTransitionMatrix(), + storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs()); + accepting = storm::storage::BitVector(product->getProductModel().getNumberOfStates()); + std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0; + for (auto& scc : bottomSccs) { + checkedBSCCs++; + if (product->getAcceptance()->isAccepting(scc)) { + acceptingBSCCs++; + for (auto& state : scc) { + accepting.set(state); + acceptingBSCCStates++; + } + } + } + + STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were accepting (" << acceptingBSCCStates << " states in accepting BSCCs)."); + + if (acceptingBSCCs == 0) { + STORM_LOG_INFO("No accepting BSCCs, skipping probability computation."); + std::vector numericResult(this->_model.getNumberOfStates(), storm::utility::zero()); + return numericResult; + } + } + + STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs..."); + + storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); + + storm::solver::SolveGoal solveGoalProduct(goal); + storm::storage::BitVector soiProduct(product->getStatesOfInterest()); + solveGoalProduct.setRelevantValues(std::move(soiProduct)); + + std::vector prodNumericResult; + + if (Nondeterministic) { + prodNumericResult + = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + accepting, + qualitative, + false // no schedulers (at the moment) + ).values); + + } else { + prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + accepting, + qualitative); + } + + std::vector numericResult = product->projectToOriginalModel(this->_model, prodNumericResult); + return numericResult; + } + + + template + std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { + 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."); + + + std::vector numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet()); + + /* + if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { + // compute 1-Pmax[!ltl] + for (auto& value : numericResult) { + value = storm::utility::one() - value; + } + } + */ + + return numericResult; + } + + template class SparseLTLHelper, false>; + template class SparseLTLHelper, true>; + +#ifdef STORM_HAVE_CARL + template class SparseLTLHelper, false>; + template class SparseLTLHelper, true>; + template class SparseLTLHelper, false>; + +#endif + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h new file mode 100644 index 000000000..6240fe1b0 --- /dev/null +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -0,0 +1,52 @@ +#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/solver/SolveGoal.h" + + +namespace storm { + + namespace automata { + // fwd + class DeterministicAutomaton; + } + + namespace modelchecker { + namespace helper { + + /*! + * Helper class for todo... + * @tparam ValueType the type a value can have + * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP) + */ + template // todo remove Model + class SparseLTLHelper: public SingleValueModelCheckerHelper { + + public: + /*! + * Initializes the helper for a discrete time (i.e. DTMC, MDP) + */ + SparseLTLHelper(Model const& model, storm::storage::SparseMatrix const& transitionMatrix); + + + /*! + * todo + * @return + */ + std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); + + + /*! + * Computes the ltl probabilities ...todo + * @return a value for each state + */ + std::vector computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& f, std::map& apSatSets); //todo was brauchen wir hier aps und ..? + + + private: + storm::storage::SparseMatrix const& _transitionMatrix; + Model const& _model; // todo remove ? + + }; + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h index 49b46db26..df1df7362 100644 --- a/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h +++ b/src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h @@ -25,6 +25,9 @@ namespace storm { } // Scheduler Production helper.setProduceScheduler(checkTask.isProduceSchedulersSet()); + + // Qualitative flag + helper.setQualitative(checkTask.isQualitativeSet()); } /*! @@ -40,6 +43,10 @@ namespace storm { if (checkTask.isBoundSet()) { helper.setValueThreshold(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } + + // Qualitative flag + helper.setQualitative(checkTask.isQualitativeSet()); + } } } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index ccb5d1a83..64c2eaa05 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -15,6 +15,7 @@ #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" @@ -161,7 +162,7 @@ namespace storm { STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); std::map apSets; - + // todo instead: std::map apSets = storm::modelchecker::helper::computeApSets(env, checkTask); for (auto& p : extracted) { STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); @@ -174,20 +175,12 @@ namespace storm { 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()); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc, dtmc.getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); + std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), *ltlFormula, apSets); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -256,14 +249,13 @@ 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(); + std::unique_ptr subResultPointer = this->check(env, stateFormula); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); + auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 31b3a5c1d..dbf044910 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -23,6 +23,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h" +#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" @@ -189,7 +190,6 @@ namespace storm { 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 << "..."); @@ -216,31 +216,25 @@ namespace storm { subTask = checkTask.substituteFormula(*ltlFormula); } - 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 SparseMdpModelType& mdp = this->getModel(); storm::solver::SolveGoal goal(mdp, subTask); - std::vector numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + storm::modelchecker::helper::SparseLTLHelper helper(mdp, mdp.getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp); + std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), subTask), *ltlFormula, apSets); - if (minimize) { + if(minimize) { // compute 1-Pmax[!ltl] for (auto& value : numericResult) { value = storm::utility::one() - value; } } + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + /* template std::vector::ValueType> SparseMdpPrctlModelChecker::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal::ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const { STORM_LOG_THROW(goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); @@ -318,6 +312,7 @@ namespace storm { std::vector numericResult = product->projectToOriginalModel(this->getModel(), prodNumericResult); return numericResult; } + */ template diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 73e706596..2a09694c5 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -46,7 +46,7 @@ namespace storm { virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; private: - std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const; + //std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const; }; } // namespace modelchecker } // namespace storm