diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp index b15b6aad6..06e4cb85d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp @@ -1,8 +1,8 @@ #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" -#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" -#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" -#include "storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" @@ -55,17 +55,17 @@ namespace storm { template>::value, int>::type> std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { if (preprocessorResult.containsOnlyTrivialObjectives()) { - return std::make_unique>(preprocessorResult); + return std::make_unique>(preprocessorResult); } else { STORM_LOG_DEBUG("Query contains reward bounded formula"); - return std::make_unique>(preprocessorResult); + return std::make_unique>(preprocessorResult); } } template template>::value, int>::type> std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { - return std::make_unique>(preprocessorResult); + return std::make_unique>(preprocessorResult); } template class PcaaWeightVectorChecker>; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp similarity index 91% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp rename to src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index 202992759..cc748983d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" @@ -32,7 +32,7 @@ namespace storm { namespace multiobjective { template - SparseMdpRewardBoundedPcaaWeightVectorChecker::SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) { + RewardBoundedMdpPcaaWeightVectorChecker::RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); @@ -48,7 +48,7 @@ namespace storm { } template - SparseMdpRewardBoundedPcaaWeightVectorChecker::~SparseMdpRewardBoundedPcaaWeightVectorChecker() { + RewardBoundedMdpPcaaWeightVectorChecker::~RewardBoundedMdpPcaaWeightVectorChecker() { swAll.stop(); if (storm::settings::getModule().isShowStatisticsSet()) { STORM_PRINT_AND_LOG("--------------------------------------------------" << std::endl); @@ -65,7 +65,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(Environment const& env, std::vector const& weightVector) { + void RewardBoundedMdpPcaaWeightVectorChecker::check(Environment const& env, std::vector const& weightVector) { ++numChecks; STORM_LOG_INFO("Analyzing weight vector #" << numChecks << ": " << storm::utility::vector::toString(weightVector)); @@ -120,7 +120,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData) { + void RewardBoundedMdpPcaaWeightVectorChecker::computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData) { ++numCheckedEpochs; swEpochModelBuild.start(); @@ -309,7 +309,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { + void RewardBoundedMdpPcaaWeightVectorChecker::updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector) { if (epochModel.epochMatrixChanged) { // Update the cached MinMaxSolver data @@ -349,20 +349,20 @@ namespace storm { } template - std::vector::ValueType> SparseMdpRewardBoundedPcaaWeightVectorChecker::getUnderApproximationOfInitialStateResults() const { + std::vector::ValueType> RewardBoundedMdpPcaaWeightVectorChecker::getUnderApproximationOfInitialStateResults() const { STORM_LOG_THROW(underApproxResult, storm::exceptions::InvalidOperationException, "Tried to retrieve results but check(..) has not been called before."); return underApproxResult.get(); } template - std::vector::ValueType> SparseMdpRewardBoundedPcaaWeightVectorChecker::getOverApproximationOfInitialStateResults() const { + std::vector::ValueType> RewardBoundedMdpPcaaWeightVectorChecker::getOverApproximationOfInitialStateResults() const { STORM_LOG_THROW(overApproxResult, storm::exceptions::InvalidOperationException, "Tried to retrieve results but check(..) has not been called before."); return overApproxResult.get(); } - template class SparseMdpRewardBoundedPcaaWeightVectorChecker>; + template class RewardBoundedMdpPcaaWeightVectorChecker>; #ifdef STORM_HAVE_CARL - template class SparseMdpRewardBoundedPcaaWeightVectorChecker>; + template class RewardBoundedMdpPcaaWeightVectorChecker>; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h similarity index 92% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h rename to src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h index 4ef24793e..0013cdc3d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h @@ -20,14 +20,14 @@ namespace storm { * - computes for each objective the value induced by this scheduler */ template - class SparseMdpRewardBoundedPcaaWeightVectorChecker : public PcaaWeightVectorChecker { + class RewardBoundedMdpPcaaWeightVectorChecker : public PcaaWeightVectorChecker { public: typedef typename SparseMdpModelType::ValueType ValueType; typedef typename SparseMdpModelType::RewardModelType RewardModelType; - SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker(); + virtual ~RewardBoundedMdpPcaaWeightVectorChecker(); /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp similarity index 83% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp rename to src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 44bf2eb7a..8505ab035 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h" #include @@ -23,13 +23,13 @@ namespace storm { template - SparseMaPcaaWeightVectorChecker::SparseMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : - SparsePcaaWeightVectorChecker(preprocessorResult) { + StandardMaPcaaWeightVectorChecker::StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardPcaaWeightVectorChecker(preprocessorResult) { this->initialize(preprocessorResult); } template - void SparseMaPcaaWeightVectorChecker::initializeModelTypeSpecificData(SparseMaModelType const& model) { + void StandardMaPcaaWeightVectorChecker::initializeModelTypeSpecificData(SparseMaModelType const& model) { markovianStates = model.getMarkovianStates(); exitRates = model.getExitRates(); @@ -59,7 +59,7 @@ namespace storm { template - void SparseMaPcaaWeightVectorChecker::boundedPhase(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) { + void StandardMaPcaaWeightVectorChecker::boundedPhase(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) { // Split the preprocessed model into transitions from/to probabilistic/Markovian states. SubModel MS = createSubModel(true, weightedRewardVector); @@ -116,7 +116,7 @@ namespace storm { } template - typename SparseMaPcaaWeightVectorChecker::SubModel SparseMaPcaaWeightVectorChecker::createSubModel(bool createMS, std::vector const& weightedRewardVector) const { + typename StandardMaPcaaWeightVectorChecker::SubModel StandardMaPcaaWeightVectorChecker::createSubModel(bool createMS, std::vector const& weightedRewardVector) const { SubModel result; storm::storage::BitVector probabilisticStates = ~markovianStates; @@ -157,7 +157,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - VT SparseMaPcaaWeightVectorChecker::getDigitizationConstant(std::vector const& weightVector) const { + VT StandardMaPcaaWeightVectorChecker::getDigitizationConstant(std::vector const& weightVector) const { STORM_LOG_DEBUG("Retrieving digitization constant"); // We need to find a delta such that for each objective it holds that lowerbound/delta , upperbound/delta are natural numbers and // sum_{obj_i} ( @@ -228,13 +228,13 @@ namespace storm { template template ::SupportsExponential, int>::type> - VT SparseMaPcaaWeightVectorChecker::getDigitizationConstant(std::vector const& weightVector) const { + VT StandardMaPcaaWeightVectorChecker::getDigitizationConstant(std::vector const& weightVector) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitize(SubModel& MS, VT const& digitizationConstant) const { + void StandardMaPcaaWeightVectorChecker::digitize(SubModel& MS, VT const& digitizationConstant) const { std::vector rateVector(MS.getNumberOfChoices()); storm::utility::vector::selectVectorValues(rateVector, MS.states, exitRates); for (uint_fast64_t row = 0; row < rateVector.size(); ++row) { @@ -257,13 +257,13 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitize(SubModel& subModel, VT const& digitizationConstant) const { + void StandardMaPcaaWeightVectorChecker::digitize(SubModel& subModel, VT const& digitizationConstant) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void StandardMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { VT const maxRate = storm::utility::vector::max_if(exitRates, markovianStates); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { @@ -291,12 +291,12 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void StandardMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } template - std::unique_ptr::MinMaxSolverData> SparseMaPcaaWeightVectorChecker::initMinMaxSolver(Environment const& env, SubModel const& PS, std::vector const& weightVector) const { + std::unique_ptr::MinMaxSolverData> StandardMaPcaaWeightVectorChecker::initMinMaxSolver(Environment const& env, SubModel const& PS, std::vector const& weightVector) const { std::unique_ptr result(new MinMaxSolverData()); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; result->solver = minMaxSolverFactory.create(env, PS.toPS); @@ -325,7 +325,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(Environment const& env, SubModel const& PS) const { + std::unique_ptr::LinEqSolverData> StandardMaPcaaWeightVectorChecker::initLinEqSolver(Environment const& env, SubModel const& PS) const { std::unique_ptr result(new LinEqSolverData()); result->env = std::make_unique(); // Unless the solver / method was explicitly specified, we switch it to Native / Power. @@ -342,12 +342,12 @@ namespace storm { template template ::SupportsExponential, int>::type> - std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(Environment const& env, SubModel const& PS) const { + std::unique_ptr::LinEqSolverData> StandardMaPcaaWeightVectorChecker::initLinEqSolver(Environment const& env, SubModel const& PS) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } template - void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { + void StandardMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { if (upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { consideredObjectives |= upperTimeBoundIt->second; @@ -366,7 +366,7 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::performPSStep(Environment const& env, SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { + void StandardMaPcaaWeightVectorChecker::performPSStep(Environment const& env, SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(env, PS.weightedSolutionVector, minMax.b); auto const& newChoices = minMax.solver->getSchedulerChoices(); @@ -415,7 +415,7 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::performMSStep(Environment const& env, SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { + void StandardMaPcaaWeightVectorChecker::performMSStep(Environment const& env, SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { MS.toMS.multiplyWithVector(MS.weightedSolutionVector, MS.auxChoiceValues); storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); @@ -438,17 +438,17 @@ namespace storm { } - template class SparseMaPcaaWeightVectorChecker>; - template double SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; - template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; - template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds( SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); - template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; + template class StandardMaPcaaWeightVectorChecker>; + template double StandardMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; + template void StandardMaPcaaWeightVectorChecker>::digitize(StandardMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; + template void StandardMaPcaaWeightVectorChecker>::digitizeTimeBounds( StandardMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); + template std::unique_ptr>::LinEqSolverData> StandardMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, StandardMaPcaaWeightVectorChecker>::SubModel const& PS ) const; #ifdef STORM_HAVE_CARL - template class SparseMaPcaaWeightVectorChecker>; - template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; - template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; - template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); - template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; + template class StandardMaPcaaWeightVectorChecker>; + template storm::RationalNumber StandardMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; + template void StandardMaPcaaWeightVectorChecker>::digitize(StandardMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; + template void StandardMaPcaaWeightVectorChecker>::digitizeTimeBounds(StandardMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); + template std::unique_ptr>::LinEqSolverData> StandardMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, StandardMaPcaaWeightVectorChecker>::SubModel const& PS ) const; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h similarity index 95% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h rename to src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h index a0a98f750..db62018d2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h @@ -4,7 +4,7 @@ #include #include -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h" #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/utility/NumberTraits.h" @@ -20,13 +20,13 @@ namespace storm { * - computes for each objective the value induced by this scheduler */ template - class SparseMaPcaaWeightVectorChecker : public SparsePcaaWeightVectorChecker { + class StandardMaPcaaWeightVectorChecker : public StandardPcaaWeightVectorChecker { public: typedef typename SparseMaModelType::ValueType ValueType; - SparseMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparseMaPcaaWeightVectorChecker() = default; + virtual ~StandardMaPcaaWeightVectorChecker() = default; protected: virtual void initializeModelTypeSpecificData(SparseMaModelType const& model) override; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp similarity index 88% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp rename to src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp index 3a194d37c..f744b0cee 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" @@ -21,13 +21,13 @@ namespace storm { namespace multiobjective { template - SparseMdpPcaaWeightVectorChecker::SparseMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : - SparsePcaaWeightVectorChecker(preprocessorResult) { + StandardMdpPcaaWeightVectorChecker::StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardPcaaWeightVectorChecker(preprocessorResult) { this->initialize(preprocessorResult); } template - void SparseMdpPcaaWeightVectorChecker::initializeModelTypeSpecificData(SparseMdpModelType const& model) { + void StandardMdpPcaaWeightVectorChecker::initializeModelTypeSpecificData(SparseMdpModelType const& model) { // set the state action rewards. Also do some sanity checks on the objectives. this->actionRewards.resize(this->objectives.size()); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { @@ -47,7 +47,7 @@ namespace storm { } template - void SparseMdpPcaaWeightVectorChecker::boundedPhase(Environment const& env,std::vector const& weightVector, std::vector& weightedRewardVector) { + void StandardMdpPcaaWeightVectorChecker::boundedPhase(Environment const& env,std::vector const& weightVector, std::vector& weightedRewardVector) { // Allocate some memory so this does not need to happen for each time epoch std::vector optimalChoicesInCurrentEpoch(this->transitionMatrix.getRowGroupCount()); std::vector choiceValues(weightedRewardVector.size()); @@ -114,9 +114,9 @@ namespace storm { } } - template class SparseMdpPcaaWeightVectorChecker>; + template class StandardMdpPcaaWeightVectorChecker>; #ifdef STORM_HAVE_CARL - template class SparseMdpPcaaWeightVectorChecker>; + template class StandardMdpPcaaWeightVectorChecker>; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h similarity index 85% rename from src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h rename to src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h index 857ed454d..071f168a2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h @@ -3,7 +3,7 @@ #include -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h" #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" namespace storm { @@ -17,7 +17,7 @@ namespace storm { * - computes for each objective the value induced by this scheduler */ template - class SparseMdpPcaaWeightVectorChecker : public SparsePcaaWeightVectorChecker { + class StandardMdpPcaaWeightVectorChecker : public StandardPcaaWeightVectorChecker { public: typedef typename SparseMdpModelType::ValueType ValueType; typedef typename SparseMdpModelType::RewardModelType RewardModelType; @@ -32,9 +32,9 @@ namespace storm { * */ - SparseMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparseMdpPcaaWeightVectorChecker() = default; + virtual ~StandardMdpPcaaWeightVectorChecker() = default; protected: virtual void initializeModelTypeSpecificData(SparseMdpModelType const& model) override; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp similarity index 93% rename from src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp rename to src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 370b51da6..8ce496426 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -1,4 +1,4 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h" #include #include @@ -27,7 +27,7 @@ namespace storm { template - SparsePcaaWeightVectorChecker::SparsePcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardPcaaWeightVectorChecker::StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives) { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported."); @@ -38,7 +38,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::initialize(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { + void StandardPcaaWeightVectorChecker::initialize(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers. // We can also merge the states that will have reward zero anyway. storm::storage::BitVector maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates; @@ -90,7 +90,7 @@ namespace storm { template - void SparsePcaaWeightVectorChecker::check(Environment const& env, std::vector const& weightVector) { + void StandardPcaaWeightVectorChecker::check(Environment const& env, std::vector const& weightVector) { checkHasBeenCalled = true; STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); @@ -121,7 +121,7 @@ namespace storm { } template - std::vector::ValueType> SparsePcaaWeightVectorChecker::getUnderApproximationOfInitialStateResults() const { + std::vector::ValueType> StandardPcaaWeightVectorChecker::getUnderApproximationOfInitialStateResults() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); std::vector res; res.reserve(this->objectives.size()); @@ -132,7 +132,7 @@ namespace storm { } template - std::vector::ValueType> SparsePcaaWeightVectorChecker::getOverApproximationOfInitialStateResults() const { + std::vector::ValueType> StandardPcaaWeightVectorChecker::getOverApproximationOfInitialStateResults() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); std::vector res; res.reserve(this->objectives.size()); @@ -143,7 +143,7 @@ namespace storm { } template - storm::storage::Scheduler::ValueType> SparsePcaaWeightVectorChecker::computeScheduler() const { + storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeScheduler() const { STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); for (auto const& obj : this->objectives) { STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound."); @@ -159,7 +159,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(Environment const& env, std::vector const& weightedRewardVector, std::vector const& weightVector) { + void StandardPcaaWeightVectorChecker::unboundedWeightedPhase(Environment const& env, std::vector const& weightedRewardVector, std::vector const& weightVector) { if (this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { this->weightedResult = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -201,7 +201,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(Environment const& env,std::vector const& weightVector) { + void StandardPcaaWeightVectorChecker::unboundedIndividualPhase(Environment const& env,std::vector const& weightVector) { if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin(); objectiveResults[objIndex] = weightedResult; @@ -294,7 +294,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::updateEcQuotient(std::vector const& weightedRewardVector) { + void StandardPcaaWeightVectorChecker::updateEcQuotient(std::vector const& weightedRewardVector) { // Check whether we need to update the currently cached ecElimResult storm::storage::BitVector newReward0Choices = storm::utility::vector::filterZero(weightedRewardVector); if (!ecQuotient || ecQuotient->origReward0Choices != newReward0Choices) { @@ -325,7 +325,7 @@ namespace storm { template - void SparsePcaaWeightVectorChecker::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, + void StandardPcaaWeightVectorChecker::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, std::vector const& reducedSolution, std::vector const& reducedOptimalChoices, std::vector const& reducedToOriginalChoiceMapping, @@ -422,11 +422,11 @@ namespace storm { - template class SparsePcaaWeightVectorChecker>; - template class SparsePcaaWeightVectorChecker>; + template class StandardPcaaWeightVectorChecker>; + template class StandardPcaaWeightVectorChecker>; #ifdef STORM_HAVE_CARL - template class SparsePcaaWeightVectorChecker>; - template class SparsePcaaWeightVectorChecker>; + template class StandardPcaaWeightVectorChecker>; + template class StandardPcaaWeightVectorChecker>; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h similarity index 96% rename from src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h rename to src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index faa85209a..86cd79c7f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -20,7 +20,7 @@ namespace storm { * - computes for each objective the value induced by this scheduler */ template - class SparsePcaaWeightVectorChecker : public PcaaWeightVectorChecker { + class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker { public: typedef typename SparseModelType::ValueType ValueType; @@ -34,9 +34,9 @@ namespace storm { * */ - SparsePcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparsePcaaWeightVectorChecker() = default; + virtual ~StandardPcaaWeightVectorChecker() = default; /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives