#pragma once #include "storm/solver/AbstractEquationSolver.h" #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/Scheduler.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/transformer/EndComponentEliminator.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" #include "storm/utility/vector.h" #include "storm/storage/BoostTypes.h" namespace storm { namespace modelchecker { namespace multiobjective { /*! * Helper Class that takes preprocessed Pcaa data and a weight vector and ... * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ template class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker { public: typedef typename SparseModelType::ValueType ValueType; using DeterministicInfiniteHorizonHelperType = typename std::conditional>::value, storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper, storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper>::type; /* * Creates a weight vextor checker. * * @param model The (preprocessed) model * @param objectives The (preprocessed) objectives * @param possibleECActions Overapproximation of the actions that are part of an EC * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 * */ StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ 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. * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown. * Also note that there is no guarantee that the under/over approximation is in fact correct * as long as the underlying solution methods are unsound (e.g., standard value iteration). */ virtual std::vector getUnderApproximationOfInitialStateResults() const override; virtual std::vector getOverApproximationOfInitialStateResults() const override; /*! * Retrieves a scheduler that induces the current values * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. * Also note that (currently) the scheduler only supports unbounded objectives. */ virtual storm::storage::Scheduler computeScheduler() const override; protected: void initialize(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const = 0; virtual DeterministicInfiniteHorizonHelperType createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const = 0; void infiniteHorizonWeightedPhase(Environment const& env, std::vector const& weightedActionRewardVector, boost::optional> const& weightedStateRewardVector); /*! * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives * * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ 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(Environment const& env, std::vector const& weightVector); /*! * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method * - determines the objectives that are relevant in the current time epoch * - determines the maximizing scheduler for the weighted reward vector of these objectives * - computes the values of these objectives w.r.t. this scheduler * * @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(Environment const& env, std::vector const& weightVector, std::vector& weightedRewardVector) = 0; void updateEcQuotient(std::vector const& weightedRewardVector); void setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; void setBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, std::vector const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector const& rewards) const; /*! * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model */ void transformEcqSolutionToOriginalModel(std::vector const& ecqSolution, std::vector const& ecqOptimalChoices, std::map const& ecqStateToOptimalMecMap, std::vector& originalSolution, std::vector& originalOptimalChoices) const; // Data regarding the given model // The transition matrix of the considered model storm::storage::SparseMatrix transitionMatrix; // The initial state of the considered model uint64_t initialState; // Overapproximation of the set of choices that are part of an end component. storm::storage::BitVector ecChoicesHint; // The actions that have reward assigned for at least one objective without upper timeBound storm::storage::BitVector actionsWithoutRewardInUnboundedPhase; // The states for which there is a scheduler yielding reward 0 for each total reward objective storm::storage::BitVector totalReward0EStates; // stores the state action rewards for each objective. std::vector> actionRewards; // stores the state rewards for each objective. // These are only relevant for LRA objectives for MAs (otherwise, they appear within the action rewards). For other objectives/models, the corresponding vector will be empty. std::vector> stateRewards; // stores the indices of the objectives for which we need to compute the long run average values storm::storage::BitVector lraObjectives; // stores the indices of the objectives for which there is no upper time bound storm::storage::BitVector objectivesWithNoUpperTimeBound; // Memory for the solution of the most recent call of check(..) // becomes true after the first call of check(..) bool checkHasBeenCalled; // The result for the weighted reward vector (for all states of the model) std::vector weightedResult; // The results for the individual objectives (w.r.t. all states of the model) std::vector> objectiveResults; // Stores for each objective the distance between the computed result (w.r.t. the initial state) and an over/under approximation for the actual result. // The distances are stored as a (possibly negative) offset that has to be added (+) to to the objectiveResults. std::vector offsetsToUnderApproximation; std::vector offsetsToOverApproximation; // The scheduler choices that optimize the weighted rewards of undounded objectives. std::vector optimalChoices; struct EcQuotient { storm::storage::SparseMatrix matrix; std::vector ecqToOriginalChoiceMapping; std::vector originalToEcqStateMapping; std::vector ecqToOriginalStateMapping; storm::storage::BitVector ecqStayInEcChoices; storm::storage::BitVector origReward0Choices; // includes total and LRA rewards storm::storage::BitVector origTotalReward0Choices; // considers just total rewards storm::storage::BitVector rowsWithSumLessOne; std::vector auxStateValues; std::vector auxChoiceValues; }; boost::optional ecQuotient; struct LraMecDecomposition { storm::storage::MaximalEndComponentDecomposition mecs; std::vector auxMecValues; }; boost::optional lraMecDecomposition; }; } } }