NondeterministicSparseTransitionParser.h

Go to the documentation of this file.

#pragma once
 
#include "storm-parsers/parser/ExplicitModelParserOptions.h"
#include "storm/storage/SparseMatrix.h"
 
#include <vector>
 
namespace storm {
namespace parser {

template<typename ValueType = double>
class NondeterministicSparseTransitionParser {
   public:
    struct FirstPassResult {
        FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), choices(0) {
            // Intentionally left empty.
        }

        uint_fast64_t numberOfNonzeroEntries;

        uint_fast64_t highestStateIndex;

        uint_fast64_t choices;
    };

    static storm::storage::SparseMatrix<ValueType> parseNondeterministicTransitions(std::string const& filename,
                                                                                    ExplicitModelParserOptions const& options = ExplicitModelParserOptions());

    template<typename MatrixValueType>
    static storm::storage::SparseMatrix<ValueType> parseNondeterministicTransitionRewards(
        std::string const& filename, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation);
 
   private:
    template<typename MatrixValueType>
    static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix<MatrixValueType> const& modelInformation);

    template<typename MatrixValueType>
    static storm::storage::SparseMatrix<ValueType> parse(std::string const& filename, bool isRewardFile,
                                                         storm::storage::SparseMatrix<MatrixValueType> const& modelInformation,
                                                         ExplicitModelParserOptions const& options = ExplicitModelParserOptions());
};
 
}  // namespace parser
}  // namespace storm