Changed WrongFileFormatException to WrongFormatException

Also, start of documentation of PrctlParser and PrctlFileParser

src/exceptions/WrongFileFormatException.h → src/exceptions/WrongFormatException.h

@@ -1,12 +1,12 @@
 /*
- * WrongFileFormatException.h
+ * WrongFormatException.h
  *
  *  Created on: 16.08.2012
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_
-#define STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_
+#ifndef STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_
+#define STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_
 
 #include "src/exceptions/BaseException.h"
 
@@ -18,10 +18,10 @@ namespace exceptions {
  * @brief This exception is thrown when an input file
  * contains invalid or missing keys.
  */
-STORM_EXCEPTION_DEFINE_NEW(WrongFileFormatException)
+STORM_EXCEPTION_DEFINE_NEW(WrongFormatException)
 
 } //namespace exceptions
 
 } //namespace storm
 
-#endif /* STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ */
+#endif /* STORM_EXCEPTIONS_WRONGFORMATEXCEPTION_H_ */

src/parser/AtomicPropositionLabelingParser.cpp

@@ -20,7 +20,7 @@
 #include <clocale>
 #include <iostream>
 
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/utility/OsDetection.h"
 
@@ -89,7 +89,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
 			LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted.");
 			if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
 			if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
-			throw storm::exceptions::WrongFileFormatException();
+			throw storm::exceptions::WrongFormatException();
 		}
 	}
 
@@ -119,7 +119,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
 				 *	if token is longer than our buffer, the following strncpy code might get risky...
 				 */
 				LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found.");
-				throw storm::exceptions::WrongFileFormatException();
+				throw storm::exceptions::WrongFormatException();
 			} else if (cnt > 0) {
 				/*
 				 *	next token is: #DECLARATION: just skip it

src/parser/AutoParser.cpp

@@ -3,7 +3,7 @@
 #include <string>
 #include <cctype>
 
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 #include "src/models/AbstractModel.h"
 #include "src/parser/DeterministicModelParser.h"
 #include "src/parser/MdpParser.h"
@@ -19,7 +19,7 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
 	if (type == storm::models::Unknown) {
 		LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
 		LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
-		throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
+		throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile;
 	} else {
 		LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
 	}

src/parser/DeterministicSparseTransitionParser.cpp

@@ -21,7 +21,7 @@
 #include <string>
 
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 #include "boost/integer/integer_mask.hpp"
 #include "src/utility/Settings.h"
 
@@ -167,7 +167,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 */
 	if (nonZeroEntryCount == 0) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
-		throw storm::exceptions::WrongFileFormatException();
+		throw storm::exceptions::WrongFormatException();
 	}
 
 	/*
@@ -268,7 +268,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 		}
 	}
 
-	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
 	 *	Finalize Matrix.

src/parser/NonDeterministicSparseTransitionParser.cpp

@@ -23,7 +23,7 @@
 
 #include "src/utility/Settings.h"
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 #include "boost/integer/integer_mask.hpp"
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -179,7 +179,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	 */
 	if (nonzero == 0) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
