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

Loads a nondeterministic model (Mdp or Ctmdp) from files. More...

#include <NondeterministicModelParser.h>

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

Detailed Description

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

Loads a nondeterministic model (Mdp or Ctmdp) 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 17 of file NondeterministicModelParser.h.

Member Function Documentation

parseMdp()

template<typename ValueType , typename RewardValueType >

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

static

Parse a Mdp.

This method is an adapter to the actual parsing function. I.e. it uses @parseNondeterministicModel 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 Mdp.

Definition at line 67 of file NondeterministicModelParser.cpp.

---

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

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