Namespaces
namespace	detail

namespace	elimination_actions

Classes
class	Action

class	ArrayEliminator

struct	ArrayEliminatorData

class	ArrayType

class	Assignment

class	AssignmentLevelFinder

struct	AssignmentLevelToLevelComparator

struct	AssignmentPartialOrderByLevelAndLValue
	This functor enables ordering the assignments first by the assignment level and then by lValue. More...

class	AssignmentsFinder

class	Automaton

class	AutomatonComposition

class	BasicType

class	BoundedType

class	ClockType

class	Composition

class	CompositionInformation

class	CompositionInformationVisitor

class	CompositionJsonExporter

class	CompositionSimplificationVisitor

class	CompositionVisitor

struct	ConditionalMetaEdge

class	Constant

class	ConstJaniTraverser

class	ContinuousType

class	Edge

class	EdgeContainer

class	EdgeDestination

class	ExpressionToJson

class	FilterExpression

class	FormulaToJaniJson

class	FunctionDefinition

struct	InformationObject

class	JaniLocalEliminator

class	JaniLocationExpander

class	JaniScopeChanger

class	JaniTraverser

class	JaniType

class	JsonExporter

class	Location
	Jani Location: More...

class	LValue

class	Model

class	ModelFeatures

class	OrderedAssignments

class	ParallelComposition

class	Property

struct	PropertyInterval
	Property intervals as per Jani Specification. More...

class	RewardModelInformation

class	SynchronizationVector

struct	SynchronizationVectorLexicographicalLess

class	TemplateEdge

struct	TemplateEdgeContainer

class	TemplateEdgeDestination

class	Variable

class	VariableSet

class	VariablesToConstantsTransformer

Typedefs
typedef storm::json< storm::RationalNumber >	ExportJsonType

Enumerations
enum class	ModelFeature { Arrays , DerivedOperators , Functions , StateExitRewards , TrigonometricFunctions }

enum class	ModelType { UNDEFINED = 0 , LTS = 1 , DTMC = 2 , CTMC = 3 , MDP = 4 , CTMDP = 5 , MA = 6 , TA = 7 , PTA = 8 , STA = 9 , HA = 10 , PHA = 11 , SHA = 12 }

Functions
std::ostream &	operator<< (std::ostream &stream, Assignment const &assignment)

storm::expressions::Variable	cloneVariable (storm::expressions::ExpressionManager &manager, storm::expressions::Variable const &var, std::string const &variablePrefix)

std::ostream &	operator<< (std::ostream &stream, Composition const &composition)

bool	checkDefiningExpression (storm::expressions::Variable const &var, storm::expressions::Expression const &definingExpression, storm::expressions::Expression const &constaintExpression)

std::ostream &	operator<< (std::ostream &stream, Edge const &edge)

void	eliminateFunctions (Model &model, std::vector< Property > &properties)
	Eliminates all function references in the given model and the given properties by replacing them with their corresponding definitions.

storm::expressions::Expression	eliminateFunctionCallsInExpression (storm::expressions::Expression const &expression, Model const &model)
	Eliminates all function calls in the given expression by replacing them with their corresponding definitions.

std::ostream &	operator<< (std::ostream &stream, LValue const &lValue)

storm::expressions::Expression	createSynchronizedGuard (std::vector< std::reference_wrapper< Edge const > > const &chosenEdges)

ConditionalMetaEdge	createSynchronizedMetaEdge (Automaton &automaton, std::vector< std::reference_wrapper< Edge const > > const &edgesToSynchronize)

std::vector< ConditionalMetaEdge >	createSynchronizingMetaEdges (Model const &oldModel, Model &newModel, Automaton &newAutomaton, std::vector< std::set< uint64_t > > &synchronizingActionIndices, SynchronizationVector const &vector, std::vector< std::reference_wrapper< Automaton const > > const &composedAutomata, storm::solver::SmtSolver &solver)

void	createCombinedLocation (std::vector< std::reference_wrapper< Automaton const > > const &composedAutomata, Automaton &newAutomaton, std::vector< uint64_t > const &locations, bool initial=false)

