WeakBisimulationData.h

Go to the documentation of this file.

#pragma once
 
#include <algorithm>
#include <cstdint>
 
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/transformer/bisimulation/Partition.h"
#include "storm/utility/constants.h"
 
namespace storm::bisimulation {

template<typename ValueType>
bool isSilentState(storm::storage::SparseMatrix<ValueType> const& transitions, Partition const& partition, uint64_t const state) {
    auto const row = transitions.getRow(state);
    return std::all_of(row.begin(), row.end(), [&partition, &state](auto const& entry) {
        return storm::utility::isZero(entry.getValue()) || partition.isSameBlock(state, entry.getColumn());
    });
}

struct WeakBisimulationData {
    WeakBisimulationData(storm::storage::BitVector divergentStates, storm::storage::BitVector stepSensitiveStates, storm::storage::BitVector silentStates);

    storm::storage::BitVector const divergentStates;

    storm::storage::BitVector const stepSensitiveStates;

    storm::storage::BitVector silentStates;

    bool isDivergent(Partition::Block const& block) const;

    bool isStepSensitive(Partition::Block const& block) const;

    bool checkBlockHomogeneity(Partition const& partition) const;
};
 
}  // namespace storm::bisimulation