diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 1b5ec197c..44e484bc0 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -29,7 +29,7 @@ namespace parser { DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::storage::SparseMatrix resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser(transitionSystemFile))); + storm::storage::SparseMatrix resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); uint_fast64_t rowCount = resultTransitionSystem.getRowCount(); @@ -42,9 +42,8 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); } if (transitionRewardFile != "") { - RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, nullptr); - result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser(transitionRewardFile, false, rewardMatrixInfo))); - delete rewardMatrixInfo; + RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, nullptr); + result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo))); } return result; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 2b21bcba5..76cd49af5 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -30,6 +30,7 @@ extern log4cplus::Logger logger; namespace storm { + namespace parser { /*! @@ -44,43 +45,36 @@ namespace parser { * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { - bool isRewardMatrix = rewardMatrixInformation != nullptr; - - uint_fast64_t nonZeroEntryCount = 0; +DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) { + DeterministicSparseTransitionParser::FirstPassResult result; - /* - * Check file header and extract number of transitions. - */ - if (!isRewardMatrix) { - // skip format hint + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] != '0') { buf = storm::parser::forwardToNextLine(buf, lineEndings); } - /* - * Check all transitions for non-zero diagonal entries and deadlock states. - */ - int_fast64_t lastRow = -1; - uint_fast64_t row, col; - uint_fast64_t readTransitionCount = 0; + // Check all transitions for non-zero diagonal entries and deadlock states. + uint_fast64_t row, col, lastRow = 0; bool rowHadDiagonalEntry = false; - double val; - maxnode = 0; while (buf[0] != '\0') { - /* - * Read row and column. - */ + + // Read the transition.. row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); - - if (!isRewardMatrix) { - if (lastRow != (int_fast64_t)row) { - if ((lastRow != -1) && (!rowHadDiagonalEntry)) { - ++nonZeroEntryCount; - rowHadDiagonalEntry = true; + // The actual read value is not needed here. + checked_strtod(buf, &buf); + + // Compensate for missing diagonal entries if desired. + if (insertDiagonalEntriesIfMissing) { + if (lastRow != row) { + if(!rowHadDiagonalEntry) { + ++result.numberOfNonzeroEntries; } - for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow < row; ++skippedRow) { - ++nonZeroEntryCount; + + // Compensate for missing rows. + for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + ++result.numberOfNonzeroEntries; } lastRow = row; rowHadDiagonalEntry = false; @@ -88,41 +82,36 @@ uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fa if (col == row) { rowHadDiagonalEntry = true; - } else if (col > row && !rowHadDiagonalEntry) { + } + + if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; - ++nonZeroEntryCount; + ++result.numberOfNonzeroEntries; } } - /* - * Check if one is larger than the current maximum id. - */ - if (row > maxnode) maxnode = row; - if (col > maxnode) maxnode = col; + // Check if a higher state id was found. + if (row > result.highestStateIndex) result.highestStateIndex = row; + if (col > result.highestStateIndex) result.highestStateIndex = col; - /* - * Read probability of this transition. - * Check, if the value is a probability, i.e. if it is between 0 and 1. - */ - val = checked_strtod(buf, &buf); - if ((val < 0.0) || (val > 1.0)) { - LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); - return 0; - } - ++nonZeroEntryCount; - ++readTransitionCount; + ++result.numberOfNonzeroEntries; buf = trimWhitespaces(buf); } - if (!rowHadDiagonalEntry && !isRewardMatrix) { - ++nonZeroEntryCount; + if(insertDiagonalEntriesIfMissing) { + if (!rowHadDiagonalEntry) { + ++result.numberOfNonzeroEntries; + } + + //Compensate for missing rows at the end of the file. + for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } } - return nonZeroEntryCount; + return result; } - - /*! * Reads a .tra file and produces a sparse matrix representing the described Markov Chain. * @@ -131,122 +120,99 @@ uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fa * @return a pointer to the created sparse matrix. */ -storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) { - /* - * Enforce locale where decimal point is '.'. - */ - setlocale(LC_NUMERIC, "C"); +storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) { - bool isRewardMatrix = rewardMatrixInformation != nullptr; + // Enforce locale where decimal point is '.'. + setlocale(LC_NUMERIC, "C"); if (!fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; } - /* - * Find out about the used line endings. - */ + // Find out about the used line endings. SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); - /* - * Open file. - */ + // Open file. MappedFile file(filename.c_str()); char* buf = file.data; - /* - * Perform first pass, i.e. count entries that are not zero. - */ - uint_fast64_t maxStateId; - uint_fast64_t nonZeroEntryCount = firstPass(file.data, lineEndings, maxStateId, rewardMatrixInformation); + // Perform first pass, i.e. count entries that are not zero. - LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros."); + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); - /* - * If first pass returned zero, the file format was wrong. - */ - if (nonZeroEntryCount == 0) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); + LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); + + // If first pass returned zero, the file format was wrong. + if (firstPass.numberOfNonzeroEntries == 0) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format."); throw storm::exceptions::WrongFormatException(); } - /* - * Perform second pass- - * - * From here on, we already know that the file header is correct. - */ - - /* - * Read file header, extract number of states. - */ - if (!isRewardMatrix) { - // skip format hint - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } + // Perform second pass. - // If the matrix that is being parsed is a reward matrix, it should match the size of the - // transition matrix. - if (isRewardMatrix) { - if (maxStateId + 1 > rewardMatrixInformation->rowCount || maxStateId + 1 > rewardMatrixInformation->columnCount) { - LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); - throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix."; - } else { - maxStateId = rewardMatrixInformation->rowCount - 1; - } + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] != '0') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); } - /* - * Creating matrix here. - * The number of non-zero elements is computed by firstPass(). - */ - LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - storm::storage::SparseMatrix resultMatrix(maxStateId + 1); - resultMatrix.initialize(nonZeroEntryCount); + // Creating matrix here. + // The number of non-zero elements is computed by firstPass(). + LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << "."); + storm::storage::SparseMatrix resultMatrix(firstPass.highestStateIndex + 1); + resultMatrix.initialize(firstPass.numberOfNonzeroEntries); if (!resultMatrix.isInitialized()) { - LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); + LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << "."); throw std::bad_alloc(); } - int_fast64_t row, lastRow = -1, col; + uint_fast64_t row, col, lastRow = 0; double val; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; - /* - * Read all transitions from file. Note that we assume that the - * transitions are listed in canonical order, otherwise this will not - * work, i.e. the values in the matrix will be at wrong places. - */ + + // Read all transitions from file. Note that we assume that the + // transitions are listed in canonical order, otherwise this will not + // work, i.e. the values in the matrix will be at wrong places. while (buf[0] != '\0') { - /* - * Read row, col and value. - */ + + // Read next transition. row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); + // Read probability of this transition. + // Check, if the value is a probability, i.e. if it is between 0 and 1. + if ((val < 0.0) || (val > 1.0)) { + LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); + throw storm::exceptions::WrongFormatException(); + } + + // Test if we moved to a new row. + // Handle all incomplete or skipped rows. if (lastRow != row) { - if ((lastRow != -1) && (!rowHadDiagonalEntry)) { - if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { + if (!rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); - } else if (!isRewardMatrix) { + } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } - // No increment for lastRow + // No increment for lastRow. rowHadDiagonalEntry = true; } - for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; - if (fixDeadlocks && !isRewardMatrix) { + if (fixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constGetOne()); rowHadDiagonalEntry = true; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); - } else if (!isRewardMatrix) { + } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); - // FIXME Why no exception at this point? This will break the App. + // Before throwing the appropriate exception we will give notice of all deadlock states. } } lastRow = row; @@ -255,14 +221,16 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (col == row) { rowHadDiagonalEntry = true; - } else if (col > row && !rowHadDiagonalEntry) { - rowHadDiagonalEntry = true; - if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { + } + + if (col > row && !rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { resultMatrix.addNextValue(row, row, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); - } else if (!isRewardMatrix) { + } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); } + rowHadDiagonalEntry = true; } resultMatrix.addNextValue(row, col, val); @@ -270,23 +238,110 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st } if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { + if (insertDiagonalEntriesIfMissing) { resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); - } else if (!isRewardMatrix) { + } else { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } } + // If we encountered deadlock and did not fix them, now is the time to throw the exception. if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; - /* - * Finalize Matrix. - */ + // Finalize Matrix. + resultMatrix.finalize(); + + return resultMatrix; +} + +/*! + * Reads a .tra file and produces a sparse matrix representing the described Markov Chain. + * + * Matrices created with this method have to be freed with the delete operator. + * @param filename input .tra file's name. + * @return a pointer to the created sparse matrix. + */ + +storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { + // Enforce locale where decimal point is '.'. + setlocale(LC_NUMERIC, "C"); + + if (!fileExistsAndIsReadable(filename.c_str())) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); + throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; + } + + // Find out about the used line endings. + SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + + // Open file. + MappedFile file(filename.c_str()); + char* buf = file.data; + + // Perform first pass, i.e. count entries that are not zero. + + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, false); + + LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); + + // If first pass returned zero, the file format was wrong. + if (firstPass.numberOfNonzeroEntries == 0) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format."); + throw storm::exceptions::WrongFormatException(); + } + + // Perform second pass. + + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] != '0') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); + } + + // The reward matrix should match the size of the transition matrix. + if (firstPass.highestStateIndex + 1 > rewardMatrixInformation.rowCount || firstPass.highestStateIndex + 1 > rewardMatrixInformation.columnCount) { + LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); + throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix."; + } else { + // If we found the right number of states or less, we set it to the number of states represented by the transition matrix. + firstPass.highestStateIndex = rewardMatrixInformation.rowCount - 1; + } + + + // Creating matrix here. + // The number of non-zero elements is computed by firstPass(). + LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << "."); + storm::storage::SparseMatrix resultMatrix(firstPass.highestStateIndex + 1); + resultMatrix.initialize(firstPass.numberOfNonzeroEntries); + if (!resultMatrix.isInitialized()) { + LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << "."); + throw std::bad_alloc(); + } + + uint_fast64_t row, col; + double val; + + // Read all transitions from file. Note that we assume that the + // transitions are listed in canonical order, otherwise this will not + // work, i.e. the values in the matrix will be at wrong places. + while (buf[0] != '\0') { + + // Read next transition. + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); + val = checked_strtod(buf, &buf); + + resultMatrix.addNextValue(row, col, val); + buf = trimWhitespaces(buf); + } + + // Finalize Matrix. resultMatrix.finalize(); return resultMatrix; } } // namespace parser + } // namespace storm diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index cca8bf9e0..7fcd62a1f 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -9,15 +9,55 @@ #include namespace storm { + namespace parser { - -/*! - * @brief Load a deterministic transition system from file and create a - * sparse adjacency matrix whose entries represent the weights of the edges - */ -storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); + +class DeterministicSparseTransitionParser { +public: + /* + * A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index. + */ + struct FirstPassResult { + + FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0) { + // Intentionally left empty. + } + + // The total number of non-zero entries of the model. + uint_fast64_t numberOfNonzeroEntries; + + // The highest state index that appears in the model. + uint_fast64_t highestStateIndex; + }; + + /*! + * @brief Load a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the weights of the edges + */ + static storm::storage::SparseMatrix parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing = true); + + /*! + * @brief Load the transition rewards for a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the rewards of the respective transitions. + */ + static storm::storage::SparseMatrix parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation); + +private: + + /* + * Performs the first pass on the input pointed to by the given buffer. + * + * @param buffer The buffer that cointains the input. + * @param lineEndings The line endings that are to be used while parsing. + * @param insertDiagonalEntriesIfMissing Flag determining whether + * @return A structure representing the result of the first pass. + */ + static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true); + +}; } // namespace parser + } // namespace storm #endif /* STORM_PARSER_TRAPARSER_H_ */ diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 94145fb66..ce89951d9 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -11,8 +11,11 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); - // Skip the format hint. - buf = storm::parser::forwardToNextLine(buf, lineEndings); + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] != '0') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); + } // Now read the transitions. int_fast64_t source, target = -1; diff --git a/test/functional/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp index e6ff86456..7cf6c1432 100644 --- a/test/functional/parser/ReadTraFileTest.cpp +++ b/test/functional/parser/ReadTraFileTest.cpp @@ -14,13 +14,13 @@ TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); } /* The following test case is based on one of the original MRMC test cases */ TEST(ReadTraFileTest, ParseFileTest1) { - storm::storage::SparseMatrix result = storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"); + storm::storage::SparseMatrix result = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"); double val = 0.0; ASSERT_TRUE(result.getValue(0, 0, &val)); @@ -65,13 +65,13 @@ TEST(ReadTraFileTest, ParseFileTest1) { } TEST(ReadTraFileTest, WrongFormatTestHeader1) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException); } TEST(ReadTraFileTest, WrongFormatTestHeader2) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException); } TEST(ReadTraFileTest, WrongFormatTestTransition) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException); }