From 85c5125610abbfc50165e6b401ad358b5f485320 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:51:10 +0200 Subject: [PATCH 1/4] removed duplicate code after big merge --- src/storm/logic/Formula.h | 3 -- src/storm/logic/FragmentSpecification.cpp | 29 ----------------- .../prctl/SparseDtmcPrctlModelChecker.cpp | 31 ++----------------- 3 files changed, 2 insertions(+), 61 deletions(-) diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 0c83e718c..29eba01ff 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -149,9 +149,6 @@ namespace storm { HOAPathFormula& asHOAPathFormula(); HOAPathFormula const& asHOAPathFormula() const; - HOAPathFormula& asHOAPathFormula(); - HOAPathFormula const& asHOAPathFormula() const; - BoundedUntilFormula& asBoundedUntilFormula(); BoundedUntilFormula const& asBoundedUntilFormula() const; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index b75dca240..2272ef61f 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -114,35 +114,6 @@ namespace storm { return rpatl; } - FragmentSpecification prctl() { - FragmentSpecification prctl = pctl(); - - prctl.setRewardOperatorsAllowed(true); - prctl.setCumulativeRewardFormulasAllowed(true); - prctl.setInstantaneousFormulasAllowed(true); - prctl.setReachabilityRewardFormulasAllowed(true); - prctl.setLongRunAverageOperatorsAllowed(true); - prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); - prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); - - return prctl; - } - - FragmentSpecification prctlstar() { - FragmentSpecification prctlstar = pctlstar(); - - prctlstar.setRewardOperatorsAllowed(true); - prctlstar.setCumulativeRewardFormulasAllowed(true); - prctlstar.setInstantaneousFormulasAllowed(true); - prctlstar.setReachabilityRewardFormulasAllowed(true); - prctlstar.setLongRunAverageOperatorsAllowed(true); - prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true); - prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true); - - return prctlstar; - - } - FragmentSpecification csl() { FragmentSpecification csl = pctl(); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 645564aa6..09791cf34 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -117,41 +117,14 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - - auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; - auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); - std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - } - - template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - - auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; - std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); - - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - } - template - std::unique_ptr SparseDtmcPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { - storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -161,7 +134,7 @@ namespace storm { storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); From d53fafa07875ec8f4017b7327548641a207ff9e8 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:51:20 +0200 Subject: [PATCH 2/4] fixed some changes which have been overwritten --- src/storm/storage/Scheduler.cpp | 4 ++-- src/storm/storage/Scheduler.h | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 6405528a0..a7acff700 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -323,9 +323,9 @@ namespace storm { } } if (numOfSkippedStatesWithUniqueChoice > 0) { - stateString << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; + out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; } - stateString << "___________________________________________________________________" << std::endl; + out << "___________________________________________________________________" << std::endl; } diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 96819be58..5e8aa3e5e 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -143,8 +143,9 @@ namespace storm { * Prints the scheduler in json format to the given output stream. */ void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false, bool skipDontCareStates = false) const; + void setPrintUndefinedChoices(bool value); - private: + protected: boost::optional memoryStructure; std::vector>> schedulerChoices; From c19639d1560135854e20b760c4cfc72713ed42a5 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:51:35 +0200 Subject: [PATCH 3/4] added missing method to visitor --- src/storm/logic/ToPrefixStringVisitor.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/logic/ToPrefixStringVisitor.cpp b/src/storm/logic/ToPrefixStringVisitor.cpp index 300a53d97..fcfede03f 100644 --- a/src/storm/logic/ToPrefixStringVisitor.cpp +++ b/src/storm/logic/ToPrefixStringVisitor.cpp @@ -59,6 +59,11 @@ namespace storm { return result; } + boost::any ToPrefixStringVisitor::visit(BoundedGloballyFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); + } + + boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string"); } From 90dba4cd5dd803255658bcd97e470aa3f2a14fc2 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:51:50 +0200 Subject: [PATCH 4/4] adapted mdpprctlhelper call in MA model checker --- .../SparseMarkovAutomatonCslModelChecker.cpp | 44 +++++++++---------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 7afb03f38..ac95d09ad 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { SparseMarkovAutomatonCslModelChecker::SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } - + template bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { auto singleObjectiveFragment = storm::logic::csrlstar().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); @@ -48,7 +48,7 @@ namespace storm { } return false; } - + template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { bool requiresSingleInitialState = false; @@ -58,7 +58,7 @@ namespace storm { return false; } } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); @@ -85,18 +85,18 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound)); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - - + + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), 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(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.values))); } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); @@ -110,7 +110,7 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); @@ -131,14 +131,14 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); @@ -146,7 +146,7 @@ namespace storm { return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); @@ -155,7 +155,7 @@ namespace storm { storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -166,7 +166,7 @@ namespace storm { return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -183,7 +183,7 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); @@ -197,7 +197,7 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); @@ -216,13 +216,13 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long run average rewards in non-closed Markov automaton."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); @@ -233,7 +233,7 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -249,12 +249,12 @@ namespace storm { } return result; } - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) { return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula()); } - + template class SparseMarkovAutomatonCslModelChecker>; template class SparseMarkovAutomatonCslModelChecker>; }