storm::bisimulation Namespace Reference

Namespaces
namespace	detail

Classes
struct	ReturnType
class	Initialization
struct	Options
class	Partition
	Represents a partition of a set of consecutive indices. More...
struct	PreservationInformation
class	Quotient
struct	QuotientData
	The index mappings between an input model and its bisimulation quotient, derived from a partition of the input model's states. More...
class	Signatures
	Computes and caches the state signatures and provides state-based order / condition for splitting in signature refinement. More...
class	SparseAccumulator
	Accumulates a value for each state (numbers are added up, elements are inserted into sets, c.f. More...
struct	WeakBisimulationData
	The state-level information that weak bisimulation requires on top of the partition. More...

Typedefs
using	WrappingSetAccumulator = SparseAccumulator<uint64_t>
	Accumulates a set of indices for each state, where only the index modulo 64 is stored, namely as a bit of a 64 bit mask.

Enumerations
enum class	BisimulationType { Strong , Weak }
	The kind of bisimulation. More...
enum class	StateLabelPreservation {   Default , All , None , FormulaPropositional ,   FormulaIndividual }
	The way state labels will be preserved by the bisimulation. More...
enum class	SignatureMode { Exact , Approximative }
enum class	SplitterRefinementMode { Strong , WeakDiscreteTime , WeakContinuousTime }
	The kind of bisimulation that splitter-based refinement computes. More...

Functions
template<typename ValueType>
ReturnType< ValueType >	performBisimulationMinimization (storm::models::sparse::Model< ValueType > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas={}, storm::bisimulation::Options options={})
	Computes the bisimulation quotient of the given model.
template ReturnType< double >	performBisimulationMinimization (storm::models::sparse::Model< double > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
template ReturnType< storm::RationalNumber >	performBisimulationMinimization (storm::models::sparse::Model< storm::RationalNumber > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
template ReturnType< storm::RationalFunction >	performBisimulationMinimization (storm::models::sparse::Model< storm::RationalFunction > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
template ReturnType< storm::Interval >	performBisimulationMinimization (storm::models::sparse::Model< storm::Interval > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
template ReturnType< storm::RationalInterval >	performBisimulationMinimization (storm::models::sparse::Model< storm::RationalInterval > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, Options options)
std::ostream &	operator<< (std::ostream &os, const Partition &partition)
template<typename ValueType, SignatureMode SignatureMode>
void	performSignatureBasedRefinement (storm::models::sparse::Model< ValueType > const &model, storm::bisimulation::Partition &partition, Signatures< ValueType, SignatureMode > &signatures)
template void	performSignatureBasedRefinement< double, SignatureMode::Exact > (storm::models::sparse::Model< double > const &model, storm::bisimulation::Partition &partition, Signatures< double, SignatureMode::Exact > &signatures)
template void	performSignatureBasedRefinement< double, SignatureMode::Approximative > (storm::models::sparse::Model< double > const &model, storm::bisimulation::Partition &partition, Signatures< double, SignatureMode::Approximative > &signatures)
template void	performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Exact > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::bisimulation::Partition &partition, Signatures< storm::RationalNumber, SignatureMode::Exact > &signatures)
template void	performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Approximative > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::bisimulation::Partition &partition, Signatures< storm::RationalNumber, SignatureMode::Approximative > &signatures)
template void	performSignatureBasedRefinement< storm::RationalFunction, SignatureMode::Exact > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::bisimulation::Partition &partition, Signatures< storm::RationalFunction, SignatureMode::Exact > &signatures)
template<typename ValueType, SignatureMode Mode>
void	performSignatureBasedRefinement (storm::models::sparse::Model< ValueType > const &model, storm::bisimulation::Partition &partition, Signatures< ValueType, Mode > &signatures)
	Performs signature-based partition refinement.
template<typename ValueType, SplitterRefinementMode Mode>
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)
	Performs splitter-based partition refinement.
template void	performSplitterBasedRefinement< double, SplitterRefinementMode::Strong > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< double, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< double, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::Strong > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::Strong > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template<typename ValueType>
bool	isSilentState (storm::storage::SparseMatrix< ValueType > const &transitions, Partition const &partition, uint64_t const state)

Typedef Documentation

WrappingSetAccumulator

using storm::bisimulation::WrappingSetAccumulator = SparseAccumulator<uint64_t>

Accumulates a set of indices for each state, where only the index modulo 64 is stored, namely as a bit of a 64 bit mask.

Two states that received the same indices thus always get the same value, whereas the values of two states that received different indices might coincide. In exchange, adding an index takes constant time without allocating any memory and the values can be compared like plain integers.

Definition at line 53 of file SparseAccumulator.h.

Enumeration Type Documentation

BisimulationType

enum class storm::bisimulation::BisimulationType

strong

The kind of bisimulation.

Enumerator
Strong
Weak

Definition at line 8 of file BisimulationType.h.

SignatureMode

enum class storm::bisimulation::SignatureMode

strong

Enumerator
Exact
Approximative

Definition at line 16 of file Signatures.h.

SplitterRefinementMode

enum class storm::bisimulation::SplitterRefinementMode

strong

The kind of bisimulation that splitter-based refinement computes.

Enumerator
Strong
WeakDiscreteTime
WeakContinuousTime

Definition at line 13 of file SplitterBasedRefinement.h.

StateLabelPreservation

enum class storm::bisimulation::StateLabelPreservation

strong

The way state labels will be preserved by the bisimulation.

Enumerator
Default
All
None
FormulaPropositional
FormulaIndividual

Definition at line 14 of file Options.h.

Function Documentation

isSilentState()

template<typename ValueType>

bool storm::bisimulation::isSilentState	(	storm::storage::SparseMatrix< ValueType > const &	transitions,
		Partition const &	partition,
		uint64_t const	state )

Returns

true iff the given state is silent with respect to the given partition, i.e., iff it cannot leave its block in a single step.

Definition at line 17 of file WeakBisimulationData.h.

operator<<()

std::ostream & storm::bisimulation::operator<<	(	std::ostream &	os,
		const Partition &	partition )

Definition at line 191 of file Partition.cpp.

performBisimulationMinimization() [1/6]

template ReturnType< double > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< double > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		Options	options )

