BisimulationDecomposition.h

Go to the documentation of this file.

#pragma once
 
#include "storm/logic/Formulas.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/storage/Decomposition.h"
#include "storm/storage/StateBlock.h"
#include "storm/storage/bisimulation/BisimulationType.h"
#include "storm/storage/bisimulation/Partition.h"
#include "storm/utility/ConstantsComparator.h"
 
namespace storm {
namespace logic {
class Formula;
}
 
namespace storage {

template<typename ModelType, typename BlockDataType>
class BisimulationDecomposition : public Decomposition<StateBlock> {
   public:
    typedef typename ModelType::ValueType ValueType;
    typedef typename ModelType::RewardModelType RewardModelType;
 
    // A class that offers the possibility to customize the bisimulation.
    struct Options {
        Options(ModelType const& model, storm::logic::Formula const& formula, ValueType const& tolerance);

        Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, ValueType const& tolerance);

        static Options preservingAllLabels(ValueType const& tolerance);

        void preserveFormula(storm::logic::Formula const& formula);

        void setType(BisimulationType t) {
            if (t == BisimulationType::Weak) {
                STORM_LOG_WARN_COND(!bounded, "Weak bisimulation does not preserve bounded properties.");
                STORM_LOG_WARN_COND(!discounted, "Weak bisimulation does not preserve discounted properties.");
                bounded = false;
                discounted = false;
            }
            type = t;
        }
 
        BisimulationType getType() const {
            return this->type;
        }
 
        bool getBounded() const {
            return this->bounded;
        }
 
        bool getDiscounted() const {
            return this->discounted;
        }
 
        bool getKeepRewards() const {
            return this->keepRewards;
        }
 
        void setKeepRewards(bool keepRewards) {
            this->keepRewards = keepRewards;
        }
 
        bool isOptimizationDirectionSet() const {
            return static_cast<bool>(optimalityType);
        }
 
        ValueType getTolerance() const {
            return storm::NumberTraits<ValueType>::IsExact ? storm::utility::zero<ValueType>() : tolerance;
        }
 
        void setTolerance(ValueType value) {
            tolerance = value;
        }
 
        OptimizationDirection getOptimizationDirection() const {
            STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
            return optimalityType.value();
        }
 
        // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
        // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
        // measure driven initial partition wrt. to the states phi and psi is taken.
        bool measureDrivenInitialPartition = false;
        std::optional<storm::storage::BitVector> phiStates;
        std::optional<storm::storage::BitVector> psiStates;

        std::optional<std::set<std::string>> respectedAtomicPropositions;

        bool buildQuotient = true;
 
       private:
        std::optional<OptimizationDirection> optimalityType;

        bool keepRewards = false;

        BisimulationType type = BisimulationType::Strong;

        bool bounded = false;

        bool discounted = false;

        ValueType tolerance;

        explicit Options(ValueType const& tolerance);

        void preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula);

        void addToRespectedAtomicPropositions(std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions,
                                              std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels);
 
        /*
         * Checks whether a measure driven partition is possible with the given formula and sets the necessary
         * data if this is the case.
         *
         * @param model The model for which to derive the data.
         * @param formula The formula for which to derive the data for the measure driven initial partition (if
         * applicable).
         */
        void checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula);
    };

    BisimulationDecomposition(ModelType const& model, Options const& options);
 
    virtual ~BisimulationDecomposition() = default;

    std::shared_ptr<ModelType> getQuotient() const;

    void computeBisimulationDecomposition();
 
   protected:
    BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options);

    void performPartitionRefinement();

    virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter,
                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) = 0;

    virtual void buildQuotient() = 0;

    virtual void initializeLabelBasedPartition();

    virtual void initializeMeasureDrivenPartition();

    virtual void initialize();

    virtual std::pair<storm::storage::BitVector, storm::storage::BitVector> getStatesWithProbability01() = 0;

    virtual void splitInitialPartitionBasedOnRewards();

    virtual void splitInitialPartitionBasedOnRewards(std::vector<ValueType> const& rewardVector);

    virtual void splitInitialPartitionBasedOnActionRewards(std::vector<std::set<ValueType>> const& rewardVector);

    void extractDecompositionBlocks();
 
    // The model to decompose.
    ModelType const& model;
 
    // The backward transitions of the model.
    storm::storage::SparseMatrix<ValueType> backwardTransitions;
 
    // The options used during construction.
    Options options;
 
    // The current partition (used by partition refinement).
    storm::storage::bisimulation::Partition<BlockDataType> partition;
 
    // A comparator used for comparing the distances of constants.
    storm::utility::ConstantsComparator<ValueType> comparator;
 
    // The quotient, if it was build. Otherwise a null pointer.
    std::shared_ptr<ModelType> quotient;
};
}  // namespace storage
}  // namespace storm