|
Storm 1.14.0.1
A Modern Probabilistic Model Checker
|
#include "storm/models/sparse/ModelForward.h"#include "storm/transformer/bisimulation/Partition.h"#include "storm/transformer/bisimulation/WeakBisimulationData.h"#include "storm/utility/OptionalRef.h"

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. | |