Signatures.h

Go to the documentation of this file.

#pragma once
 
#include <compare>
#include <cstdint>
#include <optional>
#include <span>
#include <utility>
#include <vector>
 
#include "storm/models/sparse/ModelForward.h"
#include "storm/transformer/bisimulation/Partition.h"
#include "storm/transformer/bisimulation/QuotientData.h"
 
namespace storm::bisimulation {
 
enum class SignatureMode { Exact, Approximative };

template<typename ValueType, SignatureMode Mode>
class Signatures {
   public:
    Signatures(storm::models::sparse::Model<ValueType> const& model, std::optional<std::vector<uint64_t>> const& choiceClasses,
               storm::bisimulation::Partition const& partition)
        requires(Mode == SignatureMode::Exact);
 
    Signatures(storm::models::sparse::Model<ValueType> const& model, std::optional<std::vector<uint64_t>> const& choiceClasses,
               storm::bisimulation::Partition const& partition, ValueType const& tolerance)
        requires(Mode == SignatureMode::Approximative);

    void updateStateSignature(uint64_t const stateIndex);
 
   private:
    struct StateSignature;  // Forward-declared; defined privately further down.
 
   public:
    class SplitOrder {
       public:
        explicit SplitOrder(std::vector<StateSignature> const& signatures) : signatures(signatures) {}
        bool operator()(uint64_t const state1, uint64_t const state2) const;
 
       private:
        std::vector<StateSignature> const& signatures;
    };

    SplitOrder getEquivalenceSplitOrder() const
        requires(Mode == SignatureMode::Exact);

    SplitOrder getStructuralSplitOrder() const
        requires(Mode == SignatureMode::Approximative);

    struct SplitCondition {
        SplitCondition(std::vector<StateSignature> const& signatures, ValueType const& tolerance) : signatures(signatures), tolerance(tolerance) {}
        bool operator()(uint64_t const state1, uint64_t const state2) const
            requires(Mode == SignatureMode::Approximative);
 
       private:
        std::vector<StateSignature> const& signatures;
        ValueType const tolerance;
    };

    SplitCondition getApproximateSplitCondition() const
        requires(Mode == SignatureMode::Approximative);

    void extendQuotientData(QuotientData<ValueType>& quotientData, bool const createQuotientChoiceMapping) const;
 
   private:
    // For all choices, we store the current distributions over successor blocks in choiceDistributionStorage and use a view into that for ChoiceSignatures.
    using BlockDistributionView = std::span<std::pair<Partition::Block, ValueType>>;

    struct ChoiceSignature {
        uint64_t choiceClass;  // The class of this choice according to the provided choice classes.
        // The accumulated transition values for each block, sorted by Partition::BlockCompare. This is a (non-owning) view into the choice's permanent
        // slot of Signatures::choiceDistributionStorage, see there.
        BlockDistributionView distr;
 
        // Orders by choiceClass and the set of blocks (identity and order) of distr; independent of the actual transition values.
        std::strong_ordering compareStructure(ChoiceSignature const& other) const;
        // strong_ordering in exact mode (equal signatures are substitutable); only weak_ordering in approximative mode, since ties don't imply approxEqual.
        using ComparisonResult = std::conditional_t<Mode == SignatureMode::Exact, std::strong_ordering, std::weak_ordering>;
        // Strict weak order for sorting/lower_bound. In approximative mode, ties don't imply approximate equality - see StateSignature::find.
        ComparisonResult compare(ChoiceSignature const& other) const;
        // True iff the two signatures have the same structure and their distr values pairwise differ by at most the given tolerance.
        bool approximatelyEqual(ChoiceSignature const& other, ValueType const& tolerance) const
            requires(Mode == SignatureMode::Approximative);
    };
 
    using ChoiceSignatureIterator = typename std::vector<ChoiceSignature>::const_iterator;

    struct StateSignature {
        std::pair<ChoiceSignatureIterator, bool> find(ChoiceSignature const& signature, ValueType const tolerance) const;

        std::pair<ChoiceSignatureIterator, bool> findWithHint(ChoiceSignatureIterator const hint, ChoiceSignature const& signature,
                                                              ValueType const tolerance) const
            requires(Mode == SignatureMode::Approximative);
 
        void insert(ChoiceSignature const& signature, ValueType const tolerance);
 
        std::vector<ChoiceSignature> choices;  // Always ordered and deduplicated as described above.
    };

    void addQuotientChoiceMapping(uint64_t const state, StateSignature const& representativeSignature,
                                  std::vector<uint64_t> const& choiceSignatureToQuotientChoiceIndex, std::vector<uint64_t>& toQuotientChoice) const;

    ChoiceSignature buildChoiceSignature(uint64_t const choiceIndex);

    ChoiceSignature getChoiceSignature(uint64_t const choiceIndex) const;

    class ChoiceSignatureCache {
       public:
        explicit ChoiceSignatureCache(uint64_t const numStates);

        void addValue(Partition::Block const& b, ValueType const& value);

        BlockDistributionView extract(BlockDistributionView const dest);
 
       private:
        std::vector<ValueType> values;
        std::vector<Partition::Block> support;
    } choiceSignatureCache;
 
    storm::models::sparse::Model<ValueType> const& model;
    Partition const& partition;
    std::optional<std::vector<uint64_t>> const& choiceClasses;

    mutable std::vector<std::pair<Partition::Block, ValueType>> choiceDistributionStorage;

    ValueType const halfTolerance;
 
    std::vector<StateSignature> stateSignatureCache;
};
 
}  // namespace storm::bisimulation