StandardPcaaWeightVectorChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h"
#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
#include "storm/solver/AbstractEquationSolver.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/BoostTypes.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/utility/vector.h"
 
namespace storm {
namespace modelchecker {
namespace multiobjective {
 
template<class SparseModelType>
class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseModelType> {
   public:
    typedef typename SparseModelType::ValueType ValueType;
    using DeterministicInfiniteHorizonHelperType =
        typename std::conditional<std::is_same<SparseModelType, storm::models::sparse::MarkovAutomaton<ValueType>>::value,
                                  storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType>,
                                  storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper<ValueType>>::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<SparseModelType> const& preprocessorResult);
 
    virtual void check(Environment const& env, std::vector<ValueType> const& weightVector) override;
 
    virtual std::vector<ValueType> getUnderApproximationOfInitialStateResults() const override;
    virtual std::vector<ValueType> getOverApproximationOfInitialStateResults() const override;
 
    virtual storm::storage::Scheduler<ValueType> computeScheduler() const override;
 
   protected:
    void initialize(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
    virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0;
    virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> createNondetInfiniteHorizonHelper(
        storm::storage::SparseMatrix<ValueType> const& transitions) const = 0;
    virtual DeterministicInfiniteHorizonHelperType createDetInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitions) const = 0;
 
    void infiniteHorizonWeightedPhase(Environment const& env, std::vector<ValueType> const& weightedActionRewardVector,
                                      boost::optional<std::vector<ValueType>> const& weightedStateRewardVector);
 
    void unboundedWeightedPhase(Environment const& env, std::vector<ValueType> const& weightedRewardVector, std::vector<ValueType> const& weightVector);
 
    void unboundedIndividualPhase(Environment const& env, std::vector<ValueType> const& weightVector);
 
    virtual void boundedPhase(Environment const& env, std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) = 0;
 
    void updateEcQuotient(std::vector<ValueType> const& weightedRewardVector);
 
    void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex,
                           storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne,
                           std::vector<ValueType> const& rewards) const;
    void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper,
                           std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter,
                           storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne,
                           std::vector<ValueType> const& rewards) const;
    void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper,
                                     storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne,
                                     std::vector<ValueType> const& rewards) const;
 
    void transformEcqSolutionToOriginalModel(std::vector<ValueType> const& ecqSolution, std::vector<uint_fast64_t> const& ecqOptimalChoices,
                                             std::map<uint64_t, uint64_t> const& ecqStateToOptimalMecMap, std::vector<ValueType>& originalSolution,
                                             std::vector<uint_fast64_t>& originalOptimalChoices) const;
 
    // Data regarding the given model
    // The transition matrix of the considered model
    storm::storage::SparseMatrix<ValueType> 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<std::vector<ValueType>> 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<std::vector<ValueType>> 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<ValueType> weightedResult;
    // The results for the individual objectives (w.r.t. all states of the model)
    std::vector<std::vector<ValueType>> 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<ValueType> offsetsToUnderApproximation;
    std::vector<ValueType> offsetsToOverApproximation;
    // The scheduler choices that optimize the weighted rewards of undounded objectives.
    std::vector<uint64_t> optimalChoices;
 
    struct EcQuotient {
        storm::storage::SparseMatrix<ValueType> matrix;
        std::vector<uint_fast64_t> ecqToOriginalChoiceMapping;
        std::vector<uint_fast64_t> originalToEcqStateMapping;
        std::vector<storm::storage::FlatSetStateContainer> 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<ValueType> auxStateValues;
        std::vector<ValueType> auxChoiceValues;
    };
    boost::optional<EcQuotient> ecQuotient;
 
    struct LraMecDecomposition {
        storm::storage::MaximalEndComponentDecomposition<ValueType> mecs;
        std::vector<ValueType> auxMecValues;
    };
    boost::optional<LraMecDecomposition> lraMecDecomposition;
};
 
}  // namespace multiobjective
}  // namespace modelchecker
}  // namespace storm