Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Quotient.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4
9
10namespace storm::bisimulation {
11
12template<typename ValueType>
13class Quotient {
14 public:
20 static std::shared_ptr<storm::models::sparse::Model<ValueType>> buildFromPartition(
22 storm::bisimulation::PreservationInformation const& preservationInformation, QuotientData<ValueType> const& quotientData);
23};
24
25} // namespace storm::bisimulation
static std::shared_ptr< storm::models::sparse::Model< ValueType > > buildFromPartition(storm::models::sparse::Model< ValueType > const &model, storm::bisimulation::Options const &options, storm::bisimulation::PreservationInformation const &preservationInformation, QuotientData< ValueType > const &quotientData)
Builds the quotient model from the given partition (represented by quotientData), preserving the give...
Definition Quotient.cpp:24
Base class for all sparse models.
Definition Model.h:34
The index mappings between an input model and its bisimulation quotient, derived from a partition of ...