Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicSparseTransitionParser.h
Go to the documentation of this file.
1#ifndef STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_
2#define STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_
3
5
6#include <vector>
7
8namespace storm {
9namespace parser {
10
18template<typename ValueType = double>
20 public:
31 // Intentionally left empty.
32 }
33
36
38 uint_fast64_t highestStateIndex;
39
41 uint_fast64_t choices;
42 };
43
50
58 template<typename MatrixValueType>
60 std::string const& filename, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation);
61
62 private:
77 template<typename MatrixValueType>
78 static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation);
79
91 template<typename MatrixValueType>
92 static storm::storage::SparseMatrix<ValueType> parse(std::string const& filename, bool isRewardFile,
93 storm::storage::SparseMatrix<MatrixValueType> const& modelInformation);
94};
95
96} // namespace parser
97} // namespace storm
98
99#endif /* STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H__H_ */
A class providing the functionality to parse the transitions of a nondeterministic model.
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 entrie...
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitions(std::string const &filename)
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entrie...
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18
A structure representing the result of the first pass of this parser.
uint_fast64_t numberOfNonzeroEntries
The total number of non-zero entries of the model.
uint_fast64_t highestStateIndex
The highest state index that appears in the model.
uint_fast64_t choices
The total number of nondeterministic choices within the transition system.