Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | List of all members
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: