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	UniPolyDefaultCompare
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	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
struct	TransitionToActionRewardTransformerReturnType

Typedefs
using	UniPoly = carl::UnivariatePolynomial<RationalFunctionCoefficient>
using	UniPolyAnnotationMap = std::map<UniPoly, Annotation, UniPolyDefaultCompare>
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)
std::shared_ptr< storm::models::sparse::Model< double > >	sparseRationalModelToDouble (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &inputModel, double precision)
std::shared_ptr< storm::models::sparse::Model< double > >	sparseRationalModelToDouble (std::shared_ptr< models::sparse::Model< storm::RationalNumber > > const &inputModel, double precision)
	Returns a model equivalent to `inputModel` with all probabilities, rates, and rewards converted to double.
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())
template<typename ValueType, typename RewardModelType>
TransitionToActionRewardTransformerReturnType< ValueType, RewardModelType >	transformTransitionToActionRewards (std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
	Replaces transition branch rewards from all given reward models and replaces them by equivalent state-action based rewards.
template TransitionToActionRewardTransformerReturnType< double >	transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< double > > (std::shared_ptr< storm::models::sparse::Model< double > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< storm::RationalNumber >	transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalNumber > > (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< storm::RationalFunction >	transformTransitionToActionRewards< storm::RationalFunction, storm::models::sparse::StandardRewardModel< storm::RationalFunction > > (std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< storm::Interval >	transformTransitionToActionRewards< storm::Interval, storm::models::sparse::StandardRewardModel< storm::Interval > > (std::shared_ptr< storm::models::sparse::Model< storm::Interval > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< storm::RationalInterval >	transformTransitionToActionRewards< storm::RationalInterval, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > (std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > >	transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< storm::Interval > > (std::shared_ptr< storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template TransitionToActionRewardTransformerReturnType< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >	transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > > originalModel, std::vector< std::string > const &relevantRewardModelNames)
template<typename ValueType>
TransitionToActionRewardTransformerReturnType< ValueType >	transformTransitionToActionRewards (std::shared_ptr< storm::models::sparse::Model< ValueType > > originalModel, std::vector< std::string > const &relevantRewardModelNames)

Typedef Documentation

◆ CoefficientType

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

Definition at line 34 of file RobustParameterLifter.cpp.

◆ UniPoly

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

Definition at line 33 of file BigStep.cpp.

◆ UniPolyAnnotationMap

using storm::transformer::UniPolyAnnotationMap = std::map<UniPoly, Annotation, UniPolyDefaultCompare>

Definition at line 178 of file BigStep.h.

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

◆ sparseRationalModelToDouble() [1/2]

std::shared_ptr< storm::models::sparse::Model< double > > storm::transformer::sparseRationalModelToDouble	(	std::shared_ptr< models::sparse::Model< storm::RationalNumber > > const &	inputModel,
		double	precision )

Returns a model equivalent to inputModel with all probabilities, rates, and rewards converted to double.

Parameters

precision The tolerance used to determine whether the converted transition matrix needs to be normalized. Ignored for CTMCs.

Precondition: inputModel is not null.

◆ sparseRationalModelToDouble() [2/2]

std::shared_ptr< storm::models::sparse::Model< double > > storm::transformer::sparseRationalModelToDouble	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &	inputModel,
		double	precision )

Definition at line 16 of file SparseRationalModelToDoubleTransformer.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.

◆ transformTransitionToActionRewards() [1/2]

template<typename ValueType>

TransitionToActionRewardTransformerReturnType< ValueType > storm::transformer::transformTransitionToActionRewards	(	std::shared_ptr< storm::models::sparse::Model< ValueType > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

Definition at line 43 of file TransitionToActionRewardTransformer.h.

◆ transformTransitionToActionRewards() [2/2]

template<typename ValueType, typename RewardModelType>

TransitionToActionRewardTransformerReturnType< ValueType, RewardModelType > storm::transformer::transformTransitionToActionRewards	(	std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

Replaces transition branch rewards from all given reward models and replaces them by equivalent state-action based rewards.

This is done by potentially adding intermediate states at which the corresponding reward is collected and which have a Dirac transition to the original state. Notes:

this construction potentially invalidates step-based properties, e.g., step-bounded reachability or discrete-time LRA properties. Also Until formulas with non-trivial left-hand-side will likely be invalidated
originalToNewStateIndices maps states of the original model to their positions within the transformed model. Those states are kept in the same order.
the introduced intermediate states that lead to original state 's' are located directly in front of 's'.
the number of intermediate states is kept small, e.g., if two distinct states 's_1' and 's_2' transition to 's' with the same transition reward (w.r.t. all reward models), only one intermediate state is introduced.
for Markov automata, the intermediate states are probabilistic (instantaneous). For CTMCs, the intermediate states have rate 1.
intermediate states do not get any label. All labels from the original model are preserved at the original states

possible improvement: Preprocessing: move transition rewards to action if it is the same for all successor states

Parameters

originalModel	The original model.
relevantRewardModelNames	The names of the reward models that should be transformed. Error if the model does not contain a reward model with this name.

Returns: The transformed model and the positions of the original model states in the new (larger) transformed model.

Definition at line 78 of file TransitionToActionRewardTransformer.cpp.

◆ transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< double > >()

template TransitionToActionRewardTransformerReturnType< double > storm::transformer::transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< double > >	(	std::shared_ptr< storm::models::sparse::Model< double > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< storm::Interval > >()

template TransitionToActionRewardTransformerReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > > storm::transformer::transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< storm::Interval > >	(	std::shared_ptr< storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< storm::Interval, storm::models::sparse::StandardRewardModel< storm::Interval > >()

template TransitionToActionRewardTransformerReturnType< storm::Interval > storm::transformer::transformTransitionToActionRewards< storm::Interval, storm::models::sparse::StandardRewardModel< storm::Interval > >	(	std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< storm::RationalFunction, storm::models::sparse::StandardRewardModel< storm::RationalFunction > >()

template TransitionToActionRewardTransformerReturnType< storm::RationalFunction > storm::transformer::transformTransitionToActionRewards< storm::RationalFunction, storm::models::sparse::StandardRewardModel< storm::RationalFunction > >	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< storm::RationalInterval, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >()

template TransitionToActionRewardTransformerReturnType< storm::RationalInterval > storm::transformer::transformTransitionToActionRewards< storm::RationalInterval, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >()

template TransitionToActionRewardTransformerReturnType< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > storm::transformer::transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

◆ transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalNumber > >()

template TransitionToActionRewardTransformerReturnType< storm::RationalNumber > storm::transformer::transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalNumber > >	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	originalModel,
		std::vector< std::string > const &	relevantRewardModelNames )

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ CoefficientType

◆ UniPoly

◆ UniPolyAnnotationMap

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]

◆ sparseRationalModelToDouble() [1/2]

◆ sparseRationalModelToDouble() [2/2]

◆ transformModelSpecificComponents()

◆ transformRewardModel()

◆ transformTransitionToActionRewards() [1/2]

◆ transformTransitionToActionRewards() [2/2]

◆ transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< double > >()

◆ transformTransitionToActionRewards< double, storm::models::sparse::StandardRewardModel< storm::Interval > >()

◆ transformTransitionToActionRewards< storm::Interval, storm::models::sparse::StandardRewardModel< storm::Interval > >()

◆ transformTransitionToActionRewards< storm::RationalFunction, storm::models::sparse::StandardRewardModel< storm::RationalFunction > >()

◆ transformTransitionToActionRewards< storm::RationalInterval, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >()

◆ transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalInterval > >()

◆ transformTransitionToActionRewards< storm::RationalNumber, storm::models::sparse::StandardRewardModel< storm::RationalNumber > >()