From 04c2938057398b0c3a0e5bd8ef8864ec47acc204 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 25 Feb 2020 10:24:10 +0100 Subject: [PATCH] Introduced hybrid engine for Markov automata (only reach. rewards for now) --- src/storm/api/verification.h | 25 ++ .../modelchecker/AbstractModelChecker.cpp | 6 + .../HybridMarkovAutomatonCslModelChecker.cpp | 117 +++++++ .../HybridMarkovAutomatonCslModelChecker.h | 40 +++ .../SparseMarkovAutomatonCslModelChecker.cpp | 6 +- .../helper/HybridMarkovAutomatonCslHelper.cpp | 329 ++++++++++++++++++ .../helper/HybridMarkovAutomatonCslHelper.h | 46 +++ .../SymbolicPropositionalModelChecker.cpp | 6 + src/storm/utility/Engine.cpp | 2 + 9 files changed, 574 insertions(+), 3 deletions(-) create mode 100644 src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp create mode 100644 src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h create mode 100644 src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp create mode 100644 src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 3f5b9653c..f5033568c 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -13,6 +13,7 @@ #include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" @@ -20,6 +21,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" @@ -327,6 +329,27 @@ namespace storm { return verifyWithHybridEngine(env, mdp, task); } + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(storm::Environment const& env, std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::HybridMarkovAutomatonCslModelChecker> modelchecker(*ma); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(storm::Environment const& , std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify MDPs with this data type."); + } + + template + std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { + Environment env; + return verifyWithHybridEngine(env, ma, task); + } + template std::unique_ptr verifyWithHybridEngine(storm::Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -336,6 +359,8 @@ namespace storm { result = verifyWithHybridEngine(env, model->template as>(), task); } else if (model->getType() == storm::models::ModelType::Mdp) { result = verifyWithHybridEngine(env, model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { + result = verifyWithHybridEngine(env, model->template as>(), task); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the hybrid engine."); } diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 2c12639c3..233aa1733 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -17,6 +17,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -25,6 +26,7 @@ #include "storm/storage/dd/Bdd.h" #include +#include namespace storm { namespace modelchecker { @@ -360,6 +362,10 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp new file mode 100644 index 000000000..4ef4b4542 --- /dev/null +++ b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.cpp @@ -0,0 +1,117 @@ +#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h" + +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h" + +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/utility/FilteredRewardModel.h" + +#include "storm/logic/FragmentSpecification.h" + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + template + HybridMarkovAutomatonCslModelChecker::HybridMarkovAutomatonCslModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model) { + // Intentionally left empty. + } + + template + bool HybridMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask) { + auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); + if (!storm::NumberTraits::SupportsExponential) { + singleObjectiveFragment.setBoundedUntilFormulasAllowed(false); + } + return checkTask.getFormula().isInFragment(singleObjectiveFragment); + } + + template + bool HybridMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { + return canHandleStatic(checkTask); + } + +/* template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } + */ + template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::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::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } + + /* template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + + storm::models::symbolic::StandardRewardModel timeRewardModel(this->getModel().getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), timeRewardModel, subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } + + template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); + SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); + + STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on MarkovAutomatons are not supported."); + double lowerBound = 0; + double upperBound = 0; + if (pathFormula.hasLowerBound()) { + lowerBound = pathFormula.getLowerBound(); + } + if (pathFormula.hasUpperBound()) { + upperBound = pathFormula.getNonStrictUpperBound(); + } else { + upperBound = storm::utility::infinity(); + } + + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound); + } + + template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, stateFormula); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); + } + + template + std::unique_ptr HybridMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRateVector(), rewardModel.get()); + } + */ + // Explicitly instantiate the model checker. + template class HybridMarkovAutomatonCslModelChecker>; + template class HybridMarkovAutomatonCslModelChecker>; + + template class HybridMarkovAutomatonCslModelChecker>; + + } // namespace modelchecker +} // namespace storm diff --git a/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h new file mode 100644 index 000000000..e7c293b95 --- /dev/null +++ b/src/storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h @@ -0,0 +1,40 @@ +#pragma once + +#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" + +#include "storm/models/symbolic/MarkovAutomaton.h" + +#include "storm/solver/LinearEquationSolver.h" + +#include "storm/utility/NumberTraits.h" + +namespace storm { + + namespace modelchecker { + + template + class HybridMarkovAutomatonCslModelChecker : public SymbolicPropositionalModelChecker { + public: + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + explicit HybridMarkovAutomatonCslModelChecker(ModelType const& model); + + // The implemented methods of the AbstractModelChecker interface. + static bool canHandleStatic(CheckTask const& checkTask); + virtual bool canHandle(CheckTask const& checkTask) const override; + /* virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageRewards(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; + virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + */ virtual std::unique_ptr computeReachabilityRewards(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; + + }; + + } // namespace modelchecker +} // namespace storm diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 29c006c88..8f0b27361 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -29,11 +29,11 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { - auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); + auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true); if (!storm::NumberTraits::SupportsExponential) { - singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); - multiObjectiveFragment.setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); + multiObjectiveFragment.setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); } if (checkTask.getFormula().isInFragment(singleObjectiveFragment)) { return true; diff --git a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp new file mode 100644 index 000000000..d1a2bb761 --- /dev/null +++ b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.cpp @@ -0,0 +1,329 @@ +#include "storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h" + +#include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" + +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" +#include "storm/utility/constants.h" + +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "storm/utility/Stopwatch.h" + +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + void discretizeRewardModel(typename storm::models::symbolic::Model::RewardModelType& rewardModel, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& markovianStates) { + if (rewardModel.hasStateRewards()) { + rewardModel.getStateRewardVector() *= markovianStates.ite(exitRateVector.getDdManager().template getAddOne() / exitRateVector, exitRateVector.getDdManager().template getAddZero()); + } + } + + + template + std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative) { + + auto discretizedRewardModel = rewardModel; + discretizeRewardModel(discretizedRewardModel, exitRateVector, markovianStates); + return HybridMdpPrctlHelper::computeReachabilityRewards(env, dir, model, transitionMatrix, discretizedRewardModel, targetStates, qualitative); + } + + /* + + template + std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative) { + return HybridMdpPrctlHelper::computeUntilProbabilities(env, model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates, psiStates, qualitative); + } + + template::SupportsExponential, int>::type> + std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound) { + + // If the time bounds are [0, inf], we rather call untimed reachability. + if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { + return computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative); + } + + // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0 + // or t' != inf. + + // If we identify the states that have probability 0 of reaching the target states, we can exclude them from the + // further computations. + storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, rateMatrix.notZero(), phiStates, psiStates); + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0."); + storm::dd::Bdd statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 && !psiStates; + STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); + + if (!statesWithProbabilityGreater0NonPsi.isZero()) { + if (storm::utility::isZero(upperBound)) { + // In this case, the interval is of the form [0, 0]. + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); + } else { + if (storm::utility::isZero(lowerBound)) { + // In this case, the interval is of the form [0, t]. + // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. + + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + + storm::utility::Stopwatch conversionWatch(true); + + // Create an ODD for the translation to an explicit representation. + storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd(); + + // Convert the symbolic parts to their explicit representation. + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.toVector(odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + // Finally compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, &explicitB, upperBound, uniformizationRate, values); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), + (psiStates || !statesWithProbabilityGreater0) && model.getReachableStates(), + psiStates.template toAdd(), statesWithProbabilityGreater0NonPsi, odd, subresult)); + } else if (upperBound == storm::utility::infinity()) { + // In this case, the interval is of the form [t, inf] with t != 0. + + // Start by computing the (unbounded) reachability probabilities of reaching psi states while + // staying in phi states. + std::unique_ptr unboundedResult = computeUntilProbabilities(env, model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative); + + // Compute the set of relevant states. + storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; + + // Filter the unbounded result such that it only contains values for the relevant states. + unboundedResult->filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); + + storm::utility::Stopwatch conversionWatch; + + // Build an ODD for the relevant states. + conversionWatch.start(); + storm::dd::Odd odd = relevantStates.createOdd(); + conversionWatch.stop(); + + std::vector result; + if (unboundedResult->isHybridQuantitativeCheckResult()) { + conversionWatch.start(); + std::unique_ptr explicitUnboundedResult = unboundedResult->asHybridQuantitativeCheckResult().toExplicitQuantitativeCheckResult(); + conversionWatch.stop(); + result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult().getValueVector()); + } else { + STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type."); + result = unboundedResult->asSymbolicQuantitativeCheckResult().getValueVector().toVector(odd); + } + + // Determine the uniformization rate for the transient probability computation. + ValueType uniformizationRate = 1.02 * (relevantStates.template toAdd() * exitRateVector).getMax(); + + // Compute the uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + conversionWatch.start(); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + // Compute the transient probabilities. + result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, result)); + } else { + // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. + + if (lowerBound != upperBound) { + // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'. + + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0NonPsi.template toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the (first) uniformized matrix. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + + // Create the one-step vector. + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.template toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + + // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. + storm::utility::Stopwatch conversionWatch(true); + storm::dd::Odd odd = statesWithProbabilityGreater0NonPsi.createOdd(); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + std::vector explicitB = b.toVector(odd); + conversionWatch.stop(); + + // Compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero()); + std::vector subResult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, &explicitB, upperBound - lowerBound, uniformizationRate, values); + + // Transform the explicit result to a hybrid check result, so we can easily convert it to + // a symbolic qualitative format. + HybridQuantitativeCheckResult hybridResult(model.getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && model.getReachableStates()), + psiStates.template toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult); + + // Compute the set of relevant states. + storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; + + // Filter the unbounded result such that it only contains values for the relevant states. + hybridResult.filter(SymbolicQualitativeCheckResult(model.getReachableStates(), relevantStates)); + + // Build an ODD for the relevant states. + conversionWatch.start(); + odd = relevantStates.createOdd(); + + std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); + conversionWatch.stop(); + std::vector newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().getValueVector()); + + // Then compute the transient probabilities of being in such a state after t time units. For this, + // we must re-uniformize the MarkovAutomaton, so we need to compute the second uniformized matrix. + uniformizationRate = 1.02 * (relevantStates.template toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // If the lower and upper bounds coincide, we have only determined the relevant states at this + // point, but we still need to construct the starting vector. + if (lowerBound == upperBound) { + odd = relevantStates.createOdd(); + newSubresult = psiStates.template toAdd().toVector(odd); + } + + // Finally, we compute the second set of transient probabilities. + uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + conversionWatch.start(); + explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + newSubresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !relevantStates && model.getReachableStates(), model.getManager().template getAddZero(), relevantStates, odd, newSubresult)); + } else { + // In this case, the interval is of the form [t, t] with t != 0, t != inf. + + storm::utility::Stopwatch conversionWatch; + + // Build an ODD for the relevant states. + conversionWatch.start(); + storm::dd::Odd odd = statesWithProbabilityGreater0.createOdd(); + + std::vector newSubresult = psiStates.template toAdd().toVector(odd); + conversionWatch.stop(); + + // Then compute the transient probabilities of being in such a state after t time units. For this, + // we must re-uniformize the MarkovAutomaton, so we need to compute the second uniformized matrix. + ValueType uniformizationRate = 1.02 * (statesWithProbabilityGreater0.template toAdd() * exitRateVector).getMax(); + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Finally, we compute the second set of transient probabilities. + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); + conversionWatch.start(); + storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + newSubresult = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTransientProbabilities(env, explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates(), model.getManager().template getAddZero(), statesWithProbabilityGreater0, odd, newSubresult)); + } + } + } + } else { + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); + } + } + + template::SupportsExponential, int>::type> + std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + + template + std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates) { + + storm::utility::Stopwatch conversionWatch(true); + + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + + storm::storage::SparseMatrix explicitRateMatrix = rateMatrix.toMatrix(odd, odd); + std::vector explicitExitRateVector = exitRateVector.toVector(odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(env, storm::solver::SolveGoal(), explicitRateMatrix, psiStates.toVector(odd), &explicitExitRateVector); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + + template + std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel) { + + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + storm::utility::Stopwatch conversionWatch(true); + + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + + storm::storage::SparseMatrix explicitRateMatrix = rateMatrix.toMatrix(odd, odd); + std::vector explicitExitRateVector = exitRateVector.toVector(odd); + conversionWatch.stop(); + STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms."); + + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(), explicitRateMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + */ + + // Explicit instantiations. + + // Cudd, double. + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + /* + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); +*/ + // Sylvan, double. + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); +*/ + // Sylvan, rational number. + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + /* template std::unique_ptr HybridMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + template std::unique_ptr HybridMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); +*/ + + } + } +} diff --git a/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h new file mode 100644 index 000000000..30f04956e --- /dev/null +++ b/src/storm/modelchecker/csl/helper/HybridMarkovAutomatonCslHelper.h @@ -0,0 +1,46 @@ +#pragma once + +#include + +#include "storm/models/symbolic/MarkovAutomaton.h" + +#include "storm/modelchecker/results/CheckResult.h" + +#include "storm/utility/NumberTraits.h" +#include "storm/solver/OptimizationDirection.h" + +namespace storm { + + class Environment; + + namespace modelchecker { + namespace helper { + + class HybridMarkovAutomatonCslHelper { + public: + template + static std::unique_ptr computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative); + + /* + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound); + + template + static std::unique_ptr computeUntilProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative); + + template + static std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates); + + template + static std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::MarkovAutomaton const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel); + */ + + }; + + } + } +} + diff --git a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index c66f5fbea..1185002f7 100644 --- a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -1,3 +1,4 @@ +#include #include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" #include "storm/storage/dd/Add.h" @@ -6,6 +7,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -62,21 +64,25 @@ namespace storm { template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; } diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index f025f6b9c..780417870 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -10,6 +10,7 @@ #include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" #include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" @@ -128,6 +129,7 @@ namespace storm { case ModelType::CTMC: return storm::modelchecker::HybridCtmcCslModelChecker>::canHandleStatic(checkTask); case ModelType::MA: + return storm::modelchecker::HybridMarkovAutomatonCslModelChecker>::canHandleStatic(checkTask); case ModelType::POMDP: return false; }