RobustMaximalEndComponentDecomposition.h

Go to the documentation of this file.

#pragma once
 
#include "storm/models/sparse/DeterministicModel.h"
#include "storm/storage/BoostTypes.h"
#include "storm/storage/Decomposition.h"
#include "storm/storage/StronglyConnectedComponent.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/utility/OptionalRef.h"
 
namespace storm::storage {
 
template<typename ValueType>
class RobustMaximalEndComponentDecomposition : public Decomposition<StronglyConnectedComponent> {
   public:
    /*
     * Creates an empty MEC decomposition.
     */
    RobustMaximalEndComponentDecomposition();
 
    /*
     * Creates an MEC decomposition of the given model.
     *
     * @param model The model to decompose into MECs.
     */
    template<typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
    RobustMaximalEndComponentDecomposition(storm::models::sparse::DeterministicModel<ValueType, RewardModelType> const& model);
 
    /*
     * Creates an MEC decomposition of the given model (represented by a row-grouped matrix).
     *
     * @param transitionMatrix The transition relation of model to decompose into MECs.
     * @param backwardTransition The reversed transition relation.
     * @param vector The vector of the system of equations (e.g. rewards or probabilities to go to target).
     */
    RobustMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                           storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& vector);
 
    /*
     * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix).
     * If a state-action pair (aka choice) has a transition that leaves the subsystem, the entire state-action pair is ignored.
     *
     * @param transitionMatrix The transition relation of model to decompose into MECs.
     * @param backwardTransition The reversed transition relation.
     * @param states The states of the subsystem to decompose.
     * @param vector The vector of the system of equations (e.g. rewards or probabilities to go to target).
     */
    RobustMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                           storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& vector,
                                           storm::storage::BitVector const& states);
 
    RobustMaximalEndComponentDecomposition(storm::models::sparse::DeterministicModel<ValueType> const& model, storm::storage::BitVector const& states);
 
    RobustMaximalEndComponentDecomposition(RobustMaximalEndComponentDecomposition const& other);
 
    RobustMaximalEndComponentDecomposition& operator=(RobustMaximalEndComponentDecomposition const& other);
 
    RobustMaximalEndComponentDecomposition(RobustMaximalEndComponentDecomposition&& other);
 
    RobustMaximalEndComponentDecomposition& operator=(RobustMaximalEndComponentDecomposition&& other);
 
    std::vector<uint64_t> computeStateToSccIndexMap(uint64_t numberOfStates) const;
 
   private:
    void performRobustMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                       storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                       storm::OptionalRef<std::vector<ValueType> const> vector = storm::NullRef,
                                                       storm::OptionalRef<storm::storage::BitVector const> states = storm::NullRef);
};
}  // namespace storm::storage