Storm
A Modern Probabilistic Model Checker
|
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. | |
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.
|
static |
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.
filename | The path and name of file to be parsed. |
modelInformation | The information about the transition structure of nondeterministic model in which the transition rewards shall be used. |
Definition at line 31 of file NondeterministicSparseTransitionParser.cpp.
|
static |
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges.
filename | The path and name of file to be parsed. |
Definition at line 24 of file NondeterministicSparseTransitionParser.cpp.