Namespaces
namespace	detail

Classes
class	ParameterLifter
	This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd #par parameters, the resulting matrix will have one row group consisting of 2^#par rows. More...
struct	UniPolyCompare
struct	PolynomialCache
struct	container_hash
class	Annotation
class	BigStep
	Shorthand for std::unordered_map<T, uint64_t>. More...
struct	StateWithRow
class	BinaryDtmcTransformer
class	IntervalEndComponentPreserver
class	RobustParameterLifter
	This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd #par parameters, the resulting matrix will have one row group consisting of 2^#par rows. More...
class	SparseParametricDtmcSimplifier
	This class performs different steps to simplify the given (parametric) model. More...
class	SparseParametricMdpSimplifier
	This class performs different steps to simplify the given (parametric) model. More...
class	SparseParametricModelSimplifier
	This class performs different steps to simplify the given (parametric) model. More...
struct	RationalFunctionConstructor
class	ApplyFiniteSchedulerToPomdp
struct	BinaryPomdpTransformerRowGroup
struct	BinaryPomdpTransformerRowGroupCompare
struct	PomdpTransformationResult
class	BinaryPomdpTransformer
class	GlobalPomdpMecChoiceEliminator
class	GlobalPOMDPSelfLoopEliminator
class	MakeStateSetObservationClosed
class	PomdpMemoryUnfolder
class	AddUncertainty
	This class is a convenience transformer to add uncertainty. More...
class	ChoiceSelector
class	ContinuousToDiscreteTimeModelTransformer
class	DAProduct
class	DAProductBuilder
class	EndComponentEliminator
class	GoalStateMerger
class	MakePOMDPCanonic
class	MemoryIncorporation
	Incorporates Memory into the state space of the given model, that is the resulting model is the crossproduct of of the given model plus some type of memory structure. More...
class	NonMarkovianChainTransformer
	Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata. More...
class	Product
class	ProductBuilder
struct	SubsystemBuilderReturnType
struct	SubsystemBuilderOptions
struct	LabelInformation
class	SymbolicDtmcToSparseDtmcTransformer
class	SymbolicMdpToSparseMdpTransformer
class	SymbolicCtmcToSparseCtmcTransformer
class	SymbolicMaToSparseMaTransformer

Typedefs
using	UniPoly = carl::UnivariatePolynomial<RationalFunctionCoefficient>
typedef storm::utility::parametric::CoefficientType< storm::RationalFunction >::type	CoefficientType

Enumerations
enum class	PomdpFscApplicationMode { STANDARD , SIMPLE_LINEAR , SIMPLE_LINEAR_INVERSE , SIMPLE_LOG , FULL }
enum	EliminationLabelBehavior { KeepLabels , ExtendLabels , MergeLabels , DeleteLabels }
	Specify criteria whether a state can be eliminated and how its labels should be treated. More...

