Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SplitterBasedRefinement.h File Reference
Include dependency graph for SplitterBasedRefinement.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

namespace  storm
namespace  storm::bisimulation

Enumerations

enum class  storm::bisimulation::SplitterRefinementMode { storm::bisimulation::Strong , storm::bisimulation::WeakDiscreteTime , storm::bisimulation::WeakContinuousTime }
 The kind of bisimulation that splitter-based refinement computes. More...

Functions

template<typename ValueType, SplitterRefinementMode Mode>
void storm::bisimulation::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)
 Performs splitter-based partition refinement.