storm::storage::SymbolicModelDescription Class Reference

#include <SymbolicModelDescription.h>

Public Types
enum class	ModelType {   DTMC , CTMC , MDP , MA ,   POMDP , SMG }

Public Member Functions
	SymbolicModelDescription ()=default
	SymbolicModelDescription (storm::jani::Model const &model)
	SymbolicModelDescription (storm::prism::Program const &program)
SymbolicModelDescription &	operator= (storm::jani::Model const &model)
SymbolicModelDescription &	operator= (storm::prism::Program const &program)
bool	hasModel () const
bool	isJaniModel () const
bool	isPrismProgram () const
ModelType	getModelType () const
storm::expressions::ExpressionManager &	getManager () const
void	setModel (storm::jani::Model const &model)
void	setModel (storm::prism::Program const &program)
storm::jani::Model const &	asJaniModel () const
storm::jani::Model &	asJaniModel ()
storm::prism::Program const &	asPrismProgram () const
storm::prism::Program &	asPrismProgram ()
std::vector< std::string >	getParameterNames () const
SymbolicModelDescription	toJani (bool makeVariablesGlobal=true) const
std::pair< SymbolicModelDescription, std::vector< storm::jani::Property > >	toJani (std::vector< storm::jani::Property > const &properties, bool makeVariablesGlobal) const
	Ensures that this model is a JANI model by, e.g., converting prism to jani.