void	addEdgesToReachableLocations (std::vector< std::reference_wrapper< Automaton const > > const &composedAutomata, Automaton &newAutomaton, std::vector< ConditionalMetaEdge > const &conditionalMetaEdges)

std::string	filterName (std::string const &text)

std::ostream &	operator<< (std::ostream &out, Model const &model)

std::string	toString (ModelFeature const &modelFeature)

ModelFeatures	getAllKnownModelFeatures ()

std::ostream &	operator<< (std::ostream &stream, ModelType const &type)

std::string	to_string (ModelType const &type)

ModelType	getModelType (std::string const &input)

bool	isDeterministicModel (ModelType const &modelType)

bool	isDiscreteTimeModel (ModelType const &modelType)

std::ostream &	operator<< (std::ostream &stream, OrderedAssignments const &assignments)

std::ostream &	operator<< (std::ostream &stream, SynchronizationVector const &synchronizationVector)

bool	operator== (SynchronizationVector const &vector1, SynchronizationVector const &vector2)

bool	operator!= (SynchronizationVector const &vector1, SynchronizationVector const &vector2)

std::ostream &	operator<< (std::ostream &os, FilterExpression const &fe)

std::ostream &	operator<< (std::ostream &os, Property const &p)

bool	containsArrayExpression (Model const &model)

bool	containsArrayExpression (storm::expressions::Expression const &expression)

bool	containsFunctionCallExpression (Model const &model)

std::unordered_set< std::string >	getOccurringFunctionCalls (storm::expressions::Expression const &expression)

InformationObject	collectModelInformation (Model const &model)

std::ostream &	operator<< (std::ostream &stream, JaniType const &type)

bool	operator== (Variable const &lhs, Variable const &rhs)

bool	operator!= (Variable const &lhs, Variable const &rhs)

template<typename VarType >
void	eraseFromVariableVector (std::vector< std::shared_ptr< VarType > > &varVec, storm::expressions::Variable const &variable)

storm::expressions::Expression	substituteJaniExpression (storm::expressions::Expression const &expression, std::map< storm::expressions::Variable, storm::expressions::Expression > const &identifierToExpressionMap, bool const substituteTranscendentalNumbers)

storm::expressions::Expression	substituteJaniExpression (storm::expressions::Expression const &expression, std::unordered_map< storm::expressions::Variable, storm::expressions::Expression > const &identifierToExpressionMap, bool const substituteTranscendentalNumbers)

storm::expressions::Expression	reduceNestingInJaniExpression (storm::expressions::Expression const &expression)

ExportJsonType	anyToJson (boost::any &&input)

ExportJsonType	buildExpression (storm::expressions::Expression const &exp, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables=VariableSet(), VariableSet const &localVariables=VariableSet(), std::unordered_set< std::string > const &auxiliaryVariables={})

std::string	comparisonTypeToJani (storm::logic::ComparisonType ct)

std::string	operatorTypeToJaniString (storm::expressions::OperatorType optype)

ExportJsonType	buildActionArray (std::vector< storm::jani::Action > const &actions)

ExportJsonType	buildTypeDescription (storm::expressions::Type const &type)

void	getBoundsFromConstraints (ExportJsonType &typeDesc, storm::expressions::Variable const &var, storm::expressions::Expression const &constraint, std::vector< storm::jani::Constant > const &constants)

ExportJsonType	buildConstantsArray (std::vector< storm::jani::Constant > const &constants)

ExportJsonType	buildType (storm::jani::JaniType const &type, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables=VariableSet())

ExportJsonType	buildVariablesArray (storm::jani::VariableSet const &varSet, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables=VariableSet())

ExportJsonType	buildFunctionsArray (std::unordered_map< std::string, FunctionDefinition > const &functionDefinitions, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables=VariableSet())

ExportJsonType	buildLValue (storm::jani::LValue const &lValue, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables)

