From 85c5125610abbfc50165e6b401ad358b5f485320 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:51:10 +0200 Subject: [PATCH] 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);