diff --git a/src/parser/MarkovAutomatonParser.h b/src/parser/MarkovAutomatonParser.h index 6f3ea5d01..19dcbafd0 100644 --- a/src/parser/MarkovAutomatonParser.h +++ b/src/parser/MarkovAutomatonParser.h @@ -28,7 +28,7 @@ namespace storm { * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata. * @return The parsed MarkovAutomaton. */ - static storm::models::MarkovAutomaton parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename); + static storm::models::MarkovAutomaton parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = ""); }; } // namespace parser diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 78cc5c978..10682dc04 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -2,6 +2,7 @@ #include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/FileIoException.h" #include "src/parser/MappedFile.h" #include "src/utility/cstring.h" @@ -263,7 +264,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() << "Error while parsing " << filename << ": File does not exist or is not readable."; + throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; } // Open file and prepare pointer to buffer. diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index ad4d815de..9827a7ed7 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -8,6 +8,7 @@ #include "src/parser/SparseStateRewardParser.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/OutOfRangeException.h" #include "src/utility/cstring.h" #include "src/parser/MappedFile.h" #include "log4cplus/logger.h" @@ -23,7 +24,7 @@ namespace storm { // Open file. 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::WrongFormatException() << "Error while parsing " << filename << ": File does not exist or is not readable."; } MappedFile file(filename.c_str()); @@ -40,6 +41,10 @@ namespace storm { while (buf[0] != '\0') { // Parse state number and reward value. state = checked_strtol(buf, &buf); + 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 << "\"."); diff --git a/test/functional/parser/MappedFileTest.cpp b/test/functional/parser/MappedFileTest.cpp new file mode 100644 index 000000000..f63632362 --- /dev/null +++ b/test/functional/parser/MappedFileTest.cpp @@ -0,0 +1,46 @@ +/* + * MappedFileTest.cpp + * + * Created on: Feb 25, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include +#include "src/parser/MappedFile.h" +#include "src/exceptions/FileIoException.h" + +TEST(MappedFileTest, NonExistingFile) { + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::MappedFile(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + +TEST(MappedFileTest, BasicFunctionality) { + + // Open a file and test if the content is loaded as expected. + storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt"); + std::string testString = "This is a test string.\n"; + ASSERT_EQ(file.getDataEnd() - file.getData(), testString.length()); + char const * testStringPtr = testString.c_str(); + for(char* dataPtr = file.getData(); dataPtr < file.getDataEnd(); dataPtr++) { + ASSERT_EQ(*dataPtr, *testStringPtr); + testStringPtr++; + } +} + +TEST(MappedFileTest, ExistsAndReadble) { + + // Test the fileExistsAndIsReadable() method under various circumstances. + + // File exists and is readable. + ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt")); + + // File does not exist. + ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not")); + + // File exists but is not readable. + // TODO: Find portable solution to providing a situation in which a file exists but is not readable. + //ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_CPP_TESTS_BASE_PATH "/functional/parser/unreadableFile.txt")); +} diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp new file mode 100644 index 000000000..5be7e32e4 --- /dev/null +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -0,0 +1,71 @@ +/* + * MarkovAutomatonParserTest.cpp + * + * Created on: 25.02.2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/MarkovAutomatonParser.h" +#include "src/exceptions/FileIoException.h" + +TEST(MarkovAutomatonParserTest, NonExistingFile) { + + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + +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"); + + // Test sizes and counts. + ASSERT_EQ(result.getNumberOfStates(), 6); + ASSERT_EQ(result.getNumberOfChoices(), 7); + ASSERT_EQ(result.getNumberOfTransitions(), 12); + + // Test the exit rates. These have to be 0 for all non-Markovian states. + std::vector rates = result.getExitRates(); + ASSERT_EQ(result.getExitRate(0), 2); + ASSERT_FALSE(result.isMarkovianState(1)); + ASSERT_EQ(result.getExitRate(1), 0); + ASSERT_EQ(result.getExitRate(2), 15); + ASSERT_FALSE(result.isMarkovianState(3)); + ASSERT_EQ(result.getExitRate(3), 0); + ASSERT_FALSE(result.isMarkovianState(4)); + ASSERT_EQ(result.getExitRate(4), 0); + ASSERT_FALSE(result.isMarkovianState(5)); + ASSERT_EQ(result.getExitRate(5), 0); + + // Test the labeling. + ASSERT_EQ(result.getStateLabeling().getNumberOfAtomicPropositions(), 3); + ASSERT_EQ(result.getInitialStates().getNumberOfSetBits(), 1); + ASSERT_EQ(result.getLabelsForState(4).size(), 0); + ASSERT_EQ(result.getStateLabeling().getLabeledStates("goal").getNumberOfSetBits(), 1); + + // Test the state rewards. + ASSERT_TRUE(result.hasStateRewards()); + double rewardSum = 0; + for(uint_fast64_t i = 0; i < result.getStateRewardVector().size(); i++) { + rewardSum += result.getStateRewardVector()[i]; + } + ASSERT_EQ(rewardSum, 1015.765099984); + ASSERT_EQ(result.getStateRewardVector()[0], 0); + + // Test the transition rewards. + ASSERT_FALSE(result.hasTransitionRewards()); +} + +TEST(MarkovAutomatonParserTest, 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::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); +} diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index bb8f4102b..30d84c5e0 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -9,19 +9,24 @@ #include "storm-config.h" #include "src/settings/Settings.h" -#include #include #include "src/parser/MarkovAutomatonSparseTransitionParser.h" -#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" +#include "src/exceptions/FileIoException.h" #define STATE_COUNT 6 #define CHOICE_COUNT 7 +TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile) { + + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) { // The file that will be used for the test. @@ -201,37 +206,3 @@ TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { 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) -{ - std::stringstream s; - s << std::setprecision(precision) << std::setiosflags(std::ios_base::fixed) << val; - s >> val; - return val; -} - -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"); - - // 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)); - } -} - -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", ""); - - // Test sizes and counts. - ASSERT_EQ(result.getNumberOfStates(), STATE_COUNT); - ASSERT_EQ(result.getNumberOfChoices(), CHOICE_COUNT); - ASSERT_EQ(result.getNumberOfTransitions(), 12); - - // Test - std::vector rates = result.getExitRates(); - ASSERT_EQ(rates[0], 2); -} diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp new file mode 100644 index 000000000..b9740adcb --- /dev/null +++ b/test/functional/parser/NondeterministicModelParserTest.cpp @@ -0,0 +1,31 @@ +/* + * NondeterministicModelParserTest.cpp + * + * Created on: Feb 26, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/NondeterministicModelParser.h" +#include "src/models/Mdp.h" +#include "src/models/Ctmdp.h" +#include "src/exceptions/FileIoException.h" + +TEST(NondeterministicModelParserTest, NonExistingFile) { + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! +} + +TEST(NondeterministicModelParserTest, BasicMdpParsing) { + +} + + +TEST(NondeterministicModelParserTest, BasicCtmdpParsing) { + +} + +TEST(NondeterministicModelParserTest, UnmatchedFiles) { + +} diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp new file mode 100644 index 000000000..7f2b3b866 --- /dev/null +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -0,0 +1,49 @@ +/* + * NondeterministicSparseTransitionParserTest.cpp + * + * Created on: Feb 26, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/NondeterministicSparseTransitionParser.h" +#include "src/storage/SparseMatrix.h" +#include "src/settings/InternalOptionMemento.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFormatException.h" + +TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) { + + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! +} + + +TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) { + +} + +TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { + +} + +TEST(NondeterministicSparseTransitionParserTest, Whitespaces) { + +} + +TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { + +} + +TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { + +} + +TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { + +} + +TEST(NondeterministicSparseTransitionParserTest, DoubledLines) { + +} diff --git a/test/functional/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp deleted file mode 100644 index ff447488d..000000000 --- a/test/functional/parser/ParseMdpTest.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/* - * ParseMdpTest.cpp - * - * Created on: 14.01.2013 - * Author: Thomas Heinemann - */ - - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/NondeterministicModelParser.h" - -TEST(ParseMdpTest, parseAndOutput) { - storm::models::Mdp mdp = storm::parser::NondeterministicModelParser::parseMdp( - STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra", - STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); - storm::storage::SparseMatrix const& matrix = mdp.getTransitionMatrix(); - - ASSERT_EQ(mdp.getNumberOfStates(), (uint_fast64_t)3); - ASSERT_EQ(mdp.getNumberOfTransitions(), (uint_fast64_t)11); - ASSERT_EQ(matrix.getRowCount(), (uint_fast64_t)(2 * 3)); - ASSERT_EQ(matrix.getColumnCount(), (uint_fast64_t)3); -} - - diff --git a/test/functional/parser/StateRewardParserTest.cpp b/test/functional/parser/StateRewardParserTest.cpp new file mode 100644 index 000000000..aea2e80c0 --- /dev/null +++ b/test/functional/parser/StateRewardParserTest.cpp @@ -0,0 +1,32 @@ +/* + * MarkovAutomatonParserTest.cpp + * + * Created on: 26.02.2014 + * Author: Manuel Sascha Weiand + */ + +#include "gtest/gtest.h" +#include "storm-config.h" + +#include + +#include "src/parser/SparseStateRewardParser.h" + +double round(double val, int precision) +{ + std::stringstream s; + s << std::setprecision(precision) << std::setiosflags(std::ios_base::fixed) << val; + s >> val; + return val; +} + +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"); + + // 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)); + } +} diff --git a/test/functional/parser/testStringFile.txt b/test/functional/parser/testStringFile.txt new file mode 100644 index 000000000..fe200f008 --- /dev/null +++ b/test/functional/parser/testStringFile.txt @@ -0,0 +1 @@ +This is a test string.