From 77e086f446d78c98a3bae5d049fcbef8948f2dcc Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 13 Sep 2015 16:12:54 +0200 Subject: [PATCH] small fix regarding the return type of computeValue Former-commit-id: 78b43e0f6dc78710c5223ac34b08372d8547e6cc --- .../region/AbstractSparseRegionModelChecker.cpp | 15 +++++++++------ src/modelchecker/region/ApproximationModel.cpp | 4 ++-- src/modelchecker/region/ApproximationModel.h | 3 ++- src/modelchecker/region/SamplingModel.cpp | 8 ++++---- src/modelchecker/region/SamplingModel.h | 3 ++- 5 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index 2bb506a20..a03506db1 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -9,6 +9,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/modelchecker/region/RegionCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/logic/Formulas.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/settings/SettingsManager.h" @@ -24,6 +25,8 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/UnexpectedException.h" #include "utility/ConversionHelper.h" +#include "modelchecker/results/CheckResult.h" +#include "modelchecker/results/ExplicitQuantitativeCheckResult.h" namespace storm { namespace modelchecker { @@ -138,7 +141,7 @@ namespace storm { initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula()); std::map emptySubstitution; this->getSamplingModel()->instantiate(emptySubstitution); - this->constantResult = this->getSamplingModel()->computeValues()[*this->getSamplingModel()->getModel()->getInitialStates().begin()]; + this->constantResult = this->getSamplingModel()->computeValues()->template asExplicitQuantitativeCheckResult().getValueVector()[*this->getSamplingModel()->getModel()->getInitialStates().begin()]; } //some more information for statistics... @@ -317,13 +320,13 @@ namespace storm { bool formulaSatisfied; if((this->specifiedFormulaHasUpperBound() && proveAllSat) || (!this->specifiedFormulaHasUpperBound() && !proveAllSat)){ //these are the cases in which we need to compute upper bounds - upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); + upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult().getValueVector(); lowerBounds = std::vector(); formulaSatisfied = this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ //for the remaining cases we compute lower bounds - lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); + lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize)->template asExplicitQuantitativeCheckResult().getValueVector(); upperBounds = std::vector(); formulaSatisfied = this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } @@ -343,11 +346,11 @@ namespace storm { proveAllSat=!proveAllSat; if(lowerBounds.empty()){ - lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); + lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize)->template asExplicitQuantitativeCheckResult().getValueVector(); formulaSatisfied=this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } else{ - upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); + upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult().getValueVector(); formulaSatisfied=this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); } @@ -391,7 +394,7 @@ namespace storm { return this->constantResult.get(); } this->getSamplingModel()->instantiate(point); - return this->getSamplingModel()->computeValues()[*this->getSamplingModel()->getModel()->getInitialStates().begin()]; + return this->getSamplingModel()->computeValues()->template asExplicitQuantitativeCheckResult().getValueVector()[*this->getSamplingModel()->getModel()->getInitialStates().begin()]; } template diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index f45f5fc77..d32c99d6f 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -343,7 +343,7 @@ namespace storm { } template - std::vector const& ApproximationModel::computeValues(storm::solver::OptimizationDirection const& approximationOpDir) { + std::unique_ptr ApproximationModel::computeValues(storm::solver::OptimizationDirection const& approximationOpDir) { std::unique_ptr modelChecker; switch(this->getModel()->getType()){ case storm::models::ModelType::Mdp: @@ -384,7 +384,7 @@ namespace storm { //perform model checking resultPtr = modelChecker->computeEventuallyProbabilities(this->formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(), false, approximationOpDir); } - return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); + return resultPtr; } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index 0e5866ab8..c79c50bc3 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -13,6 +13,7 @@ #include "src/utility/region.h" #include "src/modelchecker/region/ParameterRegion.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/logic/Formulas.h" #include "src/models/sparse/Model.h" #include "src/storage/SparseMatrix.h" @@ -49,7 +50,7 @@ namespace storm { * Undefined behavior if model has not been instantiated first! * @param approximationOpDir Use MAXIMIZE to get upper bounds or MINIMIZE to get lower bounds */ - std::vector const& computeValues(storm::solver::OptimizationDirection const& approximationOpDir); + std::unique_ptr computeValues(storm::solver::OptimizationDirection const& approximationOpDir); private: diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 2ff5a37e5..8249e3d62 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -13,7 +13,6 @@ #include "models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/macros.h" #include "src/utility/region.h" #include "src/utility/vector.h" @@ -185,7 +184,7 @@ namespace storm { } template - std::vector const& SamplingModel::computeValues() { + std::unique_ptr SamplingModel::computeValues() { std::unique_ptr modelChecker; switch(this->getModel()->getType()){ case storm::models::ModelType::Dtmc: @@ -204,9 +203,10 @@ namespace storm { resultPtr = modelChecker->computeReachabilityRewards(this->formula->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula()); } else { - resultPtr = modelChecker->computeEventuallyProbabilities(this->formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(), false, opDir); + storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), this->formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asSharedPointer()); + resultPtr = modelChecker->computeUntilProbabilities(newFormula, false, opDir); } - return resultPtr->asExplicitQuantitativeCheckResult().getValueVector(); + return resultPtr; } #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 5f8bd27e9..244be97d1 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -14,6 +14,7 @@ #include "src/utility/region.h" #include "src/logic/Formulas.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/models/sparse/Model.h" #include "src/storage/SparseMatrix.h" @@ -47,7 +48,7 @@ namespace storm { * Returns the reachability probabilities (or the expected rewards) for every state according to the current instantiation. * Undefined behavior if model has not been instantiated first! */ - std::vector const& computeValues(); + std::unique_ptr computeValues(); private: