From e7ca4dc0c94f280826d01e5764a6788ac5809c8e Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Wed, 17 Feb 2021 22:31:39 +0100 Subject: [PATCH 1/5] start with globally formulae - definitions of methods and functionality (not checked) --- src/storm/logic/FragmentSpecification.cpp | 1 + .../rpatl/SparseSmgRpatlModelChecker.cpp | 18 +++++++++++++++++- .../rpatl/SparseSmgRpatlModelChecker.h | 1 + .../rpatl/helper/SparseSmgRpatlHelper.cpp | 16 ++++++++++++++++ .../rpatl/helper/SparseSmgRpatlHelper.h | 1 + 5 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 2487dcd86..648dd2bf0 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -66,6 +66,7 @@ namespace storm { rpatl.setProbabilityOperatorsAllowed(true); rpatl.setReachabilityProbabilityFormulasAllowed(true); rpatl.setUntilFormulasAllowed(true); + rpatl.setGloballyFormulasAllowed(true); return rpatl; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 97dc26054..bc20aadec 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -112,6 +112,8 @@ namespace storm { return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula())); } else if (formula.isUntilFormula()) { return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula())); + } else if (formula.isGloballyFormula()) { + return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -144,7 +146,21 @@ namespace storm { return result; } - template + template + std::unique_ptr SparseSmgRpatlModelChecker::computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } + + template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index dfbd47762..4b1dc2547 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -37,6 +37,7 @@ namespace storm { std::unique_ptr computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 8d254b01f..be91ecd02 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -71,6 +71,22 @@ namespace storm { return completeScheduler; } + template + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + // TODO: the inputs are copied from until, check which of them are used + // - there is no leftsubformula, so there is no phiStates (as Input) + // - what about this "hint"? + + // TODO: SparseMdpPrctlHelper uses "useMecBasedTechnique" - should I pay attention to that? + + goal.oneMinus(); + auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), psiStates, qualitative, statesOfCoalition, produceScheduler, hint); + for (auto& element : result.values) { + element = storm::utility::one() - element; + } + return result; + } + template class SparseSmgRpatlHelper; #ifdef STORM_HAVE_CARL template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 7152ab3db..68dee01fb 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -37,6 +37,7 @@ namespace storm { // TODO should probably be renamed in the future: static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); From 734599c11495cb9c4a94deb28d5f97051906ec73 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 22 Feb 2021 12:11:21 +0100 Subject: [PATCH 2/5] correction of globally functionality --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index be91ecd02..286a5ed60 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -73,14 +73,15 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - // TODO: the inputs are copied from until, check which of them are used - // - there is no leftsubformula, so there is no phiStates (as Input) - // - what about this "hint"? - - // TODO: SparseMdpPrctlHelper uses "useMecBasedTechnique" - should I pay attention to that? - - goal.oneMinus(); - auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), psiStates, qualitative, statesOfCoalition, produceScheduler, hint); + // the idea is to implement the definition of globally as in the formula: + // G phi = not(F(not phi)) = not(true U (not phi)) + // so the phiStates are flipped, then the true U part is calculated, at the end the result is flipped again + storm::storage::BitVector notPsiStates = ~psiStates; + //goal.oneMinus(); + statesOfCoalition.complement(); + //STORM_LOG_DEBUG(storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); + //STORM_LOG_DEBUG(psiStates); + auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; } From 5b9319ee58eeb8c13cbb619fc94534f01c695b63 Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 1 Mar 2021 18:00:57 +0100 Subject: [PATCH 3/5] clean up computeGloballyProbabilities --- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 286a5ed60..f6b756352 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -72,15 +72,12 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::v(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // the idea is to implement the definition of globally as in the formula: - // G phi = not(F(not phi)) = not(true U (not phi)) - // so the phiStates are flipped, then the true U part is calculated, at the end the result is flipped again + // G phi = not(F(not psi)) = not(true U (not psi)) + // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again storm::storage::BitVector notPsiStates = ~psiStates; - //goal.oneMinus(); statesOfCoalition.complement(); - //STORM_LOG_DEBUG(storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); - //STORM_LOG_DEBUG(psiStates); auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; From 50087994f7129f41b3a62be79317c4a4d9fe311e Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 1 Mar 2021 18:12:07 +0100 Subject: [PATCH 4/5] fixed typo --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index f6b756352..f1be13d61 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -72,7 +72,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::v(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // the idea is to implement the definition of globally as in the formula: // G phi = not(F(not psi)) = not(true U (not psi)) // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again From 60ce89872c6ced517c24f7021ea697bd8f83332e Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 1 Mar 2021 19:15:33 +0100 Subject: [PATCH 5/5] fixed another small typo --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index f1be13d61..ff8d213af 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -74,7 +74,7 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // the idea is to implement the definition of globally as in the formula: - // G phi = not(F(not psi)) = not(true U (not psi)) + // G psi = not(F(not psi)) = not(true U (not psi)) // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement();