storm::parser::DeterministicModelParser< ValueType, RewardValueType > Class Template Reference

Loads a deterministic model (Dtmc or Ctmc) from files. More...

#include <DeterministicModelParser.h>

Static Public Member Functions
static storm::models::sparse::Dtmc< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > >	parseDtmc (std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
	Parse a Dtmc.
static storm::models::sparse::Ctmc< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > >	parseCtmc (std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
	Parse a Ctmc.

Detailed Description

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

Loads a deterministic model (Dtmc or Ctmc) from files.

Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards it loads the files, parses them and returns the desired model.

Definition at line 19 of file DeterministicModelParser.h.

Member Function Documentation

parseCtmc()

template<typename ValueType , typename RewardValueType >

storm::models::sparse::Ctmc< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > storm::parser::DeterministicModelParser< ValueType, RewardValueType >::parseCtmc ( std::string const &  transitionsFilename, std::string const &  labelingFilename, std::string const &  stateRewardFilename = "", std::string const &  transitionRewardFilename = "", std::string const &  choiceLabelingFilename = ""  )

static

Parse a Ctmc.

This method is an adapter to the actual parsing function. I.e. it uses @parseDeterministicModel internally to parse the given input files, takes its result and compiles it into a Ctmc.

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

transitionsFilename	The path and name of the file containing the transitions of the model.
labelingFilename	The path and name of the file containing the labels for the states of the model.
stateRewardFilename	The path and name of the file containing the state reward of the model. This file is optional.
transitionRewardFilename	The path and name of the file containing the transition rewards of the model. This file is optional.
choiceLabelingFilename	The path and name of the file containing the choice labeling of the model. This file is optional.

Returns

The parsed Ctmc.

Definition at line 74 of file DeterministicModelParser.cpp.

parseDtmc()

template<typename ValueType , typename RewardValueType >

storm::models::sparse::Dtmc< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > storm::parser::DeterministicModelParser< ValueType, RewardValueType >::parseDtmc ( std::string const &  transitionsFilename, std::string const &  labelingFilename, std::string const &  stateRewardFilename = "", std::string const &  transitionRewardFilename = "", std::string const &  choiceLabelingFilename = ""  )

static

Parse a Dtmc.

This method is an adapter to the actual parsing function. I.e. it uses @parseDeterministicModel internally to parse the given input files, takes its result and compiles it into a Dtmc.

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

transitionsFilename	The path and name of the file containing the transitions of the model.
labelingFilename	The path and name of the file containing the labels for the states of the model.
stateRewardFilename	The path and name of the file containing the state reward of the model. This file is optional.
transitionRewardFilename	The path and name of the file containing the transition rewards of the model. This file is optional.
choiceLabelingFilename	The path and name of the file containing the choice labeling of the model. This file is optional.

Returns

The parsed Dtmc.

Definition at line 65 of file DeterministicModelParser.cpp.

---

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

• src/storm-parsers/parser/DeterministicModelParser.h
• src/storm-parsers/parser/DeterministicModelParser.cpp