performBisimulationMinimization() [2/6]

template ReturnType< storm::Interval > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< storm::Interval > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		Options	options )

performBisimulationMinimization() [3/6]

template ReturnType< storm::RationalFunction > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< storm::RationalFunction > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		Options	options )

performBisimulationMinimization() [4/6]

template ReturnType< storm::RationalInterval > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< storm::RationalInterval > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		Options	options )

performBisimulationMinimization() [5/6]

template ReturnType< storm::RationalNumber > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		Options	options )

performBisimulationMinimization() [6/6]

template<typename ValueType>

ReturnType< ValueType > storm::bisimulation::performBisimulationMinimization	(	storm::models::sparse::Model< ValueType > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas = {},
		storm::bisimulation::Options	options = {} )

Computes the bisimulation quotient of the given model.

Parameters

model	the model to minimize.
formulas	the formulas that need to be preserved by the minimization.
options	the options to use for the minimization.

Definition at line 25 of file Bisimulation.cpp.

performSignatureBasedRefinement() [1/2]

template<typename ValueType, SignatureMode Mode>

void storm::bisimulation::performSignatureBasedRefinement	(	storm::models::sparse::Model< ValueType > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< ValueType, Mode > &	signatures )

Performs signature-based partition refinement.

Note

applicable to deterministic and nondeterministic models, in contrast to splitter-based refinement.

upon return, the signature of every state (as cached by signatures) is up to date with respect to the final partition.

performSignatureBasedRefinement() [2/2]

template<typename ValueType, SignatureMode SignatureMode>

void storm::bisimulation::performSignatureBasedRefinement	(	storm::models::sparse::Model< ValueType > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< ValueType, SignatureMode > &	signatures )

Definition at line 136 of file SignatureBasedRefinement.cpp.

performSignatureBasedRefinement< double, SignatureMode::Approximative >()

template void storm::bisimulation::performSignatureBasedRefinement< double, SignatureMode::Approximative >	(	storm::models::sparse::Model< double > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< double, SignatureMode::Approximative > &	signatures )

performSignatureBasedRefinement< double, SignatureMode::Exact >()

template void storm::bisimulation::performSignatureBasedRefinement< double, SignatureMode::Exact >	(	storm::models::sparse::Model< double > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< double, SignatureMode::Exact > &	signatures )

performSignatureBasedRefinement< storm::RationalFunction, SignatureMode::Exact >()

template void storm::bisimulation::performSignatureBasedRefinement< storm::RationalFunction, SignatureMode::Exact >	(	storm::models::sparse::Model< storm::RationalFunction > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< storm::RationalFunction, SignatureMode::Exact > &	signatures )

performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Approximative >()

template void storm::bisimulation::performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Approximative >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< storm::RationalNumber, SignatureMode::Approximative > &	signatures )

performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Exact >()

template void storm::bisimulation::performSignatureBasedRefinement< storm::RationalNumber, SignatureMode::Exact >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		storm::bisimulation::Partition &	partition,
		Signatures< storm::RationalNumber, SignatureMode::Exact > &	signatures )

performSplitterBasedRefinement()

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.

Note

only applicable to deterministic models.

Parameters

backwardTransitions	the transposed transition matrix of the model.
weakData	must be given iff a weak Mode is used, cf. Initialization::getWeakBisimulationData. Its silentStates are kept up to date with the partition; the other members are only read.

Definition at line 386 of file SplitterBasedRefinement.cpp.

performSplitterBasedRefinement< double, SplitterRefinementMode::Strong >()

template void storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::Strong >	(	storm::models::sparse::Model< double > const &	model,
		storm::storage::SparseMatrix< double > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		double const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< double, SplitterRefinementMode::WeakContinuousTime >()

template void storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::WeakContinuousTime >	(	storm::models::sparse::Model< double > const &	model,
		storm::storage::SparseMatrix< double > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		double const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< double, SplitterRefinementMode::WeakDiscreteTime >()

template void storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::WeakDiscreteTime >	(	storm::models::sparse::Model< double > const &	model,
		storm::storage::SparseMatrix< double > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		double const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::Strong >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::Strong >	(	storm::models::sparse::Model< storm::RationalFunction > const &	model,
		storm::storage::SparseMatrix< storm::RationalFunction > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalFunction const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakContinuousTime >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakContinuousTime >	(	storm::models::sparse::Model< storm::RationalFunction > const &	model,
		storm::storage::SparseMatrix< storm::RationalFunction > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalFunction const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakDiscreteTime >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakDiscreteTime >	(	storm::models::sparse::Model< storm::RationalFunction > const &	model,
		storm::storage::SparseMatrix< storm::RationalFunction > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalFunction const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::Strong >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::Strong >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalNumber const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakContinuousTime >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakContinuousTime >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalNumber const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )

performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakDiscreteTime >()

template void storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakDiscreteTime >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		storm::storage::SparseMatrix< storm::RationalNumber > const &	backwardTransitions,
		storm::bisimulation::Partition &	partition,
		storm::RationalNumber const	tolerance,
		storm::OptionalRef< WeakBisimulationData >	weakData )