SymbolicModelDescription	preprocess (std::string const &constantDefinitionString="") const
SymbolicModelDescription	preprocess (std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
std::map< storm::expressions::Variable, storm::expressions::Expression >	parseConstantDefinitions (std::string const &constantDefinitionString) const
void	requireNoUndefinedConstants () const
bool	hasUndefinedConstants () const
std::vector< storm::expressions::Variable >	getUndefinedConstants () const

Detailed Description

Definition at line 11 of file SymbolicModelDescription.h.

Member Enumeration Documentation

ModelType

enum class storm::storage::SymbolicModelDescription::ModelType

strong

Enumerator
DTMC
CTMC
MDP
MA
POMDP
SMG

Definition at line 13 of file SymbolicModelDescription.h.

Constructor & Destructor Documentation

SymbolicModelDescription() [1/3]

storm::storage::SymbolicModelDescription::SymbolicModelDescription ( )

default

SymbolicModelDescription() [2/3]

storm::storage::SymbolicModelDescription::SymbolicModelDescription

(

storm::jani::Model const &

model

)

Definition at line 18 of file SymbolicModelDescription.cpp.

SymbolicModelDescription() [3/3]

storm::storage::SymbolicModelDescription::SymbolicModelDescription

(

storm::prism::Program const &

program

)

Definition at line 22 of file SymbolicModelDescription.cpp.

Member Function Documentation

asJaniModel() [1/2]

storm::jani::Model & storm::storage::SymbolicModelDescription::asJaniModel

(

)

Definition at line 106 of file SymbolicModelDescription.cpp.

asJaniModel() [2/2]

storm::jani::Model const & storm::storage::SymbolicModelDescription::asJaniModel

(

)

const

Definition at line 100 of file SymbolicModelDescription.cpp.

asPrismProgram() [1/2]

storm::prism::Program & storm::storage::SymbolicModelDescription::asPrismProgram

(

)

Definition at line 118 of file SymbolicModelDescription.cpp.

asPrismProgram() [2/2]

storm::prism::Program const & storm::storage::SymbolicModelDescription::asPrismProgram

(

)

const

Definition at line 112 of file SymbolicModelDescription.cpp.

getManager()

storm::expressions::ExpressionManager & storm::storage::SymbolicModelDescription::getManager

(

)

const

Definition at line 84 of file SymbolicModelDescription.cpp.

getModelType()

SymbolicModelDescription::ModelType storm::storage::SymbolicModelDescription::getModelType

(

)

const

Definition at line 48 of file SymbolicModelDescription.cpp.

getParameterNames()

std::vector< std::string > storm::storage::SymbolicModelDescription::getParameterNames

(

)

const

Definition at line 124 of file SymbolicModelDescription.cpp.

getUndefinedConstants()

std::vector< storm::expressions::Variable > storm::storage::SymbolicModelDescription::getUndefinedConstants

(

)

const

Definition at line 206 of file SymbolicModelDescription.cpp.

hasModel()

bool storm::storage::SymbolicModelDescription::hasModel

(

)

const

Definition at line 36 of file SymbolicModelDescription.cpp.

hasUndefinedConstants()

bool storm::storage::SymbolicModelDescription::hasUndefinedConstants

(

)

const

Definition at line 198 of file SymbolicModelDescription.cpp.

isJaniModel()

bool storm::storage::SymbolicModelDescription::isJaniModel

(

)

const

Definition at line 40 of file SymbolicModelDescription.cpp.

isPrismProgram()

bool storm::storage::SymbolicModelDescription::isPrismProgram

(

)

const

Definition at line 44 of file SymbolicModelDescription.cpp.

operator=() [1/2]

SymbolicModelDescription & storm::storage::SymbolicModelDescription::operator=

(

storm::jani::Model const &

model

)

Definition at line 26 of file SymbolicModelDescription.cpp.

operator=() [2/2]

SymbolicModelDescription & storm::storage::SymbolicModelDescription::operator=

(

storm::prism::Program const &

program

)

Definition at line 31 of file SymbolicModelDescription.cpp.

parseConstantDefinitions()

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::storage::SymbolicModelDescription::parseConstantDefinitions

(

std::string const &

constantDefinitionString

)

const

Definition at line 181 of file SymbolicModelDescription.cpp.

preprocess() [1/2]

SymbolicModelDescription storm::storage::SymbolicModelDescription::preprocess

(

std::map< storm::expressions::Variable, storm::expressions::Expression > const &

constantDefinitions

)

const

Definition at line 167 of file SymbolicModelDescription.cpp.

preprocess() [2/2]

SymbolicModelDescription storm::storage::SymbolicModelDescription::preprocess

(

std::string const &

constantDefinitionString = ""

)

const

Definition at line 162 of file SymbolicModelDescription.cpp.

requireNoUndefinedConstants()

void storm::storage::SymbolicModelDescription::requireNoUndefinedConstants

(

)

const

Definition at line 190 of file SymbolicModelDescription.cpp.

setModel() [1/2]

void storm::storage::SymbolicModelDescription::setModel

(

storm::jani::Model const &

model

)

Definition at line 92 of file SymbolicModelDescription.cpp.

setModel() [2/2]

void storm::storage::SymbolicModelDescription::setModel

(

storm::prism::Program const &

program

)

Definition at line 96 of file SymbolicModelDescription.cpp.

toJani() [1/2]

SymbolicModelDescription storm::storage::SymbolicModelDescription::toJani

(

bool

makeVariablesGlobal = true

)

const

Definition at line 138 of file SymbolicModelDescription.cpp.

toJani() [2/2]

std::pair< SymbolicModelDescription, std::vector< storm::jani::Property > > storm::storage::SymbolicModelDescription::toJani	(	std::vector< storm::jani::Property > const &	properties,
		bool	makeVariablesGlobal ) const

Ensures that this model is a JANI model by, e.g., converting prism to jani.

If labels or reward models had to be converted during conversion, the renamings are applied to the given properties

Returns

The jani model of this and either the new set of properties or an empty vector if no renamings were necessary

Note

The returned property vector might be empty in case no renaming is necessary.

Definition at line 149 of file SymbolicModelDescription.cpp.

---

The documentation for this class was generated from the following files:

• src/storm/storage/SymbolicModelDescription.h
• src/storm/storage/SymbolicModelDescription.cpp