Added tests for deterministic models i.e. DeterministicModelParserTest and DeterministicSparseTransitionParserTest

- Additionally lots of small changes to other tests and test files.


Former-commit-id: d0b3f968ea

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.

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

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

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<double> 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<double> 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<double>::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<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general_input.tra");
+
+	storm::storage::SparseMatrix<double> 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<double>::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<double> 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<double> 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<double> 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<double>::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);
+}

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);

test/functional/parser/MarkovAutomatonParserTest.cpp → 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<double> 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<double> 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<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", "");