diff --git a/.gitignore b/.gitignore index 268c6f690..6f15a4cb4 100644 --- a/.gitignore +++ b/.gitignore @@ -29,6 +29,7 @@ ipch/ obj/ CMakeFiles/ # The build Dir +build/ build//CMakeLists.txt /*.vcxproj /*.filters diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index cfba4218e..d8767e8d9 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -1,5 +1,5 @@ -#ifndef BASEEXCEPTION_H_ -#define BASEEXCEPTION_H_ +#ifndef MRMC_EXCEPTIONS_BASEEXCEPTION_H_ +#define MRMC_EXCEPTIONS_BASEEXCEPTION_H_ #include #include @@ -16,6 +16,10 @@ class BaseException : public std::exception : exception(cp), stream(cp.stream.str()) { } + + BaseException(const char* cstr) { + stream << cstr; + } ~BaseException() throw() { } @@ -38,4 +42,18 @@ class BaseException : public std::exception } // namespace exceptions } // namespace mrmc -#endif // BASEEXCEPTION_H_ +/* Macro to generate descendant exception classes. + * As all classes are nearly the same, this makes changing common features much easier. + */ +#define MRMC_EXCEPTION_DEFINE_NEW(exception_name) class exception_name : public BaseException { \ +public: \ + exception_name() : BaseException() { \ + } \ + exception_name(const char* cstr) : BaseException(cstr) { \ + } \ + exception_name(const exception_name& cp) : BaseException(cp) { \ + } \ +}; + + +#endif // MRMC_EXCEPTIONS_BASEEXCEPTION_H_ diff --git a/src/exceptions/FileIoException.h b/src/exceptions/FileIoException.h new file mode 100644 index 000000000..0d31af7fd --- /dev/null +++ b/src/exceptions/FileIoException.h @@ -0,0 +1,23 @@ +/* + * FileIoException.h + * + * Created on: 16.08.2012 + * Author: Thomas Heinemann + */ + +#ifndef MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ +#define MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { + +namespace exceptions { + +MRMC_EXCEPTION_DEFINE_NEW(FileIoException) + +} + +} + +#endif /* MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ */ diff --git a/src/exceptions/InvalidArgumentException.h b/src/exceptions/InvalidArgumentException.h new file mode 100644 index 000000000..c6c07e68a --- /dev/null +++ b/src/exceptions/InvalidArgumentException.h @@ -0,0 +1,18 @@ +#ifndef MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ +#define MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { + +namespace exceptions { + +/*! + * @brief This exception is thrown when a parameter is invalid in this context + */ +MRMC_EXCEPTION_DEFINE_NEW(InvalidArgumentException) + +} // namespace exceptions + +} // namespace mrmc +#endif // MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ diff --git a/src/exceptions/InvalidSettings.h b/src/exceptions/InvalidSettings.h deleted file mode 100644 index 0ac7b14b8..000000000 --- a/src/exceptions/InvalidSettings.h +++ /dev/null @@ -1,16 +0,0 @@ -#ifndef INVALIDSETTINGS_H_ -#define INVALIDSETTINGS_H_ - -#include "src/exceptions/BaseException.h" - -namespace mrmc { -namespace exceptions { - -class InvalidSettings : public BaseException -{ -}; - -} // namespace exceptions -} // namespace mrmc - -#endif // INVALIDSETTINGS_H_ diff --git a/src/exceptions/InvalidSettingsException.h b/src/exceptions/InvalidSettingsException.h new file mode 100644 index 000000000..a399d82ae --- /dev/null +++ b/src/exceptions/InvalidSettingsException.h @@ -0,0 +1,14 @@ +#ifndef MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ +#define MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { +namespace exceptions { + +MRMC_EXCEPTION_DEFINE_NEW(InvalidSettingsException) + +} // namespace exceptions +} // namespace mrmc + +#endif // MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ diff --git a/src/exceptions/InvalidStateException.h b/src/exceptions/InvalidStateException.h new file mode 100644 index 000000000..c971321bf --- /dev/null +++ b/src/exceptions/InvalidStateException.h @@ -0,0 +1,20 @@ +#ifndef MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ +#define MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { + +namespace exceptions { + +/*! + * @brief This exception is thrown when a memory request can't be + * fulfilled. + */ +MRMC_EXCEPTION_DEFINE_NEW(InvalidStateException) + +} // namespace exceptions + +} // namespace mrmc + +#endif // MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ diff --git a/src/exceptions/NoConvergence.h b/src/exceptions/NoConvergence.h deleted file mode 100644 index bd5b71af9..000000000 --- a/src/exceptions/NoConvergence.h +++ /dev/null @@ -1,56 +0,0 @@ -#ifndef MRMC_EXCEPTIONS_NO_CONVERGENCE_H_ -#define MRMC_EXCEPTIONS_NO_CONVERGENCE_H_ - -#include - -namespace mrmc { -namespace exceptions { - -//!This exception is thrown when an iterative solver failed to converge with the given maxIterations -class NoConvergence : public std::exception -{ - public: -/* The Visual C++-Version of the exception class has constructors accepting - * a char*-constant; The GCC version does not have these - * - * As the "extended" constructor is used in the sparse matrix code, a dummy - * constructor is used under linux (which will ignore the parameter) - */ -#ifdef _WIN32 - NoConvergence() : exception("::mrmc::NoConvergence"){ - iterations = -1; - maxIterations = -1; - } - NoConvergence(const char * const s, int iterations, int maxIterations): exception(s) { - this->iterations = iterations; - this->maxIterations = maxIterations; - } -#else - NoConvergence() : exception() { - iterations = -1; - maxIterations = -1; - } - NoConvergence(const char * const s, int iterations, int maxIterations): exception() { - this->iterations = iterations; - this->maxIterations = maxIterations; - } - -#endif - virtual const char* what() const throw() - { return "mrmc::NoConvergence"; } - - int getIterationCount() const { - return iterations; - } - int getMaxIterationCount() const { - return maxIterations; - } - private: - int iterations; - int maxIterations; -}; - -} // namespace exceptions -} // namespace mrmc - -#endif // MRMC_EXCEPTIONS_NO_CONVERGENCE_H_ diff --git a/src/exceptions/NoConvergenceException.h b/src/exceptions/NoConvergenceException.h new file mode 100644 index 000000000..1e7753b1c --- /dev/null +++ b/src/exceptions/NoConvergenceException.h @@ -0,0 +1,17 @@ +#ifndef MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ +#define MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { +namespace exceptions { + +/*! + * @brief This exception is thrown when an iterative solver failed to converge with the given maxIterations + */ +MRMC_EXCEPTION_DEFINE_NEW(NoConvergenceException) + +} // namespace exceptions +} // namespace mrmc + +#endif // MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ diff --git a/src/exceptions/OutOfRangeException.h b/src/exceptions/OutOfRangeException.h new file mode 100644 index 000000000..decd36fda --- /dev/null +++ b/src/exceptions/OutOfRangeException.h @@ -0,0 +1,18 @@ +#ifndef MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ +#define MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { + +namespace exceptions { + +/* + * @briefThis exception is thrown when a parameter is not in the range of valid values + */ +MRMC_EXCEPTION_DEFINE_NEW(OutOfRangeException) + +} // namespace exceptions + +} // namespace mrmc +#endif // MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ diff --git a/src/exceptions/WrongFileFormatException.h b/src/exceptions/WrongFileFormatException.h new file mode 100644 index 000000000..182660a30 --- /dev/null +++ b/src/exceptions/WrongFileFormatException.h @@ -0,0 +1,27 @@ +/* + * WrongFileFormatException.h + * + * Created on: 16.08.2012 + * Author: Thomas Heinemann + */ + +#ifndef MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ +#define MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace mrmc { + +namespace exceptions { + +/*! + * @brief This exception is thrown when an input file + * contains invalid or missing keys. + */ +MRMC_EXCEPTION_DEFINE_NEW(WrongFileFormatException) + +} //namespace exceptions + +} //namespace mrmc + +#endif /* MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ */ diff --git a/src/exceptions/file_IO_exception.h b/src/exceptions/file_IO_exception.h deleted file mode 100644 index b2270fbe2..000000000 --- a/src/exceptions/file_IO_exception.h +++ /dev/null @@ -1,33 +0,0 @@ -/* - * file_IO_exception.h - * - * Created on: 16.08.2012 - * Author: Thomas Heinemann - */ - -#ifndef MRMC_EXCEPTIONS_FILE_IO_EXCEPTION_H_ -#define MRMC_EXCEPTIONS_FILE_IO_EXCEPTION_H_ - -namespace mrmc { - -namespace exceptions { - -class file_IO_exception : public std::exception { - public: -#ifdef _WIN32 - file_IO_exception() : exception("::mrmc::file_IO_exception"){}; - file_IO_exception(const char * const s): exception(s) {}; -#else - file_IO_exception() {}; - file_IO_exception(const char * const s): exception() {}; -#endif - virtual const char* what() const throw(){ - { return "mrmc::file_IO_exception"; } - } -}; - -} - -} - -#endif /* MRMC_EXCEPTIONS_FILE_IO_EXCEPTION_H_ */ diff --git a/src/exceptions/invalid_argument.h b/src/exceptions/invalid_argument.h deleted file mode 100644 index 31db957a4..000000000 --- a/src/exceptions/invalid_argument.h +++ /dev/null @@ -1,34 +0,0 @@ -#ifndef MRMC_EXCEPTIONS_INVALID_ARGUMENT_H_ -#define MRMC_EXCEPTIONS_INVALID_ARGUMENT_H_ - -#include - -namespace mrmc { - -namespace exceptions { - -//!This exception is thrown when a parameter is invalid in this context -class invalid_argument : public std::exception -{ - public: -/* The Visual C++-Version of the exception class has constructors accepting - * a char*-constant; The GCC version does not have these - * - * As the "extended" constructor is used in the sparse matrix code, a dummy - * constructor is used under linux (which will ignore the parameter) - */ -#ifdef _WIN32 - invalid_argument() : exception("::mrmc::invalid_argument"){} - invalid_argument(const char * const s): exception(s) {} -#else - invalid_argument() : exception() {} - invalid_argument(const char * const s): exception() {} -#endif - virtual const char* what() const throw() - { return "mrmc::invalid_argument"; } -}; - -} // namespace exceptions - -} // namespace mrmc -#endif // MRMC_EXCEPTIONS_INVALID_ARGUMENT_H_ diff --git a/src/exceptions/invalid_state.h b/src/exceptions/invalid_state.h deleted file mode 100644 index 132c99644..000000000 --- a/src/exceptions/invalid_state.h +++ /dev/null @@ -1,37 +0,0 @@ -#ifndef MRMC_EXCEPTIONS_INVALID_STATE_H_ -#define MRMC_EXCEPTIONS_INVALID_STATE_H_ - -#include - -namespace mrmc { - -namespace exceptions { - -//!This exception is thrown when a memory request can't be -//!fulfilled. -class invalid_state : public std::exception -{ - public: -/* The Visual C++-Version of the exception class has constructors accepting - * a char*-constant; The GCC version does not have these - * - * As the "extended" constructor is used in the sparse matrix code, a dummy - * constructor is used under linux (which will ignore the parameter) - */ -#ifdef _WIN32 - invalid_state() : exception("::mrmc::invalid_state"){} - invalid_state(const char * const s): exception(s) {} -#else - invalid_state() : exception() {} - invalid_state(const char * const s): exception() {} - -#endif - virtual const char* what() const throw() - { return "mrmc::invalid_state"; } -}; - -} // namespace exceptions - -} // namespace mrmc - -#endif // MRMC_EXCEPTIONS_INVALID_STATE_H_ diff --git a/src/exceptions/out_of_range.h b/src/exceptions/out_of_range.h deleted file mode 100644 index 5b1bfaac9..000000000 --- a/src/exceptions/out_of_range.h +++ /dev/null @@ -1,34 +0,0 @@ -#ifndef MRMC_EXCEPTIONS_OUT_OF_RANGE_H_ -#define MRMC_EXCEPTIONS_OUT_OF_RANGE_H_ - -#include - -namespace mrmc { - -namespace exceptions { - -//!This exception is thrown when a parameter is not in the range of valid values -class out_of_range : public std::exception -{ - public: -/* The Visual C++-Version of the exception class has constructors accepting - * a char*-constant; The GCC version does not have these - * - * As the "extended" constructor is used in the sparse matrix code, a dummy - * constructor is used under linux (which will ignore the parameter) - */ -#ifdef _WIN32 - out_of_range() : exception("::mrmc::out_of_range"){} - out_of_range(const char * const s): exception(s) {} -#else - out_of_range() : exception() {} - out_of_range(const char * const s): exception() {} -#endif - virtual const char* what() const throw() - { return "mrmc::out_of_range"; } -}; - -} // namespace exceptions - -} // namespace mrmc -#endif // MRMC_EXCEPTIONS_OUT_OF_RANGE_H_ diff --git a/src/exceptions/wrong_file_format.h b/src/exceptions/wrong_file_format.h deleted file mode 100644 index afe996733..000000000 --- a/src/exceptions/wrong_file_format.h +++ /dev/null @@ -1,35 +0,0 @@ -/* - * wrong_file_format.h - * - * Created on: 16.08.2012 - * Author: Thomas Heinemann - */ - -#ifndef WRONG_FILE_FORMAT_H_ -#define WRONG_FILE_FORMAT_H_ - -#include - -namespace mrmc { - -namespace exceptions { - -class wrong_file_format : public std::exception { - public: -#ifdef _WIN32 - wrong_file_format() : exception("::mrmc::wrong_file_format"){}; - wrong_file_format(const char * const s): exception(s) {}; -#else - wrong_file_format() {}; - wrong_file_format(const char * const s): exception() {}; -#endif - virtual const char* what() const throw(){ - { return "mrmc::wrong_file_format"; } - } -}; - -} //namespace exceptions - -} //namespace mrmc - -#endif /* WRONG_FILE_FORMAT_H_ */ diff --git a/src/formula/And.h b/src/formula/And.h index 7a42193b8..62cc46964 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef AND_H_ -#define AND_H_ +#ifndef MRMC_FORMULA_AND_H_ +#define MRMC_FORMULA_AND_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" #include namespace mrmc { @@ -27,11 +27,11 @@ namespace formula { * The subtrees are seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class And : public PCTLStateFormula { +class And : public PctlStateFormula { public: /*! @@ -50,7 +50,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - And(PCTLStateFormula* left, PCTLStateFormula* right) { + And(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -75,7 +75,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -84,21 +84,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -121,7 +121,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { And* result = new And(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -146,12 +146,12 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula } //namespace mrmc -#endif /* AND_H_ */ +#endif /* MRMC_FORMULA_AND_H_ */ diff --git a/src/formula/AP.h b/src/formula/Ap.h similarity index 70% rename from src/formula/AP.h rename to src/formula/Ap.h index 990365ff0..1f636d7df 100644 --- a/src/formula/AP.h +++ b/src/formula/Ap.h @@ -1,14 +1,14 @@ /* - * AP.h + * Ap.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef AP_H_ -#define AP_H_ +#ifndef MRMC_FORMULA_AP_H_ +#define MRMC_FORMULA_AP_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -20,21 +20,21 @@ namespace formula { * * This class represents the leaves in the formula tree. * - * @see PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class AP : public PCTLStateFormula { +class Ap : public PctlStateFormula { public: /*! * Constructor * - * Creates a new atomic proposition leaf, with the label AP + * Creates a new atomic proposition leaf, with the label Ap * * @param ap The string representing the atomic proposition */ - AP(std::string ap) { + Ap(std::string ap) { this->ap = ap; } @@ -42,12 +42,12 @@ public: * Destructor. * At this time, empty... */ - virtual ~AP() { } + virtual ~Ap() { } /*! * @returns the name of the atomic proposition */ - const std::string& getAP() const { + const std::string& getAp() const { return ap; } @@ -56,16 +56,16 @@ public: * */ virtual std::string toString() const { - return getAP(); + return getAp(); } /*! * Clones the called object. * - * @returns a new AP-object that is identical the called object. + * @returns a new Ap-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { - return new AP(ap); + virtual PctlStateFormula* clone() const { + return new Ap(ap); } /*! @@ -78,7 +78,7 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkAP(*this); + return modelChecker.checkAp(*this); } private: @@ -89,4 +89,4 @@ private: } //namespace mrmc -#endif /* AP_H_ */ +#endif /* MRMC_FORMULA_AP_H_ */ diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 51131602d..281c112bc 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -5,11 +5,11 @@ * Author: Thomas Heinemann */ -#ifndef BOUNDEDUNTIL_H_ -#define BOUNDEDUNTIL_H_ +#ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_ +#define MRMC_FORMULA_BOUNDEDUNTIL_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" #include "boost/integer/integer_mask.hpp" #include @@ -30,11 +30,11 @@ namespace formula { * The subtrees are seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class BoundedUntil : public PCTLPathFormula { +class BoundedUntil : public PctlPathFormula { public: /*! @@ -53,7 +53,7 @@ public: * @param right The left formula subtree * @param bound The maximal number of steps */ - BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, + BoundedUntil(PctlStateFormula* left, PctlStateFormula* right, uint_fast64_t bound) { this->left = left; this->right = right;; @@ -80,7 +80,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -89,21 +89,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -144,7 +144,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { BoundedUntil* result = new BoundedUntil(); result->setBound(bound); if (left != NULL) { @@ -171,8 +171,8 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; uint_fast64_t bound; }; @@ -180,4 +180,4 @@ private: } //namespace mrmc -#endif /* BOUNDEDUNTIL_H_ */ +#endif /* MRMC_FORMULA_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 5b8b4bffc..8db8c1f0d 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -5,21 +5,21 @@ * Author: chris */ -#ifndef FORMULAS_H_ -#define FORMULAS_H_ +#ifndef MRMC_FORMULA_FORMULAS_H_ +#define MRMC_FORMULA_FORMULAS_H_ #include "And.h" -#include "AP.h" +#include "Ap.h" #include "BoundedUntil.h" #include "Next.h" #include "Not.h" #include "Or.h" -#include "PCTLformula.h" -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" #include "ProbabilisticOperator.h" #include "ProbabilisticNoBoundsOperator.h" #include "ProbabilisticIntervalOperator.h" #include "Until.h" -#endif /* FORMULAS_H_ */ +#endif /* MRMC_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/Next.h b/src/formula/Next.h index 2eb00be05..07924846e 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -5,11 +5,11 @@ * Author: Thomas Heinemann */ -#ifndef NEXT_H_ -#define NEXT_H_ +#ifndef MRMC_FORMULA_NEXT_H_ +#define MRMC_FORMULA_NEXT_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -27,11 +27,11 @@ namespace formula { * The subtree is seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class Next : public PCTLPathFormula { +class Next : public PctlPathFormula { public: /*! @@ -46,7 +46,7 @@ public: * * @param child The child node */ - Next(PCTLStateFormula* child) { + Next(PctlStateFormula* child) { this->child = child; } @@ -65,7 +65,7 @@ public: /*! * @returns the child node */ - const PCTLStateFormula& getChild() const { + const PctlStateFormula& getChild() const { return *child; } @@ -73,7 +73,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PCTLStateFormula* child) { + void setChild(PctlStateFormula* child) { this->child = child; } @@ -95,7 +95,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { Next* result = new Next(); if (child != NULL) { result->setChild(child); @@ -117,11 +117,11 @@ public: } private: - PCTLStateFormula* child; + PctlStateFormula* child; }; } //namespace formula } //namespace mrmc -#endif /* NEXT_H_ */ +#endif /* MRMC_FORMULA_NEXT_H_ */ diff --git a/src/formula/Not.h b/src/formula/Not.h index 574d287a1..26ae6320c 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef NOT_H_ -#define NOT_H_ +#ifndef MRMC_FORMULA_NOT_H_ +#define MRMC_FORMULA_NOT_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -23,11 +23,11 @@ namespace formula { * The subtree is seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class Not : public PCTLStateFormula { +class Not : public PctlStateFormula { public: /*! @@ -41,7 +41,7 @@ public: * Constructor * @param child The child node */ - Not(PCTLStateFormula* child) { + Not(PctlStateFormula* child) { this->child = child; } @@ -60,7 +60,7 @@ public: /*! * @returns The child node */ - const PCTLStateFormula& getChild() const { + const PctlStateFormula& getChild() const { return *child; } @@ -68,7 +68,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PCTLStateFormula* child) { + void setChild(PctlStateFormula* child) { this->child = child; } @@ -88,7 +88,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { Not* result = new Not(); if (child != NULL) { result->setChild(child); @@ -110,11 +110,11 @@ public: } private: - PCTLStateFormula* child; + PctlStateFormula* child; }; } //namespace formula } //namespace MRMC -#endif /* NOT_H_ */ +#endif /* MRMC_FORMULA_NOT_H_ */ diff --git a/src/formula/Or.h b/src/formula/Or.h index 5a60d9770..bc1302185 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef OR_H_ -#define OR_H_ +#ifndef MRMC_FORMULA_OR_H_ +#define MRMC_FORMULA_OR_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -26,11 +26,11 @@ namespace formula { * The subtrees are seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class Or : public PCTLStateFormula { +class Or : public PctlStateFormula { public: /*! @@ -49,7 +49,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - Or(PCTLStateFormula* left, PCTLStateFormula* right) { + Or(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +74,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -83,21 +83,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -120,7 +120,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { Or* result = new Or(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -145,12 +145,12 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula } //namespace mrmc -#endif /* OR_H_ */ +#endif /* MRMC_FORMULA_OR_H_ */ diff --git a/src/formula/PCTLformula.h b/src/formula/PctlFormula.h similarity index 76% rename from src/formula/PCTLformula.h rename to src/formula/PctlFormula.h index add5c5198..a4d910483 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PctlFormula.h @@ -1,12 +1,12 @@ /* - * PCTLformula.h + * Pctlformula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef PCTLFORMULA_H_ -#define PCTLFORMULA_H_ +#ifndef MRMC_FORMULA_PCTLFORMULA_H_ +#define MRMC_FORMULA_PCTLFORMULA_H_ #include @@ -23,16 +23,16 @@ namespace formula { * @attention This class is abstract. * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes - * PCTLPathFormula and PCTLStateFormula offer the method clone(). + * PctlPathFormula and PctlStateFormula offer the method clone(). */ template -class PCTLFormula { +class PctlFormula { public: /*! * virtual destructor */ - virtual ~PCTLFormula() { } + virtual ~PctlFormula() { } /*! * @note This function is not implemented in this class. @@ -45,4 +45,4 @@ public: } //namespace mrmc -#endif /* PCTLFORMULA_H_ */ +#endif /* MRMC_FORMULA_PCTLFORMULA_H_ */ diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PctlPathFormula.h similarity index 83% rename from src/formula/PCTLPathFormula.h rename to src/formula/PctlPathFormula.h index a70a35f53..9b6a38b94 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PctlPathFormula.h @@ -1,14 +1,14 @@ /* - * PCTLPathFormula.h + * PctlPathFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef PCTLPATHFORMULA_H_ -#define PCTLPATHFORMULA_H_ +#ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_ +#define MRMC_FORMULA_PCTLPATHFORMULA_H_ -#include "PCTLformula.h" +#include "PctlFormula.h" #include "modelChecker/DtmcPrctlModelChecker.h" #include @@ -26,13 +26,13 @@ namespace formula { * clone(). */ template -class PCTLPathFormula : public PCTLFormula { +class PctlPathFormula : public PctlFormula { public: /*! * empty destructor */ - virtual ~PCTLPathFormula() { } + virtual ~PctlPathFormula() { } /*! * Clones the called object. @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const = 0; + virtual PctlPathFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -62,4 +62,4 @@ public: } //namespace mrmc -#endif /* PCTLPATHFORMULA_H_ */ +#endif /* MRMC_FORMULA_PCTLPATHFORMULA_H_ */ diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PctlStateFormula.h similarity index 83% rename from src/formula/PCTLStateFormula.h rename to src/formula/PctlStateFormula.h index a8ca831c3..c4eee14f2 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PctlStateFormula.h @@ -1,14 +1,14 @@ /* - * PCTLStateFormula.h + * PctlStateFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef PCTLSTATEFORMULA_H_ -#define PCTLSTATEFORMULA_H_ +#ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_ +#define MRMC_FORMULA_PCTLSTATEFORMULA_H_ -#include "PCTLformula.h" +#include "PctlFormula.h" #include "storage/BitVector.h" #include "modelChecker/DtmcPrctlModelChecker.h" @@ -26,13 +26,13 @@ namespace formula { * clone(). */ template -class PCTLStateFormula : public PCTLFormula { +class PctlStateFormula : public PctlFormula { public: /*! * empty destructor */ - virtual ~PCTLStateFormula() { } + virtual ~PctlStateFormula() { } /*! * Clones the called object. @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const = 0; + virtual PctlStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -63,4 +63,4 @@ public: } //namespace mrmc -#endif /* PCTLSTATEFORMULA_H_ */ +#endif /* MRMC_FORMULA_PCTLSTATEFORMULA_H_ */ diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h index c7ffb9ba3..5fd2943af 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef PROBABILISTICINTERVALOPERATOR_H_ -#define PROBABILISTICINTERVALOPERATOR_H_ +#ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ +#define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ -#include "PCTLStateFormula.h" -#include "PCTLPathFormula.h" -#include "utility/const_templates.h" +#include "PctlStateFormula.h" +#include "PctlPathFormula.h" +#include "utility/ConstTemplates.h" namespace mrmc { @@ -35,14 +35,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticOperator * @see ProbabilisticNoBoundsOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticIntervalOperator : public PCTLStateFormula { +class ProbabilisticIntervalOperator : public PctlStateFormula { public: /*! @@ -61,7 +61,7 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula& pathFormula) { + ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) { this->lower = lowerBound; this->upper = upperBound; this->pathFormula = &pathFormula; @@ -82,7 +82,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -105,7 +105,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -141,7 +141,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { ProbabilisticIntervalOperator* result = new ProbabilisticIntervalOperator(); result->setInterval(lower, upper); if (pathFormula != NULL) { @@ -166,11 +166,11 @@ public: private: T lower; T upper; - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } //namespace formula } //namespace mrmc -#endif /* PROBABILISTICINTERVALOPERATOR_H_ */ +#endif /* MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h index 09a2fc4c3..b89080ca7 100644 --- a/src/formula/ProbabilisticNoBoundsOperator.h +++ b/src/formula/ProbabilisticNoBoundsOperator.h @@ -5,11 +5,11 @@ * Author: thomas */ -#ifndef PROBABILISTICNOBOUNDSOPERATOR_H_ -#define PROBABILISTICNOBOUNDSOPERATOR_H_ +#ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ +#define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ -#include "PCTLformula.h" -#include "PCTLPathFormula.h" +#include "PctlFormula.h" +#include "PctlPathFormula.h" namespace mrmc { namespace formula { @@ -26,20 +26,20 @@ namespace formula { * * @note * This class is a hybrid of a state and path formula, and may only appear as the outermost operator. - * Hence, it is seen as neither a state nor a path formula, but is directly derived from PCTLformula. + * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula. * * The subtree is seen as part of the object and deleted with it * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticOperator * @see ProbabilisticIntervalOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticNoBoundsOperator: public mrmc::formula::PCTLFormula { +class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula { public: /*! * Empty constructor @@ -54,7 +54,7 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundsOperator(PCTLPathFormula &pathFormula) { + ProbabilisticNoBoundsOperator(PctlPathFormula &pathFormula) { this->pathFormula = &pathFormula; } @@ -68,7 +68,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -77,7 +77,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -92,9 +92,10 @@ public: } private: - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } /* namespace formula */ } /* namespace mrmc */ -#endif /* PROBABILISTICNOBOUNDSOPERATOR_H_ */ + +#endif /* MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index cbceee0d4..b1131ef4b 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef PROBABILISTICOPERATOR_H_ -#define PROBABILISTICOPERATOR_H_ +#ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_ +#define MRMC_FORMULA_PROBABILISTICOPERATOR_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { namespace formula { @@ -32,14 +32,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticIntervalOperator * @see ProbabilisticNoBoundsOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula { +class ProbabilisticOperator : public mrmc::formula::PctlStateFormula { public: /*! * Empty constructor @@ -55,7 +55,7 @@ public: * @param bound The expected value for path formulas * @param pathFormula The child node */ - ProbabilisticOperator(T bound, PCTLPathFormula& pathFormula) { + ProbabilisticOperator(T bound, PctlPathFormula& pathFormula) { this->bound = bound; this->pathFormula = &pathFormula; } @@ -73,7 +73,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -89,7 +89,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -109,7 +109,7 @@ public: * * @returns a new ProbabilisticOperator-object that is identical to the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { ProbabilisticOperator* result = new ProbabilisticOperator(); result->setBound(bound); if (pathFormula != NULL) { @@ -134,9 +134,9 @@ public: } /*! - * Returns a string representation of this PCTLStateFormula + * Returns a string representation of this PctlStateFormula * - * @returns a string representation of this PCTLStateFormula + * @returns a string representation of this PctlStateFormula */ virtual std::string toString() const { std::string result = " P="; @@ -148,9 +148,10 @@ public: } private: T bound; - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } /* namespace formula */ } /* namespace mrmc */ -#endif /* PROBABILISTICOPERATOR_H_ */ + +#endif /* MRMC_FORMULA_PROBABILISTICOPERATOR_H_ */ diff --git a/src/formula/Until.h b/src/formula/Until.h index 1b492e68b..3f094e3a3 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -5,11 +5,11 @@ * Author: Thomas Heinemann */ -#ifndef UNTIL_H_ -#define UNTIL_H_ +#ifndef MRMC_FORMULA_UNTIL_H_ +#define MRMC_FORMULA_UNTIL_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -28,11 +28,11 @@ namespace formula { * The subtrees are seen as part of the object and deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) * - * @see PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class Until : public PCTLPathFormula { +class Until : public PctlPathFormula { public: /*! @@ -49,7 +49,7 @@ public: * @param left The left formula subtree * @param right The left formula subtree */ - Until(PCTLStateFormula* left, PCTLStateFormula* right) { + Until(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +74,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -83,21 +83,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -120,7 +120,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { Until* result = new Until(); if (left != NULL) { result->setLeft(left->clone()); @@ -145,12 +145,12 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula } //namespace mrmc -#endif /* UNTIL_H_ */ +#endif /* MRMC_FORMULA_UNTIL_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 76aa00531..9556fd966 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -5,8 +5,8 @@ * Author: Thomas Heinemann */ -#ifndef DTMCPRCTLMODELCHECKER_H_ -#define DTMCPRCTLMODELCHECKER_H_ +#ifndef MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ +#define MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ namespace mrmc { @@ -23,8 +23,8 @@ class DtmcPrctlModelChecker; } -#include "src/formula/PCTLPathFormula.h" -#include "src/formula/PCTLStateFormula.h" +#include "src/formula/PctlPathFormula.h" +#include "src/formula/PctlStateFormula.h" #include "src/formula/Formulas.h" @@ -96,7 +96,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { + mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PctlStateFormula& formula) const { return formula.check(*this); } @@ -117,16 +117,16 @@ public: /*! * The check method for a formula with an AP node as root in its formula tree * - * @param formula The AP state formula to check + * @param formula The Ap state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) const { - if (formula.getAP().compare("true") == 0) { + mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap& formula) const { + if (formula.getAp().compare("true") == 0) { return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); - } else if (formula.getAP().compare("false") == 0) { + } else if (formula.getAp().compare("false") == 0) { return new mrmc::storage::BitVector(model->getNumberOfStates()); } - return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP())); + return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAp())); } /*! @@ -226,7 +226,7 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { + std::vector* checkPathFormula(const mrmc::formula::PctlPathFormula& formula) const { return formula.check(*this); } @@ -262,4 +262,4 @@ private: } //namespace mrmc -#endif /* DTMCPRCTLMODELCHECKER_H_ */ +#endif /* MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 4730ab9cc..9a1760292 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -5,16 +5,16 @@ * Author: */ -#ifndef EIGENDTMCPRCTLMODELCHECKER_H_ -#define EIGENDTMCPRCTLMODELCHECKER_H_ +#ifndef MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ +#define MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ -#include "src/utility/vector.h" +#include "src/utility/Vector.h" #include "src/models/Dtmc.h" #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" -#include "src/utility/const_templates.h" -#include "src/exceptions/NoConvergence.h" +#include "src/utility/ConstTemplates.h" +#include "src/exceptions/NoConvergenceException.h" #include "Eigen/Sparse" #include "Eigen/src/IterativeLinearSolvers/BiCGSTAB.h" @@ -197,7 +197,7 @@ public: LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { // NoConvergence - throw mrmc::exceptions::NoConvergence("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations()); + throw mrmc::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations()); } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { // NumericalIssue LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); @@ -226,4 +226,4 @@ public: } //namespace mrmc -#endif /* EIGENDTMCPRCTLMODELCHECKER_H_ */ +#endif /* MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 8d2af9f2a..5dde36fc4 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -5,17 +5,17 @@ * Author: Christian Dehnert */ -#ifndef GMMXXDTMCPRCTLMODELCHECKER_H_ -#define GMMXXDTMCPRCTLMODELCHECKER_H_ +#ifndef MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ +#define MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ #include #include "src/models/Dtmc.h" #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" -#include "src/utility/vector.h" +#include "src/utility/Vector.h" -#include "src/utility/settings.h" +#include "src/utility/Settings.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -250,7 +250,7 @@ public: */ static void validateLeMethod(const std::string& lemethod) { if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0) { - throw exceptions::InvalidSettings() << "Argument " << lemethod << " for option 'lemethod' is invalid."; + throw exceptions::InvalidSettingsException() << "Argument " << lemethod << " for option 'lemethod' is invalid."; } } @@ -260,7 +260,7 @@ public: */ static void validatePreconditioner(const std::string& preconditioner) { if (preconditioner.compare("ilu") != 0 && preconditioner.compare("diagonal") != 0 && preconditioner.compare("ildlt") && preconditioner.compare("none") != 0) { - throw exceptions::InvalidSettings() << "Argument " << preconditioner << " for option 'precond' is invalid."; + throw exceptions::InvalidSettingsException() << "Argument " << preconditioner << " for option 'precond' is invalid."; } } }; @@ -269,4 +269,4 @@ public: } //namespace mrmc -#endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */ +#endif /* MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 34c2da73b..f4d52b783 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -1,14 +1,15 @@ /* - * labeling.h + * AtomicPropositionsLabeling.h * * Created on: 10.09.2012 * Author: Thomas Heinemann */ -#ifndef MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ -#define MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ +#ifndef MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ +#define MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ #include "src/storage/BitVector.h" +#include "src/exceptions/OutOfRangeException.h" #include #include #include @@ -81,10 +82,10 @@ public: */ uint_fast64_t addAtomicProposition(std::string ap) { if (nameToLabelingMap.count(ap) != 0) { - throw std::out_of_range("Atomic Proposition already exists."); + throw mrmc::exceptions::OutOfRangeException("Atomic Proposition already exists."); } if (apsCurrent >= apCountMax) { - throw std::out_of_range("Added more atomic propositions than" + throw mrmc::exceptions::OutOfRangeException("Added more atomic propositions than" "previously declared."); } nameToLabelingMap[ap] = apsCurrent; @@ -109,10 +110,10 @@ public: */ void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) { if (nameToLabelingMap.count(ap) == 0) { - throw std::out_of_range("Atomic Proposition '" + ap + "' unknown."); + throw mrmc::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown."; } if (state >= stateCount) { - throw std::out_of_range("State index out of range."); + throw mrmc::exceptions::OutOfRangeException("State index out of range."); } this->singleLabelings[nameToLabelingMap[ap]]->set(state, true); } @@ -124,7 +125,7 @@ public: */ std::set getPropositionsForState(uint_fast64_t state) { if (state >= stateCount) { - throw std::out_of_range("State index out of range."); + throw mrmc::exceptions::OutOfRangeException("State index out of range."); } std::set result; for (auto it = nameToLabelingMap.begin(); @@ -228,4 +229,4 @@ private: } // namespace mrmc -#endif /* MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ */ +#endif /* MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ */ diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 8fa263f54..dc871e143 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -1,12 +1,12 @@ /* - * dtmc.h + * Dtmc.h * * Created on: 14.11.2012 * Author: Christian Dehnert */ -#ifndef DTMC_H_ -#define DTMC_H_ +#ifndef MRMC_MODELS_DTMC_H_ +#define MRMC_MODELS_DTMC_H_ #include #include @@ -155,4 +155,4 @@ private: } // namespace mrmc -#endif /* DTMC_H_ */ +#endif /* MRMC_MODELS_DTMC_H_ */ diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 4563bfc59..6d45bad88 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -1,12 +1,12 @@ /* - * backward_transitions.h + * GraphTransitions.h * * Created on: 17.11.2012 * Author: Christian Dehnert */ -#ifndef GRAPHTRANSITIONS_H_ -#define BACKWARDTRANSITIONS_H_ +#ifndef MRMC_MODELS_GRAPHTRANSITIONS_H_ +#define MRMC_MODELS_GRAPHTRANSITIONS_H_ #include "src/storage/SquareSparseMatrix.h" @@ -175,4 +175,4 @@ private: } // namespace mrmc -#endif /* GRAPHTRANSITIONS_H_ */ +#endif /* MRMC_MODELS_GRAPHTRANSITIONS_H_ */ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 7d334408c..9bb62172a 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -12,7 +12,7 @@ * Description: Central part of the application containing the main() Method */ -#include "src/utility/osDetection.h" +#include "src/utility/OsDetection.h" #include #include #include @@ -24,20 +24,19 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/modelChecker/EigenDtmcPrctlModelChecker.h" #include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" -#include "src/parser/readLabFile.h" -#include "src/parser/readTraFile.h" -#include "src/parser/readPrctlFile.h" +#include "src/parser/LabParser.h" +#include "src/parser/TraParser.h" +#include "src/parser/PrctlParser.h" #include "src/solver/GraphAnalyzer.h" -#include "src/utility/settings.h" +#include "src/utility/Settings.h" #include "src/formula/Formulas.h" -#include "src/exceptions/NoConvergence.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" -#include "src/exceptions/InvalidSettings.h" +#include "src/exceptions/InvalidSettingsException.h" log4cplus::Logger logger; @@ -76,7 +75,7 @@ int main(const int argc, const char* argv[]) { try { mrmc::settings::Settings::registerModule >(); s = mrmc::settings::newInstance(argc, argv, nullptr); - } catch (mrmc::exceptions::InvalidSettings& e) { + } catch (mrmc::exceptions::InvalidSettingsException& e) { LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what() << "."); LOG4CPLUS_FATAL(logger, "Could not recover from settings error, terminating."); std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; @@ -91,7 +90,7 @@ int main(const int argc, const char* argv[]) { return 0; } if (s->isSet("test-prctl")) { - mrmc::parser::PRCTLParser parser(s->getString("test-prctl").c_str()); + mrmc::parser::PrctlParser parser(s->getString("test-prctl").c_str()); delete s; return 0; } diff --git a/src/parser/readLabFile.cpp b/src/parser/LabParser.cpp similarity index 92% rename from src/parser/readLabFile.cpp rename to src/parser/LabParser.cpp index 3b195eb6d..45274347d 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/LabParser.cpp @@ -1,17 +1,16 @@ /*! - * readLabFile.cpp + * LabParser.cpp * * Created on: 21.11.2012 * Author: Gereon Kremer */ -#include "parser.h" +#include "src/parser/LabParser.h" -#include "readLabFile.h" - -#include "src/exceptions/wrong_file_format.h" -#include "src/exceptions/file_IO_exception.h" +#include "src/exceptions/WrongFileFormatException.h" +#include "src/exceptions/FileIoException.h" +#include "src/utility/OsDetection.h" #include #include #include @@ -23,12 +22,6 @@ #include #include -#if defined LINUX || defined MACOSX - #include -#elif defined WINDOWS - #define strncpy strncpy_s -#endif - #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -97,7 +90,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) 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 mrmc::exceptions::wrong_file_format(); + throw mrmc::exceptions::WrongFileFormatException(); } } @@ -127,7 +120,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) * 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 mrmc::exceptions::wrong_file_format(); + throw mrmc::exceptions::WrongFileFormatException(); } else if (cnt > 0) { /* * next token is: #DECLARATION: just skip it diff --git a/src/parser/readLabFile.h b/src/parser/LabParser.h similarity index 84% rename from src/parser/readLabFile.h rename to src/parser/LabParser.h index c668097f0..bb1e2d992 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/LabParser.h @@ -1,10 +1,10 @@ -#ifndef READLABFILE_H_ -#define READLABFILE_H_ +#ifndef MRMC_PARSER_LABPARSER_H_ +#define MRMC_PARSER_LABPARSER_H_ #include "src/models/AtomicPropositionsLabeling.h" #include "boost/integer/integer_mask.hpp" -#include "src/parser/parser.h" +#include "src/parser/Parser.h" #include @@ -32,4 +32,4 @@ class LabParser : Parser { } // namespace parser } // namespace mrmc -#endif /* READLABFILE_H_ */ +#endif /* MRMC_PARSER_LABPARSER_H_ */ diff --git a/src/parser/parser.cpp b/src/parser/Parser.cpp similarity index 77% rename from src/parser/parser.cpp rename to src/parser/Parser.cpp index f5295f71f..1e25ee404 100644 --- a/src/parser/parser.cpp +++ b/src/parser/Parser.cpp @@ -1,19 +1,10 @@ -#include "src/parser/parser.h" +#include "src/parser/Parser.h" -#if defined LINUX || defined MACOSX -# include -# include -#elif defined WINDOWS -#endif - -#include -#include -#include #include #include -#include "src/exceptions/file_IO_exception.h" -#include "src/exceptions/wrong_file_format.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFileFormatException.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -22,7 +13,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 - * mrmc::exceptions::wrong_file_format will be thrown. + * mrmc::exceptions::WrongFileFormatException will be thrown. * @param str String to parse * @param end New pointer will be written there * @return Result of strtol() @@ -32,7 +23,7 @@ uint_fast64_t mrmc::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 mrmc::exceptions::wrong_file_format(); + throw mrmc::exceptions::WrongFileFormatException("Error while parsing integer. Next input token is not a number."); } return res; } @@ -66,20 +57,20 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { if (stat64(filename, &(this->st)) != 0) { #endif LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in stat()"); } this->file = open(filename, O_RDONLY); if (this->file < 0) { LOG4CPLUS_ERROR(logger, "Error in open(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in open()"); } this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0); if (this->data == (char*)-1) { close(this->file); LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in mmap()"); } this->dataend = this->data + this->st.st_size; #elif defined WINDOWS @@ -89,20 +80,20 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { */ if (_stat64(filename, &(this->st)) != 0) { LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in stat()"); } this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL); if (this->file == INVALID_HANDLE_VALUE) { LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileA()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in CreateFileA()"); } this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL); if (this->mapping == NULL) { CloseHandle(this->file); LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMappingA()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in CreateFileMappingA()"); } this->data = static_cast(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size)); @@ -110,7 +101,7 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { CloseHandle(this->mapping); CloseHandle(this->file); LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ")."); - throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()"); + throw exceptions::FileIoException("mrmc::parser::MappedFile Error in MapViewOfFile()"); } this->dataend = this->data + this->st.st_size; #endif diff --git a/src/parser/parser.h b/src/parser/Parser.h similarity index 87% rename from src/parser/parser.h rename to src/parser/Parser.h index 0950ed848..81938ecf7 100644 --- a/src/parser/parser.h +++ b/src/parser/Parser.h @@ -1,21 +1,14 @@ /* - * parser.h + * Parser.h * * Created on: 21.11.2012 * Author: Gereon Kremer */ -#ifndef PARSER_H_ -#define PARSER_H_ +#ifndef MRMC_PARSER_PARSER_H_ +#define MRMC_PARSER_PARSER_H_ -#include "src/utility/osDetection.h" - -#if defined LINUX || defined MACOSX -# include -#elif defined WINDOWS -# include -# include -#endif +#include "src/utility/OsDetection.h" #include #include @@ -23,8 +16,8 @@ #include #include -#include "src/exceptions/file_IO_exception.h" -#include "src/exceptions/wrong_file_format.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFileFormatException.h" namespace mrmc { @@ -119,4 +112,4 @@ namespace parser { } // namespace parser } // namespace mrmc -#endif /* PARSER_H_ */ +#endif /* MRMC_PARSER_PARSER_H_ */ diff --git a/src/parser/readPrctlFile.cpp b/src/parser/PrctlParser.cpp similarity index 95% rename from src/parser/readPrctlFile.cpp rename to src/parser/PrctlParser.cpp index 973132a55..f1a23077a 100644 --- a/src/parser/readPrctlFile.cpp +++ b/src/parser/PrctlParser.cpp @@ -1,9 +1,6 @@ -#include "src/parser/readPrctlFile.h" - -#include "src/parser/parser.h" +#include "src/parser/PrctlParser.h" #include - #include //#include @@ -61,7 +58,7 @@ namespace /*! * @brief Resulting formula. */ - mrmc::formula::PCTLFormula* result; + mrmc::formula::PctlFormula* result; struct dump { @@ -133,7 +130,7 @@ namespace }; } -mrmc::parser::PRCTLParser::PRCTLParser(const char* filename) +mrmc::parser::PrctlParser::PrctlParser(const char* filename) { SpiritParser p; mrmc::parser::MappedFile file(filename); diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h new file mode 100644 index 000000000..24dc746bb --- /dev/null +++ b/src/parser/PrctlParser.h @@ -0,0 +1,33 @@ +#ifndef MRMC_PARSER_PRCTLPARSER_H_ +#define MRMC_PARSER_PRCTLPARSER_H_ + +#include "src/formula/PctlFormula.h" +#include "src/parser/Parser.h" + +namespace mrmc { +namespace parser { + +/*! + * @brief Load PRCTL file + */ +class PrctlParser : Parser +{ + public: + PrctlParser(const char * filename); + + /*! + * @brief return formula object parsed from file. + */ + mrmc::formula::PctlFormula* getFormula() + { + return this->formula; + } + + private: + mrmc::formula::PctlFormula* formula; +}; + +} // namespace parser +} // namespace mrmc + +#endif /* MRMC_PARSER_PRCTLPARSER_H_ */ diff --git a/src/parser/readTraFile.cpp b/src/parser/TraParser.cpp similarity index 93% rename from src/parser/readTraFile.cpp rename to src/parser/TraParser.cpp index 1a6137fbf..7f38187d7 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/TraParser.cpp @@ -1,15 +1,13 @@ /*! - * readTraFile.cpp + * TraParser.cpp * * Created on: 20.11.2012 * Author: Gereon Kremer */ -#include "parser.h" - -#include "src/parser/readTraFile.h" -#include "src/exceptions/file_IO_exception.h" -#include "src/exceptions/wrong_file_format.h" +#include "src/parser/TraParser.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFileFormatException.h" #include "boost/integer/integer_mask.hpp" #include #include @@ -19,10 +17,6 @@ #include #include #include -#if defined LINUX || defined MACOSX - #include -#elif defined WINDOWS -#endif #include #include @@ -137,7 +131,7 @@ TraParser::TraParser(const char * filename) if (non_zero == 0) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); - throw mrmc::exceptions::wrong_file_format(); + throw mrmc::exceptions::WrongFileFormatException(); } /* @@ -190,7 +184,7 @@ TraParser::TraParser(const char * filename) if ((val <= 0.0) || (val > 1.0)) { LOG4CPLUS_ERROR(logger, "Found transition probability of " << val << ", but we think probabilities should be from (0,1]."); - throw mrmc::exceptions::wrong_file_format(); + throw mrmc::exceptions::WrongFileFormatException(); } this->matrix->addNextValue(row,col,val); buf = skipWS(buf); diff --git a/src/parser/readTraFile.h b/src/parser/TraParser.h similarity index 80% rename from src/parser/readTraFile.h rename to src/parser/TraParser.h index ba09b1aea..a7079ea66 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/TraParser.h @@ -1,9 +1,10 @@ -#ifndef READTRAFILE_H_ -#define READTRAFILE_H_ +#ifndef MRMC_PARSER_TRAPARSER_H_ +#define MRMC_PARSER_TRAPARSER_H_ #include "src/storage/SquareSparseMatrix.h" -#include "src/parser/parser.h" +#include "src/parser/Parser.h" +#include "src/utility/OsDetection.h" #include @@ -35,4 +36,4 @@ class TraParser : Parser { } // namespace parser } // namespace mrmc -#endif /* READTRAFILE_H_ */ +#endif /* MRMC_PARSER_TRAPARSER_H_ */ diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h deleted file mode 100644 index a011f15d7..000000000 --- a/src/parser/readPrctlFile.h +++ /dev/null @@ -1,33 +0,0 @@ -#ifndef READPRCTLFILE_H_ -#define READPRCTLFILE_H_ - -#include "src/formula/PCTLformula.h" -#include "src/parser/parser.h" - -namespace mrmc { -namespace parser { - -/*! - * @brief Load PRCTL file - */ -class PRCTLParser : Parser -{ - public: - PRCTLParser(const char * filename); - - /*! - * @brief return formula object parsed from file. - */ - mrmc::formula::PCTLFormula* getFormula() - { - return this->formula; - } - - private: - mrmc::formula::PCTLFormula* formula; -}; - -} // namespace parser -} // namespace mrmc - -#endif /* READPRCTLFILE_H_ */ diff --git a/src/reward/reward_model.h b/src/reward/RewardModel.h similarity index 93% rename from src/reward/reward_model.h rename to src/reward/RewardModel.h index 99fd32c97..c2ffb8b79 100644 --- a/src/reward/reward_model.h +++ b/src/reward/RewardModel.h @@ -1,12 +1,12 @@ /* - * reward_model.h + * RewardModel.h * * Created on: 25.10.2012 * Author: Philipp Berger */ -#ifndef MRMC_REWARD_REWARD_MODEL_H_ -#define MRMC_REWARD_REWARD_MODEL_H_ +#ifndef MRMC_REWARD_REWARDMODEL_H_ +#define MRMC_REWARD_REWARDMODEL_H_ #include @@ -76,4 +76,4 @@ class RewardModel { } //namespace mrmc -#endif /* MRMC_REWARD_REWARD_MODEL_H_ */ +#endif /* MRMC_REWARD_REWARDMODEL_H_ */ diff --git a/src/solver/GraphAnalyzer.h b/src/solver/GraphAnalyzer.h index 34864520e..6660ad2f9 100644 --- a/src/solver/GraphAnalyzer.h +++ b/src/solver/GraphAnalyzer.h @@ -5,11 +5,11 @@ * Author: Christian Dehnert */ -#ifndef GRAPHANALYZER_H_ -#define GRAPHANALYZER_H_ +#ifndef MRMC_SOLVER_GRAPHANALYZER_H_ +#define MRMC_SOLVER_GRAPHANALYZER_H_ #include "src/models/Dtmc.h" -#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -38,7 +38,7 @@ public: // Check for valid parameter. if (existsPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); } // Get the backwards transition relation from the model to ease the search. @@ -85,7 +85,7 @@ public: // Check for valid parameter. if (alwaysPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); } GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); @@ -109,11 +109,11 @@ public: // Check for valid parameters. if (existsPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::invalid_argument("Parameter 'existsPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); } if (alwaysPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::invalid_argument("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw mrmc::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); } // Perform search. @@ -127,4 +127,4 @@ public: } // namespace mrmc -#endif /* GRAPHANALYZER_H_ */ +#endif /* MRMC_SOLVER_GRAPHANALYZER_H_ */ diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index a7c063eb4..041272daf 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -1,16 +1,16 @@ -#ifndef MRMC_VECTOR_BITVECTOR_H_ -#define MRMC_VECTOR_BITVECTOR_H_ +#ifndef MRMC_STORAGE_BITVECTOR_H_ +#define MRMC_STORAGE_BITVECTOR_H_ #include #include #include #include "boost/integer/integer_mask.hpp" -#include "src/exceptions/invalid_state.h" -#include "src/exceptions/invalid_argument.h" -#include "src/exceptions/out_of_range.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" -#include "src/utility/osDetection.h" +#include "src/utility/OsDetection.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -102,7 +102,7 @@ public: // Check whether the given length is valid. if (length == 0) { LOG4CPLUS_ERROR(logger, "Trying to create bit vector of size 0."); - throw mrmc::exceptions::invalid_argument("Trying to create a bit vector of size 0."); + throw mrmc::exceptions::InvalidArgumentException("Trying to create a bit vector of size 0."); } // Compute the correct number of buckets needed to store the given number of bits @@ -205,7 +205,7 @@ public: */ void set(const uint_fast64_t index, const bool value) { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw mrmc::exceptions::out_of_range(); + if (bucket >= this->bucketCount) throw mrmc::exceptions::OutOfRangeException(); uint_fast64_t mask = static_cast(1) << (index & mod64mask); if (value) { this->bucketArray[bucket] |= mask; @@ -223,7 +223,7 @@ public: */ bool get(const uint_fast64_t index) const { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw mrmc::exceptions::out_of_range(); + if (bucket >= this->bucketCount) throw mrmc::exceptions::OutOfRangeException(); uint_fast64_t mask = static_cast(1) << (index & mod64mask); return ((this->bucketArray[bucket] & mask) == mask); } @@ -544,4 +544,4 @@ private: } // namespace mrmc -#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ +#endif // MRMC_STORAGE_BITVECTOR_H_ diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 9373583c4..64eaf0d41 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -7,14 +7,14 @@ #include #include "boost/integer/integer_mask.hpp" -#include "src/exceptions/invalid_state.h" -#include "src/exceptions/invalid_argument.h" -#include "src/exceptions/out_of_range.h" -#include "src/exceptions/file_IO_exception.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" +#include "src/exceptions/FileIoException.h" #include "src/storage/BitVector.h" #include "src/storage/JacobiDecomposition.h" -#include "src/utility/const_templates.h" +#include "src/utility/ConstTemplates.h" #include "Eigen/Sparse" #include "gmm/gmm_matrix.h" @@ -78,7 +78,7 @@ public: // Check whether copying the matrix is safe. if (!ssm.hasError()) { LOG4CPLUS_ERROR(logger, "Trying to copy sparse matrix in error state."); - throw mrmc::exceptions::invalid_argument("Trying to copy sparse matrix in error state."); + throw mrmc::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state."); } else { // Try to prepare the internal storage and throw an error in case // of a failure. @@ -142,15 +142,15 @@ public: if (internalStatus != MatrixStatus::UnInitialized) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize matrix that is not uninitialized."); - throw mrmc::exceptions::invalid_state("Trying to initialize matrix that is not uninitialized."); + throw mrmc::exceptions::InvalidStateException("Trying to initialize matrix that is not uninitialized."); } else if (rowCount == 0) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to create initialize a matrix with 0 rows."); - throw mrmc::exceptions::invalid_argument("Trying to create initialize a matrix with 0 rows."); + throw mrmc::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows."); } else if (((rowCount * rowCount) - rowCount) < nonZeroEntries) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize a matrix with more non-zero entries than there can be."); - throw mrmc::exceptions::invalid_argument("Trying to initialize a matrix with more non-zero entries than there can be."); + throw mrmc::exceptions::InvalidArgumentException("Trying to initialize a matrix with more non-zero entries than there can be."); } else { // If it is safe, initialize necessary members and prepare the // internal storage. @@ -181,7 +181,7 @@ public: if (!eigenSparseMatrix.isCompressed()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize from an Eigen matrix that is not in compressed form."); - throw mrmc::exceptions::invalid_argument("Trying to initialize from an Eigen matrix that is not in compressed form."); + throw mrmc::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that is not in compressed form."); } // Compute the actual (i.e. non-diagonal) number of non-zero entries. @@ -274,7 +274,7 @@ public: if ((row > rowCount) || (col > rowCount)) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to add a value at illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::out_of_range("Trying to add a value at illegal position."); + throw mrmc::exceptions::OutOfRangeException("Trying to add a value at illegal position."); } if (row == col) { // Set a diagonal element. @@ -307,11 +307,11 @@ public: if (!isInitialized()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to finalize an uninitialized matrix."); - throw mrmc::exceptions::invalid_state("Trying to finalize an uninitialized matrix."); + throw mrmc::exceptions::InvalidStateException("Trying to finalize an uninitialized matrix."); } else if (currentSize != nonZeroEntryCount) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to finalize a matrix that was initialized with more non-zero entries than given."); - throw mrmc::exceptions::invalid_state("Trying to finalize a matrix that was initialized with more non-zero entries than given."); + throw mrmc::exceptions::InvalidStateException("Trying to finalize a matrix that was initialized with more non-zero entries than given."); } else { // Fill in the missing entries in the row_indications array. // (Can happen because of empty rows at the end.) @@ -345,7 +345,7 @@ public: // Check for illegal access indices. if ((row > rowCount) || (col > rowCount)) { LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::out_of_range("Trying to read a value from illegal position."); + throw mrmc::exceptions::OutOfRangeException("Trying to read a value from illegal position."); return false; } @@ -395,7 +395,7 @@ public: // Check for illegal access indices. if ((row > rowCount) || (col > rowCount)) { LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::out_of_range("Trying to read a value from illegal position."); + throw mrmc::exceptions::OutOfRangeException("Trying to read a value from illegal position."); } // Read elements on the diagonal directly. @@ -422,7 +422,7 @@ public: ++rowStart; } - throw mrmc::exceptions::invalid_argument("Trying to get a reference to a non-existant value."); + throw mrmc::exceptions::InvalidArgumentException("Trying to get a reference to a non-existant value."); } /*! @@ -514,7 +514,7 @@ public: if (!isReadReady()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to convert a matrix that is not in a readable state to an Eigen matrix."); - throw mrmc::exceptions::invalid_state("Trying to convert a matrix that is not in a readable state to an Eigen matrix."); + throw mrmc::exceptions::InvalidStateException("Trying to convert a matrix that is not in a readable state to an Eigen matrix."); } else { // Create the resulting matrix. int_fast32_t eigenRows = static_cast(rowCount); @@ -669,7 +669,7 @@ public: } } // Fill in sentinel element at the end. - result->jc[rowCount] = realNonZeros; + result->jc[rowCount] = static_cast(realNonZeros); // Now, we can copy the temporary array to the GMMXX format. result->ir.resize(realNonZeros); @@ -732,7 +732,7 @@ public: // Check whether the accessed state exists. if (row > rowCount) { LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing."); - throw mrmc::exceptions::out_of_range("Trying to make an illegal row absorbing."); + throw mrmc::exceptions::OutOfRangeException("Trying to make an illegal row absorbing."); return false; } @@ -796,7 +796,7 @@ public: // Check for valid constraint. if (constraint.getNumberOfSetBits() == 0) { LOG4CPLUS_ERROR(logger, "Trying to create a sub-matrix of size 0."); - throw mrmc::exceptions::invalid_argument("Trying to create a sub-matrix of size 0."); + throw mrmc::exceptions::InvalidArgumentException("Trying to create a sub-matrix of size 0."); } // First, we need to determine the number of non-zero entries of the diff --git a/src/utility/const_templates.h b/src/utility/ConstTemplates.h similarity index 94% rename from src/utility/const_templates.h rename to src/utility/ConstTemplates.h index ea2231cba..8a4abef6a 100644 --- a/src/utility/const_templates.h +++ b/src/utility/ConstTemplates.h @@ -1,12 +1,12 @@ /* - * const_templates.h + * ConstTemplates.h * * Created on: 11.10.2012 * Author: Thomas Heinemann */ -#ifndef CONST_TEMPLATES_H_ -#define CONST_TEMPLATES_H_ +#ifndef MRMC_UTILITY_CONSTTEMPLATES_H_ +#define MRMC_UTILITY_CONSTTEMPLATES_H_ namespace mrmc { @@ -93,4 +93,4 @@ inline double constGetOne(double&) { } //namespace mrmc -#endif /* CONST_TEMPLATES_H_ */ +#endif /* MRMC_UTILITY_CONSTTEMPLATES_H_ */ diff --git a/src/utility/ioUtility.cpp b/src/utility/IoUtility.cpp similarity index 94% rename from src/utility/ioUtility.cpp rename to src/utility/IoUtility.cpp index 01872a3c9..299527044 100644 --- a/src/utility/ioUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -1,13 +1,13 @@ /* - * ioUtility.cpp + * IoUtility.cpp * * Created on: 17.10.2012 * Author: Thomas Heinemann */ -#include "src/utility/ioUtility.h" -#include "src/parser/readTraFile.h" -#include "src/parser/readLabFile.h" +#include "src/utility/IoUtility.h" +#include "src/parser/TraParser.h" +#include "src/parser/LabParser.h" #include diff --git a/src/utility/ioUtility.h b/src/utility/IoUtility.h similarity index 90% rename from src/utility/ioUtility.h rename to src/utility/IoUtility.h index 04a389a1d..5b691d9b2 100644 --- a/src/utility/ioUtility.h +++ b/src/utility/IoUtility.h @@ -1,12 +1,12 @@ /* - * ioUtility.h + * IoUtility.h * * Created on: 17.10.2012 * Author: Thomas Heinemann */ -#ifndef UTILITY_H_ -#define UTILITY_H_ +#ifndef MRMC_UTILITY_IOUTILITY_H_ +#define MRMC_UTILITY_IOUTILITY_H_ #include "src/models/Dtmc.h" @@ -42,4 +42,4 @@ mrmc::models::Dtmc* parseDTMC(const char* tra_file, const char* lab_file } //namespace mrmc -#endif /* UTILITY_H_ */ +#endif /* MRMC_UTILITY_IOUTILITY_H_ */ diff --git a/src/utility/osDetection.h b/src/utility/OsDetection.h similarity index 65% rename from src/utility/osDetection.h rename to src/utility/OsDetection.h index a88e8354c..af8896adf 100644 --- a/src/utility/osDetection.h +++ b/src/utility/OsDetection.h @@ -1,15 +1,21 @@ -#pragma once +#ifndef MRMC_UTILITY_OSDETECTION_H_ +#define MRMC_UTILITY_OSDETECTION_H_ #if defined __linux__ || defined __linux # define LINUX #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ # define MACOSX # define _DARWIN_USE_64_BIT_INODE +# include +# include #elif defined _WIN32 || defined _WIN64 # define WINDOWS # define NOMINMAX # include # include +# define strncpy strncpy_s #else # error Could not detect Operating System #endif + +#endif // MRMC_UTILITY_OSDETECTION_H_ \ No newline at end of file diff --git a/src/utility/settings.cpp b/src/utility/Settings.cpp similarity index 94% rename from src/utility/settings.cpp rename to src/utility/Settings.cpp index 05cfe1759..bf79a0441 100644 --- a/src/utility/settings.cpp +++ b/src/utility/Settings.cpp @@ -1,11 +1,11 @@ /* - * settings.cpp + * Settings.cpp * * Created on: 22.11.2012 * Author: Gereon Kremer */ -#include "src/utility/settings.h" +#include "src/utility/Settings.h" #include "src/exceptions/BaseException.h" @@ -102,16 +102,16 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) { LOG4CPLUS_ERROR(logger, "Could not read config file"); } catch (bpo::required_option e) { - throw mrmc::exceptions::InvalidSettings() << "Required option missing"; + throw mrmc::exceptions::InvalidSettingsException() << "Required option missing"; } catch (bpo::validation_error e) { - throw mrmc::exceptions::InvalidSettings() << "Validation failed: " << e.what(); + throw mrmc::exceptions::InvalidSettingsException() << "Validation failed: " << e.what(); } catch (bpo::invalid_command_line_syntax e) { - throw mrmc::exceptions::InvalidSettings() << e.what(); + throw mrmc::exceptions::InvalidSettingsException() << e.what(); } catch (bpo::error e) { - throw mrmc::exceptions::InvalidSettings() << e.what(); + throw mrmc::exceptions::InvalidSettingsException() << e.what(); } } diff --git a/src/utility/settings.h b/src/utility/Settings.h similarity index 96% rename from src/utility/settings.h rename to src/utility/Settings.h index 69cb0be92..5b76d839e 100644 --- a/src/utility/settings.h +++ b/src/utility/Settings.h @@ -1,12 +1,12 @@ /* - * settings.h + * Settings.h * * Created on: 22.11.2012 * Author: Gereon Kremer */ -#ifndef SETTINGS_H_ -#define SETTINGS_H_ +#ifndef MRMC_SETTINGS_SETTINGS_H_ +#define MRMC_SETTINGS_SETTINGS_H_ #include #include @@ -14,7 +14,7 @@ #include #include #include -#include "src/exceptions/InvalidSettings.h" +#include "src/exceptions/InvalidSettingsException.h" namespace mrmc { @@ -52,7 +52,7 @@ namespace settings { */ template const T& get(const std::string &name) const { - if (this->vm.count(name) == 0) throw mrmc::exceptions::InvalidSettings() << "Could not read option " << name << "."; + if (this->vm.count(name) == 0) throw mrmc::exceptions::InvalidSettingsException() << "Could not read option " << name << "."; return this->vm[name].as(); } @@ -209,4 +209,4 @@ namespace settings { } // namespace settings } // namespace mrmc -#endif // SETTINGS_H_ +#endif // MRMC_SETTINGS_SETTINGS_H_ diff --git a/src/utility/vector.h b/src/utility/Vector.h similarity index 88% rename from src/utility/vector.h rename to src/utility/Vector.h index d872fc124..d33de256c 100644 --- a/src/utility/vector.h +++ b/src/utility/Vector.h @@ -1,12 +1,12 @@ /* - * vector.h + * Vector.h * * Created on: 06.12.2012 * Author: Christian Dehnert */ -#ifndef VECTOR_H_ -#define VECTOR_H_ +#ifndef MRMC_UTILITY_VECTOR_H_ +#define MRMC_UTILITY_VECTOR_H_ #include "Eigen/src/Core/Matrix.h" @@ -40,4 +40,4 @@ void setVectorValues(Eigen::Matrix* eigenVector, const mrmc: } //namespace mrmc -#endif /* VECTOR_H_ */ +#endif /* MRMC_UTILITY_VECTOR_H_ */ diff --git a/test/eigen/sparse_matrix_test.cpp b/test/eigen/EigenSparseMatrixTest.cpp similarity index 97% rename from test/eigen/sparse_matrix_test.cpp rename to test/eigen/EigenSparseMatrixTest.cpp index 39f6d274d..67b70f986 100644 --- a/test/eigen/sparse_matrix_test.cpp +++ b/test/eigen/EigenSparseMatrixTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "Eigen/Sparse" -#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/InvalidArgumentException.h" #include "boost/integer/integer_mask.hpp" TEST(EigenSparseMatrixTest, BasicReadWriteTest) { diff --git a/test/parser/parse_dtmc_test.cpp b/test/parser/ParseDtmcTest.cpp similarity index 90% rename from test/parser/parse_dtmc_test.cpp rename to test/parser/ParseDtmcTest.cpp index 239ba735f..475db9414 100644 --- a/test/parser/parse_dtmc_test.cpp +++ b/test/parser/ParseDtmcTest.cpp @@ -1,5 +1,5 @@ /* - * parse_dtmc_test.cpp + * ParseDtmcTest.cpp * * Created on: 03.12.2012 * Author: Thomas Heinemann @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "mrmc-config.h" -#include "src/utility/ioUtility.h" +#include "src/utility/IoUtility.h" TEST(ParseDtmcTest, parseAndOutput) { mrmc::models::Dtmc* myDtmc; diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/ReadLabFileTest.cpp similarity index 92% rename from test/parser/read_lab_file_test.cpp rename to test/parser/ReadLabFileTest.cpp index 24eb98356..97e201151 100644 --- a/test/parser/read_lab_file_test.cpp +++ b/test/parser/ReadLabFileTest.cpp @@ -1,5 +1,5 @@ /* - * read_lab_file_test.cpp + * ReadLabFileTest.cpp * * Created on: 12.09.2012 * Author: Thomas Heinemann @@ -8,15 +8,15 @@ #include "gtest/gtest.h" #include "mrmc-config.h" #include "src/models/AtomicPropositionsLabeling.h" -#include "src/parser/readLabFile.h" -#include "src/exceptions/file_IO_exception.h" -#include "src/exceptions/wrong_file_format.h" +#include "src/parser/LabParser.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFileFormatException.h" #include TEST(ReadLabFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception); + ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); } TEST(ReadLabFileTest, ParseTest) { @@ -86,14 +86,14 @@ TEST(ReadLabFileTest, ParseTest) { } TEST(ReadLabFileTest, WrongHeaderTest1) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadLabFileTest, WrongHeaderTest2) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadLabFileTest, WrongPropositionTest) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::WrongFileFormatException); } diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/ReadTraFileTest.cpp similarity index 87% rename from test/parser/read_tra_file_test.cpp rename to test/parser/ReadTraFileTest.cpp index 509ea79d8..99c374a6b 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/test/parser/ReadTraFileTest.cpp @@ -1,5 +1,5 @@ /* - * read_tra_file_test.cpp + * ReadTraFileTest.cpp * * Created on: 16.08.2012 * Author: Thomas Heinemann @@ -8,15 +8,15 @@ #include "gtest/gtest.h" #include "mrmc-config.h" #include "src/storage/SquareSparseMatrix.h" -#include "src/parser/readTraFile.h" -#include "src/exceptions/file_IO_exception.h" -#include "src/exceptions/wrong_file_format.h" +#include "src/parser/TraParser.h" +#include "src/exceptions/FileIoException.h" +#include "src/exceptions/WrongFileFormatException.h" -#include "src/utility/ioUtility.h" +#include "src/utility/IoUtility.h" TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception); + ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); } /* The following test case is based on one of the original MRMC test cases @@ -69,13 +69,13 @@ TEST(ReadTraFileTest, ParseFileTest1) { } TEST(ReadTraFileTest, WrongFormatTestHeader1) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadTraFileTest, WrongFormatTestHeader2) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadTraFileTest, WrongFormatTestTransition) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format); + ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::WrongFileFormatException); } diff --git a/test/reward/reward_model_test.cpp b/test/reward/RewardModelTest.cpp similarity index 82% rename from test/reward/reward_model_test.cpp rename to test/reward/RewardModelTest.cpp index 58a77fa1c..b44b05d82 100644 --- a/test/reward/reward_model_test.cpp +++ b/test/reward/RewardModelTest.cpp @@ -1,11 +1,11 @@ #include "gtest/gtest.h" #include "Eigen/Sparse" -#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/InvalidArgumentException.h" #include "boost/integer/integer_mask.hpp" #include -#include "reward/reward_model.h" +#include "reward/RewardModel.h" TEST(RewardModelTest, ReadWriteTest) { // 50 entries diff --git a/test/storage/BitVectorTest.cpp b/test/storage/BitVectorTest.cpp index a556fb790..02c52c728 100644 --- a/test/storage/BitVectorTest.cpp +++ b/test/storage/BitVectorTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "src/storage/BitVector.h" -#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/InvalidArgumentException.h" TEST(BitVectorTest, GetSetTest) { mrmc::storage::BitVector *bv = NULL; diff --git a/test/storage/SquareSparseMatrixTest.cpp b/test/storage/SquareSparseMatrixTest.cpp index da42aacc4..40648118e 100644 --- a/test/storage/SquareSparseMatrixTest.cpp +++ b/test/storage/SquareSparseMatrixTest.cpp @@ -1,12 +1,13 @@ #include "gtest/gtest.h" #include "src/storage/SquareSparseMatrix.h" -#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" TEST(SquareSparseMatrixTest, ZeroRowsTest) { mrmc::storage::SquareSparseMatrix *ssm = new mrmc::storage::SquareSparseMatrix(0); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); - ASSERT_THROW(ssm->initialize(50), mrmc::exceptions::invalid_argument); + ASSERT_THROW(ssm->initialize(50), mrmc::exceptions::InvalidArgumentException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); delete ssm; @@ -16,7 +17,7 @@ TEST(SquareSparseMatrixTest, TooManyEntriesTest) { mrmc::storage::SquareSparseMatrix *ssm = new mrmc::storage::SquareSparseMatrix(2); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); - ASSERT_THROW(ssm->initialize(10), mrmc::exceptions::invalid_argument); + ASSERT_THROW(ssm->initialize(10), mrmc::exceptions::InvalidArgumentException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); delete ssm; @@ -29,16 +30,16 @@ TEST(SquareSparseMatrixTest, addNextValueTest) { ASSERT_NO_THROW(ssm->initialize(1)); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Initialized); - ASSERT_THROW(ssm->addNextValue(-1, 1, 1), mrmc::exceptions::out_of_range); + ASSERT_THROW(ssm->addNextValue(-1, 1, 1), mrmc::exceptions::OutOfRangeException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); - ASSERT_THROW(ssm->addNextValue(1, -1, 1), mrmc::exceptions::out_of_range); + ASSERT_THROW(ssm->addNextValue(1, -1, 1), mrmc::exceptions::OutOfRangeException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); - ASSERT_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::out_of_range); + ASSERT_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::OutOfRangeException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); - ASSERT_THROW(ssm->addNextValue(1, 6, 1), mrmc::exceptions::out_of_range); + ASSERT_THROW(ssm->addNextValue(1, 6, 1), mrmc::exceptions::OutOfRangeException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); delete ssm; @@ -57,7 +58,7 @@ TEST(SquareSparseMatrixTest, finalizeTest) { ASSERT_NO_THROW(ssm->addNextValue(1, 5, 1)); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Initialized); - ASSERT_THROW(ssm->finalize(), mrmc::exceptions::invalid_state); + ASSERT_THROW(ssm->finalize(), mrmc::exceptions::InvalidStateException); ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix::MatrixStatus::Error); delete ssm;