MaximalEndComponentDecomposition.h

Go to the documentation of this file.

#pragma once
 
#include <string>
 
#include "storm/models/sparse/NondeterministicModel.h"
#include "storm/storage/Decomposition.h"
#include "storm/storage/MaximalEndComponent.h"
#include "storm/utility/OptionalRef.h"
 
namespace storm::storage {
 
template<typename ValueType>
class MaximalEndComponentDecomposition : public Decomposition<MaximalEndComponent> {
   public:
    /*
     * Creates an empty MEC decomposition.
     */
    MaximalEndComponentDecomposition();
 
    /*
     * Creates an MEC decomposition of the given model.
     *
     * @param model The model to decompose into MECs.
     */
    template<typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
    MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<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.
     */
    MaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                     storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
    /*
     * 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.
     */
    MaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                     storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states);
 
    /*
     * 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, independent of how the given
     * 'choices' vector is set for that choice.
     *
     * @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 choices The choices of the subsystem to decompose.
     */
    MaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                     storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states,
                                     storm::storage::BitVector const& choices);
 
    MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<ValueType> const& model, storm::storage::BitVector const& states);
 
    MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other);
 
    MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition const& other);
 
    MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other);
 
    MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition&& other);
 
    std::string statistics(uint64_t totalNumberOfStates) const;
 
   private:
    void performMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                 storm::OptionalRef<storm::storage::BitVector const> states = storm::NullRef,
                                                 storm::OptionalRef<storm::storage::BitVector const> choices = storm::NullRef);
};
}  // namespace storm::storage