Refactured the MarkovAutomatonParser tests, added to them and split them into two files.

- Also prepared files for the NondeterministicModelPArser tests.


Former-commit-id: f8909e2ef5

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<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
+			static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "");
 		};
 
 	} // namespace parser

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.

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 << "\".");

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 <string>
+#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"));
+}

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<double> 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<double> 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);
+}

test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp

@@ -9,19 +9,24 @@
 #include "storm-config.h"
 #include "src/settings/Settings.h"
 
-#include <cmath>
 #include <vector>
 
 #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<double> 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<double> 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<double> rates = result.getExitRates();
-	ASSERT_EQ(rates[0], 2);
-}

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) {
+
+}

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) {
+
+}

test/functional/parser/ParseMdpTest.cpp

@@ -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<double> 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<double> 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);
-}
-
-

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 <cmath>
+
+#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<double> 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/functional/parser/testStringFile.txt

@@ -0,0 +1 @@
+This is a test string.