SplitterBasedRefinement.h

Go to the documentation of this file.

#pragma once
 
#include "storm/models/sparse/ModelForward.h"
#include "storm/transformer/bisimulation/Partition.h"
#include "storm/transformer/bisimulation/WeakBisimulationData.h"
#include "storm/utility/OptionalRef.h"
 
namespace storm::bisimulation {

enum class SplitterRefinementMode {
    Strong,             // Strong bisimulation.
    WeakDiscreteTime,   // Weak bisimulation on a discrete-time model, i.e., transition probabilities are considered conditioned on leaving the own block.
    WeakContinuousTime  // Weak bisimulation on a continuous-time model, i.e., transition rates into the own block are ignored.
};

template<typename ValueType, SplitterRefinementMode Mode = SplitterRefinementMode::Strong>
void performSplitterBasedRefinement(storm::models::sparse::Model<ValueType> const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                    storm::bisimulation::Partition& partition, ValueType const tolerance,
                                    storm::OptionalRef<WeakBisimulationData> weakData = storm::NullRef);
 
}  // namespace storm::bisimulation