ExportJsonType	buildAssignmentArray (storm::jani::OrderedAssignments const &orderedAssignments, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables, bool commentExpressions)

ExportJsonType	buildLocationsArray (std::vector< storm::jani::Location > const &locations, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables, bool commentExpressions)

ExportJsonType	buildInitialLocations (storm::jani::Automaton const &automaton)

ExportJsonType	buildDestinations (std::vector< EdgeDestination > const &destinations, std::map< uint64_t, std::string > const &locationNames, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables, bool commentExpressions)

ExportJsonType	buildEdge (Edge const &edge, std::map< uint64_t, std::string > const &actionNames, std::map< uint64_t, std::string > const &locationNames, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables, bool commentExpressions)

ExportJsonType	buildEdges (std::vector< Edge > const &edges, std::map< uint64_t, std::string > const &actionNames, std::map< uint64_t, std::string > const &locationNames, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, VariableSet const &localVariables, bool commentExpressions)

ExportJsonType	buildAutomataArray (std::vector< storm::jani::Automaton > const &automata, std::map< uint64_t, std::string > const &actionNames, std::vector< storm::jani::Constant > const &constants, VariableSet const &globalVariables, bool commentExpressions)

std::string	janiFilterTypeString (storm::modelchecker::FilterType const &ft)

ExportJsonType	convertFilterExpression (storm::jani::FilterExpression const &fe, storm::jani::Model const &model, storm::jani::ModelFeatures &modelFeatures)

Typedef Documentation

◆ ExportJsonType

typedef storm::json<storm::RationalNumber> storm::jani::ExportJsonType

Definition at line 14 of file JSONExporter.h.

Enumeration Type Documentation

◆ ModelFeature

enum class storm::jani::ModelFeature

strong

Enumerator
Arrays
DerivedOperators
Functions
StateExitRewards
TrigonometricFunctions

Definition at line 9 of file ModelFeatures.h.

◆ ModelType

enum class storm::jani::ModelType

strong

Enumerator
UNDEFINED
LTS
DTMC
CTMC
MDP
CTMDP
MA
TA
PTA
STA
HA
PHA
SHA

Definition at line 8 of file ModelType.h.

Function Documentation

◆ addEdgesToReachableLocations()

void storm::jani::addEdgesToReachableLocations	(	std::vector< std::reference_wrapper< Automaton const > > const &	composedAutomata,
		Automaton &	newAutomaton,
		std::vector< ConditionalMetaEdge > const &	conditionalMetaEdges
	)

Definition at line 369 of file Model.cpp.

◆ anyToJson()

ExportJsonType storm::jani::anyToJson ( boost::any && input )

Definition at line 44 of file JSONExporter.cpp.

◆ buildActionArray()

ExportJsonType storm::jani::buildActionArray ( std::vector< storm::jani::Action > const & actions )

Definition at line 829 of file JSONExporter.cpp.

◆ buildAssignmentArray()

ExportJsonType storm::jani::buildAssignmentArray	(	storm::jani::OrderedAssignments const &	orderedAssignments,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables,
		bool	commentExpressions
	)

Definition at line 1003 of file JSONExporter.cpp.

◆ buildAutomataArray()

ExportJsonType storm::jani::buildAutomataArray	(	std::vector< storm::jani::Automaton > const &	automata,
		std::map< uint64_t, std::string > const &	actionNames,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		bool	commentExpressions
	)

Definition at line 1122 of file JSONExporter.cpp.

◆ buildConstantsArray()

ExportJsonType storm::jani::buildConstantsArray ( std::vector< storm::jani::Constant > const & constants )

Definition at line 889 of file JSONExporter.cpp.

◆ buildDestinations()

ExportJsonType storm::jani::buildDestinations	(	std::vector< EdgeDestination > const &	destinations,
		std::map< uint64_t, std::string > const &	locationNames,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables,
		bool	commentExpressions
	)

Definition at line 1052 of file JSONExporter.cpp.

◆ buildEdge()

