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

Loads a labeled Markov automaton from files. More...

#include <MarkovAutomatonParser.h>

Static Public Member Functions
static storm::models::sparse::MarkovAutomaton< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > >	parseMarkovAutomaton (std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
	Parses the given Markov automaton and returns an object representing the automaton.

Detailed Description

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

Loads a labeled Markov automaton from files.

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

Definition at line 17 of file MarkovAutomatonParser.h.

Member Function Documentation

parseMarkovAutomaton()

template<typename ValueType , typename RewardValueType >

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

static

Parses the given Markov automaton and returns an object representing the automaton.

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 name of the file containing the transitions of the Markov automaton.
labelingFilename	The name of the file containing the labels for the states of the Markov automaton.
stateRewardFilename	The name of the file that contains the state reward of the Markov automaton.
transitionRewardFilename	The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata.
choiceLabelingFilename	The name of the file that contains the choice labels.

Returns

The parsed MarkovAutomaton.

Definition at line 18 of file MarkovAutomatonParser.cpp.

---

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

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