Initialization.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <functional>
#include <memory>
#include <optional>
#include <ranges>
#include <span>
#include <variant>
#include <vector>
 
#include "storm/logic/FormulasForwardDeclarations.h"
#include "storm/models/sparse/ModelForward.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/transformer/bisimulation/Options.h"
#include "storm/transformer/bisimulation/Partition.h"
#include "storm/transformer/bisimulation/PreservationInformation.h"
#include "storm/transformer/bisimulation/WeakBisimulationData.h"
 
namespace storm::bisimulation {
 
template<typename ValueType>
class Initialization {
   public:
    Initialization(storm::models::sparse::Model<ValueType> const& model, Options const& options,
                   std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
 
    PreservationInformation getPreservationInformation() const;
 
    std::optional<std::vector<uint64_t>> getChoiceClasses() const;
 
    Partition getInitialStatePartition(std::optional<std::vector<uint64_t>> const& choiceClasses = {}) const;

    WeakBisimulationData getWeakBisimulationData(Partition& partition, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                 PreservationInformation const& preservationInformation) const;
 
   private:
    storm::models::sparse::Model<ValueType> const& model;
    Options const options;
    std::vector<std::shared_ptr<storm::logic::Formula const>> const formulas;

    struct PreservedAnnotations {
        std::vector<std::span<uint64_t const>> integers;
        std::vector<std::span<ValueType const>> values;

        void addBoolean(storm::storage::BitVector const& annotation);

        void addBoolean(storm::storage::BitVector&& annotation);

        auto getBooleans() const {
            return optionallyOwnedBooleans | std::views::transform([](auto const& annotation) -> storm::storage::BitVector const& {
                       return std::visit([](auto const& bitVector) -> storm::storage::BitVector const& { return bitVector; }, annotation);
                   });
        }

        bool empty() const;

        void applySplit(Partition& partition, ValueType const& tolerance, std::vector<uint64_t> const& extraAnnotation = {}) const;
 
       private:
        // A Boolean annotation is either owned by this object or stored somewhere else.
        using OptionallyOwnedBitVector = std::variant<std::reference_wrapper<storm::storage::BitVector const>, storm::storage::BitVector>;
 
        std::vector<OptionallyOwnedBitVector> optionallyOwnedBooleans;
    } preservedStateAnnotations, preservedChoiceAnnotations;
};
 
}  // namespace storm::bisimulation