ExportJsonType storm::jani::buildEdge	(	Edge const &	edge,
		std::map< uint64_t, std::string > const &	actionNames,
		std::map< uint64_t, std::string > const &	locationNames,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables,
		bool	commentExpressions
	)

Definition at line 1081 of file JSONExporter.cpp.

◆ buildEdges()

ExportJsonType storm::jani::buildEdges	(	std::vector< Edge > const &	edges,
		std::map< uint64_t, std::string > const &	actionNames,
		std::map< uint64_t, std::string > const &	locationNames,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables,
		bool	commentExpressions
	)

Definition at line 1109 of file JSONExporter.cpp.

◆ buildExpression()

ExportJsonType storm::jani::buildExpression	(	storm::expressions::Expression const &	exp,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables = `VariableSet()`,
		VariableSet const &	localVariables = `VariableSet()`,
		std::unordered_set< std::string > const &	auxiliaryVariables = `{}`
	)

Definition at line 50 of file JSONExporter.cpp.

◆ buildFunctionsArray()

ExportJsonType storm::jani::buildFunctionsArray	(	std::unordered_map< std::string, FunctionDefinition > const &	functionDefinitions,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables = `VariableSet()`
	)

Definition at line 960 of file JSONExporter.cpp.

◆ buildInitialLocations()

ExportJsonType storm::jani::buildInitialLocations ( storm::jani::Automaton const & automaton )

Definition at line 1044 of file JSONExporter.cpp.

◆ buildLocationsArray()

ExportJsonType storm::jani::buildLocationsArray	(	std::vector< storm::jani::Location > const &	locations,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables,
		bool	commentExpressions
	)

Definition at line 1022 of file JSONExporter.cpp.

◆ buildLValue()

ExportJsonType storm::jani::buildLValue	(	storm::jani::LValue const &	lValue,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables
	)

Definition at line 985 of file JSONExporter.cpp.

◆ buildType()

ExportJsonType storm::jani::buildType	(	storm::jani::JaniType const &	type,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables = `VariableSet()`
	)

Definition at line 911 of file JSONExporter.cpp.

◆ buildTypeDescription()

ExportJsonType storm::jani::buildTypeDescription ( storm::expressions::Type const & type )

Definition at line 846 of file JSONExporter.cpp.

◆ buildVariablesArray()

ExportJsonType storm::jani::buildVariablesArray	(	storm::jani::VariableSet const &	varSet,
		std::vector< storm::jani::Constant > const &	constants,
		VariableSet const &	globalVariables,
		VariableSet const &	localVariables = `VariableSet()`
	)

Definition at line 942 of file JSONExporter.cpp.

◆ checkDefiningExpression()

bool storm::jani::checkDefiningExpression	(	storm::expressions::Variable const &	var,
		storm::expressions::Expression const &	definingExpression,
		storm::expressions::Expression const &	constaintExpression
	)

Definition at line 11 of file Constant.cpp.

◆ cloneVariable()

storm::expressions::Variable storm::jani::cloneVariable	(	storm::expressions::ExpressionManager &	manager,
		storm::expressions::Variable const &	var,
		std::string const &	variablePrefix
	)

Definition at line 25 of file Automaton.cpp.

◆ collectModelInformation()

InformationObject storm::jani::collectModelInformation ( Model const & model )

Definition at line 81 of file InformationCollector.cpp.

◆ comparisonTypeToJani()

std::string storm::jani::comparisonTypeToJani ( storm::logic::ComparisonType ct )

Definition at line 116 of file JSONExporter.cpp.

◆ containsArrayExpression() [1/2]

bool storm::jani::containsArrayExpression ( Model const & model )

Definition at line 100 of file ArrayExpressionFinder.cpp.

◆ containsArrayExpression() [2/2]

bool storm::jani::containsArrayExpression ( storm::expressions::Expression const & expression )

Definition at line 106 of file ArrayExpressionFinder.cpp.

◆ containsFunctionCallExpression()

bool storm::jani::containsFunctionCallExpression ( Model const & model )

