Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::parser::AutoParser< ValueType, RewardValueType > Class Template Reference

This class automatically chooses the correct parser for the given files and returns the corresponding model. More...

#include <AutoParser.h>

Static Public Member Functions

static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel (std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
 Checks the given files and parses the model within these files.
 

Detailed Description

template<typename ValueType = double, typename RewardValueType = double>
class storm::parser::AutoParser< ValueType, RewardValueType >

This class automatically chooses the correct parser for the given files and returns the corresponding model.

The choice of the parser is made using the model hint at the beginning of the given transition file.

Definition at line 26 of file AutoParser.h.

Member Function Documentation

◆ parseModel()

template<typename ValueType , typename RewardValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > storm::parser::AutoParser< ValueType, RewardValueType >::parseModel ( std::string const &  transitionsFilename,
std::string const &  labelingFilename,
std::string const &  stateRewardFilename = "",
std::string const &  transitionRewardFilename = "",
std::string const &  choiceLabelingFilename = "" 
)
static

Checks the given files and parses the model within these files.

This parser analyzes the format hint in the first line of the transition file. If this is a valid format, it will use the parser for this format, otherwise it will throw an exception.

When the files are parsed successfully, a shared pointer owning the resulting model is returned. The concrete model can be obtained using the as<Type>() member of the AbstractModel class.

Note
The number of states of the model is determined by the transitions file. The labeling file may therefore not contain labels of states that are not contained in the transitions file.
Parameters
transitionsFilenameThe path and name of the file containing the transitions of the model.
labelingFilenameThe path and name of the file containing the labels for the states of the model.
stateRewardFilenameThe path and name of the file that contains the state reward of the model. This file is optional.
transitionRewardFilenameThe path and name of the file that contains the transition rewards of the model. This file is optional.
choiceLabelingFilenameThe path and name of the file that contains the choice labeling of the model. This file is optional. Note: this file is only meaningful for certain models (currently only MDPs). If the model is not of a type for which this input is meaningful, this file will not be parsed.
Returns
A shared_ptr containing the resulting model.

Definition at line 25 of file AutoParser.cpp.


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