-		throw storm::exceptions::WrongFileFormatException();
+		throw storm::exceptions::WrongFormatException();
 	}
 
 	/*
@@ -288,7 +288,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		curRow++;
 	}
 
-	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
 	 * Finalize matrix.

src/parser/Parser.cpp

@@ -5,7 +5,7 @@
 #include <string>
 
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -14,7 +14,7 @@ extern log4cplus::Logger logger;
 /*!
  *	Calls strtol() internally and checks if the new pointer is different
  *	from the original one, i.e. if str != *end. If they are the same, a
- *	storm::exceptions::WrongFileFormatException will be thrown.
+ *	storm::exceptions::WrongFormatException will be thrown.
  *	@param str String to parse
  *	@param end New pointer will be written there
  *	@return Result of strtol()
@@ -24,7 +24,7 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end)
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number.");
 		LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
-		throw storm::exceptions::WrongFileFormatException("Error while parsing integer. Next input token is not a number.");
+		throw storm::exceptions::WrongFormatException("Error while parsing integer. Next input token is not a number.");
 	}
 	return res;
 }
@@ -32,7 +32,7 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end)
 /*!
  *	Calls strtod() internally and checks if the new pointer is different
  *	from the original one, i.e. if str != *end. If they are the same, a
- *	storm::exceptions::WrongFileFormatException will be thrown.
+ *	storm::exceptions::WrongFormatException will be thrown.
  *	@param str String to parse
  *	@param end New pointer will be written there
  *	@return Result of strtod()
@@ -42,7 +42,7 @@ double storm::parser::Parser::checked_strtod(const char* str, char** end) {
 	if (str == *end) {
 		LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
 		LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
-		throw storm::exceptions::WrongFileFormatException("Error while parsing floating point. Next input token is not a number.");
+		throw storm::exceptions::WrongFormatException("Error while parsing floating point. Next input token is not a number.");
 	}
 	return res;
 }

src/parser/Parser.h

@@ -17,7 +17,7 @@
 
 #include <boost/integer/integer_mask.hpp>
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
 

src/parser/PrctlFileParser.cpp

@@ -14,7 +14,6 @@ PrctlFileParser::PrctlFileParser(std::string filename) {
 	// Open file and initialize result.
 	std::ifstream inputFileStream(filename, std::ios::in);
 
-	// Prepare iterators to input.
 	// TODO: Right now, this parses the whole contents of the file into a string first.
 	// While this is usually not necessary, because there exist adapters that make an input stream
 	// iterable in both directions without storing it into a string, using the corresponding

src/parser/PrctlFileParser.h

@@ -13,9 +13,31 @@
 namespace storm {
 namespace parser {
 
+/*!
+ * Reads a PRCTL formula from a file and return the formula tree.
+ *
+ * @note
+ * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
+ * class PrctlParser). However, it will not delete this object.
+ */
 class PrctlFileParser: public storm::parser::PrctlParser {
 public:
+	/*!
+	 * Reads the formula from the given file and parses it into the formula tree
+	 *
+	 * If the contents of the file could not be parsed successfully, it will throw a wrongFileFormatException.
+	 *
+	 * @param filename The name of the file to parse
+	 * @throw wrongFormatException If the input could not be parsed successfully
+	 */
 	PrctlFileParser(std::string filename);
+
+	/*!
+	 * Destructor.
+	 * At this time, empty
+	 *
+	 * Will not delete the constructed formula!
+	 */
 	virtual ~PrctlFileParser();
 };
 

src/parser/PrctlParser.cpp

@@ -3,7 +3,7 @@
 #include "src/utility/ConstTemplates.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 // Used for Boost spirit.
 #include <boost/typeof/typeof.hpp>
@@ -142,6 +142,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 } //namespace parser
 
 void storm::parser::PrctlParser::parse(std::string formulaString) {
+	// Prepare iterators to input.
 	BaseIteratorType stringIteratorBegin = formulaString.begin();
 	BaseIteratorType stringIteratorEnd = formulaString.end();
 	PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString);
@@ -179,10 +180,10 @@ void storm::parser::PrctlParser::parse(std::string formulaString) {
 		std::cerr << msg.str();
 
 		// Now propagate exception.
-		throw storm::exceptions::WrongFileFormatException() << msg.str();
+		throw storm::exceptions::WrongFormatException() << msg.str();
 	}
 	if (result_pointer == nullptr) {
-		throw storm::exceptions::WrongFileFormatException() << "Syntax error in formula";
+		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
 	}
 
 	formula = result_pointer;

src/parser/PrctlParser.h