Definition at line 115 of file FunctionCallExpressionFinder.cpp.

◆ convertFilterExpression()

ExportJsonType storm::jani::convertFilterExpression	(	storm::jani::FilterExpression const &	fe,
		storm::jani::Model const &	model,
		storm::jani::ModelFeatures &	modelFeatures
	)

Definition at line 1194 of file JSONExporter.cpp.

◆ createCombinedLocation()

void storm::jani::createCombinedLocation	(	std::vector< std::reference_wrapper< Automaton const > > const &	composedAutomata,
		Automaton &	newAutomaton,
		std::vector< uint64_t > const &	locations,
		bool	initial = `false`
	)

Definition at line 349 of file Model.cpp.

◆ createSynchronizedGuard()

storm::expressions::Expression storm::jani::createSynchronizedGuard ( std::vector< std::reference_wrapper< Edge const > > const & chosenEdges )

Definition at line 159 of file Model.cpp.

◆ createSynchronizedMetaEdge()

ConditionalMetaEdge storm::jani::createSynchronizedMetaEdge	(	Automaton &	automaton,
		std::vector< std::reference_wrapper< Edge const > > const &	edgesToSynchronize
	)

Definition at line 170 of file Model.cpp.

◆ createSynchronizingMetaEdges()

std::vector< ConditionalMetaEdge > storm::jani::createSynchronizingMetaEdges	(	Model const &	oldModel,
		Model &	newModel,
		Automaton &	newAutomaton,
		std::vector< std::set< uint64_t > > &	synchronizingActionIndices,
		SynchronizationVector const &	vector,
		std::vector< std::reference_wrapper< Automaton const > > const &	composedAutomata,
		storm::solver::SmtSolver &	solver
	)

Definition at line 230 of file Model.cpp.

◆ eliminateFunctionCallsInExpression()

storm::expressions::Expression storm::jani::eliminateFunctionCallsInExpression	(	storm::expressions::Expression const &	expression,
		Model const &	model
	)

Eliminates all function calls in the given expression by replacing them with their corresponding definitions.

Only global function definitions are considered.

Definition at line 426 of file FunctionEliminator.cpp.

◆ eliminateFunctions()

void storm::jani::eliminateFunctions	(	Model &	model,
		std::vector< Property > &	properties
	)

Eliminates all function references in the given model and the given properties by replacing them with their corresponding definitions.

Definition at line 418 of file FunctionEliminator.cpp.

◆ eraseFromVariableVector()

template<typename VarType >

void storm::jani::eraseFromVariableVector	(	std::vector< std::shared_ptr< VarType > > &	varVec,
		storm::expressions::Variable const &	variable
	)

Definition at line 157 of file VariableSet.cpp.

◆ filterName()

std::string storm::jani::filterName ( std::string const & text )

Definition at line 1632 of file Model.cpp.

◆ getAllKnownModelFeatures()

ModelFeatures storm::jani::getAllKnownModelFeatures ( )

Definition at line 76 of file ModelFeatures.cpp.

◆ getBoundsFromConstraints()

void storm::jani::getBoundsFromConstraints	(	ExportJsonType &	typeDesc,
		storm::expressions::Variable const &	var,
		storm::expressions::Expression const &	constraint,
		std::vector< storm::jani::Constant > const &	constants
	)

Definition at line 863 of file JSONExporter.cpp.

◆ getModelType()

ModelType storm::jani::getModelType ( std::string const & input )

Definition at line 42 of file ModelType.cpp.

◆ getOccurringFunctionCalls()

std::unordered_set< std::string > storm::jani::getOccurringFunctionCalls ( storm::expressions::Expression const & expression )

Definition at line 121 of file FunctionCallExpressionFinder.cpp.

◆ isDeterministicModel()

bool storm::jani::isDeterministicModel ( ModelType const & modelType )

Definition at line 82 of file ModelType.cpp.

◆ isDiscreteTimeModel()

bool storm::jani::isDiscreteTimeModel ( ModelType const & modelType )

Definition at line 89 of file ModelType.cpp.

