diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 1d03397ca..026c1fa5c 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -129,7 +129,7 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) { - return multiobjective::performMultiObjectiveModelChecking(this->getModel(), checkTask.getFormula()); + return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula()); } template class SparseMarkovAutomatonCslModelChecker>; diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index ef33a1ab4..ae03a7d9e 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -31,7 +31,7 @@ namespace storm { } template - std::unique_ptr SparseCbAchievabilityQuery::check() { + std::unique_ptr SparseCbAchievabilityQuery::check(Environment const& env) { bool result = this->checkAchievability(); diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h index 3ccb69b40..215555835 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h @@ -26,7 +26,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() override; + virtual std::unique_ptr check(Environment const& env) override; private: diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h index 8d22580aa..1e7f0879a 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h @@ -7,6 +7,9 @@ #include "storm/storage/expressions/ExpressionManager.h" namespace storm { + + class Environment; + namespace modelchecker { namespace multiobjective { @@ -23,7 +26,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() = 0; + virtual std::unique_ptr check(Environment const& env) = 0; protected: diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index a64e471ee..10276ffa6 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -23,7 +23,7 @@ namespace storm { namespace multiobjective { template - std::unique_ptr performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection) { + std::unique_ptr performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection) { storm::utility::Stopwatch swTotal(true); storm::utility::Stopwatch swPreprocessing(true); STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); @@ -72,7 +72,7 @@ namespace storm { break; } - result = query->check(); + result = query->check(env); if(storm::settings::getModule().isExportPlotSet()) { query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); @@ -91,7 +91,7 @@ namespace storm { break; } - result = query->check(); + result = query->check(env); if(storm::settings::getModule().isExportPlotSet()) { STORM_LOG_ERROR("Can not export plot for the constrained based solver."); @@ -112,10 +112,10 @@ namespace storm { } - template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); } } diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h index 380f79384..be0a7ef6e 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h @@ -7,12 +7,15 @@ #include "storm/logic/Formulas.h" namespace storm { + + class Environment; + namespace modelchecker { namespace multiobjective { template - std::unique_ptr performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS); + std::unique_ptr performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h index aefa139b8..4bdbe3dc3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h @@ -10,6 +10,9 @@ namespace storm { + + class Environment; + namespace modelchecker { namespace multiobjective { @@ -35,7 +38,7 @@ namespace storm { virtual ~PcaaWeightVectorChecker() = default; - virtual void check(std::vector const& weightVector) = 0; + virtual void check(Environment const& env, std::vector const& weightVector) = 0; /*! * Retrieves the results of the individual objectives at the initial state of the given model. diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 8597fdc42..2aedebbe3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -57,7 +57,7 @@ namespace storm { template - void SparseMaPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { + void SparseMaPcaaWeightVectorChecker::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); @@ -73,11 +73,11 @@ namespace storm { // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch // No EC elimination is necessary as we assume non-zenoness - std::unique_ptr minMax = initMinMaxSolver(PS, weightVector); + std::unique_ptr minMax = initMinMaxSolver(env, PS, weightVector); // create a linear equation solver for the model induced by the optimal choice vector. // the solver will be updated whenever the optimal choice vector has changed. - std::unique_ptr linEq = initLinEqSolver(PS); + std::unique_ptr linEq = initLinEqSolver(env, PS); // Store the optimal choices of PS as computed by the minMax solver. std::vector optimalChoicesAtCurrentEpoch(PS.getNumberOfStates(), std::numeric_limits::max()); @@ -92,12 +92,12 @@ namespace storm { updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, upperTimeBoundIt, upperTimeBounds); // Compute the values that can be obtained at probabilistic states in the current time epoch - performPSStep(PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch, consideredObjectives, weightVector); + performPSStep(env, PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch, consideredObjectives, weightVector); // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass. // Only perform such a step if there is time left. if (currentEpoch>0) { - performMSStep(MS, PS, consideredObjectives, weightVector); + performMSStep(env, MS, PS, consideredObjectives, weightVector); --currentEpoch; } else { break; @@ -113,7 +113,6 @@ namespace storm { } } - template typename SparseMaPcaaWeightVectorChecker::SubModel SparseMaPcaaWeightVectorChecker::createSubModel(bool createMS, std::vector const& weightedRewardVector) const { SubModel result; @@ -295,14 +294,14 @@ namespace storm { } template - std::unique_ptr::MinMaxSolverData> SparseMaPcaaWeightVectorChecker::initMinMaxSolver(SubModel const& PS, std::vector const& weightVector) const { + std::unique_ptr::MinMaxSolverData> SparseMaPcaaWeightVectorChecker::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(PS.toPS); + result->solver = minMaxSolverFactory.create(env, PS.toPS); result->solver->setHasUniqueSolution(true); result->solver->setTrackScheduler(true); result->solver->setCachingEnabled(true); - auto req = result->solver->getRequirements(storm::solver::OptimizationDirection::Maximize); + auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize); boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true)); if (lowerBound) { result->solver->setLowerBound(lowerBound.get()); @@ -324,7 +323,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(SubModel const& PS) const { + std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(Environment const& env, SubModel const& PS) const { std::unique_ptr result(new LinEqSolverData()); auto factory = std::make_unique>(); // We choose Jacobi since we call the solver very frequently on 'easy' inputs (note that jacobi without preconditioning has very little overhead). @@ -336,7 +335,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(SubModel const& PS) const { + std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::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."); } @@ -360,9 +359,9 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { + 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 { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector - minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); + minMax.solver->solveEquations(env, PS.weightedSolutionVector, minMax.b); auto const& newChoices = minMax.solver->getSchedulerChoices(); if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives @@ -409,7 +408,7 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { + void SparseMaPcaaWeightVectorChecker::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); @@ -436,13 +435,13 @@ namespace storm { 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( SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; + template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, SparseMaPcaaWeightVectorChecker>::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( SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; + template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver(Environment const& env, SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index af8dd0e91..790db57d7 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -79,7 +79,7 @@ namespace storm { * @param weightVector the weight vector of the current check * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; + virtual void boundedPhase(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) override; /*! * Retrieves the data for a submodel of the data->preprocessedModel @@ -117,15 +117,15 @@ namespace storm { /*! * Initializes the data for the MinMax solver */ - std::unique_ptr initMinMaxSolver(SubModel const& PS, std::vector const& weightVector) const; + std::unique_ptr initMinMaxSolver(Environment const& env, SubModel const& PS, std::vector const& weightVector) const; /*! * Initializes the data for the LinEq solver */ template ::SupportsExponential, int>::type = 0> - std::unique_ptr initLinEqSolver(SubModel const& PS) const; + std::unique_ptr initLinEqSolver(Environment const& env, SubModel const& PS) const; template ::SupportsExponential, int>::type = 0> - std::unique_ptr initLinEqSolver(SubModel const& PS) const; + std::unique_ptr initLinEqSolver(Environment const& env, SubModel const& PS) const; /* * Updates the reward vectors within the split model, @@ -141,7 +141,7 @@ namespace storm { * * The resulting values represent the rewards at probabilistic states that are obtained at the current time epoch. */ - void performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const; + void 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; /* * Performs a step for the Markovian states, that is @@ -149,7 +149,7 @@ namespace storm { * * The resulting values represent the rewards at Markovian states that are obtained after one (digitized) time unit has passed. */ - void performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const; + void performMSStep(Environment const& env, SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const; // Data regarding the given Markov automaton diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index 4588779fe..3a194d37c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -33,7 +33,13 @@ namespace storm { for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& formula = *this->objectives[objIndex].formula; STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); - STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + if (formula.getSubformula().isCumulativeRewardFormula()) { + auto const& cumulativeRewardFormula = formula.getSubformula().asCumulativeRewardFormula(); + STORM_LOG_THROW(!cumulativeRewardFormula.isMultiDimensional() && !cumulativeRewardFormula.getTimeBoundReference().isRewardBound(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + } else { + STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + + } typename SparseMdpModelType::RewardModelType const& rewModel = model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); this->actionRewards[objIndex] = rewModel.getTotalRewardVector(model.getTransitionMatrix()); @@ -41,7 +47,7 @@ namespace storm { } template - void SparseMdpPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { + void SparseMdpPcaaWeightVectorChecker::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()); @@ -88,7 +94,6 @@ namespace storm { storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->transitionMatrix.getRowGroupIndices(), &optimalChoicesInCurrentEpoch); // get values for individual objectives - // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. for (auto objIndex : consideredObjectives) { std::vector& objectiveResult = this->objectiveResults[objIndex]; std::vector const& objectiveRewards = this->actionRewards[objIndex]; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h index 28687776f..857ed454d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h @@ -48,7 +48,7 @@ namespace storm { * @param weightVector the weight vector of the current check * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; + virtual void boundedPhase(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) override; }; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index f82fef6ac..95c3052c5 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -10,6 +10,10 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/environment/Environment.h" +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + #include "storm/settings/SettingsManager.h" #include "storm/utility/export.h" #include "storm/settings/modules/IOSettings.h" @@ -62,7 +66,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(std::vector const& weightVector) { + void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(Environment const& env, std::vector const& weightVector) { ++numChecks; STORM_LOG_INFO("Analyzing weight vector #" << numChecks << ": " << storm::utility::vector::toString(weightVector)); @@ -73,13 +77,14 @@ namespace storm { auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); EpochCheckingData cachedData; ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); - + Environment newEnv = env; + newEnv.solver().minMax().setPrecision(precision); storm::utility::ProgressMeasurement progress("epochs"); progress.setMaxCount(epochOrder.size()); progress.startNewMeasurement(0); uint64_t numCheckedEpochs = 0; for (auto const& epoch : epochOrder) { - computeEpochSolution(epoch, weightVector, cachedData, precision); + computeEpochSolution(newEnv, epoch, weightVector, cachedData); if (storm::settings::getModule().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { std::vector cdfEntry; for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) { @@ -115,7 +120,7 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData, ValueType const& precision) { + void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData) { ++numCheckedEpochs; swEpochModelBuild.start(); @@ -198,10 +203,7 @@ namespace storm { } } } else { - - - updateCachedData(epochModel, cachedData, weightVector, precision); - + updateCachedData(env, epochModel, cachedData, weightVector); // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives assert(cachedData.bMinMax.capacity() >= epochModel.epochMatrix.getRowCount()); @@ -223,7 +225,7 @@ namespace storm { } // Invoke the min max solver - cachedData.minMaxSolver->solveEquations(cachedData.xMinMax, cachedData.bMinMax); + cachedData.minMaxSolver->solveEquations(env, cachedData.xMinMax, cachedData.bMinMax); for (auto const& state : epochModel.epochInStates) { result.emplace_back(); result.back().reserve(solutionSize); @@ -243,7 +245,7 @@ namespace storm { subMatrix.convertToEquationSystem(); } cachedData.linEqSolver = linEqSolverFactory.create(std::move(subMatrix)); - cachedData.linEqSolver->setPrecision(precision); + cachedData.linEqSolver->setPrecision(storm::utility::convertNumber(env.solver().minMax().getPrecision())); cachedData.linEqSolver->setCachingEnabled(true); } @@ -308,19 +310,18 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::updateCachedData(typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector, ValueType const& precision) { + void SparseMdpRewardBoundedPcaaWeightVectorChecker::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 cachedData.bMinMax.resize(epochModel.epochMatrix.getRowCount()); cachedData.xMinMax.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxSolverFactory; - cachedData.minMaxSolver = minMaxSolverFactory.create(epochModel.epochMatrix); + cachedData.minMaxSolver = minMaxSolverFactory.create(env, epochModel.epochMatrix); cachedData.minMaxSolver->setHasUniqueSolution(); - cachedData.minMaxSolver->setPrecision(precision); cachedData.minMaxSolver->setTrackScheduler(true); cachedData.minMaxSolver->setCachingEnabled(true); - auto req = cachedData.minMaxSolver->getRequirements(); + auto req = cachedData.minMaxSolver->getRequirements(env); boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true)); if (lowerBound) { cachedData.minMaxSolver->setLowerBound(lowerBound.get()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 531f8b37c..4ef24793e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -34,7 +34,7 @@ namespace storm { * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ - virtual void check(std::vector const& weightVector) override; + virtual void check(Environment const& env, std::vector const& weightVector) override; /*! * Retrieves the results of the individual objectives at the initial state of the given model. @@ -62,9 +62,9 @@ namespace storm { std::vector::SolutionType> solutions; }; - void computeEpochSolution(typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData, ValueType const& precision); + void computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector, EpochCheckingData& cachedData); - void updateCachedData(typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector, ValueType const& precision); + void updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis; uint64_t numCheckedEpochs, numChecks; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index fde7aa351..409bd9ba9 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -46,21 +46,21 @@ namespace storm { } template - std::unique_ptr SparsePcaaAchievabilityQuery::check() { + std::unique_ptr SparsePcaaAchievabilityQuery::check(Environment const& env) { - bool result = this->checkAchievability(); + bool result = this->checkAchievability(env); return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); } template - bool SparsePcaaAchievabilityQuery::checkAchievability() { + bool SparsePcaaAchievabilityQuery::checkAchievability(Environment const& env) { // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx. while(!this->maxStepsPerformed()){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecision(separatingVector); - this->performRefinementStep(std::move(separatingVector)); + this->performRefinementStep(env, std::move(separatingVector)); if(!checkIfThresholdsAreSatisfied(this->overApproximation)){ return false; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h index 70531cdba..c5f3ae1a6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h @@ -30,7 +30,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() override; + virtual std::unique_ptr check(Environment const& env) override; private: @@ -39,7 +39,7 @@ namespace storm { /* * Returns whether the given thresholds are achievable. */ - bool checkAchievability(); + bool checkAchievability(Environment const& env); /* * Updates the precision of the weightVectorChecker w.r.t. the provided weights diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 778841289..fe7a7b367 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -31,10 +31,10 @@ namespace storm { } template - std::unique_ptr SparsePcaaParetoQuery::check() { + std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { // refine the approximation - exploreSetOfAchievablePoints(); + exploreSetOfAchievablePoints(env); // obtain the data for the checkresult std::vector> paretoOptimalPoints; @@ -52,13 +52,13 @@ namespace storm { } template - void SparsePcaaParetoQuery::exploreSetOfAchievablePoints() { + void SparsePcaaParetoQuery::exploreSetOfAchievablePoints(Environment const& env) { //First consider the objectives individually for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(); ++objIndex) { WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); - this->performRefinementStep(std::move(direction)); + this->performRefinementStep(env, std::move(direction)); } while(!this->maxStepsPerformed()) { @@ -82,7 +82,7 @@ namespace storm { } STORM_LOG_INFO("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber(farestDistance)); WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); - this->performRefinementStep(std::move(direction)); + this->performRefinementStep(env, std::move(direction)); } STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index 0e8bb2268..5208f00cd 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -31,7 +31,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() override; + virtual std::unique_ptr check(Environment const& env) override; private: @@ -39,7 +39,7 @@ namespace storm { /* * Performs refinement steps until the approximation is sufficiently precise */ - void exploreSetOfAchievablePoints(); + void exploreSetOfAchievablePoints(Environment const& env); }; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 2bbd64b37..538752ab2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -66,11 +66,11 @@ namespace storm { } template - std::unique_ptr SparsePcaaQuantitativeQuery::check() { + std::unique_ptr SparsePcaaQuantitativeQuery::check(Environment const& env) { // First find one solution that achieves the given thresholds ... - if (this->checkAchievability()) { + if (this->checkAchievability(env)) { // ... then improve it - GeometryValueType result = this->improveSolution(); + GeometryValueType result = this->improveSolution(env); // transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult auto const& obj = this->objectives[indexOfOptimizingObjective]; @@ -94,7 +94,7 @@ namespace storm { } template - bool SparsePcaaQuantitativeQuery::checkAchievability() { + bool SparsePcaaQuantitativeQuery::checkAchievability(Environment const& env) { if (this->objectives.size() > 1) { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); @@ -102,7 +102,7 @@ namespace storm { while(!this->maxStepsPerformed()){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecisionInAchievabilityPhase(separatingVector); - this->performRefinementStep(std::move(separatingVector)); + this->performRefinementStep(env, std::move(separatingVector)); //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded thresholds[indexOfOptimizingObjective] = std::min(thresholds[indexOfOptimizingObjective], this->refinementSteps.back().lowerBoundPoint[indexOfOptimizingObjective]); if (!checkIfThresholdsAreSatisfied(this->overApproximation)){ @@ -139,7 +139,7 @@ namespace storm { } template - GeometryValueType SparsePcaaQuantitativeQuery::improveSolution() { + GeometryValueType SparsePcaaQuantitativeQuery::improveSolution(Environment const& env) { this->diracWeightVectorsToBeChecked.clear(); // Only check weight vectors that can actually improve the solution WeightVector directionOfOptimizingObjective(this->objectives.size(), storm::utility::zero()); @@ -155,7 +155,7 @@ namespace storm { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(storm::settings::getModule().getPrecision())); WeightVector separatingVector = directionOfOptimizingObjective; - this->performRefinementStep(std::move(separatingVector)); + this->performRefinementStep(env, std::move(separatingVector)); } std::pair optimizationRes = this->underApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty."); @@ -177,7 +177,7 @@ namespace storm { } WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecisionInImprovingPhase(separatingVector); - this->performRefinementStep(std::move(separatingVector)); + this->performRefinementStep(env, std::move(separatingVector)); } STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); return result; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index 89e3fd111..164a87f21 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -30,7 +30,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() override; + virtual std::unique_ptr check(Environment const& env) override; private: @@ -39,7 +39,7 @@ namespace storm { /* * Returns whether the given thresholds are achievable. */ - bool checkAchievability(); + bool checkAchievability(Environment const& env); /* * Updates the precision of the weightVectorChecker w.r.t. the provided weights @@ -50,7 +50,7 @@ namespace storm { /* * Given that the thresholds are achievable, this function further refines the approximations and returns the optimized value */ - GeometryValueType improveSolution(); + GeometryValueType improveSolution(Environment const& env); /* * Returns true iff there is one point in the given polytope that satisfies the given thresholds. diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index e230d838b..2164665e0 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -73,10 +73,10 @@ namespace storm { } template - void SparsePcaaQuery::performRefinementStep(WeightVector&& direction) { + void SparsePcaaQuery::performRefinementStep(Environment const& env, WeightVector&& direction) { // Normalize the direction vector so that the entries sum up to one storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero())); - weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); + weightVectorChecker->check(env, storm::utility::vector::convertNumericVector(direction)); STORM_LOG_DEBUG("weighted objectives checker result (under approximation) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getUnderApproximationOfInitialStateResults()))); RefinementStep step; step.weightVector = direction; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index a85222ddf..d92f0ccee 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -7,6 +7,9 @@ #include "storm/storage/geometry/Polytope.h" namespace storm { + + class Environment; + namespace modelchecker { namespace multiobjective { @@ -27,7 +30,7 @@ namespace storm { /* * Invokes the computation and retrieves the result */ - virtual std::unique_ptr check() = 0; + virtual std::unique_ptr check(Environment const& env) = 0; /* * Exports the current approximations and the currently processed points into respective .csv files located at the given directory. @@ -65,7 +68,7 @@ namespace storm { /* * Refines the current result w.r.t. the given direction vector. */ - void performRefinementStep(WeightVector&& direction); + void performRefinementStep(Environment const& env, WeightVector&& direction); /* * Updates the overapproximation after a refinement step has been performed diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 45819b113..ff74ed473 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -90,7 +90,7 @@ namespace storm { template - void SparsePcaaWeightVectorChecker::check(std::vector const& weightVector) { + void SparsePcaaWeightVectorChecker::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))); @@ -103,13 +103,13 @@ namespace storm { } } - unboundedWeightedPhase(weightedRewardVector, weightVector); + unboundedWeightedPhase(env, weightedRewardVector, weightVector); - unboundedIndividualPhase(weightVector); + unboundedIndividualPhase(env, weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound for (auto const& obj : this->objectives) { if (!obj.formula->getSubformula().isTotalRewardFormula()) { - boundedPhase(weightVector, weightedRewardVector); + boundedPhase(env, weightVector, weightedRewardVector); break; } } @@ -159,7 +159,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, std::vector const& weightVector) { + void SparsePcaaWeightVectorChecker::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()); @@ -172,10 +172,10 @@ namespace storm { storm::utility::vector::selectVectorValues(ecQuotient->auxChoiceValues, ecQuotient->ecqToOriginalChoiceMapping, weightedRewardVector); storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(ecQuotient->matrix); + std::unique_ptr> solver = solverFactory.create(env, ecQuotient->matrix); solver->setTrackScheduler(true); solver->setHasUniqueSolution(true); - auto req = solver->getRequirements(); + auto req = solver->getRequirements(env); boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); if (lowerBound) { solver->setLowerBound(lowerBound.get()); @@ -187,13 +187,13 @@ namespace storm { req.clearUpperBounds(); } STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); - solver->setRequirementsChecked(true); + solver->setRequirementsChecked(env, true); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); // Use the (0...0) vector as initial guess for the solution. std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero()); - solver->solveEquations(ecQuotient->auxStateValues, ecQuotient->auxChoiceValues); + solver->solveEquations(env, ecQuotient->auxStateValues, ecQuotient->auxChoiceValues); this->weightedResult = std::vector(transitionMatrix.getRowGroupCount()); @@ -201,7 +201,7 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { + void SparsePcaaWeightVectorChecker::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; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 6365ad2dc..faa85209a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -43,7 +43,7 @@ namespace storm { * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ - virtual void check(std::vector const& weightVector) override; + virtual void check(Environment const& env, std::vector const& weightVector) override; /*! * Retrieves the results of the individual objectives at the initial state of the given model. @@ -72,13 +72,13 @@ namespace storm { * * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ - void unboundedWeightedPhase(std::vector const& weightedRewardVector, std::vector const& weightVector); + void unboundedWeightedPhase(Environment const& env, std::vector const& weightedRewardVector, std::vector const& weightVector); /*! * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase * */ - void unboundedIndividualPhase(std::vector const& weightVector); + void unboundedIndividualPhase(Environment const& env, std::vector const& weightVector); /*! * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method @@ -89,7 +89,7 @@ namespace storm { * @param weightVector the weight vector of the current check * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. */ - virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) = 0; + virtual void boundedPhase(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) = 0; void updateEcQuotient(std::vector const& weightedRewardVector); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 488fffb73..680b7ed27 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -197,7 +197,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) { - return multiobjective::performMultiObjectiveModelChecking(this->getModel(), checkTask.getFormula()); + return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula()); } template class SparseMdpPrctlModelChecker>;