@@ -10,16 +10,29 @@ namespace storm {
 namespace parser {
 
 /*!
- *	@brief Load PRCTL file
+ * Reads a PRCTL formula from a string and return the formula tree.
+ *
+ * If you want to read the formula from a file, use the PrctlFileParser class instead.
+ *
+ * @note
+ * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
+ * class PrctlParser). However, it will not delete this object.
  */
 class PrctlParser : Parser
 {
 	public:
-		PrctlParser() { }
+		/*!
+		 * Reads a PRCTL formula from its string representation and parses it into the formula tree
+		 *
+		 * If the string could not be parsed successfully, it will throw a wrongFormatException.
+		 *
+		 * @param formulaString The string representation of the formula
+		 * @throw wrongFormatException If the input could not be parsed successfully
+		 */
 		PrctlParser(std::string formulaString);
 		 
 		/*!
-		 *	@brief return formula object parsed from file.
+		 *	@return the parsed formula object
 		 */
 	storm::formula::AbstractFormula<double>* getFormula()
 		{
@@ -27,6 +40,15 @@ class PrctlParser : Parser
 		}
 	
 	protected:
+		/*!
+		 * Empty constructor.
+		 * Should only be used by subclasses which don't get a string representation of the formula
+		 * directly.
+		 */
+		PrctlParser() {
+			//intentionally left empty
+		}
+
 		/*!
 		 * Parses a formula and stores the result in the field "formula"
 		 * @param formula The string representation of the formula to parse
@@ -36,6 +58,9 @@ class PrctlParser : Parser
 	private:
 		storm::formula::AbstractFormula<double>* formula;
 
+		/*!
+		 * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.
+		 */
 		template<typename Iterator, typename Skipper>
 		struct PrctlGrammar;
 

src/parser/SparseStateRewardParser.cpp

@@ -20,7 +20,7 @@
 #include <vector>
 #include <clocale>
 
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/utility/OsDetection.h"
 #include "log4cplus/logger.h"
@@ -59,7 +59,7 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::
 			reward = checked_strtod(buf, &buf);
 			if (reward < 0.0) {
 				LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\".");
-				throw storm::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value.";
+				throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value.";
 			}
 
 			(*this->stateRewards)[state] = reward;

test/parser/PrctlParserTest.cpp

@@ -134,7 +134,7 @@ TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_THROW(
 			prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"),
-			storm::exceptions::WrongFileFormatException
+			storm::exceptions::WrongFormatException
 	);
 
 	delete prctlParser;
@@ -144,7 +144,7 @@ TEST(PrctlParserTest, wrongFormulaTest) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_THROW(
 			prctlParser = new storm::parser::PrctlFileParser("& a"),
-			storm::exceptions::WrongFileFormatException
+			storm::exceptions::WrongFormatException
 	);
 	delete prctlParser;
 }
@@ -153,7 +153,7 @@ TEST(PrctlParserTest, wrongFormulaTest2) {
 	storm::parser::PrctlParser* prctlParser = nullptr;
 	ASSERT_THROW(
 			prctlParser = new storm::parser::PrctlFileParser("P>0 [ F & a ]"),
-			storm::exceptions::WrongFileFormatException
+			storm::exceptions::WrongFormatException
 	);
 	delete prctlParser;
 }

test/parser/ReadLabFileTest.cpp

@@ -10,7 +10,7 @@
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/parser/AtomicPropositionLabelingParser.h"
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 #include <memory>
 
@@ -86,14 +86,14 @@ TEST(ReadLabFileTest, ParseTest) {
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest1) {
-   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException);
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest2) {
-   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException);
 }
 
 TEST(ReadLabFileTest, WrongPropositionTest) {
-   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException);
 }
 

test/parser/ReadTraFileTest.cpp

@@ -10,7 +10,7 @@
 #include "src/storage/SparseMatrix.h"
 #include "src/parser/DeterministicSparseTransitionParser.h"
 #include "src/exceptions/FileIoException.h"
-#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 #include "src/utility/IoUtility.h"
 
@@ -75,13 +75,13 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader1) {
-   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader2) {
-   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestTransition) {
-   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFileFormatException);
+   ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException);
 }