Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::parser::NondeterministicSparseTransitionParser< ValueType > Class Template Reference

A class providing the functionality to parse the transitions of a nondeterministic model. More...

#include <NondeterministicSparseTransitionParser.h>

Classes

struct  FirstPassResult
 A structure representing the result of the first pass of this parser. More...
 

Static Public Member Functions

static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitions (std::string const &filename)
 Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.
 
template<typename MatrixValueType >
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitionRewards (std::string const &filename, storm::storage::SparseMatrix< MatrixValueType > const &modelInformation)
 Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.
 

Detailed Description

template<typename ValueType = double>
class storm::parser::NondeterministicSparseTransitionParser< ValueType >

A class providing the functionality to parse the transitions of a nondeterministic model.

The file is parsed in two passes. The first pass tests the file format and collects statistical data needed for the second pass. The second pass then collects the actual file data and compiles it into a Result.

Definition at line 19 of file NondeterministicSparseTransitionParser.h.

Member Function Documentation

◆ parseNondeterministicTransitionRewards()

template<typename ValueType >
template<typename MatrixValueType >
template storm::storage::SparseMatrix< double > storm::parser::NondeterministicSparseTransitionParser< ValueType >::parseNondeterministicTransitionRewards ( std::string const &  filename,
storm::storage::SparseMatrix< MatrixValueType > const &  modelInformation 
)
static

Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.

Parameters
filenameThe path and name of file to be parsed.
modelInformationThe information about the transition structure of nondeterministic model in which the transition rewards shall be used.
Returns
A struct containing the parsed file contents, i.e. the transition reward matrix and the mapping between its rows and the states of the model.

Definition at line 31 of file NondeterministicSparseTransitionParser.cpp.

◆ parseNondeterministicTransitions()

template<typename ValueType >
storm::storage::SparseMatrix< ValueType > storm::parser::NondeterministicSparseTransitionParser< ValueType >::parseNondeterministicTransitions ( std::string const &  filename)
static

Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.

Parameters
filenameThe path and name of file to be parsed.

Definition at line 24 of file NondeterministicSparseTransitionParser.cpp.


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