◆ janiFilterTypeString()

std::string storm::jani::janiFilterTypeString ( storm::modelchecker::FilterType const & ft )

Definition at line 1168 of file JSONExporter.cpp.

◆ operator!=() [1/2]

bool storm::jani::operator!=	(	SynchronizationVector const &	vector1,
		SynchronizationVector const &	vector2
	)

Definition at line 113 of file ParallelComposition.cpp.

◆ operator!=() [2/2]

bool storm::jani::operator!=	(	Variable const &	lhs,
		Variable const &	rhs
	)

Definition at line 169 of file Variable.cpp.

◆ operator<<() [1/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	os,
		FilterExpression const &	fe
	)

Definition at line 6 of file Property.cpp.

◆ operator<<() [2/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	os,
		Property const &	p
	)

Definition at line 129 of file Property.cpp.

◆ operator<<() [3/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	out,
		Model const &	model
	)

Definition at line 1654 of file Model.cpp.

◆ operator<<() [4/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		Assignment const &	assignment
	)

Definition at line 91 of file Assignment.cpp.

◆ operator<<() [5/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		Composition const &	composition
	)

Definition at line 25 of file Composition.cpp.

◆ operator<<() [6/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		Edge const &	edge
	)

Definition at line 175 of file Edge.cpp.

◆ operator<<() [7/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		JaniType const &	type
	)

Definition at line 76 of file JaniType.cpp.

◆ operator<<() [8/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		LValue const &	lValue
	)

Definition at line 141 of file LValue.cpp.

◆ operator<<() [9/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		ModelType const &	type
	)

Definition at line 6 of file ModelType.cpp.

◆ operator<<() [10/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		OrderedAssignments const &	assignments
	)

Definition at line 310 of file OrderedAssignments.cpp.

◆ operator<<() [11/11]

std::ostream & storm::jani::operator<<	(	std::ostream &	stream,
		SynchronizationVector const &	synchronizationVector
	)

Definition at line 89 of file ParallelComposition.cpp.

◆ operator==() [1/2]

bool storm::jani::operator==	(	SynchronizationVector const &	vector1,
		SynchronizationVector const &	vector2
	)

Definition at line 103 of file ParallelComposition.cpp.

◆ operator==() [2/2]

bool storm::jani::operator==	(	Variable const &	lhs,
		Variable const &	rhs
	)

Definition at line 165 of file Variable.cpp.

◆ operatorTypeToJaniString()

std::string storm::jani::operatorTypeToJaniString ( storm::expressions::OperatorType optype )

Definition at line 586 of file JSONExporter.cpp.

◆ reduceNestingInJaniExpression()

storm::expressions::Expression storm::jani::reduceNestingInJaniExpression ( storm::expressions::Expression const & expression )

Definition at line 6 of file JaniReduceNestingExpressionVisitor.cpp.

◆ substituteJaniExpression() [1/2]

storm::expressions::Expression storm::jani::substituteJaniExpression	(	storm::expressions::Expression const &	expression,
		std::map< storm::expressions::Variable, storm::expressions::Expression > const &	identifierToExpressionMap,
		bool const	substituteTranscendentalNumbers
	)

Definition at line 8 of file JaniExpressionSubstitutionVisitor.cpp.

◆ substituteJaniExpression() [2/2]

storm::expressions::Expression storm::jani::substituteJaniExpression	(	storm::expressions::Expression const &	expression,
		std::unordered_map< storm::expressions::Variable, storm::expressions::Expression > const &	identifierToExpressionMap,
		bool const	substituteTranscendentalNumbers
	)

Definition at line 16 of file JaniExpressionSubstitutionVisitor.cpp.

◆ to_string()

std::string storm::jani::to_string ( ModelType const & type )

Definition at line 10 of file ModelType.cpp.

◆ toString()

std::string storm::jani::toString ( ModelFeature const & modelFeature )

Definition at line 8 of file ModelFeatures.cpp.

Namespaces

Classes

Typedefs

Enumerations

Functions