From 77fe1e1bda1913717279ef63704b209a624f33f0 Mon Sep 17 00:00:00 2001 From: masawei Date: Thu, 27 Feb 2014 04:31:30 +0100 Subject: [PATCH] Added NondeterministcModelParser tests and SparseStateRewardParser tests. - Done with the tests. At least for now. |- There are tests for all parsers and helper classes now. Next up: Some minor fixes and finally the merge. Former-commit-id: ebb2ea50d53c0289a5806f7f00d4ec1b52d2f16e --- ...NondeterministicSparseTransitionParser.cpp | 83 ++++--- .../parser/MarkovAutomatonParserTest.cpp | 4 +- .../NondeterministicModelParserTest.cpp | 72 ++++++ ...eterministicSparseTransitionParserTest.cpp | 213 +++++++++++++++++- ...st.cpp => SparseStateRewardParserTest.cpp} | 19 +- 5 files changed, 353 insertions(+), 38 deletions(-) rename test/functional/parser/{StateRewardParserTest.cpp => SparseStateRewardParserTest.cpp} (50%) diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 6dc1ffbc2..05e4c4a81 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -12,6 +12,7 @@ #include "src/parser/MappedFile.h" #include "src/settings/Settings.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" #include "src/utility/cstring.h" @@ -44,7 +45,7 @@ namespace storm { if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; } // Open file. @@ -57,7 +58,7 @@ namespace storm { // If first pass returned zero, the file format was wrong. if (firstPass.numberOfNonzeroEntries == 0) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": erroneous file format."; } // Perform second pass. @@ -73,16 +74,18 @@ namespace storm { // The reward matrix should match the size of the transition matrix. if (firstPass.choices > modelInformation.transitionMatrix.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.transitionMatrix.getColumnCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size."); - throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size."; + throw storm::exceptions::OutOfRangeException() << "Reward matrix size exceeds transition matrix size."; } else if (firstPass.choices != modelInformation.transitionMatrix.getRowCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count."); - throw storm::exceptions::WrongFormatException() << "Reward matrix row count does not match transition matrix row count."; + throw storm::exceptions::OutOfRangeException() << "Reward matrix row count does not match transition matrix row count."; + } else if(firstPass.numberOfNonzeroEntries > modelInformation.transitionMatrix.getEntryCount()) { + LOG4CPLUS_ERROR(logger, "The reward matrix has more entries than the transition matrix. There must be a reward for a non existent transition"); + throw storm::exceptions::OutOfRangeException() << "The reward matrix has more entries than the transition matrix."; } else { firstPass.highestStateIndex = modelInformation.transitionMatrix.getColumnCount() - 1; } } - // Create the matrix builder. // The matrix to be build should have as many columns as we have nodes and as many rows as we have choices. // Those two values, as well as the number of nonzero elements, was been calculated in the first run. @@ -93,7 +96,7 @@ namespace storm { std::vector rowMapping(firstPass.highestStateIndex + 2, 0); // Initialize variables for the parsing run. - uint_fast64_t source = 0, target = 0, lastsource = 0, choice = 0, lastchoice = 0, curRow = 0; + uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; double val = 0.0; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; @@ -108,33 +111,33 @@ namespace storm { if (isRewardFile) { // If we have switched the source state, we possibly need to insert the rows of the last // source state. - if (source != lastsource) { - curRow += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource]) -(lastchoice + 1); + if (source != lastSource) { + curRow += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource]) -(lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. - for (uint_fast64_t i = lastsource + 1; i < source; ++i) { + for (uint_fast64_t i = lastSource + 1; i < source; ++i) { curRow += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows // for them - if (source != lastsource) { + if (source != lastSource) { curRow += choice + 1; - } else if (choice != lastchoice) { - curRow += choice - lastchoice; + } else if (choice != lastChoice) { + curRow += choice - lastChoice; } } else { // Increase line count if we have either finished reading the transitions of a certain state // or we have finished reading one nondeterministic choice of a state. - if ((source != lastsource || choice != lastchoice)) { + if ((source != lastSource || choice != lastChoice)) { ++curRow; } // Check if we have skipped any source node, i.e. if any node has no // outgoing transitions. If so, insert a self-loop. // Also add self-loops to rowMapping. - for (uint_fast64_t node = lastsource + 1; node < source; node++) { + for (uint_fast64_t node = lastSource + 1; node < source; node++) { hadDeadlocks = true; if (fixDeadlocks) { rowMapping.at(node) = curRow; @@ -145,7 +148,7 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); } } - if (source != lastsource) { + if (source != lastSource) { // Add this source to rowMapping, if this is the first choice we encounter for this state. rowMapping.at(source) = curRow; } @@ -156,8 +159,8 @@ namespace storm { val = checked_strtod(buf, &buf); matrixBuilder.addNextValue(curRow, target, val); - lastsource = source; - lastchoice = choice; + lastSource = source; + lastChoice = choice; // Proceed to beginning of next line in file and next row in matrix. buf = forwardToLineEnd(buf); @@ -165,7 +168,7 @@ namespace storm { buf = trimWhitespaces(buf); } - for (uint_fast64_t node = lastsource + 1; node <= firstPass.highestStateIndex + 1; node++) { + for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex + 1; node++) { rowMapping.at(node) = curRow + 1; } @@ -186,7 +189,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; double val = 0.0; NondeterministicSparseTransitionParser::FirstPassResult result; @@ -201,6 +204,11 @@ namespace storm { // Read the name of the nondeterministic choice. choice = checked_strtol(buf, &buf); + if (source < lastSource) { + LOG4CPLUS_ERROR(logger, "The current source state " << source << " is smaller than the last one " << lastSource << "."); + throw storm::exceptions::InvalidArgumentException() << "The current source state " << source << " is smaller than the last one " << lastSource << "."; + } + // Check if we encountered a state index that is bigger than all previously seen. if (source > result.highestStateIndex) { result.highestStateIndex = source; @@ -209,32 +217,34 @@ namespace storm { if (isRewardFile) { // If we have switched the source state, we possibly need to insert rows for skipped choices of the last // source state. - if (source != lastsource) { + if (source != lastSource) { // number of choices skipped = number of choices of last state - number of choices read - result.choices += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource]) - (lastchoice + 1); + result.choices += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource]) - (lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. - for (uint_fast64_t i = lastsource + 1; i < source; ++i) { + for (uint_fast64_t i = lastSource + 1; i < source; ++i) { result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows // for them. - if (source != lastsource) { + if (source != lastSource) { result.choices += choice + 1; - } else if (choice != lastchoice) { - result.choices += choice - lastchoice; + } else if (choice != lastChoice) { + result.choices += choice - lastChoice; } } else { // If we have skipped some states, we need to reserve the space for the self-loop insertion // in the second pass. - if (source > lastsource + 1) { - result.numberOfNonzeroEntries += source - lastsource - 1; - result.choices += source - lastsource - 1; - } else if (source != lastsource || choice != lastchoice) { + if (source > lastSource + 1) { + result.numberOfNonzeroEntries += source - lastSource - 1; + result.choices += source - lastSource - 1; + } + + if (source != lastSource || choice != lastChoice) { // If we have switched the source state or the nondeterministic choice, we need to // reserve one row more. ++result.choices; @@ -250,14 +260,19 @@ namespace storm { // Read value and check whether it's positive. val = checked_strtod(buf, &buf); - if ((val < 0.0) || (val > 1.0)) { + if (!isRewardFile && (val < 0.0 || val > 1.0 )) { LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\"."); NondeterministicSparseTransitionParser::FirstPassResult nullResult; return nullResult; } + else if (val < 0.0) { + LOG4CPLUS_ERROR(logger, "Expected a positive reward value but got \"" << std::string(buf, 0, 16) << "\"."); + NondeterministicSparseTransitionParser::FirstPassResult nullResult; + return nullResult; + } - lastchoice = choice; - lastsource = source; + lastChoice = choice; + lastSource = source; // Increase number of non-zero values. result.numberOfNonzeroEntries++; @@ -271,11 +286,11 @@ namespace storm { if (isRewardFile) { // If not all rows were filled for the last state, we need to insert them. - result.choices += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource] ) - (lastchoice + 1); + result.choices += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource] ) - (lastChoice + 1); // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. - for (uint_fast64_t i = lastsource + 1; i < modelInformation.rowMapping.size() - 1; ++i) { + for (uint_fast64_t i = lastSource + 1; i < modelInformation.rowMapping.size() - 1; ++i) { result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); } } diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp index 5be7e32e4..9e257d36a 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -20,7 +20,7 @@ TEST(MarkovAutomatonParserTest, NonExistingFile) { TEST(MarkovAutomatonParserTest, BasicParsing) { // Get the parsing result. - storm::models::MarkovAutomaton result = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general_input_01.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_general_input_01.state.rew"); + storm::models::MarkovAutomaton result = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_general_input.state.rew"); // Test sizes and counts. ASSERT_EQ(result.getNumberOfStates(), 6); @@ -67,5 +67,5 @@ TEST(MarkovAutomatonParserTest, UnmatchedFiles) { ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_unmatched.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_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general_input_01.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_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_unmatched.state.rew"), storm::exceptions::OutOfRangeException); } diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp index b9740adcb..e327777e2 100644 --- a/test/functional/parser/NondeterministicModelParserTest.cpp +++ b/test/functional/parser/NondeterministicModelParserTest.cpp @@ -15,17 +15,89 @@ TEST(NondeterministicModelParserTest, NonExistingFile) { // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + + ASSERT_THROW(storm::parser::NondeterministicModelParser::parseCtmdp(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); } TEST(NondeterministicModelParserTest, BasicMdpParsing) { + // Parse a Mdp and check the result. + storm::models::Mdp mdp(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.trans.rew")); + + ASSERT_EQ(mdp.getNumberOfStates(), 6); + ASSERT_EQ(mdp.getNumberOfTransitions(), 22); + ASSERT_EQ(mdp.getNumberOfChoices(), 11); + + ASSERT_EQ(mdp.getInitialStates().getNumberOfSetBits(), 2); + ASSERT_TRUE(mdp.getInitialStates().get(0)); + ASSERT_TRUE(mdp.getInitialStates().get(4)); + ASSERT_EQ(mdp.getStateLabeling().getNumberOfAtomicPropositions(), 4); + ASSERT_EQ(mdp.getLabelsForState(0).size(), 3); + + ASSERT_TRUE(mdp.hasStateRewards()); + ASSERT_EQ(mdp.getStateRewardVector()[0], 0); + ASSERT_EQ(mdp.getStateRewardVector()[4], 42); + double rewardSum = 0; + for(uint_fast64_t i = 0; i < mdp.getStateRewardVector().size(); i++) { + rewardSum += mdp.getStateRewardVector()[i]; + } + ASSERT_EQ(rewardSum, 158.32); + + ASSERT_TRUE(mdp.hasTransitionRewards()); + ASSERT_EQ(mdp.getTransitionRewardMatrix().getEntryCount(), 17); + rewardSum = 0; + for(uint_fast64_t i = 0; i < mdp.getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += mdp.getTransitionRewardMatrix().getRowSum(i); + } + ASSERT_EQ(rewardSum, 1376.864); } TEST(NondeterministicModelParserTest, BasicCtmdpParsing) { + // Parse a Ctmdp and check the result. + storm::models::Ctmdp ctmdp(storm::parser::NondeterministicModelParser::parseCtmdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.trans.rew")); + + ASSERT_EQ(ctmdp.getNumberOfStates(), 6); + ASSERT_EQ(ctmdp.getNumberOfTransitions(), 22); + ASSERT_EQ(ctmdp.getNumberOfChoices(), 11); + ASSERT_EQ(ctmdp.getInitialStates().getNumberOfSetBits(), 2); + ASSERT_TRUE(ctmdp.getInitialStates().get(0)); + ASSERT_TRUE(ctmdp.getInitialStates().get(4)); + ASSERT_EQ(ctmdp.getStateLabeling().getNumberOfAtomicPropositions(), 4); + ASSERT_EQ(ctmdp.getLabelsForState(0).size(), 3); + + ASSERT_TRUE(ctmdp.hasStateRewards()); + ASSERT_EQ(ctmdp.getStateRewardVector()[0], 0); + ASSERT_EQ(ctmdp.getStateRewardVector()[4], 42); + double rewardSum = 0; + for(uint_fast64_t i = 0; i < ctmdp.getStateRewardVector().size(); i++) { + rewardSum += ctmdp.getStateRewardVector()[i]; + } + ASSERT_EQ(rewardSum, 158.32); + + ASSERT_TRUE(ctmdp.hasTransitionRewards()); + ASSERT_EQ(ctmdp.getTransitionRewardMatrix().getEntryCount(), 17); + rewardSum = 0; + for(uint_fast64_t i = 0; i < ctmdp.getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += ctmdp.getTransitionRewardMatrix().getRowSum(i); + } + ASSERT_EQ(rewardSum, 1376.864); } TEST(NondeterministicModelParserTest, UnmatchedFiles) { + // 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_input.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_input.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_input.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); } diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index 7f2b3b866..554c65df2 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -17,33 +17,244 @@ TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) { // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + + storm::parser::NondeterministicSparseTransitionParser::Result nullInformation; + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", nullInformation), storm::exceptions::FileIoException); } TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) { + // Parse a nondeterministic transitions file and test the result. + storm::parser::NondeterministicSparseTransitionParser::Result result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra")); + + // Test the row mapping, i.e. at which row which state starts. + ASSERT_EQ(result.rowMapping.size(), 7); + ASSERT_EQ(result.rowMapping[0], 0); + ASSERT_EQ(result.rowMapping[1], 4); + ASSERT_EQ(result.rowMapping[2], 5); + ASSERT_EQ(result.rowMapping[3], 7); + ASSERT_EQ(result.rowMapping[4], 8); + ASSERT_EQ(result.rowMapping[5], 9); + ASSERT_EQ(result.rowMapping[6], 11); + + // Test the transition matrix. + ASSERT_EQ(result.transitionMatrix.getColumnCount(), 6); + ASSERT_EQ(result.transitionMatrix.getRowCount(), 11); + ASSERT_EQ(result.transitionMatrix.getEntryCount(), 22); + + // Test every entry of the matrix. + storm::storage::SparseMatrix::const_iterator cIter = result.transitionMatrix.begin(0); + + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 0.9); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.9); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 0.5); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.5); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 0.001); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.999); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.7); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.3); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0.6); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 1); } TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { + // Parse a nondeterministic transitions file and test the result. + storm::parser::NondeterministicSparseTransitionParser::Result modelInformation(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra")); + storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.trans.rew", modelInformation).transitionMatrix); + + // Test the transition matrix. + ASSERT_EQ(result.getColumnCount(), 6); + ASSERT_EQ(result.getRowCount(), 11); + ASSERT_EQ(result.getEntryCount(), 17); + + // Test every entry of the matrix. + storm::storage::SparseMatrix::const_iterator cIter = result.begin(0); + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 30); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 15.2); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 75); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 2.45); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 0.114); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 90); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 55); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 87); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 13); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 999); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.7); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.3); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 6); } TEST(NondeterministicSparseTransitionParserTest, Whitespaces) { + // Test the resilience of the parser against whitespaces. + // Do so by comparing the hashes of the transition matices and the rowMapping vectors element by element. + storm::parser::NondeterministicSparseTransitionParser::Result correctResult(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra")); + storm::parser::NondeterministicSparseTransitionParser::Result whitespaceResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_whitespaces_input.tra"); + ASSERT_EQ(correctResult.transitionMatrix.hash(), whitespaceResult.transitionMatrix.hash()); + ASSERT_EQ(correctResult.rowMapping.size(), whitespaceResult.rowMapping.size()); + for(uint_fast64_t i = 0; i < correctResult.rowMapping.size(); i++) { + ASSERT_EQ(correctResult.rowMapping[i], whitespaceResult.rowMapping[i]); + } + // Do the same (minus the unused rowMapping) for the corresponding transition rewards file (with and without whitespaces) + uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general_input.trans.rew", correctResult).transitionMatrix.hash(); + ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_whitespaces_input.trans.rew", whitespaceResult).transitionMatrix.hash()); } TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { + // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception. + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedTransitionOrder_input.tra"), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedStateOrder_input.tra"), storm::exceptions::InvalidArgumentException); + storm::parser::NondeterministicSparseTransitionParser::Result modelInformation = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input.tra"); + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedTransitionOrder_input.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedStateOrder_input.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException); } TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { + // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. + storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true); + + // Parse a transitions file with the fixDeadlocks Flag set and test if it works. + storm::parser::NondeterministicSparseTransitionParser::Result result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock_input.tra")); + + ASSERT_EQ(result.rowMapping.size(), 8); + ASSERT_EQ(result.rowMapping[5], 9); + ASSERT_EQ(result.rowMapping[6], 10); + ASSERT_EQ(result.rowMapping[7], 12); + + ASSERT_EQ(result.transitionMatrix.getColumnCount(), 7); + ASSERT_EQ(result.transitionMatrix.getRowCount(), 12); + ASSERT_EQ(result.transitionMatrix.getEntryCount(), 23); + + storm::storage::SparseMatrix::const_iterator cIter = result.transitionMatrix.begin(8); + + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.7); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.3); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0.6); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 1); } TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { + // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. + storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false); + ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock_input.tra"), storm::exceptions::WrongFormatException); } 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_input.tra"), storm::exceptions::InvalidArgumentException); } diff --git a/test/functional/parser/StateRewardParserTest.cpp b/test/functional/parser/SparseStateRewardParserTest.cpp similarity index 50% rename from test/functional/parser/StateRewardParserTest.cpp rename to test/functional/parser/SparseStateRewardParserTest.cpp index aea2e80c0..0fc88ed2f 100644 --- a/test/functional/parser/StateRewardParserTest.cpp +++ b/test/functional/parser/SparseStateRewardParserTest.cpp @@ -1,5 +1,5 @@ /* - * MarkovAutomatonParserTest.cpp + * SparseStateRewardParserTest.cpp * * Created on: 26.02.2014 * Author: Manuel Sascha Weiand @@ -12,6 +12,12 @@ #include "src/parser/SparseStateRewardParser.h" +TEST(SparseStateRewardParserTest, NonExistingFile) { + + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::SparseStateRewardParser::parseSparseStateReward(42, STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + double round(double val, int precision) { std::stringstream s; @@ -30,3 +36,14 @@ TEST(SparseStateRewardParserTest, BasicParsing) { ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7)); } } + +TEST(SparseStateRewardParserTest, Whitespaces) { + + // Get the parsing result. + std::vector result = storm::parser::SparseStateRewardParser::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_whitespaces.state.rew"); + + // Now test if the correct value were parsed. + for(int i = 0; i < 100; i++) { + ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7)); + } +}