DeterministicSparseTransitionParser.h

Go to the documentation of this file.

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

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

        uint_fast64_t numberOfNonzeroEntries;

        uint_fast64_t highestStateIndex;
    };

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

    template<typename MatrixValueType>
    static storm::storage::SparseMatrix<ValueType> parseDeterministicTransitionRewards(std::string const& filename,
                                                                                       storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix);
 
   private:
    /*
     * Performs the first pass on the input pointed to by the given buffer to obtain the number of
     * transitions and the maximum node id.
     *
     * @param buffer The buffer that contains the input.
     * @param reserveDiagonalElements A flag indicating whether the diagonal elements should be counted as if they
     * were present to enable fixes later.
     * @return A structure representing the result of the first pass.
     */
    static FirstPassResult firstPass(char const* buffer, bool reserveDiagonalElements);
 
    /*
     * The main parsing routine.
     * Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix.
     *
     * @param filename The path and name of the file to be parsed.
     * @param rewardFile A flag set iff the file to be parsed contains transition rewards.
     * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed
     * file.
     * @param transitionMatrix The transition matrix of the system (this is only meaningful if isRewardFile is set to true).
     * @return A SparseMatrix containing the parsed file contents.
     */
    template<typename MatrixValueType>
    static storm::storage::SparseMatrix<ValueType> parse(std::string const& filename, bool isRewardFile,
                                                         storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix,
                                                         ExplicitModelParserOptions const& options = ExplicitModelParserOptions());
};
 
}  // namespace parser
}  // namespace storm