diff --git a/.gitignore b/.gitignore index bd4e15887..88a8bf3d9 100644 --- a/.gitignore +++ b/.gitignore @@ -46,3 +46,7 @@ build//CMakeLists.txt *.*~ # CMake generated/configured files src/utility/storm-version.cpp +.DS_Store +.idea +*.out + diff --git a/examples/mdp/csma/csma3_4.nm b/examples/mdp/csma/csma3_4.nm index c1b97fc3f..8739053e5 100644 --- a/examples/mdp/csma/csma3_4.nm +++ b/examples/mdp/csma/csma3_4.nm @@ -129,4 +129,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4; label "one_delivered" = s1=4|s2=4|s3=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3); diff --git a/examples/mdp/csma/csma4_4.nm b/examples/mdp/csma/csma4_4.nm index 90f182dde..e1ba511f4 100644 --- a/examples/mdp/csma/csma4_4.nm +++ b/examples/mdp/csma/csma4_4.nm @@ -134,4 +134,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1); +formula min_collisions = min(cd1,cd2,cd3,cd4); +formula max_collisions = max(cd1,cd2,cd3,cd4); diff --git a/examples/mdp/csma/csma4_6.nm b/examples/mdp/csma/csma4_6.nm index 8e9fb110a..12e5f0152 100644 --- a/examples/mdp/csma/csma4_6.nm +++ b/examples/mdp/csma/csma4_6.nm @@ -136,4 +136,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1); +formula min_collisions = min(cd1,cd2,cd3,cd4); +formula max_collisions = max(cd1,cd2,cd3,cd4); diff --git a/examples/pdtmc/tiny/tiny.pm b/examples/pdtmc/tiny/tiny.pm new file mode 100644 index 000000000..e644a10fc --- /dev/null +++ b/examples/pdtmc/tiny/tiny.pm @@ -0,0 +1,16 @@ +dtmc + +module tiny + s : [0 .. 3] init 0; + + [] s = 0 -> 1/3 : (s'=1) + 1/3 : (s'=2) + 1/3 : (s'=3); + [] s = 1 -> 1 : (s'=2); + [] s = 2 -> 1/2 : (s'=2) + 1/2 : (s'=1); + [] s = 3 -> 1 : (s'=3); + +endmodule + +rewards + s=1 : 10; + s=3 : 5; +endrewards diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 0ffbdf4ba..96b6298d0 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -1025,9 +1025,6 @@ namespace storm { for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) { stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation); } - for (auto const& el : stateInformation.get().valuations) { - std::cout << "state: " << el << std::endl; - } } return modelComponents; diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 36b6df27e..54643d32a 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -231,7 +231,7 @@ namespace storm { } } - + if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL if (settings.isParametricSet()) { diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 1c24bc091..93f9e1777 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -108,14 +108,14 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> modelProgramPair = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(modelProgramPair.first != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); + STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(modelProgramPair.first, modelProgramPair.first, ValueType, LibraryType, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); // Print some information about the model. - modelProgramPair.first->printModelInformationToStream(std::cout); + modelProgramPair.model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. if (!formulas.empty()) { @@ -124,7 +124,7 @@ namespace storm { // Start by building a mapping from constants of the (translated) model to their defining expressions. std::map constantSubstitution; - for (auto const& constant : modelProgramPair.second.getConstants()) { + for (auto const& constant : modelProgramPair.program.getConstants()) { if (constant.isDefined()) { constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); } @@ -135,20 +135,20 @@ namespace storm { preparedFormulas.emplace_back(formula->substitute(constantSubstitution)); } - if (modelProgramPair.first->isSparseModel()) { + if (modelProgramPair.model->isSparseModel()) { if(storm::settings::generalSettings().isCounterexampleSet()) { // If we were requested to generate a counterexample, we now do so for each formula. for(auto const& formula : preparedFormulas) { - generateCounterexample(program, modelProgramPair.first->as>(), formula); + generateCounterexample(program, modelProgramPair.model->as>(), formula); } } else { - verifySparseModel(modelProgramPair.first->as>(), preparedFormulas); + verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); } - } else if (modelProgramPair.first->isSymbolicModel()) { + } else if (modelProgramPair.model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(modelProgramPair.first->as>(), preparedFormulas); + verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as>(), preparedFormulas); + verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 8f96b19cd..babf9edfc 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -103,6 +103,10 @@ namespace storm { return false; } + bool Formula::isLongRunAverageRewardFormula() const { + return false; + } + bool Formula::isProbabilityOperatorFormula() const { return false; } @@ -351,6 +355,14 @@ namespace storm { return dynamic_cast(*this); } + LongRunAverageRewardFormula& Formula::asLongRunAverageRewardFormula() { + return dynamic_cast(*this); + } + + LongRunAverageRewardFormula const& Formula::asLongRunAverageRewardFormula() const { + return dynamic_cast(*this); + } + ProbabilityOperatorFormula& Formula::asProbabilityOperatorFormula() { return dynamic_cast(*this); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 98b1ac349..1a6933703 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -35,6 +35,7 @@ namespace storm { class CumulativeRewardFormula; class InstantaneousRewardFormula; class ReachabilityRewardFormula; + class LongRunAverageRewardFormula; class ProbabilityOperatorFormula; class RewardOperatorFormula; @@ -76,6 +77,7 @@ namespace storm { virtual bool isCumulativeRewardFormula() const; virtual bool isInstantaneousRewardFormula() const; virtual bool isReachabilityRewardFormula() const; + virtual bool isLongRunAverageRewardFormula() const; virtual bool isProbabilityOperatorFormula() const; virtual bool isRewardOperatorFormula() const; @@ -163,6 +165,9 @@ namespace storm { ReachabilityRewardFormula& asReachabilityRewardFormula(); ReachabilityRewardFormula const& asReachabilityRewardFormula() const; + + LongRunAverageRewardFormula& asLongRunAverageRewardFormula(); + LongRunAverageRewardFormula const& asLongRunAverageRewardFormula() const; ProbabilityOperatorFormula& asProbabilityOperatorFormula(); ProbabilityOperatorFormula const& asProbabilityOperatorFormula() const; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 6d2f61880..faf4ca164 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -15,6 +15,7 @@ #include "src/logic/RewardPathFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/ReachabilityRewardFormula.h" +#include "src/logic/LongRunAverageRewardFormula.h" #include "src/logic/RewardOperatorFormula.h" #include "src/logic/StateFormula.h" #include "src/logic/LongRunAverageOperatorFormula.h" diff --git a/src/logic/LongRunAverageRewardFormula.cpp b/src/logic/LongRunAverageRewardFormula.cpp new file mode 100644 index 000000000..896e94a31 --- /dev/null +++ b/src/logic/LongRunAverageRewardFormula.cpp @@ -0,0 +1,21 @@ +#include "src/logic/LongRunAverageRewardFormula.h" + +namespace storm { + namespace logic { + LongRunAverageRewardFormula::LongRunAverageRewardFormula() { + // Intentionally left empty. + } + + bool LongRunAverageRewardFormula::isLongRunAverageRewardFormula() const { + return true; + } + + std::shared_ptr LongRunAverageRewardFormula::substitute(std::map const& substitution) const { + return std::shared_ptr(new LongRunAverageRewardFormula()); + } + + std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out) const { + return out << "LRA"; + } + } +} \ No newline at end of file diff --git a/src/logic/LongRunAverageRewardFormula.h b/src/logic/LongRunAverageRewardFormula.h new file mode 100644 index 000000000..449d5fd0e --- /dev/null +++ b/src/logic/LongRunAverageRewardFormula.h @@ -0,0 +1,29 @@ +#ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ +#define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ + +#include + +#include "src/logic/RewardPathFormula.h" + + +namespace storm { + namespace logic { + class LongRunAverageRewardFormula : public RewardPathFormula { + public: + LongRunAverageRewardFormula(); + + virtual ~LongRunAverageRewardFormula() { + // Intentionally left empty. + } + + virtual bool isLongRunAverageRewardFormula() const override; + + virtual std::shared_ptr substitute(std::map const& substitution) const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + }; + } +} + +#endif /* STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ */ \ No newline at end of file diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index e0a4f127b..2b840d83c 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -72,6 +72,8 @@ namespace storm { return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), rewardModelName, qualitative, optimalityType); } else if (rewardPathFormula.isReachabilityRewardFormula()) { return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), rewardModelName, qualitative, optimalityType); + } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { + return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), rewardModelName, qualitative, optimalityType); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } @@ -88,7 +90,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); } - std::unique_ptr AbstractModelChecker::computeLongRunAverage(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); + } + + std::unique_ptr AbstractModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages."); } @@ -255,15 +261,15 @@ namespace storm { std::unique_ptr result; if (stateFormula.hasOptimalityType()) { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); + result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); } else if (stateFormula.hasBound()) { if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Maximize); + result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Maximize); } else { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Minimize); + result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Minimize); } } else { - result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false); + result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false); } if (stateFormula.hasBound()) { diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 4c1347ea3..5fca10010 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -47,9 +47,10 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); // The methods to compute the long-run average and expected time. - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); // The methods to check state formulas. diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 21591a9e4..42c9466d1 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -88,11 +88,11 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverage(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); } // Explicitly instantiate the model checker. diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index cfdd5326b..ed4125c7e 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -24,7 +24,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Ctmc const& getModel() const override; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 14631fba5..3648f8bb4 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -94,12 +94,12 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 8423cac53..78e2fd91f 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -27,7 +27,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e9069a040..b93643d62 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -68,13 +68,13 @@ namespace storm { } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverage(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 1062dd0ec..a3d0fc1fb 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -24,7 +24,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index f68444152..e59523866 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -276,7 +276,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeLongRunAverage(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); // Create ODD for the translation. @@ -285,7 +285,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h index 90b40ad01..ca7d7aa35 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -28,7 +28,7 @@ namespace storm { static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeLongRunAverage(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 453496ce2..564b635bc 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -427,7 +427,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeLongRunAverage(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); if (psiStates.empty()) { diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index fae4d8498..fb4f7e74f 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -26,7 +26,7 @@ namespace storm { template static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverage(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 67a20c543..4c9e1643e 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -194,7 +194,7 @@ namespace storm { return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory); } template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // If there are no goal states, we avoid the computation and directly return zero. diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 73534fb6a..5b24fe569 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -22,7 +22,7 @@ namespace storm { static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeExpectedTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 4d4eb6e3d..6614bf8e7 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -47,6 +47,13 @@ namespace storm { return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } + template + std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + } + template std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); @@ -89,7 +96,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -98,7 +105,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverage(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), qualitative, *this->linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), qualitative, *this->linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 7fc7b40c5..5d68a8785 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -21,10 +21,11 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index d83541c94..f7b44adcb 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -29,7 +29,16 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isGloballyFormula()) { + return true; + } + return false; } template @@ -42,6 +51,14 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } + template + std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + } + template std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 3a1fbc64b..4cd1d6e27 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -28,6 +28,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index d268754f5..5103fc3a0 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -33,7 +33,22 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isGloballyFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isConditionalPathFormula()) { + storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); + if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { + return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); + } + } + return false; } template @@ -66,6 +81,14 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); @@ -89,13 +112,27 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverage(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative , boost::optional const& optimalityType) { + STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template class SparseDtmcPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index f6ec4b0e4..384130263 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -23,10 +23,12 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 3340d31f4..eabe827f3 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -38,7 +38,22 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isGloballyFormula()) { + return true; + } + if (formula.isConditionalPathFormula()) { + storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); + if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { + return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); + } + } + return false; } template @@ -72,6 +87,30 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); + } + + template + std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); + STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(optimalityType.get(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + } + template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType, boost::optional> const& bound) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); @@ -118,11 +157,11 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverage(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 14f4462d2..d36bdcec1 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -36,11 +36,13 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional(), boost::optional> const& bound =boost::optional>()); virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index b69c443a5..920102389 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -31,7 +31,16 @@ namespace storm { template bool SymbolicDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isGloballyFormula()) { + return true; + } + return false; } template @@ -44,6 +53,14 @@ namespace storm { return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } + template + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + } + template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 54c5c00b5..8c8d4140d 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -18,6 +18,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 7924cfada..296236f07 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -31,7 +31,16 @@ namespace storm { template bool SymbolicMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { - return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); + if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { + return true; + } + if (formula.isProbabilityOperatorFormula()) { + return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + } + if (formula.isGloballyFormula()) { + return true; + } + return false; } template @@ -44,6 +53,14 @@ namespace storm { return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); } + template + std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + } + template std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index 605ef089a..e5160faa8 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -20,6 +20,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 6ca927aac..869242db4 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -24,7 +24,7 @@ namespace storm { namespace helper { template - std::unique_ptr HybridDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); @@ -50,7 +50,7 @@ namespace storm { // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all // maybe states. @@ -83,13 +83,20 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { - storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); + std::unique_ptr HybridDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + result->asQuantitativeCheckResult().oneMinus(); + return result; + } + + template + std::unique_ptr HybridDtmcPrctlHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { + storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); } template - std::unique_ptr HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound); @@ -105,12 +112,12 @@ namespace storm { // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all // maybe states. - storm::dd::Add prob1StatesAsColumn = psiStates.template toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); - storm::dd::Add subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); + storm::dd::Add prob1StatesAsColumn = psiStates.template toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -134,7 +141,7 @@ namespace storm { template - std::unique_ptr HybridDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -156,12 +163,12 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Compute the reward vector to add in each step based on the available reward models. - storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables()); + storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables()); // Create the ODD for the translation between symbolic and explicit storage. storm::dd::Odd odd = model.getReachableStates().createOdd(); @@ -182,7 +189,7 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -207,14 +214,14 @@ namespace storm { storm::dd::Odd odd = maybeStates.createOdd(); // Create the matrix and the vector for the equation system. - storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting // non-maybe states in the matrix. - storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; + storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; // Then compute the state reward vector to use in the computation. - storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); + storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed // for solving the equation system (i.e. compute (I-A)). diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h index eaffd782b..9cbfa83d3 100644 --- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h @@ -18,19 +18,21 @@ namespace storm { template class HybridDtmcPrctlHelper { public: - typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; + typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index c980e6dcc..b7b7bf385 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -85,6 +85,13 @@ namespace storm { } } } + + template + std::unique_ptr HybridMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + result->asQuantitativeCheckResult().oneMinus(); + return result; + } template std::unique_ptr HybridMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h index 32658e7ac..54287cca5 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h @@ -27,6 +27,8 @@ namespace storm { static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index e7b218c48..b1401cd8a 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -6,9 +6,10 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" - #include "src/solver/LinearEquationSolver.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" @@ -103,6 +104,15 @@ namespace storm { return result; } + template + std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector result = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative, linearEquationSolverFactory); + for (auto& entry : result) { + entry = storm::utility::one() - entry; + } + return result; + } + template std::vector SparseDtmcPrctlHelper::computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Create the vector with which to multiply and initialize it correctly. @@ -214,8 +224,115 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverage(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverage(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); + } + + template + std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory); + + // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined. + storm::storage::BitVector beforeStates(targetStates.size(), true); + uint_fast64_t state = 0; + uint_fast64_t beforeStateIndex = 0; + for (auto const& value : probabilitiesToReachConditionStates) { + if (value == storm::utility::zero()) { + beforeStates.set(state, false); + } else { + probabilitiesToReachConditionStates[beforeStateIndex] = value; + ++beforeStateIndex; + } + ++state; + } + probabilitiesToReachConditionStates.resize(beforeStateIndex); + + // If there were any before states, we can compute their conditional probabilities. If not, the result + // is undefined for all states. + std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + if (targetStates.empty()) { + storm::utility::vector::setVectorValues(result, beforeStates, storm::utility::zero()); + } else if (!beforeStates.empty()) { + // If there are some states for which the conditional probability is defined and there are some + // states that can reach the target states without visiting condition states first, we need to + // do more work. + + // First, compute the relevant states and some offsets. + storm::storage::BitVector allStates(targetStates.size(), true); + std::vector numberOfBeforeStatesUpToState = beforeStates.getNumberOfSetBitsBeforeIndices(); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates); + statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates); + uint_fast64_t normalStatesOffset = beforeStates.getNumberOfSetBits(); + std::vector numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices(); + + // All transitions going to states with probability zero, need to be redirected to a deadlock state. + bool addDeadlockState = false; + uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits(); + + // Now, we create the matrix of 'before' and 'normal' states. + storm::storage::SparseMatrixBuilder builder; + + // Start by creating the transitions of the 'before' states. + uint_fast64_t currentRow = 0; + for (auto beforeState : beforeStates) { + if (conditionStates.get(beforeState)) { + // For condition states, we move to the 'normal' states. + ValueType zeroProbability = storm::utility::zero(); + for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { + if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) { + builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue()); + } else { + zeroProbability += successorEntry.getValue(); + } + } + if (!storm::utility::isZero(zeroProbability)) { + builder.addNextValue(currentRow, deadlockState, zeroProbability); + } + } else { + // For non-condition states, we scale the probabilities going to other before states. + for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { + if (beforeStates.get(successorEntry.getColumn())) { + builder.addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()], successorEntry.getValue() * probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] / probabilitiesToReachConditionStates[currentRow]); + } + } + } + ++currentRow; + } + + // Then, create the transitions of the 'normal' states. + for (auto state : statesWithProbabilityGreater0) { + ValueType zeroProbability = storm::utility::zero(); + for (auto const& successorEntry : transitionMatrix.getRow(state)) { + if (statesWithProbabilityGreater0.get(successorEntry.getColumn())) { + builder.addNextValue(currentRow, normalStatesOffset + numberOfNormalStatesUpToState[successorEntry.getColumn()], successorEntry.getValue()); + } else { + zeroProbability += successorEntry.getValue(); + } + } + if (!storm::utility::isZero(zeroProbability)) { + addDeadlockState = true; + builder.addNextValue(currentRow, deadlockState, zeroProbability); + } + ++currentRow; + } + if (addDeadlockState) { + builder.addNextValue(deadlockState, deadlockState, storm::utility::one()); + } + + // Build the new transition matrix and the new targets. + storm::storage::SparseMatrix newTransitionMatrix = builder.build(); + storm::storage::BitVector newTargetStates = targetStates % beforeStates; + newTargetStates.resize(newTransitionMatrix.getRowCount()); + for (auto state : targetStates % statesWithProbabilityGreater0) { + newTargetStates.set(normalStatesOffset + state, true); + } + + // Finally, compute the conditional probabiltities by a reachability query. + std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), newTargetStates, qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, beforeStates, conditionalProbabilities); + } + + return result; } template class SparseDtmcPrctlHelper; diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index d698ae29f..d1414dbce 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -12,6 +12,8 @@ namespace storm { namespace modelchecker { + class CheckResult; + namespace helper { template > @@ -23,6 +25,8 @@ namespace storm { static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -31,7 +35,9 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverage(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); private: static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 5eb52f1fc..2f4d9389d 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + #include "src/models/sparse/StandardRewardModel.h" #include "src/storage/MaximalEndComponentDecomposition.h" @@ -23,7 +25,7 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. storm::storage::BitVector maybeStates; @@ -60,7 +62,7 @@ namespace storm { std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Create the vector with which to multiply and initialize it correctly. - std::vector result(transitionMatrix.getRowCount()); + std::vector result(transitionMatrix.getRowGroupCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); @@ -73,8 +75,6 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); - // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; @@ -91,7 +91,7 @@ namespace storm { LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(numberOfStates); + std::vector result(transitionMatrix.getRowGroupCount()); // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); @@ -136,6 +136,27 @@ namespace storm { return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, getPolicy, minMaxLinearEquationSolverFactory)); } + template + std::vector SparseMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique) { + + if (useMecBasedTechnique) { + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, psiStates); + storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount()); + for (auto const& mec : mecDecomposition) { + for (auto const& stateActionsPair : mec) { + statesInPsiMecs.set(stateActionsPair.first, true); + } + } + + return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).result); + } else { + std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result; + for (auto& element : result) { + element = storm::utility::one() - element; + } + return std::move(result); + } + } template template @@ -168,7 +189,7 @@ namespace storm { if (rewardModel.hasStateRewards()) { result = rewardModel.getStateRewardVector(); } else { - result.resize(transitionMatrix.getRowCount()); + result.resize(transitionMatrix.getRowGroupCount()); } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); @@ -216,7 +237,7 @@ namespace storm { // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; - storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); + storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates); } else { @@ -229,7 +250,7 @@ namespace storm { LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Check whether we need to compute exact rewards for some states. if (qualitative) { @@ -282,7 +303,7 @@ namespace storm { } template - std::vector SparseMdpPrctlHelper::computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); if (psiStates.empty()) { @@ -475,6 +496,109 @@ namespace storm { return solver->getContinuousValue(lambda); } + template + std::unique_ptr SparseMdpPrctlHelper::computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + // For the max-case, we can simply take the given target states. For the min-case, however, we need to + // find the MECs of non-target states and make them the new target states. + storm::storage::BitVector fixedTargetStates; + if (dir == OptimizationDirection::Maximize) { + fixedTargetStates = targetStates; + } else { + fixedTargetStates = storm::storage::BitVector(targetStates.size()); + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, ~targetStates); + for (auto const& mec : mecDecomposition) { + for (auto const& stateActionsPair : mec) { + fixedTargetStates.set(stateActionsPair.first); + } + } + } + + // We solve the max-case and later adjust the result if the optimization direction was to minimize. + storm::storage::BitVector initialStatesBitVector(transitionMatrix.getRowGroupCount()); + initialStatesBitVector.set(initialState); + + storm::storage::BitVector allStates(initialStatesBitVector.size(), true); + std::vector conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).result); + + // If the conditional probability is undefined for the initial state, we return directly. + if (storm::utility::isZero(conditionProbabilities[initialState])) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::infinity())); + } + + std::vector targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).result); + + storm::storage::BitVector statesWithProbabilityGreater0E(transitionMatrix.getRowGroupCount(), true); + storm::storage::sparse::state_type state = 0; + for (auto const& element : conditionProbabilities) { + if (storm::utility::isZero(element)) { + statesWithProbabilityGreater0E.set(state, false); + } + ++state; + } + + // Determine those states that need to be equipped with a restart mechanism. + storm::storage::BitVector problematicStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, conditionStates | fixedTargetStates); + + // Otherwise, we build the transformed MDP. + storm::storage::BitVector relevantStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStatesBitVector, allStates, conditionStates | fixedTargetStates); + std::vector numberOfStatesBeforeRelevantStates = relevantStates.getNumberOfSetBitsBeforeIndices(); + storm::storage::sparse::state_type newGoalState = relevantStates.getNumberOfSetBits(); + storm::storage::sparse::state_type newStopState = newGoalState + 1; + storm::storage::sparse::state_type newFailState = newStopState + 1; + + // Build the transitions of the (relevant) states of the original model. + storm::storage::SparseMatrixBuilder builder(0, newFailState + 1, 0, true, true); + uint_fast64_t currentRow = 0; + for (auto state : relevantStates) { + builder.newRowGroup(currentRow); + if (fixedTargetStates.get(state)) { + builder.addNextValue(currentRow, newGoalState, conditionProbabilities[state]); + if (!storm::utility::isZero(conditionProbabilities[state])) { + builder.addNextValue(currentRow, newFailState, 1 - conditionProbabilities[state]); + } + ++currentRow; + } else if (conditionStates.get(state)) { + builder.addNextValue(currentRow, newGoalState, targetProbabilities[state]); + if (!storm::utility::isZero(targetProbabilities[state])) { + builder.addNextValue(currentRow, newStopState, 1 - targetProbabilities[state]); + } + ++currentRow; + } else { + for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state + 1]; ++row) { + for (auto const& successorEntry : transitionMatrix.getRow(row)) { + builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[successorEntry.getColumn()], successorEntry.getValue()); + } + ++currentRow; + } + if (problematicStates.get(state)) { + builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one()); + ++currentRow; + } + } + } + + // Now build the transitions of the newly introduced states. + builder.newRowGroup(currentRow); + builder.addNextValue(currentRow, newGoalState, storm::utility::one()); + ++currentRow; + builder.newRowGroup(currentRow); + builder.addNextValue(currentRow, newStopState, storm::utility::one()); + ++currentRow; + builder.newRowGroup(currentRow); + builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one()); + ++currentRow; + + // Finally, build the matrix and dispatch the query as a reachability query. + storm::storage::BitVector newGoalStates(newFailState + 1); + newGoalStates.set(newGoalState); + storm::storage::SparseMatrix newTransitionMatrix = builder.build(); + storm::storage::SparseMatrix newBackwardTransitions = newTransitionMatrix.transpose(true); + std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).result); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, dir == OptimizationDirection::Maximize ? goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]] : storm::utility::one() - goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]])); + } + template class SparseMdpPrctlHelper; template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 9d6764c05..706f61403 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -25,6 +25,8 @@ namespace storm { } namespace modelchecker { + class CheckResult; + namespace helper { template @@ -38,6 +40,8 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); + template static std::vector computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -51,8 +55,10 @@ namespace storm { static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); #endif - static std::vector computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::unique_ptr computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + private: static std::vector computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 605a5d2e4..06581d841 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -67,6 +67,13 @@ namespace storm { } } + template + storm::dd::Add SymbolicDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + result = result.getDdManager().template getAddOne() - result; + return result; + } + template storm::dd::Add SymbolicDtmcPrctlHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h index ef0ba9097..498454520 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h @@ -23,6 +23,8 @@ namespace storm { static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); static storm::dd::Add computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 8a51270e9..17705fdbb 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -75,6 +75,13 @@ namespace storm { } } + template + std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr result = computeUntilProbabilities(!minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + result->asQuantitativeCheckResult().oneMinus(); + return result; + } + template std::unique_ptr SymbolicMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h index 838327664..25b01d449 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h @@ -26,6 +26,8 @@ namespace storm { static std::unique_ptr computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index aefc6f023..6ec1e6d86 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include +#include #include #include "src/adapters/CarlAdapter.h" @@ -21,14 +22,60 @@ #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" - +#include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { + template + uint_fast64_t estimateComplexity(ValueType const& value) { + return 1; + } + +#ifdef STORM_HAVE_CARL + template<> + uint_fast64_t estimateComplexity(storm::RationalFunction const& value) { + if (storm::utility::isConstant(value)) { + return 1; + } + if (value.denominator().isConstant()) { + return value.nominator().complexity(); + } else { + return value.denominator().complexity() * value.nominator().complexity(); + } + } +#endif + + bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; + } + + bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed; + } + + bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed; + } + + bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::DynamicPenalty || + order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression; + } + + bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) { + return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty; + } + template - SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { + SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly) : SparsePropositionalModelChecker(model), computeResultsForInitialStatesOnly(computeResultsForInitialStatesOnly) { // Intentionally left empty. } @@ -52,68 +99,479 @@ namespace storm { return true; } } + } else if (formula.isBoundedUntilFormula()) { + storm::logic::BoundedUntilFormula const& boundedUntilFormula = formula.asBoundedUntilFormula(); + if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) { + return true; + } } else if (formula.isReachabilityRewardFormula()) { - storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); + storm::logic::ReachabilityRewardFormula const& reachabilityRewardFormula = formula.asReachabilityRewardFormula(); if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { return true; } } else if (formula.isConditionalPathFormula()) { - storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula(); + storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); } - } else if (formula.isPropositionalFormula()) { + } else if (formula.isLongRunAverageOperatorFormula()) { + storm::logic::LongRunAverageOperatorFormula const& longRunAverageOperatorFormula = formula.asLongRunAverageOperatorFormula(); + if (longRunAverageOperatorFormula.getSubformula().isPropositionalFormula()) { + return true; + } + } else if (formula.isLongRunAverageRewardFormula()) { + return true; + } + + else if (formula.isPropositionalFormula()) { return true; } return false; } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(stateFormula); + storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + if (psiStates.empty()) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::vector(numberOfStates, storm::utility::zero()))); + } + if (psiStates.full()) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::vector(numberOfStates, storm::utility::one()))); + } + + storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); + STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + + storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), psiStates); + + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + STORM_LOG_DEBUG("The long-run probability for all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } + if (maybeStates.empty()) { + STORM_LOG_DEBUG("The long-run probability for all states was found in a preprocessing step."); + furtherComputationNeeded = false; + } + + if (furtherComputationNeeded) { + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + std::vector stateValues(maybeStates.size(), storm::utility::zero()); + storm::utility::vector::setVectorValues(stateValues, psiStates, storm::utility::one()); + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateValues); + } + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial states only, we need to filter the result to only + // communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); + } + return checkResult; + } + + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + // Do some sanity checks to establish some required properties. + RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); + + storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); + STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + + storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + + // Get the state-reward values from the reward model. + std::vector stateRewardValues = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix()); + + storm::storage::BitVector maybeStates(stateRewardValues.size()); + uint_fast64_t index = 0; + for (auto const& value : stateRewardValues) { + if (value != storm::utility::zero()) { + maybeStates.set(index, true); + } + ++index; + } + + storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); + + storm::storage::BitVector allStates(numberOfStates, true); + maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, maybeStates); + + std::vector result(numberOfStates, storm::utility::zero()); + + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + furtherComputationNeeded = false; + } + + if (furtherComputationNeeded) { + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateRewardValues); + } + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial states only, we need to filter the result to only + // communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); + } + return checkResult; + } + + template + std::vector::ValueType> SparseDtmcEliminationModelChecker::computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector& stateValues) { + + std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); + + // Start by decomposing the DTMC into its BSCCs. + std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now(); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); + auto sccDecompositionEnd = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); + + // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. + FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); + flexibleMatrix.filter(maybeStates, maybeStates); + FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); + flexibleBackwardTransitions.filter(maybeStates, maybeStates); + auto conversionEnd = std::chrono::high_resolution_clock::now(); + + std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); + + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); + boost::optional> distanceBasedPriorities; + if (eliminationOrderNeedsDistances(order)) { + distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, stateValues, + eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); + } + + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + storm::storage::BitVector regularStatesInBsccs(numberOfStates); + storm::storage::BitVector relevantBsccs(bsccDecomposition.size()); + storm::storage::BitVector bsccRepresentativesAsBitVector(numberOfStates); + std::vector bsccRepresentatives; + uint_fast64_t currentIndex = 0; + for (auto const& bscc : bsccDecomposition) { + // Since all states in an SCC can reach all other states, we only need to check whether an arbitrary + // state is a maybe state. + if (maybeStates.get(*bscc.cbegin())) { + relevantBsccs.set(currentIndex); + bsccRepresentatives.push_back(*bscc.cbegin()); + bsccRepresentativesAsBitVector.set(*bscc.cbegin(), true); + for (auto const& state : bscc) { + regularStatesInBsccs.set(state, true); + } + } + ++currentIndex; + } + regularStatesInBsccs &= ~bsccRepresentativesAsBitVector; + + // Compute the average time to stay in each state for all states in BSCCs. + std::vector averageTimeInStates(stateValues.size(), storm::utility::one()); + + // First, we eliminate all states in BSCCs (except for the representative states). + { + std::unique_ptr priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); + + ValueUpdateCallback valueUpdateCallback = [&stateValues,&averageTimeInStates] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { + stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]); + averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]); + }; + + PredecessorUpdateCallback predecessorCallback = [&stateValues,&averageTimeInStates] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { + stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state])); + averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); + }; + + boost::optional priorityUpdateCallback = PriorityUpdateCallback([&flexibleMatrix,&flexibleBackwardTransitions,&stateValues,&priorityQueue] (storm::storage::sparse::state_type const& state) { + priorityQueue->update(state, flexibleMatrix, flexibleBackwardTransitions, stateValues); + }); + + boost::optional predecessorFilterCallback = boost::none; + + while (priorityQueue->hasNextState()) { + storm::storage::sparse::state_type state = priorityQueue->popNextState(); + eliminateState(state, flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorCallback, priorityUpdateCallback, predecessorFilterCallback, true); + STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); + } + } + + // Now, we set the values of all states in BSCCs to that of the representative value (and clear the + // transitions of the representative states while doing so). + auto representativeIt = bsccRepresentatives.begin(); + for (auto sccIndex : relevantBsccs) { + // We only need to set the values for all states of the BSCC if we are not computing the values for the + // initial states only. + ValueType bsccValue = stateValues[*representativeIt] / averageTimeInStates[*representativeIt]; + auto const& bscc = bsccDecomposition[sccIndex]; + if (!computeResultsForInitialStatesOnly) { + for (auto const& state : bscc) { + stateValues[state] = bsccValue; + } + } else { + for (auto const& state : bscc) { + stateValues[state] = storm::utility::zero(); + } + stateValues[*representativeIt] = bsccValue; + } + + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); + representativeForwardRow.clear(); + representativeForwardRow.shrink_to_fit(); + + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& representativeBackwardRow = flexibleBackwardTransitions.getRow(*representativeIt); + auto it = representativeBackwardRow.begin(), ite = representativeBackwardRow.end(); + for (; it != ite; ++it) { + if (it->getColumn() == *representativeIt) { + break; + } + } + representativeBackwardRow.erase(it); + + ++representativeIt; + } + + // If there are states remaining that are not in BSCCs, we need to eliminate them now. + storm::storage::BitVector remainingStates = maybeStates & ~regularStatesInBsccs; + + // Set the value initial value of all states not in a BSCC to zero, because a) any previous value would + // incorrectly influence the result and b) the value have been erroneously changed for the predecessors of + // BSCCs by the previous state elimination. + for (auto state : remainingStates) { + if (!bsccRepresentativesAsBitVector.get(state)) { + stateValues[state] = storm::utility::zero(); + } + } + + // We only need to eliminate the remaining states if there was some BSCC that has a non-zero value, i.e. + // that consists of maybe states. + if (!relevantBsccs.empty()) { + performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, remainingStates, initialStates, computeResultsForInitialStatesOnly, stateValues, distanceBasedPriorities); + } + + std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::chrono::high_resolution_clock::duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart; + std::chrono::milliseconds sccDecompositionTimeInMilliseconds = std::chrono::duration_cast(sccDecompositionTime); + std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; + std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast(conversionTime); + std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; + std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast(modelCheckingTime); + std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; + std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); + + STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); + STORM_PRINT_AND_LOG(" * time for SCC decomposition: " << sccDecompositionTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); + } + + // Now, we return the value for the only initial state. + STORM_LOG_DEBUG("Simplifying and returning result."); + for (auto& value : stateValues) { + value = storm::utility::simplify(value); + } + return stateValues; + } + + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + // Start by determining the states that have a non-zero probability of reaching the target states within the + // time bound. + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getDiscreteTimeBound()); + statesWithProbabilityGreater0 &= ~psiStates; + + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } else if (statesWithProbabilityGreater0.empty()) { + STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); + furtherComputationNeeded = false; + } + + storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); + storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); + + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + + if (furtherComputationNeeded) { + uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); + + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, phiStates, psiStates, true, timeBound); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + statesWithProbabilityGreater0 &= reachableStates; + } + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true); + + std::vector distancesFromInitialStates; + storm::storage::BitVector relevantStates; + if (computeResultsForInitialStatesOnly) { + // Determine the set of initial states of the sub-model. + storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0; + + // Precompute the distances of the relevant states to the initial states. + distancesFromInitialStates = storm::utility::graph::getDistances(submatrix, subInitialStates, statesWithProbabilityGreater0); + + // Set all states to be relevant for later use. + relevantStates = storm::storage::BitVector(statesWithProbabilityGreater0.getNumberOfSetBits(), true); + } + + // Create the vector of one-step probabilities to go to target states. + std::vector b = transitionMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0, psiStates); + + // Create the vector with which to multiply. + std::vector subresult(b); + std::vector tmp(subresult.size()); + + // Subtract one from the time bound because initializing the sub-result to b already accounts for one step. + --timeBound; + + // Perform matrix-vector multiplications until the time-bound is met. + for (uint_fast64_t timeStep = 0; timeStep < timeBound; ++timeStep) { + submatrix.multiplyWithVector(subresult, tmp); + storm::utility::vector::addVectors(tmp, b, subresult); + + // If we are computing the results for the initial states only, we can use the minimal distance from + // each state to the initial states to determine whether we still need to consider the values for + // these states. If not, we can null-out all their probabilities. + if (computeResultsForInitialStatesOnly) { + for (auto state : relevantStates) { + if (distancesFromInitialStates[state] > (timeBound - timeStep)) { + for (auto& element : submatrix.getRow(state)) { + element.setValue(storm::utility::zero()); + } + b[state] = storm::utility::zero(); + relevantStates.set(state, false); + } + } + } + } + + // Set the values of the resulting vector accordingly. + storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); + } + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the + // result to only communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates)); + } + return checkResult; + } + + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + // Retrieve the appropriate bitvectors by model checking the subformulas. + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - - // If the initial state is known to have either probability 0 or 1, we can directly return the result. - if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { - STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, statesWithProbability0.get(*this->getModel().getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one())); + + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { + STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } else if (maybeStates.empty()) { + STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); + furtherComputationNeeded = false; } - // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); - - // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). - maybeStates &= reachableStates; - - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); - - // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - - // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - - // Before starting the model checking process, we assign priorities to states so we can use them to - // impose ordering constraints later. - std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); - - boost::optional> missingStateRewards; - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities))); + std::vector result(maybeStates.size()); + if (furtherComputationNeeded) { + // If we compute the results for the initial states only, we can cut off all maybe state that are not + // reachable from them. + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + + // Determine the set of initial states of the sub-model. + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); + storm::utility::vector::setVectorValues(result, maybeStates, subresult); + } + + // Construct full result. + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the + // result to only communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + } + return checkResult; } template @@ -126,8 +584,6 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); // Then, compute the subset of states that has a reachability reward less than infinity. storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); @@ -135,41 +591,57 @@ namespace storm { infinityStates.complement(); storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; - // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result. - if (infinityStates.get(initialState)) { - STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); - // This is a work around, because not all (e.g. storm::RationalFunction) data types can represent an - // infinity value. - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::infinity())); + // Determine whether we need to perform some further computation. + bool furtherComputationNeeded = true; + if (computeResultsForInitialStatesOnly) { + if (this->getModel().getInitialStates().isSubsetOf(infinityStates)) { + STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } + if (this->getModel().getInitialStates().isSubsetOf(psiStates)) { + STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); + furtherComputationNeeded = false; + } } - if (psiStates.get(initialState)) { - STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::zero())); + + std::vector result(maybeStates.size()); + if (furtherComputationNeeded) { + // If we compute the results for the initial states only, we can cut off all maybe state that are not + // reachable from them. + if (computeResultsForInitialStatesOnly) { + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + } + + // Determine the set of initial states of the sub-model. + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + // Project the state reward vector to all maybe-states. + std::vector stateRewardValues = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); + + std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); + storm::utility::vector::setVectorValues(result, maybeStates, subresult); } - // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); - - // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). - maybeStates &= reachableStates; - - // Create a vector for the probabilities to go to a state with probability 1 in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); - - // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - - // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - - // Before starting the model checking process, we assign priorities to states so we can use them to - // impose ordering constraints later. - std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); - - // Project the state reward vector to all maybe-states. - boost::optional> optionalStateRewards = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, optionalStateRewards, statePriorities))); + // Construct full result. + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::zero()); + + // Construct check result based on whether we have computed values for all states or just the initial states. + std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); + if (computeResultsForInitialStatesOnly) { + // If we computed the results for the initial (and inf) states only, we need to filter the result to + // only communicate these results. + checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); + } + return checkResult; } template @@ -189,6 +661,7 @@ namespace storm { // Do some sanity checks to establish some required properties. // STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states."); storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); @@ -229,7 +702,7 @@ namespace storm { // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << this->getModel().getInitialStates() << ")"); - + // Create a dummy vector for the one-step probabilities. std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); @@ -257,29 +730,37 @@ namespace storm { // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. - std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); - - std::vector states(statesToEliminate.begin(), statesToEliminate.end()); - - // Sort the states according to the priorities. - std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities[a] < statePriorities[b]; }); + boost::optional> distanceBasedPriorities; + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); + if (eliminationOrderNeedsDistances(order)) { + distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities, + eliminationOrderNeedsForwardDistances(order), + eliminationOrderNeedsReversedDistances(order)); + } - STORM_LOG_INFO("Computing conditional probilities." << std::endl); - STORM_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); - boost::optional> missingStateRewards; std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); + + std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); + + STORM_LOG_INFO("Computing conditional probilities." << std::endl); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); - for (auto const& state : states) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards); - } - STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl); + uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); + STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); + performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); + STORM_LOG_INFO("Eliminated " << numberOfStatesToEliminate << " states." << std::endl); + + // Prepare some callbacks for the elimination procedure. + ValueUpdateCallback valueUpdateCallback = [&oneStepProbabilities] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]); }; + PredecessorUpdateCallback predecessorUpdateCallback = [&oneStepProbabilities] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state])); }; + boost::optional phiFilterCallback = PredecessorFilterCallback([&phiStates] (storm::storage::sparse::state_type const& state) { return phiStates.get(state); }); + boost::optional psiFilterCallback = PredecessorFilterCallback([&psiStates] (storm::storage::sparse::state_type const& state) { return psiStates.get(state); }); // Eliminate the transitions going into the initial state (if there are any). if (!flexibleBackwardTransitions.getRow(*newInitialStates.begin()).empty()) { - eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false); + eliminateState(*newInitialStates.begin(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, boost::none, false); } // Now we need to basically eliminate all chains of not-psi states after phi states and chains of not-phi @@ -314,7 +795,7 @@ namespace storm { // Eliminate the successor only if there possibly is a psi state reachable through it. if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated."); - eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, phiStates); + eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, phiFilterCallback, false); hasNonPsiSuccessor = true; } } @@ -325,7 +806,7 @@ namespace storm { } else { STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state."); STORM_LOG_TRACE("Is a psi state."); - + // At this point, we know that the state satisfies psi and not phi. // This means, we must compute the probability to reach phi states, which in turn means that we need // to eliminate all chains of non-phi states between the current state and phi states. @@ -343,7 +824,7 @@ namespace storm { typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn()); if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) { STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated."); - eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, psiStates); + eliminateState(element.getColumn(), flexibleMatrix, flexibleBackwardTransitions, valueUpdateCallback, predecessorUpdateCallback, boost::none, psiFilterCallback, false); hasNonPhiSuccessor = true; } } @@ -409,79 +890,133 @@ namespace storm { } template - typename SparseDtmcEliminationModelChecker::ValueType SparseDtmcEliminationModelChecker::computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards, boost::optional> const& statePriorities) { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); + std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { - // Create a bit vector that represents the subsystem of states we still have to eliminate. - storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + STORM_LOG_TRACE("Creating state priority queue for states " << states); + + // Get the settings to customize the priority queue. + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); + + std::vector sortedStates(states.begin(), states.end()); + + if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { + std::random_device randomDevice; + std::mt19937 generator(randomDevice()); + std::shuffle(sortedStates.begin(), sortedStates.end(), generator); + return std::make_unique(sortedStates); + } else { + if (eliminationOrderNeedsDistances(order)) { + STORM_LOG_THROW(static_cast(distanceBasedStatePriorities), storm::exceptions::InvalidStateException, "Unable to build state priority queue without distance-based priorities."); + std::sort(sortedStates.begin(), sortedStates.end(), [&distanceBasedStatePriorities] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distanceBasedStatePriorities.get()[state1] < distanceBasedStatePriorities.get()[state2]; } ); + return std::make_unique(sortedStates); + } else if (eliminationOrderIsPenaltyBased(order)) { + std::vector> statePenalties(sortedStates.size()); + PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; + for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { + statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities)); + } + + std::sort(statePenalties.begin(), statePenalties.end(), [] (std::pair const& statePenalty1, std::pair const& statePenalty2) { return statePenalty1.second < statePenalty2.second; } ); + + if (eliminationOrderIsStatic(order)) { + // For the static penalty version, we need to strip the penalties to create the queue. + for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { + sortedStates[index] = statePenalties[index].first; + } + return std::make_unique(sortedStates); + } else { + // For the dynamic penalty version, we need to give the full state-penalty pairs. + return std::make_unique(statePenalties, penaltyFunction); + } + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Illlegal elimination order selected."); + } + + template + std::unique_ptr::StatePriorityQueue> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { + std::vector sortedStates(states.begin(), states.end()); + return std::unique_ptr(new StaticStatePriorityQueue(sortedStates)); + } + + template + void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::unique_ptr& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { + + ValueUpdateCallback valueUpdateCallback = [&values] (storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { values[state] = storm::utility::simplify(loopProbability * values[state]); }; + PredecessorUpdateCallback predecessorCallback = [&values] (storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { values[predecessor] = storm::utility::simplify(values[predecessor] + storm::utility::simplify(probability * values[state])); }; + boost::optional priorityUpdateCallback = PriorityUpdateCallback([&transitionMatrix,&backwardTransitions,&values,&priorityQueue] (storm::storage::sparse::state_type const& state) { priorityQueue->update(state, transitionMatrix, backwardTransitions, values); }); + boost::optional predecessorFilterCallback = boost::none; + + while (priorityQueue->hasNextState()) { + storm::storage::sparse::state_type state = priorityQueue->popNextState(); + bool removeForwardTransitions = computeResultsForInitialStatesOnly && !initialStates.get(state); + eliminateState(state, transitionMatrix, backwardTransitions, valueUpdateCallback, predecessorCallback, priorityUpdateCallback, predecessorFilterCallback, removeForwardTransitions); + if (removeForwardTransitions) { + values[state] = storm::utility::zero(); + } + STORM_LOG_ASSERT(checkConsistent(transitionMatrix, backwardTransitions), "The forward and backward transition matrices became inconsistent."); + } + } + + template + void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); + + std::size_t numberOfStatesToEliminate = statePriorities->size(); + STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); + performPrioritizedStateElimination(statePriorities, transitionMatrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); + STORM_LOG_DEBUG("Eliminated " << numberOfStatesToEliminate << " states." << std::endl); + } + + template + uint_fast64_t SparseDtmcEliminationModelChecker::performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { + // When using the hybrid technique, we recursively treat the SCCs up to some size. + std::vector entryStateQueue; + STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); + uint_fast64_t maximalDepth = treatScc(transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); + + // If the entry states were to be eliminated last, we need to do so now. + if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { + STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); + std::vector sortedStates(entryStateQueue.begin(), entryStateQueue.end()); + std::unique_ptr queuePriorities = std::unique_ptr(new StaticStatePriorityQueue(sortedStates)); + performPrioritizedStateElimination(queuePriorities, transitionMatrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); + } + STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); + return maximalDepth; + } + + template + std::vector::ValueType> SparseDtmcEliminationModelChecker::computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget) { + std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); - FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true); + FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions); auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); + + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder(); + boost::optional> distanceBasedPriorities; + if (eliminationOrderNeedsDistances(order)) { + distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, oneStepProbabilitiesToTarget, + eliminationOrderNeedsForwardDistances(order), eliminationOrderNeedsReversedDistances(order)); + } + + // Create a bit vector that represents the subsystem of states we still have to eliminate. + storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + uint_fast64_t maximalDepth = 0; if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { - // If we are required to do pure state elimination, we simply create a vector of all states to - // eliminate and sort it according to the given priorities. - - // Remove the initial state from the states which we need to eliminate. - subsystem &= ~initialStates; - std::vector states(subsystem.begin(), subsystem.end()); - - if (statePriorities) { - std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); - } - - STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); - for (auto const& state : states) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); - } - STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl); + performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { - // When using the hybrid technique, we recursively treat the SCCs up to some size. - std::vector entryStateQueue; - STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); - maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, stateRewards, statePriorities); - - // If the entry states were to be eliminated last, we need to do so now. - STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { - for (auto const& state : entryStateQueue) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); - } - } - STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); + maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); } - - // Finally eliminate initial state. - if (!stateRewards) { - // If we are computing probabilities, then we can simply call the state elimination procedure. It - // will scale the transition row of the initial state with 1/(1-loopProbability). - STORM_LOG_INFO("Eliminating initial state " << *initialStates.begin() << "." << std::endl); - eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards); - } else { - // If we are computing rewards, we cannot call the state elimination procedure for technical reasons. - // Instead, we need to get rid of a potential loop in this state explicitly. - - // Start by finding the self-loop element. Since it can only be the only remaining outgoing transition - // of the initial state, this amounts to checking whether the outgoing transitions of the initial - // state are non-empty. - if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) { - STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more."); - STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); - ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); - loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); - STORM_LOG_DEBUG("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability); - stateRewards.get()[(*initialStates.begin())] *= loopProbability; - flexibleMatrix.getRow(*initialStates.begin()).clear(); - } - } - - // Make sure that we have eliminated all transitions from the initial state. - STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); + + STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated."); + STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated."); std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); @@ -507,63 +1042,17 @@ namespace storm { STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); } } - + // Now, we return the value for the only initial state. STORM_LOG_DEBUG("Simplifying and returning result."); - if (stateRewards) { - return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); - } else { - return oneStepProbabilities[*initialStates.begin()]; - } - } - - template - std::vector SparseDtmcEliminationModelChecker::getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities) { - std::vector statePriorities(transitionMatrix.getRowCount()); - std::vector states(transitionMatrix.getRowCount()); - for (std::size_t index = 0; index < states.size(); ++index) { - states[index] = index; + for (auto& value : values) { + value = storm::utility::simplify(value); } - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { - std::random_shuffle(states.begin(), states.end()); - } else { - std::vector distances; - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed) { - distances = storm::utility::graph::getDistances(transitionMatrix, initialStates); - } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed) { - // Since the target states were eliminated from the matrix already, we construct a replacement by - // treating all states that have some non-zero probability to go to a target state in one step. - storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount()); - for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { - if (oneStepProbabilities[index] != storm::utility::zero()) { - pseudoTargetStates.set(index); - } - } - - distances = storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates); - } else { - STORM_LOG_ASSERT(false, "Illegal sorting order selected."); - } - - // In case of the forward or backward ordering, we can sort the states according to the distances. - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward) { - std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } ); - } else { - // Otherwise, we sort them according to descending distances. - std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } ); - } - } - - // Now convert the ordering of the states to priorities. - for (std::size_t index = 0; index < states.size(); ++index) { - statePriorities[states[index]] = index; - } - - return statePriorities; + return values; } template - uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, boost::optional>& stateRewards, boost::optional> const& statePriorities) { + uint_fast64_t SparseDtmcEliminationModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -579,27 +1068,21 @@ namespace storm { storm::storage::BitVector remainingSccs(decomposition.size(), true); // First, get rid of the trivial SCCs. - std::vector> trivialSccs; + storm::storage::BitVector statesInTrivialSccs(matrix.getNumberOfRows()); for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); if (scc.isTrivial()) { - storm::storage::sparse::state_type onlyState = *scc.begin(); - trivialSccs.emplace_back(onlyState, sccIndex); + // Put the only state of the trivial SCC into the set of states to eliminate. + statesInTrivialSccs.set(*scc.begin(), true); + remainingSccs.set(sccIndex, false); } } - // If we are given priorities, sort the trivial SCCs accordingly. - if (statePriorities) { - std::sort(trivialSccs.begin(), trivialSccs.end(), [&statePriorities] (std::pair const& a, std::pair const& b) { return statePriorities.get()[a.first] < statePriorities.get()[b.first]; }); - } - - STORM_LOG_TRACE("Eliminating " << trivialSccs.size() << " trivial SCCs."); - for (auto const& stateIndexPair : trivialSccs) { - eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards); - remainingSccs.set(stateIndexPair.second, false); - } + std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); + STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs."); + performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all trivial SCCs."); - + // And then recursively treat the remaining sub-SCCs. STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { @@ -619,39 +1102,25 @@ namespace storm { } // Recursively descend in SCC-hierarchy. - uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, stateRewards, statePriorities); + uint_fast64_t depth = treatScc(matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, eliminateEntryStates || !storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); maximalDepth = std::max(maximalDepth, depth); } - } else { // In this case, we perform simple state elimination in the current SCC. STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); - storm::storage::BitVector remainingStates = scc & ~entryStates; - - std::vector states(remainingStates.begin(), remainingStates.end()); - - // If we are given priorities, sort the trivial SCCs accordingly. - if (statePriorities) { - std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); - } - - // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified) - // transition probability matrix. - for (auto const& state : states) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); - } - + std::unique_ptr statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); + performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all states of SCC."); } // Finally, eliminate the entry states (if we are required to do so). if (eliminateEntryStates) { - STORM_LOG_TRACE("Finally, eliminating/adding entry states."); - for (auto state : entryStates) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); - } + STORM_LOG_TRACE("Finally, eliminating entry states."); + std::unique_ptr naivePriorities = createNaivePriorityQueue(entryStates); + performPrioritizedStateElimination(naivePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated/added entry states."); } else { + STORM_LOG_TRACE("Finally, adding entry states to queue."); for (auto state : entryStates) { entryStateQueue.push_back(state); } @@ -661,12 +1130,16 @@ namespace storm { } template - void SparseDtmcEliminationModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { + void SparseDtmcEliminationModelChecker::eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, + ValueUpdateCallback const& callback, PredecessorUpdateCallback const& predecessorCallback, + boost::optional const& priorityUpdateCallback, + boost::optional const& predecessorFilterCallback, bool removeForwardTransitions) { - bool hasSelfLoop = false; - ValueType loopProbability = storm::utility::zero(); + STORM_LOG_TRACE("Eliminating state " << state << "."); // Start by finding loop probability. + bool hasSelfLoop = false; + ValueType loopProbability = storm::utility::zero(); typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { if (entryIt->getColumn() >= state) { @@ -675,7 +1148,7 @@ namespace storm { hasSelfLoop = true; // If we do not clear the forward transitions completely, we need to remove the self-loop, - // because we scale all the other outgoing transitions with it anyway.. + // because we scale all the other outgoing transitions with it anyway. if (!removeForwardTransitions) { currentStateSuccessors.erase(entryIt); } @@ -685,36 +1158,35 @@ namespace storm { } // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop. - std::size_t scaledSuccessors = 0; + STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); if (hasSelfLoop) { STORM_LOG_ASSERT(loopProbability != storm::utility::one(), "Must not eliminate state with probability 1 self-loop."); - loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); - storm::utility::simplify(loopProbability); + loopProbability = storm::utility::simplify(storm::utility::one() / (storm::utility::one() - loopProbability)); for (auto& entry : matrix.getRow(state)) { // Only scale the non-diagonal entries. if (entry.getColumn() != state) { - ++scaledSuccessors; entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability)); } } - if (!stateRewards) { - oneStepProbabilities[state] = oneStepProbabilities[state] * loopProbability; - } + callback(state, loopProbability); } - STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); - // Now connect the predecessors of the state being eliminated with its successors. typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); - std::size_t predecessorForwardTransitionCount = 0; // In case we have a constrained elimination, we need to keep track of the new predecessors. typename FlexibleSparseMatrix::row_type newCurrentStatePredecessors; + + std::vector newBackwardProbabilities(currentStateSuccessors.size()); + for (auto& backwardProbabilities : newBackwardProbabilities) { + backwardProbabilities.reserve(currentStatePredecessors.size()); + } // Now go through the predecessors and eliminate the ones (satisfying the constraint if given). for (auto const& predecessorEntry : currentStatePredecessors) { uint_fast64_t predecessor = predecessorEntry.getColumn(); - + STORM_LOG_TRACE("Found predecessor " << predecessor << "."); + // Skip the state itself as one of its predecessors. if (predecessor == state) { assert(hasSelfLoop); @@ -722,17 +1194,16 @@ namespace storm { } // Skip the state if the elimination is constrained, but the predecessor is not in the constraint. - if (constrained && !predecessorConstraint.get(predecessor)) { - newCurrentStatePredecessors.emplace_back(predecessor, storm::utility::one()); + if (predecessorFilterCallback && !predecessorFilterCallback.get()(predecessor)) { + newCurrentStatePredecessors.emplace_back(predecessorEntry); STORM_LOG_TRACE("Not eliminating predecessor " << predecessor << ", because it does not fit the filter."); continue; } STORM_LOG_TRACE("Eliminating predecessor " << predecessor << "."); // First, find the probability with which the predecessor can move to the current state, because - // the other probabilities need to be scaled with this factor. + // the forward probabilities of the state to be eliminated need to be scaled with this factor. typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); - predecessorForwardTransitionCount += predecessorForwardTransitions.size(); typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); // Make sure we have found the probability and set it to zero. @@ -750,6 +1221,7 @@ namespace storm { newSuccessors.reserve((last1 - first1) + (last2 - first2)); std::insert_iterator result(newSuccessors, newSuccessors.end()); + uint_fast64_t successorOffsetInNewBackwardTransitions = 0; // Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs). for (; first1 != last1; ++result) { // Skip the transitions to the state that is currently being eliminated. @@ -768,108 +1240,118 @@ namespace storm { break; } if (first2->getColumn() < first1->getColumn()) { - *result = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + auto successorEntry = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + *result = successorEntry; + newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, successorEntry.getValue()); +// std::cout << "(1) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first2; + ++successorOffsetInNewBackwardTransitions; } else if (first1->getColumn() < first2->getColumn()) { *result = *first1; ++first1; } else { - *result = storm::storage::MatrixEntry(first1->getColumn(), storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()))); + auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); + *result = storm::storage::MatrixEntry(first1->getColumn(), probability); + newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); +// std::cout << "(2) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; ++first1; ++first2; + ++successorOffsetInNewBackwardTransitions; } } for (; first2 != last2; ++first2) { if (first2->getColumn() != state) { - *result = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + auto stateProbability = storm::utility::simplify(std::move(*first2 * multiplyFactor)); + *result = stateProbability; + newBackwardProbabilities[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, stateProbability.getValue()); +// std::cout << "(3) adding " << first2->getColumn() << " -> " << newBackwardProbabilities[successorOffsetInNewBackwardTransitions].back() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; + ++successorOffsetInNewBackwardTransitions; } } // Now move the new transitions in place. predecessorForwardTransitions = std::move(newSuccessors); - - if (!stateRewards) { - // Add the probabilities to go to a target state in just one step if we have to compute probabilities. - oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]); - STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor states."); - } else { - // If we are computing rewards, we basically scale the state reward of the state to eliminate and - // add the result to the state reward of the predecessor. - if (hasSelfLoop) { - stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * loopProbability * stateRewards.get()[state]); - } else { - stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]); - } + STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor state " << predecessor << "."); + + predecessorCallback(predecessor, multiplyFactor, state); + + if (priorityUpdateCallback) { + STORM_LOG_TRACE("Updating priority of predecessor."); + priorityUpdateCallback.get()(predecessor); } } // Finally, we need to add the predecessor to the set of predecessors of every successor. + uint_fast64_t successorOffsetInNewBackwardTransitions = 0; for (auto const& successorEntry : currentStateSuccessors) { + if (successorEntry.getColumn() == state) { + continue; + } + typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); +// std::cout << "old backward trans of " << successorEntry.getColumn() << std::endl; +// for (auto const& trans : successorBackwardTransitions) { +// std::cout << trans << std::endl; +// } // Delete the current state as a predecessor of the successor state only if we are going to remove the // current state's forward transitions. if (removeForwardTransitions) { typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); - STORM_LOG_ASSERT(elimIt != successorBackwardTransitions.end(), "Expected a proper backward transition, but found none."); + STORM_LOG_ASSERT(elimIt != successorBackwardTransitions.end(), "Expected a proper backward transition from " << successorEntry.getColumn() << " to " << state << ", but found none."); successorBackwardTransitions.erase(elimIt); } typename FlexibleSparseMatrix::row_type::iterator first1 = successorBackwardTransitions.begin(); typename FlexibleSparseMatrix::row_type::iterator last1 = successorBackwardTransitions.end(); - typename FlexibleSparseMatrix::row_type::iterator first2 = currentStatePredecessors.begin(); - typename FlexibleSparseMatrix::row_type::iterator last2 = currentStatePredecessors.end(); + typename FlexibleSparseMatrix::row_type::iterator first2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].begin(); + typename FlexibleSparseMatrix::row_type::iterator last2 = newBackwardProbabilities[successorOffsetInNewBackwardTransitions].end(); + +// std::cout << "adding backward trans " << successorEntry.getColumn() << "[" << successorOffsetInNewBackwardTransitions << "]" << std::endl; +// for (auto const& trans : newBackwardProbabilities[successorOffsetInNewBackwardTransitions]) { +// std::cout << trans << std::endl; +// } typename FlexibleSparseMatrix::row_type newPredecessors; newPredecessors.reserve((last1 - first1) + (last2 - first2)); std::insert_iterator result(newPredecessors, newPredecessors.end()); - if (!constrained) { - for (; first1 != last1; ++result) { - if (first2 == last2) { - std::copy(first1, last1, result); - break; - } - if (first2->getColumn() < first1->getColumn()) { - if (first2->getColumn() != state) { - *result = *first2; - } - ++first2; - } else { - *result = *first1; - if (first1->getColumn() == first2->getColumn()) { - ++first2; - } - ++first1; - } + for (; first1 != last1; ++result) { + if (first2 == last2) { + std::copy(first1, last1, result); + break; } - std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state; }); - } else { - // If the elimination is constrained, we need to be more selective when we set the new predecessors - // of the successor state. - for (; first1 != last1; ++result) { - if (first2 == last2) { - std::copy(first1, last1, result); - break; + if (first2->getColumn() < first1->getColumn()) { + if (first2->getColumn() != state) { + *result = *first2; } - if (first2->getColumn() < first1->getColumn()) { - if (first2->getColumn() != state) { - *result = *first2; - } - ++first2; - } else { + ++first2; + } else if (first1->getColumn() == first2->getColumn()) { + if (estimateComplexity(first1->getValue()) > estimateComplexity(first2->getValue())) { *result = *first1; - if (first1->getColumn() == first2->getColumn()) { - ++first2; - } - ++first1; + } else { + *result = *first2; } + ++first1; + ++first2; + } else { + *result = *first1; + ++first1; } - std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state && (!constrained || predecessorConstraint.get(a.getColumn())); }); + } + if (predecessorFilterCallback) { + std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state && predecessorFilterCallback.get()(a.getColumn()); }); + } else { + std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry const& a) { return a.getColumn() != state; }); } // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); +// std::cout << "new backward trans of " << successorEntry.getColumn() << std::endl; +// for (auto const& trans : successorBackwardTransitions) { +// std::cout << trans << std::endl; +// } + ++successorOffsetInNewBackwardTransitions; } STORM_LOG_TRACE("Fixed predecessor lists of successor states."); @@ -878,11 +1360,58 @@ namespace storm { currentStateSuccessors.clear(); currentStateSuccessors.shrink_to_fit(); } - if (!constrained) { + if (predecessorFilterCallback) { + currentStatePredecessors = std::move(newCurrentStatePredecessors); + } else { currentStatePredecessors.clear(); currentStatePredecessors.shrink_to_fit(); + } + } + + template + std::vector SparseDtmcEliminationModelChecker::getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse) { + std::vector statePriorities(transitionMatrix.getRowCount()); + std::vector states(transitionMatrix.getRowCount()); + for (std::size_t index = 0; index < states.size(); ++index) { + states[index] = index; + } + + std::vector distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities, + storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || + storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed); + + // In case of the forward or backward ordering, we can sort the states according to the distances. + if (forward ^ reverse) { + std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } ); } else { - currentStatePredecessors = std::move(newCurrentStatePredecessors); + // Otherwise, we sort them according to descending distances. + std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } ); + } + + // Now convert the ordering of the states to priorities. + for (uint_fast64_t index = 0; index < states.size(); ++index) { + statePriorities[states[index]] = index; + } + + return statePriorities; + } + + template + std::vector SparseDtmcEliminationModelChecker::getStateDistances(storm::storage::SparseMatrix::ValueType> const& transitionMatrix, storm::storage::SparseMatrix::ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector::ValueType> const& oneStepProbabilities, bool forward) { + if (forward) { + return storm::utility::graph::getDistances(transitionMatrix, initialStates); + } else { + // Since the target states were eliminated from the matrix already, we construct a replacement by + // treating all states that have some non-zero probability to go to a target state in one step as target + // states. + storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount()); + for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { + if (oneStepProbabilities[index] != storm::utility::zero()) { + pseudoTargetStates.set(index); + } + } + + return storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates); } } @@ -936,6 +1465,35 @@ namespace storm { } } + template + bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::empty() const { + for (auto const& row : this->data) { + if (!row.empty()) { + return false; + } + } + return true; + } + + template + void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter) { + for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) { + auto& row = this->data[rowIndex]; + if (!rowFilter.get(rowIndex)) { + row.clear(); + row.shrink_to_fit(); + continue; + } + row_type newRow; + for (auto const& element : row) { + if (columnFilter.get(element.getColumn())) { + newRow.push_back(element); + } + } + row = std::move(newRow); + } + } + template typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); @@ -961,6 +1519,146 @@ namespace storm { return flexibleMatrix; } + template + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t penalty = 0; + bool hasParametricSelfLoop = false; + + for (auto const& predecessor : backwardTransitions.getRow(state)) { + for (auto const& successor : transitionMatrix.getRow(state)) { + penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue()); +// STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << "."); + } + if (predecessor.getColumn() == state) { + hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue()); + } + penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state]); +// STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << "."); + } + + // If it is a self-loop that is parametric, we increase the penalty a lot. + if (hasParametricSelfLoop) { + penalty *= 10; +// STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop."); + } + +// STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << "."); + return penalty; + } + + template + uint_fast64_t SparseDtmcEliminationModelChecker::computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); + } + + template + void SparseDtmcEliminationModelChecker::StatePriorityQueue::update(storm::storage::sparse::state_type, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + // Intentionally left empty. + } + + template + SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::StaticStatePriorityQueue(std::vector const& sortedStates) : StatePriorityQueue(), sortedStates(sortedStates), currentPosition(0) { + // Intentionally left empty. + } + + template + bool SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::hasNextState() const { + return currentPosition < sortedStates.size(); + } + + template + storm::storage::sparse::state_type SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::popNextState() { + ++currentPosition; + return sortedStates[currentPosition - 1]; + } + + template + std::size_t SparseDtmcEliminationModelChecker::StaticStatePriorityQueue::size() const { + return sortedStates.size() - currentPosition; + } + + template + SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { + // Insert all state-penalty pairs into our priority queue. + for (auto const& statePenalty : sortedStatePenaltyPairs) { + priorityQueue.insert(priorityQueue.end(), statePenalty); + } + + // Insert all state-penalty pairs into auxiliary mapping. + for (auto const& statePenalty : sortedStatePenaltyPairs) { + stateToPriorityMapping.emplace(statePenalty); + } + } + + template + bool SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::hasNextState() const { + return !priorityQueue.empty(); + } + + template + storm::storage::sparse::state_type SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::popNextState() { + auto it = priorityQueue.begin(); + STORM_LOG_TRACE("Popping state " << it->first << " with priority " << it->second << "."); + storm::storage::sparse::state_type result = it->first; + priorityQueue.erase(priorityQueue.begin()); + return result; + } + + template + void SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + // First, we need to find the priority until now. + auto priorityIt = stateToPriorityMapping.find(state); + + // If the priority queue does not store the priority of the given state, we must not update it. + if (priorityIt == stateToPriorityMapping.end()) { + return; + } + uint_fast64_t lastPriority = priorityIt->second; + + uint_fast64_t newPriority = penaltyFunction(state, transitionMatrix, backwardTransitions, oneStepProbabilities); + + if (lastPriority != newPriority) { + // Erase and re-insert into the priority queue with the new priority. + auto queueIt = priorityQueue.find(std::make_pair(state, lastPriority)); + priorityQueue.erase(queueIt); + priorityQueue.emplace(state, newPriority); + + // Finally, update the probability in the mapping. + priorityIt->second = newPriority; + } + } + + template + std::size_t SparseDtmcEliminationModelChecker::DynamicPenaltyStatePriorityQueue::size() const { + return priorityQueue.size(); + } + + template + bool SparseDtmcEliminationModelChecker::checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions) { + for (uint_fast64_t forwardIndex = 0; forwardIndex < transitionMatrix.getNumberOfRows(); ++forwardIndex) { + for (auto const& forwardEntry : transitionMatrix.getRow(forwardIndex)) { + if (forwardEntry.getColumn() == forwardIndex) { + continue; + } + + bool foundCorrespondingElement = false; + for (auto const& backwardEntry : backwardTransitions.getRow(forwardEntry.getColumn())) { + if (backwardEntry.getColumn() == forwardIndex) { + foundCorrespondingElement = true; + } + } + + if (!foundCorrespondingElement) { +// std::cout << "forward entry: " << forwardIndex << " -> " << forwardEntry << std::endl; +// transitionMatrix.print(); +// backwardTransitions.print(); + return false; + } + } + } + return true; + } + template class SparseDtmcEliminationModelChecker>; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 856fd7536..692a6be57 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -15,14 +15,23 @@ namespace storm { typedef typename SparseDtmcModelType::ValueType ValueType; typedef typename SparseDtmcModelType::RewardModelType RewardModelType; - explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); + /*! + * Creates an elimination-based model checker for the given model. + * + * @param model The model to analyze. + * @param computeResultsForInitialStatesOnly If set to true, the results are only computed for + */ + explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly = true); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - + virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + private: class FlexibleSparseMatrix { public: @@ -44,12 +53,15 @@ namespace storm { void print() const; + bool empty() const; + + void filter(storm::storage::BitVector const& rowFilter, storm::storage::BitVector const& columnFilter); + /*! - * Checks whether the given state has a self-loop with an arbitrary probability in the given probability matrix. + * Checks whether the given state has a self-loop with an arbitrary probability in the probability matrix. * * @param state The state for which to check whether it possesses a self-loop. - * @param matrix The matrix in which to look for the loop. - * @return True iff the given state has a self-loop with an arbitrary probability in the given probability matrix. + * @return True iff the given state has a self-loop with an arbitrary probability in the probability matrix. */ bool hasSelfLoop(storm::storage::sparse::state_type state); @@ -57,15 +69,90 @@ namespace storm { std::vector data; }; - ValueType computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards, boost::optional> const& statePriorities = {}); + class StatePriorityQueue { + public: + virtual bool hasNextState() const = 0; + virtual storm::storage::sparse::state_type popNextState() = 0; + virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + virtual std::size_t size() const = 0; + }; + + class StaticStatePriorityQueue : public StatePriorityQueue { + public: + StaticStatePriorityQueue(std::vector const& sortedStates); + + virtual bool hasNextState() const override; + virtual storm::storage::sparse::state_type popNextState() override; + virtual std::size_t size() const override; + + private: + std::vector sortedStates; + uint_fast64_t currentPosition; + }; + + struct PriorityComparator { + bool operator()(std::pair const& first, std::pair const& second) { + return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; + } + }; - uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, boost::optional>& stateRewards, boost::optional> const& statePriorities = {}); + typedef std::function const& oneStepProbabilities)> PenaltyFunctionType; + + class DynamicPenaltyStatePriorityQueue : public StatePriorityQueue { + public: + DynamicPenaltyStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, PenaltyFunctionType const& penaltyFunction); + + virtual bool hasNextState() const override; + virtual storm::storage::sparse::state_type popNextState() override; + virtual void update(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) override; + virtual std::size_t size() const override; + + private: + std::set, PriorityComparator> priorityQueue; + std::unordered_map stateToPriorityMapping; + PenaltyFunctionType penaltyFunction; + }; + + static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector& stateValues); + + static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); + + static std::unique_ptr createStatePriorityQueue(boost::optional> const& stateDistances, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + + static std::unique_ptr createNaivePriorityQueue(storm::storage::BitVector const& states); + + static void performPrioritizedStateElimination(std::unique_ptr& priorityQueue, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); + + static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); + + static void performOrdinaryStateElimination(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); + + static uint_fast64_t performHybridStateElimination(storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities); + + static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& values, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::BitVector const& initialStates, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, bool computeResultsForInitialStatesOnly, boost::optional> const& distanceBasedPriorities = boost::none); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); + + typedef std::function ValueUpdateCallback; + typedef std::function PredecessorUpdateCallback; + typedef std::function PriorityUpdateCallback; + typedef std::function PredecessorFilterCallback; + + static void eliminateState(storm::storage::sparse::state_type state, FlexibleSparseMatrix& matrix, FlexibleSparseMatrix& backwardTransitions, ValueUpdateCallback const& valueUpdateCallback, PredecessorUpdateCallback const& predecessorCallback, boost::optional const& priorityUpdateCallback = boost::none, boost::optional const& predecessorFilterCallback = boost::none, bool removeForwardTransitions = true); + + static std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); + + static std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); + + static uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + + static uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, FlexibleSparseMatrix const& transitionMatrix, FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); + + static bool checkConsistent(FlexibleSparseMatrix& transitionMatrix, FlexibleSparseMatrix& backwardTransitions); - void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); + // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. + bool computeResultsForInitialStatesOnly; - std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); }; } // namespace modelchecker diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 16339f38b..3f22b4ff2 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -218,6 +218,19 @@ namespace storm { return true; } + template + void ExplicitQuantitativeCheckResult::oneMinus() { + if (this->isResultForAllStates()) { + for (auto& element : boost::get(values)) { + element = storm::utility::one() - element; + } + } else { + for (auto& element : boost::get(values)) { + element.second = storm::utility::one() - element.second; + } + } + } + template class ExplicitQuantitativeCheckResult; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 542abe059..9734a176f 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -49,6 +49,8 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; + virtual void oneMinus() override; + private: // The values of the quantitative check result. boost::variant values; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 51a254722..0f0ad01e2 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -164,6 +164,17 @@ namespace storm { return max; } + template + void HybridQuantitativeCheckResult::oneMinus() { + storm::dd::Add one = symbolicValues.getDdManager().template getAddOne(); + storm::dd::Add zero = symbolicValues.getDdManager().template getAddZero(); + symbolicValues = symbolicStates.ite(one - symbolicValues, zero); + + for (auto& element : explicitValues) { + element = storm::utility::one() - element; + } + } + // Explicitly instantiate the class. template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 9e40ae29e..02e1dc4ed 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -50,6 +50,8 @@ namespace storm { virtual ValueType getMax() const; + virtual void oneMinus() override; + private: // The set of all reachable states. storm::dd::Bdd reachableStates; diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index 425e7b6ef..32f348818 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -7,11 +7,12 @@ namespace storm { namespace modelchecker { class QuantitativeCheckResult : public CheckResult { public: - virtual ~QuantitativeCheckResult() = default; virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; + virtual void oneMinus() = 0; + virtual bool isQuantitative() const override; }; } diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index bd4d6b2ba..ff65f22a7 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -89,6 +89,12 @@ namespace storm { return this->values.getMax(); } + template + void SymbolicQuantitativeCheckResult::oneMinus() { + storm::dd::Add one = values.getDdManager().template getAddOne(); + values = one - values; + } + // Explicitly instantiate the class. template class SymbolicQuantitativeCheckResult; template class SymbolicQuantitativeCheckResult; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index b69b950e6..9cbb272a3 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -38,6 +38,8 @@ namespace storm { virtual ValueType getMax() const; + virtual void oneMinus() override; + private: // The set of all reachable states. storm::dd::Bdd reachableStates; diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index f6ff87f5b..7054e26ef 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -337,12 +337,8 @@ namespace storm { STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping."); storm::expressions::Expression const* expression = this->identifiers_->find(identifier); if (expression == nullptr) { - if (allowBacktracking) { - pass = false; - return manager->boolean(false); - } else { - pass = false; - } + pass = false; + return manager->boolean(false); } return *expression; } else { diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index bcffe38e3..e3c0c9718 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -101,7 +101,7 @@ namespace storm { qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> expectedTimeOperator; - qi::rule(), Skipper> steadyStateOperator; + qi::rule(), Skipper> longRunAverageOperator; qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; @@ -131,6 +131,7 @@ namespace storm { qi::rule(), Skipper> cumulativeRewardFormula; qi::rule(), Skipper> reachabilityRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(), Skipper> longRunAverageRewardFormula; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; @@ -139,6 +140,7 @@ namespace storm { std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; + std::shared_ptr createLongRunAverageRewardFormula() const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; @@ -243,6 +245,9 @@ namespace storm { // Set the identifier mapping to actually generate expressions. expressionParser.setIdentifierMapping(&identifiers_); + longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; + longRunAverageRewardFormula.name("long run average reward formula"); + instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); @@ -252,7 +257,7 @@ namespace storm { reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)]; reachabilityRewardFormula.name("reachability reward formula"); - rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula; + rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula; rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -267,7 +272,7 @@ namespace storm { booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); - operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator; + operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator; operatorFormula.name("operator formulas"); atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; @@ -303,8 +308,8 @@ namespace storm { operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); - steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; - steadyStateOperator.name("long-run average operator"); + longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + longRunAverageOperator.name("long-run average operator"); rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); rewardModelName.name("reward model name"); @@ -338,7 +343,7 @@ namespace storm { debug(andStateFormula); debug(probabilityOperator); debug(rewardOperator); - debug(steadyStateOperator); + debug(longRunAverageOperator); debug(pathFormulaWithoutUntil); debug(pathFormula); debug(conditionalFormula); @@ -362,7 +367,7 @@ namespace storm { qi::on_error(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -409,6 +414,10 @@ namespace storm { return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); } + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { + return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); + } + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h index 3e78935bd..cd2a35b06 100644 --- a/src/parser/SpiritErrorHandler.h +++ b/src/parser/SpiritErrorHandler.h @@ -22,7 +22,7 @@ namespace storm { stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; stream << "\t" << line << std::endl << "\t"; auto caretColumn = boost::spirit::get_column(lineStart, where); - stream << std::string(caretColumn - 1, ' ') << "^" << std::endl; + stream << "\t" << std::string(caretColumn - 1, ' ') << "^" << std::endl; STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, stream.str()); return qi::fail; diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp index 6a2528a5b..c98e5821f 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp +++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp @@ -17,11 +17,11 @@ namespace storm { const std::string SparseDtmcEliminationModelCheckerSettings::maximalSccSizeOptionName = "sccsize"; SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { - std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); + std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand", "spen", "dpen", "regex"}; + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); std::vector methods = {"state", "hybrid"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("state").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") @@ -51,6 +51,12 @@ namespace storm { return EliminationOrder::BackwardReversed; } else if (eliminationOrderAsString == "rand") { return EliminationOrder::Random; + } else if (eliminationOrderAsString == "spen") { + return EliminationOrder::StaticPenalty; + } else if (eliminationOrderAsString == "dpen") { + return EliminationOrder::DynamicPenalty; + } else if (eliminationOrderAsString == "regex") { + return EliminationOrder::RegularExpression; } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination order selected."); } diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h index 55a9b14b4..19716c3b2 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h +++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h @@ -15,7 +15,7 @@ namespace storm { /*! * An enum that contains all available state elimination orders. */ - enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random }; + enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random, StaticPenalty, DynamicPenalty, RegularExpression }; /*! * An enum that contains all available techniques to solve parametric systems. diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 16610f4ad..94e41e796 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -408,7 +408,7 @@ namespace storm { std::vector MathsatSmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_MSAT - STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable."); STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); size_t numUnsatAssumpations; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 0dcc3cbec..cd5f46009 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -564,6 +564,21 @@ namespace storm { return result; } + + std::vector BitVector::getNumberOfSetBitsBeforeIndices() const { + std::vector bitsSetBeforeIndices; + bitsSetBeforeIndices.reserve(this->size()); + uint_fast64_t lastIndex = 0; + uint_fast64_t currentNumberOfSetBits = 0; + for (auto index : *this) { + while (lastIndex <= index) { + bitsSetBeforeIndices.push_back(currentNumberOfSetBits); + ++lastIndex; + } + ++currentNumberOfSetBits; + } + return bitsSetBeforeIndices; + } size_t BitVector::size() const { return static_cast (bitCount); diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 8aed9e387..f9c088ceb 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -412,6 +412,13 @@ namespace storm { */ uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const; + /*! + * Retrieves a vector that holds at position i the number of bits set before index i. + * + * @return The resulting vector of 'offsets'. + */ + std::vector getNumberOfSetBitsBeforeIndices() const; + /*! * Retrieves the number of bits this bit vector can store. * diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h new file mode 100644 index 000000000..c50b6d306 --- /dev/null +++ b/src/storage/ModelProgramPair.h @@ -0,0 +1,12 @@ +#include "../models/ModelBase.h" +#include "prism/Program.h" + + +namespace storm { + namespace storage { + struct ModelProgramPair { + std::shared_ptr model; + storm::prism::Program program; + }; + } +} \ No newline at end of file diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 93010b53e..1bc2f9af0 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -412,7 +412,6 @@ namespace storm { template void SparseMatrix::updateNonzeroEntryCount() const { - //SparseMatrix* self = const_cast*>(this); this->nonzeroEntryCount = 0; for (auto const& element : *this) { if (element.getValue() != storm::utility::zero()) { @@ -426,6 +425,18 @@ namespace storm { this->nonzeroEntryCount += difference; } + template + void SparseMatrix::updateDimensions() const { + this->nonzeroEntryCount = 0; + this->columnCount = 0; + for (auto const& element : *this) { + if (element.getValue() != storm::utility::zero()) { + ++this->nonzeroEntryCount; + this->columnCount = std::max(element.getColumn() + 1, this->columnCount); + } + } + } + template typename SparseMatrix::index_type SparseMatrix::getRowGroupCount() const { return rowGroupIndices.size() - 1; @@ -554,34 +565,12 @@ namespace storm { // Start by creating a temporary vector that stores for each index whose bit is set to true the number of // bits that were set before that particular index. - std::vector columnBitsSetBeforeIndex; - columnBitsSetBeforeIndex.reserve(columnCount); - - // Compute the information to fill this vector. - index_type lastIndex = 0; - index_type currentNumberOfSetBits = 0; - for (auto index : columnConstraint) { - while (lastIndex <= index) { - columnBitsSetBeforeIndex.push_back(currentNumberOfSetBits); - ++lastIndex; - } - ++currentNumberOfSetBits; - } + std::vector columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices(); std::vector* rowBitsSetBeforeIndex; if (&rowGroupConstraint == &columnConstraint) { rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex; } else { - rowBitsSetBeforeIndex = new std::vector(rowCount); - - lastIndex = 0; - currentNumberOfSetBits = 0; - for (auto index : rowGroupConstraint) { - while (lastIndex <= index) { - rowBitsSetBeforeIndex->push_back(currentNumberOfSetBits); - ++lastIndex; - } - ++currentNumberOfSetBits; - } + rowBitsSetBeforeIndex = new std::vector(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); } // Then, we need to determine the number of entries and the number of rows of the submatrix. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 7cc81fdb5..99eea1c06 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -514,6 +514,11 @@ namespace storm { * Recompute the nonzero entry count */ void updateNonzeroEntryCount() const; + + /*! + * Recomputes the number of columns and the number of non-zero entries. + */ + void updateDimensions() const; /*! * Change the nonzero entry count by the provided value. @@ -939,7 +944,7 @@ namespace storm { index_type rowCount; // The number of columns of the matrix. - index_type columnCount; + mutable index_type columnCount; // The number of entries in the matrix. index_type entryCount; diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index ae9b61e3a..08845a24b 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -96,7 +96,16 @@ namespace storm { } newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer(); } else if (formula.isRewardOperatorFormula()) { - optimalityType = formula.asRewardOperatorFormula().getOptimalityType(); + if (formula.asRewardOperatorFormula().hasOptimalityType()) { + optimalityType = formula.asRewardOperatorFormula().getOptimalityType(); + } else if (formula.asRewardOperatorFormula().hasBound()) { + storm::logic::ComparisonType comparisonType = formula.asRewardOperatorFormula().getComparisonType(); + if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) { + optimalityType = OptimizationDirection::Maximize; + } else { + optimalityType = OptimizationDirection::Minimize; + } + } newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer(); } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index bba5fd160..900482a72 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -73,8 +73,8 @@ namespace storm { template<> storm::RationalFunction infinity() { - // FIXME: this does not work. - return storm::RationalFunction(carl::rationalize(std::numeric_limits::infinity())); + // FIXME: this should be treated more properly. + return storm::RationalFunction(-1.0); } #endif diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 17384fa55..193b0ff28 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -27,28 +27,55 @@ namespace storm { namespace graph { template - storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { + storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps) { storm::storage::BitVector reachableStates(initialStates); + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + // Initialize the stack used for the DFS with the states. std::vector stack(initialStates.begin(), initialStates.end()); + // Initialize the stack for the step bound, if the number of steps is bounded. + std::vector stepStack; + std::vector remainingSteps; + if (useStepBound) { + stepStack.reserve(numberOfStates); + stepStack.insert(stepStack.begin(), targetStates.getNumberOfSetBits(), maximalSteps); + remainingSteps.resize(numberOfStates); + for (auto state : targetStates) { + remainingSteps[state] = maximalSteps; + } + } + // Perform the actual DFS. - uint_fast64_t currentState = 0; + uint_fast64_t currentState = 0, currentStepBound = 0; while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); + if (useStepBound) { + currentStepBound = stepStack.back(); + stepStack.pop_back(); + } + for (auto const& successor : transitionMatrix.getRowGroup(currentState)) { // Only explore the state if the transition was actually there and the successor has not yet // been visited. - if (successor.getValue() != storm::utility::zero() && !reachableStates.get(successor.getColumn())) { + if (successor.getValue() != storm::utility::zero() && !reachableStates.get(successor.getColumn()) && (!useStepBound || remainingSteps[successor.getColumn()] < currentStepBound - 1)) { // If the successor is one of the target states, we need to include it, but must not explore // it further. if (targetStates.get(successor.getColumn())) { reachableStates.set(successor.getColumn()); } else if (constraintStates.get(successor.getColumn())) { - // However, if the state is in the constrained set of states, we need to follow it. + // However, if the state is in the constrained set of states, we potentially need to follow it. + if (useStepBound) { + remainingSteps[successor.getColumn()] = currentStepBound - 1; + stepStack.push_back(currentStepBound - 1); + + if (currentStepBound == 0) { + continue; + } + } reachableStates.set(successor.getColumn()); stack.push_back(successor.getColumn()); } @@ -60,7 +87,7 @@ namespace storm { } template - std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { + std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem) { std::vector distances(transitionMatrix.getRowGroupCount()); std::vector> stateQueue; @@ -80,8 +107,10 @@ namespace storm { for (auto const& successorEntry : transitionMatrix.getRowGroup(stateDistancePair.first)) { if (!statesInQueue.get(successorEntry.getColumn())) { - stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); - statesInQueue.set(successorEntry.getColumn()); + if (!subsystem || subsystem.get()[successorEntry.getColumn()]) { + stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); + statesInQueue.set(successorEntry.getColumn()); + } } } ++currentPosition; @@ -126,18 +155,18 @@ namespace storm { } for (typename storm::storage::SparseMatrix::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) { - if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) { + if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) { // If we don't have a bound on the number of steps to take, just add the state to the stack. - if (!useStepBound) { - statesWithProbabilityGreater0.set(entryIt->getColumn(), true); - stack.push_back(entryIt->getColumn()); - } else if (currentStepBound > 0) { + if (useStepBound) { // If there is at least one more step to go, we need to push the state and the new number of steps. remainingSteps[entryIt->getColumn()] = currentStepBound - 1; - statesWithProbabilityGreater0.set(entryIt->getColumn(), true); - stack.push_back(entryIt->getColumn()); stepStack.push_back(currentStepBound - 1); + if (currentStepBound == 0) { + continue; + } } + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); } } } @@ -377,18 +406,19 @@ namespace storm { } for (typename storm::storage::SparseMatrix::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) { - if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) { + if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) { // If we don't have a bound on the number of steps to take, just add the state to the stack. - if (!useStepBound) { - statesWithProbabilityGreater0.set(entryIt->getColumn(), true); - stack.push_back(entryIt->getColumn()); - } else if (currentStepBound > 0) { + if (useStepBound) { // If there is at least one more step to go, we need to push the state and the new number of steps. remainingSteps[entryIt->getColumn()] = currentStepBound - 1; - statesWithProbabilityGreater0.set(entryIt->getColumn(), true); - stack.push_back(entryIt->getColumn()); stepStack.push_back(currentStepBound - 1); + + if (currentStepBound == 0) { + continue; + } } + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); } } } @@ -525,7 +555,7 @@ namespace storm { } for(typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { - if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) || (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) { + if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) && (!useStepBound || remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) { // Check whether the predecessor has at least one successor in the current state set for every // nondeterministic choice. bool addToStatesWithProbabilityGreater0 = true; @@ -547,16 +577,17 @@ namespace storm { // If we need to add the state, then actually add it and perform further search from the state. if (addToStatesWithProbabilityGreater0) { // If we don't have a bound on the number of steps to take, just add the state to the stack. - if (!useStepBound) { - statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); - stack.push_back(predecessorEntryIt->getColumn()); - } else if (currentStepBound > 0) { + if (useStepBound) { // If there is at least one more step to go, we need to push the state and the new number of steps. remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; - statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); - stack.push_back(predecessorEntryIt->getColumn()); stepStack.push_back(currentStepBound - 1); + + if (currentStepBound == 0) { + continue; + } } + statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); } } } @@ -925,9 +956,9 @@ namespace storm { - template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); - template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); @@ -991,9 +1022,9 @@ namespace storm { - template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); - template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); @@ -1046,9 +1077,9 @@ namespace storm { #ifdef STORM_HAVE_CARL - template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); - template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); diff --git a/src/utility/graph.h b/src/utility/graph.h index b7a318b10..913a8aaab 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -55,9 +55,11 @@ namespace storm { * @param initialStates The set of states from which to start the search. * @param constraintStates The set of states that must not be left. * @param targetStates The target states that may not be passed. + * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. + * @param maximalSteps The maximal number of steps to reach the psi states. */ template - storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); /*! * Performs a breadth-first search through the underlying graph structure to compute the distance from all @@ -65,10 +67,11 @@ namespace storm { * * @param transitionMatrix The transition relation of the graph structure to search. * @param initialStates The set of states from which to start the search. + * @param subsystem The subsystem to consider. * @return The distances of each state to the initial states of the sarch. */ template - std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); + std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem = boost::none); /*! * Performs a backward depth-first search trough the underlying graph structure diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index c6f09b375..a690af6f8 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -11,7 +11,6 @@ namespace storm { storm::prism::Program parseProgram(std::string const& path) { storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify(); program.checkValidity(); - std::cout << program << std::endl; return program; } diff --git a/src/utility/storm.h b/src/utility/storm.h index d607f01ad..af70bb89c 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -46,6 +46,7 @@ // Headers for model processing. #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" +#include "src/storage/ModelProgramPair.h" // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -83,8 +84,8 @@ namespace storm { std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); template - std::pair, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> result; + storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + storm::storage::ModelProgramPair result; storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); @@ -103,16 +104,16 @@ namespace storm { } storm::builder::ExplicitPrismModelBuilder builder; - result.first = builder.translateProgram(program, options); - result.second = builder.getTranslatedProgram(); + result.model = builder.translateProgram(program, options); + result.program = builder.getTranslatedProgram(); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constants); storm::builder::DdPrismModelBuilder builder; - result.first = builder.translateProgram(program, options); - result.second = builder.getTranslatedProgram(); + result.model = builder.translateProgram(program, options); + result.program = builder.getTranslatedProgram(); } return result; diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index a3ca2dc46..9c3347b72 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -131,7 +131,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.0448979, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); }