Functions
std::ostream &	operator<< (std::ostream &os, const Annotation &annotation)
std::pair< std::map< uint64_t, std::set< uint64_t > >, std::set< uint64_t > >	findSubgraph (const storm::storage::FlexibleSparseMatrix< RationalFunction > &transitionMatrix, const uint64_t root, const std::map< RationalFunctionVariable, std::map< uint64_t, std::set< uint64_t > > > &treeStates, const boost::optional< std::vector< RationalFunction > > &stateRewardVector, const RationalFunctionVariable parameter)
Interval	evaluateExtremaAnnotations (std::map< UniPoly, std::set< double > > extremaAnnotations, Interval input)
PomdpFscApplicationMode	parsePomdpFscApplicationMode (std::string const &mode)
template<typename ValueType>
std::shared_ptr< RawPolynomialCache >	getCache (storm::models::sparse::Pomdp< ValueType > const &)
template<>
std::shared_ptr< RawPolynomialCache >	getCache (storm::models::sparse::Pomdp< storm::RationalFunction > const &model)
template<class SparseModelType>
storm::storage::MemoryStructure	getGoalMemory (SparseModelType const &model, storm::logic::Formula const &propositionalGoalStateFormula)
template<class SparseModelType>
storm::storage::MemoryStructure	getUntilFormulaMemory (SparseModelType const &model, storm::logic::Formula const &leftSubFormula, storm::logic::Formula const &rightSubFormula)
template<class SparseModelType>
storm::storage::MemoryStructure	incorporateGoalMemoryHelper (SparseModelType const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	permuteStates (storm::models::sparse::Model< ValueType > const &originalModel, std::vector< uint64_t > const &permutation)
	Applies the given permutation to the states of the given model.
template std::shared_ptr< storm::models::sparse::Model< double > >	permuteStates (storm::models::sparse::Model< double > const &originalModel, std::vector< uint64_t > const &permutation)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	permuteStates (storm::models::sparse::Model< storm::RationalNumber > const &originalModel, std::vector< uint64_t > const &permutation)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	permuteStates (storm::models::sparse::Model< storm::RationalFunction > const &originalModel, std::vector< uint64_t > const &permutation)
template std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	permuteStates (storm::models::sparse::Model< storm::Interval > const &originalModel, std::vector< uint64_t > const &permutation)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > >	permuteStates (storm::models::sparse::Model< storm::RationalInterval > const &originalModel, std::vector< uint64_t > const &permutation)
template<typename ValueType, typename RewardModelType>
void	transformModelSpecificComponents (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystem, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &components)
template<typename RewardModelType>
RewardModelType	transformRewardModel (RewardModelType const &originalRewardModel, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &subsystemActions, bool makeRowGroupingTrivial)
template<typename ValueType, typename RewardModelType>
SubsystemBuilderReturnType< ValueType, RewardModelType >	internalBuildSubsystem (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, SubsystemBuilderOptions const &options)
template<typename ValueType, typename RewardModelType>
SubsystemBuilderReturnType< ValueType, RewardModelType >	buildSubsystem (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates, SubsystemBuilderOptions options)
template SubsystemBuilderReturnType< double >	buildSubsystem (storm::models::sparse::Model< double > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > >	buildSubsystem (storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >	buildSubsystem (storm::models::sparse::Model< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< storm::RationalNumber >	buildSubsystem (storm::models::sparse::Model< storm::RationalNumber > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< storm::RationalFunction >	buildSubsystem (storm::models::sparse::Model< storm::RationalFunction > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< storm::Interval >	buildSubsystem (storm::models::sparse::Model< storm::Interval > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
template SubsystemBuilderReturnType< storm::RationalInterval >	buildSubsystem (storm::models::sparse::Model< storm::RationalInterval > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())

Typedef Documentation

◆ CoefficientType

typedef storm::utility::parametric::CoefficientType<storm::RationalFunction>::type storm::transformer::CoefficientType

Definition at line 31 of file RobustParameterLifter.cpp.

◆ UniPoly

typedef RawUnivariatePolynomial storm::transformer::UniPoly = carl::UnivariatePolynomial<RationalFunctionCoefficient>

Definition at line 33 of file BigStep.cpp.

Enumeration Type Documentation

◆ EliminationLabelBehavior

enum storm::transformer::EliminationLabelBehavior

Specify criteria whether a state can be eliminated and how its labels should be treated.

KeepLabels: only eliminate if the labels of the state and the successors are the same.
ExtendLabels: only eliminate if the labels of the state are a subset of the labels of the successors.
MergeLabels: eliminate state and add labels of state to labels of the successors.
DeleteLabels: eliminate state and do not add its labels to the successors (except "init" label).

Enumerator
KeepLabels
ExtendLabels
MergeLabels
DeleteLabels

Definition at line 16 of file NonMarkovianChainTransformer.h.

◆ PomdpFscApplicationMode

enum class storm::transformer::PomdpFscApplicationMode

strong

Enumerator
STANDARD
SIMPLE_LINEAR
SIMPLE_LINEAR_INVERSE
SIMPLE_LOG
FULL

Definition at line 11 of file ApplyFiniteSchedulerToPomdp.h.

Function Documentation

◆ buildSubsystem() [1/8]

template SubsystemBuilderReturnType< double > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< double > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [2/8]

template SubsystemBuilderReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [3/8]

template SubsystemBuilderReturnType< storm::Interval > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< storm::Interval > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [4/8]

template SubsystemBuilderReturnType< storm::RationalFunction > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< storm::RationalFunction > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [5/8]

template SubsystemBuilderReturnType< storm::RationalInterval > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< storm::RationalInterval > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [6/8]

template SubsystemBuilderReturnType< storm::RationalNumber > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< storm::RationalNumber > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [7/8]

template SubsystemBuilderReturnType< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates = true,
		SubsystemBuilderOptions	options = SubsystemBuilderOptions() )

◆ buildSubsystem() [8/8]

template<typename ValueType, typename RewardModelType>

SubsystemBuilderReturnType< ValueType, RewardModelType > storm::transformer::buildSubsystem	(	storm::models::sparse::Model< ValueType, RewardModelType > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		bool	keepUnreachableStates,
		SubsystemBuilderOptions	options )

Definition at line 203 of file SubsystemBuilder.cpp.

◆ evaluateExtremaAnnotations()

Interval storm::transformer::evaluateExtremaAnnotations	(	std::map< UniPoly, std::set< double > >	extremaAnnotations,
		Interval	input )

Definition at line 507 of file RobustParameterLifter.cpp.

◆ findSubgraph()

std::pair< std::map< uint64_t, std::set< uint64_t > >, std::set< uint64_t > > storm::transformer::findSubgraph	(	const storm::storage::FlexibleSparseMatrix< RationalFunction > &	transitionMatrix,
		const uint64_t	root,
		const std::map< RationalFunctionVariable, std::map< uint64_t, std::set< uint64_t > > > &	treeStates,
		const boost::optional< std::vector< RationalFunction > > &	stateRewardVector,
		const RationalFunctionVariable	parameter )

Definition at line 293 of file BigStep.cpp.

◆ getCache() [1/2]

template<>

std::shared_ptr< RawPolynomialCache > storm::transformer::getCache ( storm::models::sparse::Pomdp< storm::RationalFunction > const & model )

Definition at line 38 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ getCache() [2/2]

template<typename ValueType>

std::shared_ptr< RawPolynomialCache > storm::transformer::getCache ( storm::models::sparse::Pomdp< ValueType > const & )

Definition at line 33 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ getGoalMemory()

template<class SparseModelType>

storm::storage::MemoryStructure storm::transformer::getGoalMemory	(	SparseModelType const &	model,
		storm::logic::Formula const &	propositionalGoalStateFormula )

Definition at line 22 of file MemoryIncorporation.cpp.

◆ getUntilFormulaMemory()

template<class SparseModelType>

storm::storage::MemoryStructure storm::transformer::getUntilFormulaMemory	(	SparseModelType const &	model,
		storm::logic::Formula const &	leftSubFormula,
		storm::logic::Formula const &	rightSubFormula )

Definition at line 49 of file MemoryIncorporation.cpp.

◆ incorporateGoalMemoryHelper()

template<class SparseModelType>

storm::storage::MemoryStructure storm::transformer::incorporateGoalMemoryHelper	(	SparseModelType const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas )

Definition at line 59 of file MemoryIncorporation.cpp.

◆ internalBuildSubsystem()

template<typename ValueType, typename RewardModelType>

SubsystemBuilderReturnType< ValueType, RewardModelType > storm::transformer::internalBuildSubsystem	(	storm::models::sparse::Model< ValueType, RewardModelType > const &	originalModel,
		storm::storage::BitVector const &	subsystemStates,
		storm::storage::BitVector const &	subsystemActions,
		SubsystemBuilderOptions const &	options )

Definition at line 65 of file SubsystemBuilder.cpp.

◆ operator<<()

std::ostream & storm::transformer::operator<<	(	std::ostream &	os,
		const Annotation &	annotation )

Definition at line 264 of file BigStep.cpp.

◆ parsePomdpFscApplicationMode()

PomdpFscApplicationMode storm::transformer::parsePomdpFscApplicationMode ( std::string const & mode )

Definition at line 9 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ permuteStates() [1/6]

template std::shared_ptr< storm::models::sparse::Model< double > > storm::transformer::permuteStates	(	storm::models::sparse::Model< double > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

◆ permuteStates() [2/6]

template std::shared_ptr< storm::models::sparse::Model< storm::Interval > > storm::transformer::permuteStates	(	storm::models::sparse::Model< storm::Interval > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

◆ permuteStates() [3/6]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > storm::transformer::permuteStates	(	storm::models::sparse::Model< storm::RationalFunction > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

◆ permuteStates() [4/6]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > storm::transformer::permuteStates	(	storm::models::sparse::Model< storm::RationalInterval > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

◆ permuteStates() [5/6]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > storm::transformer::permuteStates	(	storm::models::sparse::Model< storm::RationalNumber > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

◆ permuteStates() [6/6]

template<typename ValueType>

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::transformer::permuteStates	(	storm::models::sparse::Model< ValueType > const &	originalModel,
		std::vector< uint64_t > const &	permutation )

Applies the given permutation to the states of the given model.

The permutation must be a permutation of the numbers 0, 1, ..., n-1 for n = model.getNumberOfStates(). The state at position i of the input model will be moved to position permutation[i] in the output model.

Template Parameters

ValueType

Parameters

originalModel
permutation

Returns

Definition at line 21 of file StatePermuter.cpp.

◆ transformModelSpecificComponents()

template<typename ValueType, typename RewardModelType>

void storm::transformer::transformModelSpecificComponents	(	storm::models::sparse::Model< ValueType, RewardModelType > const &	originalModel,
		storm::storage::BitVector const &	subsystem,
		storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &	components )

Definition at line 24 of file SubsystemBuilder.cpp.

◆ transformRewardModel()

template<typename RewardModelType>

RewardModelType storm::transformer::transformRewardModel	(	RewardModelType const &	originalRewardModel,
		storm::storage::BitVector const &	subsystem,
		storm::storage::BitVector const &	subsystemActions,
		bool	makeRowGroupingTrivial )

Definition at line 43 of file SubsystemBuilder.cpp.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ CoefficientType

◆ UniPoly

Enumeration Type Documentation

◆ EliminationLabelBehavior

◆ PomdpFscApplicationMode

Function Documentation

◆ buildSubsystem() [1/8]

◆ buildSubsystem() [2/8]

◆ buildSubsystem() [3/8]

◆ buildSubsystem() [4/8]

◆ buildSubsystem() [5/8]

◆ buildSubsystem() [6/8]

◆ buildSubsystem() [7/8]

◆ buildSubsystem() [8/8]

◆ evaluateExtremaAnnotations()

◆ findSubgraph()

◆ getCache() [1/2]

◆ getCache() [2/2]

◆ getGoalMemory()

◆ getUntilFormulaMemory()

◆ incorporateGoalMemoryHelper()

◆ internalBuildSubsystem()

◆ operator<<()

◆ parsePomdpFscApplicationMode()

◆ permuteStates() [1/6]

◆ permuteStates() [2/6]

◆ permuteStates() [3/6]

◆ permuteStates() [4/6]

◆ permuteStates() [5/6]

◆ permuteStates() [6/6]

◆ transformModelSpecificComponents()

◆ transformRewardModel()