diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index b77a67af4..43c5d308a 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -125,7 +125,8 @@ namespace storm { // Now eliminate remaining whitespaces such as empty lines and start parsing. buf = trimWhitespaces(buf); - uint_fast64_t state; + uint_fast64_t state = 0; + uint_fast64_t lastState = -1; cnt = 0; // Now parse the assignments of labels to nodes. @@ -135,6 +136,12 @@ namespace storm { // Stop at the end of the line. state = checked_strtol(buf, &buf); + // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). + if(state <= lastState && lastState != -1) { + LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + } + while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { cnt = skipWord(buf) - buf; if (cnt == 0) { @@ -160,6 +167,7 @@ namespace storm { } } buf = trimWhitespaces(buf); + lastState = state; } return labeling; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index b302f68a6..67e31484f 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -181,8 +181,16 @@ namespace storm { if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; } - // Finally, build the actual matrix and return it. - return resultMatrix.build(); + // Finally, build the actual matrix, test and return it. + storm::storage::SparseMatrix result = resultMatrix.build(); + + // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. + if(isRewardFile && !result.isSubmatrixOf(transitionMatrix)) { + LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file."); + throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file."; + } + + return result; } DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, bool insertDiagonalEntriesIfMissing) { @@ -197,7 +205,7 @@ namespace storm { } // Check all transitions for non-zero diagonal entries and deadlock states. - uint_fast64_t row, col, lastRow = 0; + uint_fast64_t row, col, lastRow = 0, lastCol = -1; bool rowHadDiagonalEntry = false; while (buf[0] != '\0') { @@ -218,7 +226,6 @@ namespace storm { for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { ++result.numberOfNonzeroEntries; } - lastRow = row; rowHadDiagonalEntry = false; } @@ -237,6 +244,16 @@ namespace storm { if (col > result.highestStateIndex) result.highestStateIndex = col; ++result.numberOfNonzeroEntries; + + // Have we already seen this transition? + if (row == lastRow && col == lastCol) { + LOG4CPLUS_ERROR(logger, "The same transition (" << row << ", " << col << ") is given twice."); + throw storm::exceptions::InvalidArgumentException() << "The same transition (" << row << ", " << col << ") is given twice."; + } + + lastRow = row; + lastCol = col; + buf = trimWhitespaces(buf); } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 05e4c4a81..6e16b2f43 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -174,7 +174,16 @@ namespace storm { if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; - return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping); + // Finally, build the actual matrix, test and return it together with the rowMapping. + storm::storage::SparseMatrix resultMatrix = matrixBuilder.build(); + + // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. + if(isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation.transitionMatrix)) { + LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file."); + throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file."; + } + + return NondeterministicSparseTransitionParser::Result(resultMatrix, rowMapping); } NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, Result const & modelInformation) { @@ -189,7 +198,7 @@ namespace storm { } // Read all transitions. - uint_fast64_t source = 0, target = 0, choice = 0, lastChoice = 0, lastSource = 0; + uint_fast64_t source = 0, target = 0, choice = 0, lastChoice = 0, lastSource = 0, lastTarget = -1; double val = 0.0; NondeterministicSparseTransitionParser::FirstPassResult result; @@ -251,13 +260,19 @@ namespace storm { } } - // Read target and check if we encountered a state index that is bigger than all previously - // seen. + // Read target and check if we encountered a state index that is bigger than all previously seen. target = checked_strtol(buf, &buf); + if (target > result.highestStateIndex) { result.highestStateIndex = target; } + // Also, have we already seen this transition? + if (target == lastTarget && choice == lastChoice && source == lastSource) { + LOG4CPLUS_ERROR(logger, "The same transition (" << source << ", " << choice << ", " << target << ") is given twice."); + throw storm::exceptions::InvalidArgumentException() << "The same transition (" << source << ", " << choice << ", " << target << ") is given twice."; + } + // Read value and check whether it's positive. val = checked_strtod(buf, &buf); if (!isRewardFile && (val < 0.0 || val > 1.0 )) { @@ -273,6 +288,7 @@ namespace storm { lastChoice = choice; lastSource = source; + lastTarget = target; // Increase number of non-zero values. result.numberOfNonzeroEntries++; diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index c0e0dd28f..a71d741ad 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -35,18 +35,30 @@ namespace storm { std::vector stateRewards(stateCount); // Now parse state reward assignments. - uint_fast64_t state; + uint_fast64_t state = 0; + uint_fast64_t lastState = -1; double reward; // Iterate over states. while (buf[0] != '\0') { + // Parse state number and reward value. state = checked_strtol(buf, &buf); + + // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). + // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index). + if(state <= lastState && lastState != -1) { + LOG4CPLUS_ERROR(logger, "State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + } + if(stateCount <= state) { LOG4CPLUS_ERROR(logger, "Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states."); throw storm::exceptions::OutOfRangeException() << "Found reward for a state of an invalid index \"" << state << "\""; } + reward = checked_strtod(buf, &buf); + if (reward < 0.0) { LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\"."); throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value."; @@ -55,6 +67,7 @@ namespace storm { stateRewards[state] = reward; buf = trimWhitespaces(buf); + lastState = state; } return stateRewards; } diff --git a/test/functional/parser/AtomicPropositionLabelingParserTest.cpp b/test/functional/parser/AtomicPropositionLabelingParserTest.cpp index b41cc487b..538c54936 100644 --- a/test/functional/parser/AtomicPropositionLabelingParserTest.cpp +++ b/test/functional/parser/AtomicPropositionLabelingParserTest.cpp @@ -122,8 +122,10 @@ TEST(AtomicPropositionLabelingParserTest, LabelForNonExistentState) { // This behavior might not be ideal as multiple lines for one state are not necessary and might indicate a corrupt or wrong file. TEST(AtomicPropositionLabelingParserTest, DoubledLines) { // There are multiple lines attributing labels to the same state. - storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/doubledLines.lab"); - ASSERT_EQ(labeling.getPropositionsForState(1).size(), 3); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/doubledLines.lab"), storm::exceptions::WrongFormatException); + + // There is a line for a state that has been skipped. + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/doubledLinesSkipped.lab"), storm::exceptions::WrongFormatException); } TEST(AtomicPropositionLabelingParserTest, WrongProposition) { diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp index b4acacce7..69f1ff086 100644 --- a/test/functional/parser/DeterministicModelParserTest.cpp +++ b/test/functional/parser/DeterministicModelParserTest.cpp @@ -83,19 +83,19 @@ TEST(DeterministicModelParserTest, BasicCtmcParsing) { ASSERT_EQ(rewardSum, 125.4); } -TEST(DeterministicModelParserTest, UnmatchedFiles) { +TEST(DeterministicModelParserTest, MismatchedFiles) { // Test file combinations that do not match, i.e. differing number of states, transitions, etc. // The labeling file contains a label for a non existent state. - ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab"), storm::exceptions::OutOfRangeException); // The state reward file contains a reward for a non existent state. - ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_unmatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew"), storm::exceptions::OutOfRangeException); // The transition reward file contains rewards for a non existent state. - ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_unmatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"), storm::exceptions::OutOfRangeException); // The transition reward file contains rewards for a non existent transition - ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_unmatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_unmatched.trans.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mismatched.trans.rew"), storm::exceptions::OutOfRangeException); } diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index 296df6e4f..0e78f0992 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -101,7 +101,7 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { - // First parse a transition file. Then parse a transition reward file for the resulting transitiion matrix. + // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); storm::storage::SparseMatrix rewardMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew", transitionMatrix); @@ -223,7 +223,17 @@ TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { } TEST(DeterministicSparseTransitionParserTest, DoubledLines) { + // There is a redundant line in the transition file. As the transition already exists this should throw an exception. // Note: If two consecutive lines are doubled no exception is thrown. ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_doubledLines.tra"), storm::exceptions::InvalidArgumentException); } + +TEST(DeterministicSparseTransitionParserTest, RewardForNonExistentTransition) { + + // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); + + // There is a reward for a transition that does not exist in the transition matrix. + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_rewardForNonExTrans.trans.rew", transitionMatrix), storm::exceptions::WrongFormatException); +} diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp index c403e6a22..017be55af 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -59,13 +59,13 @@ TEST(MarkovAutomatonParserTest, BasicParsing) { ASSERT_FALSE(result.hasTransitionRewards()); } -TEST(MarkovAutomatonParserTest, UnmatchedFiles) { +TEST(MarkovAutomatonParserTest, MismatchedFiles) { // Test file combinations that do not match, i.e. differing number of states, transitions, etc. // The labeling file contains a label for a non existent state. - ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_unmatched.lab"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_mismatched.lab"), storm::exceptions::OutOfRangeException); // The state reward file contains a reward for a non existent state. - ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_unmatched.state.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_mismatched.state.rew"), storm::exceptions::OutOfRangeException); } diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp index 0e9e02801..cf56975b7 100644 --- a/test/functional/parser/NondeterministicModelParserTest.cpp +++ b/test/functional/parser/NondeterministicModelParserTest.cpp @@ -86,18 +86,18 @@ TEST(NondeterministicModelParserTest, BasicCtmdpParsing) { ASSERT_EQ(rewardSum, 1376.864); } -TEST(NondeterministicModelParserTest, UnmatchedFiles) { +TEST(NondeterministicModelParserTest, MismatchedFiles) { // Test file combinations that do not match, i.e. differing number of states, transitions, etc. // The labeling file contains a label for a non existent state. - ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab"), storm::exceptions::OutOfRangeException); // The state reward file contains a reward for a non existent state. - ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_unmatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew"), storm::exceptions::OutOfRangeException); // The transition reward file contains rewards for a non existent state. - ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_unmatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"), storm::exceptions::OutOfRangeException); // The transition reward file contains rewards for a non existent transition - ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_unmatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_unmatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_unmatched.trans.rew"), storm::exceptions::OutOfRangeException); + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mismatched.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_mismatched.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mismatched.trans.rew"), storm::exceptions::OutOfRangeException); } diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index a80442cf1..8fc55cf1c 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -255,6 +255,14 @@ TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { TEST(NondeterministicSparseTransitionParserTest, DoubledLines) { // There is a redundant line in the transition file. As the transition already exists this should throw an exception. - // Note: If two consecutive lines are doubled no exception is thrown. ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_doubledLines.tra"), storm::exceptions::InvalidArgumentException); } + +TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) { + + // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. + storm::parser::NondeterministicSparseTransitionParser::Result transitionResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"); + + // There is a reward for a transition that does not exist in the transition matrix. + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_rewardForNonExTrans.trans.rew", transitionResult), storm::exceptions::WrongFormatException); +} diff --git a/test/functional/parser/SparseStateRewardParserTest.cpp b/test/functional/parser/SparseStateRewardParserTest.cpp index 5f9838e93..2b6462ca0 100644 --- a/test/functional/parser/SparseStateRewardParserTest.cpp +++ b/test/functional/parser/SparseStateRewardParserTest.cpp @@ -12,6 +12,8 @@ #include "src/parser/SparseStateRewardParser.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/OutOfRangeException.h" TEST(SparseStateRewardParserTest, NonExistingFile) { @@ -48,3 +50,16 @@ TEST(SparseStateRewardParserTest, Whitespaces) { ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7)); } } + +TEST(SparseStateRewardParserTest, DoubledLines) { + // There are multiple lines attributing a reward to the same state. + ASSERT_THROW(storm::parser::SparseStateRewardParser::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_doubledLines.state.rew"), storm::exceptions::WrongFormatException); + + // There is a line for a state that has been skipped. + ASSERT_THROW(storm::parser::SparseStateRewardParser::parseSparseStateReward(11, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_doubledLinesSkipped.state.rew"), storm::exceptions::WrongFormatException); +} + +TEST(SparseStateRewardParserTest, RewardForNonExistentState) { + // The index of one of the state that are to be given rewards is higher than the number of states in the model. + ASSERT_THROW(storm::parser::SparseStateRewardParser::parseSparseStateReward(99, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_basic.state.rew"), storm::exceptions::OutOfRangeException); +}