diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 775792897..78cc5c978 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -124,9 +124,13 @@ namespace storm { // And the corresponding probability/rate. double val = checked_strtod(buf, &buf); - if (val <= 0.0) { - LOG4CPLUS_ERROR(logger, "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << "."); - throw storm::exceptions::WrongFormatException() << "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << "."; + if (val < 0.0) { + LOG4CPLUS_ERROR(logger, "Illegal negative probability/rate value for transition from " << source << " to " << target << ": " << val << "."); + throw storm::exceptions::WrongFormatException() << "Illegal negative probability/rate value for transition from " << source << " to " << target << ": " << val << "."; + } + if (!isMarkovianChoice && val > 1.0) { + LOG4CPLUS_ERROR(logger, "Illegal probability value for transition from " << source << " to " << target << ": " << val << "."); + throw storm::exceptions::WrongFormatException() << "Illegal probability value for transition from " << source << " to " << target << ": " << val << "."; } // We need to record that we found at least one successor state for the current choice. diff --git a/test/functional/parser/AutoParserTest.cpp b/test/functional/parser/AutoParserTest.cpp index cbd322f87..a9a15a228 100644 --- a/test/functional/parser/AutoParserTest.cpp +++ b/test/functional/parser/AutoParserTest.cpp @@ -73,6 +73,19 @@ TEST(AutoParserTest, Decision) { ASSERT_EQ(modelPtr->getNumberOfTransitions(), 36); // Ctmdp + // Note: For now we use the Mdp from above just given the ctmdp hint, since the implementation of the Ctmdp model seems not Quite right yet. + // We still do this test so that the code responsible for Ctmdps is executed at least once during testing. + // TODO: Fix the Ctmdp implementation and use an actual Ctmdp for testing. + modelPtr.reset(); + modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); + ASSERT_EQ(modelPtr->getType(), storm::models::CTMDP); + ASSERT_EQ(modelPtr->getNumberOfStates(), 12); + ASSERT_EQ(modelPtr->getNumberOfTransitions(), 36); // MA + modelPtr.reset(); + modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ma.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab"); + ASSERT_EQ(modelPtr->getType(), storm::models::MA); + ASSERT_EQ(modelPtr->getNumberOfStates(), 12); + ASSERT_EQ(modelPtr->getNumberOfTransitions(), 35); } diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp new file mode 100644 index 000000000..2e5ddfa16 --- /dev/null +++ b/test/functional/parser/DeterministicModelParserTest.cpp @@ -0,0 +1,101 @@ +/* + * DeterministicModelParserTest.cpp + * + * Created on: Feb 24, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/DeterministicModelParser.h" +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" +#include "src/exceptions/FileIoException.h" + +TEST(DeterministicModelParserTest, NonExistingFile) { + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + + ASSERT_THROW(storm::parser::DeterministicModelParser::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + +TEST(DeterministicModelParserTest, BasicDtmcParsing) { + + // Parse a Dtmc and check the result. + storm::models::Dtmc dtmc(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.trans.rew")); + + ASSERT_EQ(dtmc.getNumberOfStates(), 8); + ASSERT_EQ(dtmc.getNumberOfTransitions(), 21); + + ASSERT_EQ(dtmc.getInitialStates().getNumberOfSetBits(), 2); + ASSERT_TRUE(dtmc.getInitialStates().get(0)); + ASSERT_TRUE(dtmc.getInitialStates().get(7)); + ASSERT_EQ(dtmc.getStateLabeling().getNumberOfAtomicPropositions(), 5); + ASSERT_EQ(dtmc.getLabelsForState(6).size(), 2); + + ASSERT_TRUE(dtmc.hasStateRewards()); + ASSERT_EQ(dtmc.getStateRewardVector()[7], 42); + double rewardSum = 0; + for(uint_fast64_t i = 0; i < dtmc.getStateRewardVector().size(); i++) { + rewardSum += dtmc.getStateRewardVector()[i]; + } + ASSERT_EQ(rewardSum, 263.32); + + ASSERT_TRUE(dtmc.hasTransitionRewards()); + ASSERT_EQ(dtmc.getTransitionRewardMatrix().getEntryCount(), 17); + rewardSum = 0; + for(uint_fast64_t i = 0; i < dtmc.getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += dtmc.getTransitionRewardMatrix().getRowSum(i); + } + ASSERT_EQ(rewardSum, 125.4); +} + + +TEST(DeterministicModelParserTest, BasicCtmcParsing) { + + // Parse a Ctmc and check the result. + storm::models::Ctmc ctmc(storm::parser::DeterministicModelParser::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general_input.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.trans.rew")); + + ASSERT_EQ(ctmc.getNumberOfStates(), 8); + ASSERT_EQ(ctmc.getNumberOfTransitions(), 21); + + ASSERT_EQ(ctmc.getInitialStates().getNumberOfSetBits(), 2); + ASSERT_TRUE(ctmc.getInitialStates().get(0)); + ASSERT_TRUE(ctmc.getInitialStates().get(7)); + ASSERT_EQ(ctmc.getStateLabeling().getNumberOfAtomicPropositions(), 5); + ASSERT_EQ(ctmc.getLabelsForState(6).size(), 2); + + ASSERT_TRUE(ctmc.hasStateRewards()); + ASSERT_EQ(ctmc.getStateRewardVector()[7], 42); + double rewardSum = 0; + for(uint_fast64_t i = 0; i < ctmc.getStateRewardVector().size(); i++) { + rewardSum += ctmc.getStateRewardVector()[i]; + } + ASSERT_EQ(rewardSum, 263.32); + + ASSERT_TRUE(ctmc.hasTransitionRewards()); + ASSERT_EQ(ctmc.getTransitionRewardMatrix().getEntryCount(), 17); + rewardSum = 0; + for(uint_fast64_t i = 0; i < ctmc.getTransitionRewardMatrix().getRowCount(); i++) { + rewardSum += ctmc.getTransitionRewardMatrix().getRowSum(i); + } + ASSERT_EQ(rewardSum, 125.4); +} + +TEST(DeterministicModelParserTest, 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::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_input.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_input.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_input.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); +} diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp new file mode 100644 index 000000000..0c4b528b0 --- /dev/null +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -0,0 +1,229 @@ +/* + * DeterministicSparseTransitionParserTest.cpp + * + * Created on: Feb 24, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/DeterministicSparseTransitionParser.h" +#include "src/storage/SparseMatrix.h" +#include "src/settings/InternalOptionMemento.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFormatException.h" + +TEST(DeterministicSparseTransitionParserTest, NonExistingFile) { + + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + + storm::storage::SparseMatrix nullMatrix; + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", nullMatrix), storm::exceptions::FileIoException); +} + + +TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { + + // Parse a deterministic transitions file and test the resulting matrix. + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra"); + + ASSERT_EQ(transitionMatrix.getColumnCount(), 8); + ASSERT_EQ(transitionMatrix.getEntryCount(), 21); + + // Test every entry of the matrix. + storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(0); + + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 0); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 0); + 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, 0); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.4); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.4); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0.2); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 0.7); + cIter++; + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 0.9); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 0.224653); + cIter++; + ASSERT_EQ(cIter->first, 7); + ASSERT_EQ(cIter->second, 0.775347); +} + +TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { + + // First parse a transition file. Then parse a transition reward file for the resulting transitiion matrix. + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra"); + + storm::storage::SparseMatrix rewardMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.trans.rew", transitionMatrix); + + ASSERT_EQ(rewardMatrix.getColumnCount(), 8); + ASSERT_EQ(rewardMatrix.getEntryCount(), 17); + + // Test every entry of the matrix. + storm::storage::SparseMatrix::const_iterator cIter = rewardMatrix.begin(0); + + ASSERT_EQ(cIter->first, 1); + ASSERT_EQ(cIter->second, 10); + cIter++; + ASSERT_EQ(cIter->first, 2); + ASSERT_EQ(cIter->second, 5); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 5.5); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 21.4); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 4); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 2); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 3); + ASSERT_EQ(cIter->second, 0.1); + cIter++; + ASSERT_EQ(cIter->first, 4); + ASSERT_EQ(cIter->second, 1.1); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 9.5); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 6.7); + cIter++; + ASSERT_EQ(cIter->first, 0); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 5); + ASSERT_EQ(cIter->second, 0); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 12); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 35.224653); + cIter++; + ASSERT_EQ(cIter->first, 7); + ASSERT_EQ(cIter->second, 9.875347); +} + + +TEST(DeterministicSparseTransitionParserTest, Whitespaces) { + + // Test the resilience of the parser against whitespaces. + // Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with whitespaces. + uint_fast64_t correctHash = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra").hash(); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_whitespaces_input.tra"); + ASSERT_EQ(correctHash, transitionMatrix.hash()); + + // Do the same for the corresponding transition rewards file (with and without whitespaces) + correctHash = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general_input.trans.rew", transitionMatrix).hash(); + ASSERT_EQ(correctHash, storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_whitespaces_input.trans.rew", transitionMatrix).hash()); +} + +TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) { + + // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception. + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedTransitionOrder_input.tra"), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedStateOrder_input.tra"), storm::exceptions::InvalidArgumentException); + + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra"); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedTransitionOrder_input.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedStateOrder_input.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException); +} + +TEST(DeterministicSparseTransitionParserTest, 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::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock_input.tra"); + + ASSERT_EQ(transitionMatrix.getColumnCount(), 9); + ASSERT_EQ(transitionMatrix.getEntryCount(), 23); + + storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(7); + ASSERT_EQ(cIter->first, 7); + ASSERT_EQ(cIter->second, 1); + cIter++; + ASSERT_EQ(cIter->first, 6); + ASSERT_EQ(cIter->second, 0.224653); + cIter++; + ASSERT_EQ(cIter->first, 7); + ASSERT_EQ(cIter->second, 0.775347); + cIter++; + ASSERT_EQ(cIter->first, 8); + ASSERT_EQ(cIter->second, 0); +} + +TEST(DeterministicSparseTransitionParserTest, 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::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock_input.tra"), storm::exceptions::WrongFormatException); +} + +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_input.tra"), storm::exceptions::InvalidArgumentException); +} diff --git a/test/functional/parser/LabFileParserTest.cpp b/test/functional/parser/LabFileParserTest.cpp index fb236682d..0b4d58c28 100644 --- a/test/functional/parser/LabFileParserTest.cpp +++ b/test/functional/parser/LabFileParserTest.cpp @@ -118,6 +118,14 @@ TEST(LabFileParserTest, LabelForNonExistentState) { ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/labelForNonexistentState.lab"), storm::exceptions::OutOfRangeException); } +// Note: As implemented at the moment, each label given for a state in any line is set to true for that state (logical or over all lines for that state). +// This behavior might not be ideal as multiple lines for one state are not necessary and might indicate a corrupt or wrong file. +TEST(LabFileParserTest, 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); +} + TEST(LabFileParserTest, WrongProposition) { // Swapped the state index and the label at one entry. ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/labParser/swappedStateAndProposition.lab"), storm::exceptions::WrongFormatException); diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp similarity index 77% rename from test/functional/parser/MarkovAutomatonParserTest.cpp rename to test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index e063f1f35..bb8f4102b 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -16,11 +16,13 @@ #include "src/parser/SparseStateRewardParser.h" #include "src/utility/cstring.h" #include "src/parser/MarkovAutomatonParser.h" +#include "src/settings/InternalOptionMemento.h" +#include "src/exceptions/WrongFormatException.h" #define STATE_COUNT 6 #define CHOICE_COUNT 7 -TEST(MarkovAutomatonSparseTransitionParserTest, BasicParseTest) { +TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) { // The file that will be used for the test. std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra"; @@ -98,9 +100,9 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParseTest) { ASSERT_EQ(transitionMatrix.end(), cIter); } -TEST(MarkovAutomatonSparseTransitionParserTest, WhiteSpaceTest) { +TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { // The file that will be used for the test. - std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_whitespace_input_01.tra"; + std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_whitespaces_input.tra"; // Execute the parser. storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename); @@ -175,50 +177,30 @@ TEST(MarkovAutomatonSparseTransitionParserTest, WhiteSpaceTest) { ASSERT_EQ(transitionMatrix.end(), cIter); } -//TODO: Deadlock Test. I am quite sure that the deadlock state handling does not behave quite right. -// Find a way to test this by manipulating the fixDeadlocks flag of the settings. +TEST(MarkovAutomatonSparseTransitionParserTest, 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); -/* -TEST(MarkovAutomatonSparseTransitionParserTest, DeadlockTest) { - // Save the fixDeadlocks flag, since it will be manipulated during the test. - bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); - storm::settings::Settings::getInstance()->set("fixDeadlocks"); - - - // The file that will be used for the test. - std::string filename = "/functional/parser/tra_files/ma_general_input_01.tra"; - - storm::parser::MarkovAutomatonSparseTransitionParser::ResultType result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename); - - // Test if the result of the first pass has been transfered correctly - ASSERT_EQ(result.transitionMatrix.colCount, 7); - ASSERT_EQ(result.transitionMatrix.nonZeroEntryCount, 8); - ASSERT_EQ(result.markovianChoices.getNumberOfSetBits(), 2); - - // Test the general structure of the transition system (that will be an Markov automaton). - //TODO + // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works. + storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock_input.tra"); - //Do the test again but this time without the fixDeadlock flag. This should throw an exception. - storm::settings::Settings::getInstance()->unset("fixDeadlocks"); - - bool thrown = false; - - try { - // Parse the file, again. - result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename); - } catch(Exception &exception) { - // Print the exception and remember that it was thrown. - exception.print(std::cout); - thrown = true; - } + // Test if the result is consistent with the parsed Markov Automaton. + storm::storage::SparseMatrix resultMatrix(result.transitionMatrixBuilder.build(0,0)); + ASSERT_EQ(resultMatrix.getColumnCount(), STATE_COUNT + 1); + ASSERT_EQ(resultMatrix.getEntryCount(), 13); + ASSERT_EQ(result.markovianChoices.size(), CHOICE_COUNT +1); + ASSERT_EQ(result.markovianStates.size(), STATE_COUNT +1); + ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); + ASSERT_EQ(result.exitRates.size(), STATE_COUNT + 1); + ASSERT_EQ(result.nondeterministicChoiceIndices.size(), 8); +} - ASSERT_TRUE(thrown); +TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { + // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. + storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false); - // Reset the fixDeadlocks flag to its original value. - if(fixDeadlocks) { - storm::settings::Settings::getInstance()->set("fixDeadlocks"); - } -}*/ + ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock_input.tra"), storm::exceptions::WrongFormatException); +} double round(double val, int precision) { @@ -228,7 +210,7 @@ double round(double val, int precision) return val; } -TEST(SparseStateRewardParserTest, BasicParseTest) { +TEST(SparseStateRewardParserTest, BasicParsing) { // Get the parsing result. std::vector result = storm::parser::SparseStateRewardParser::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_basic.state.rew"); @@ -239,7 +221,7 @@ TEST(SparseStateRewardParserTest, BasicParseTest) { } } -TEST(MarkovAutomatonParserTest, BasicParseTest) { +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", "");