From cbf719568aa044b8b43021c57fcde660bab0c623 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 11:15:12 +0100 Subject: [PATCH 01/10] Added correct return value computation in method MakeRowsAbsorbing of class SquareSparseMatrix. --- src/storage/SquareSparseMatrix.h | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index a81302b1c..e50340538 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -665,13 +665,12 @@ public: * This function makes the rows given by the bit vector absorbing. */ bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) { + bool result = true; for (auto row : rows) { - makeRowAbsorbing(row); + result = result && makeRowAbsorbing(row); } - //FIXME: Had no return value; as I compile with -Werror ATM, build did not work so I added: - return false; - //(Thomas Heinemann, 06.12.2012) + return result; } /*! From ede5f56e5a769d893d36789e31a4381f354fb5af Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 11:30:31 +0100 Subject: [PATCH 02/10] Set model checker in copy constructor as const. --- src/modelChecker/DtmcPrctlModelChecker.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 83e29e38b..72faaef68 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -69,7 +69,7 @@ public: * * @param modelChecker The model checker that is copied. */ - explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + explicit DtmcPrctlModelChecker(const mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { this->model = new mrmc::models::Dtmc(modelChecker->getModel()); } From f80a7bcab32263a8406a34991164b7bca83cbe6a Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 11:42:35 +0100 Subject: [PATCH 03/10] Deleted DtmcPrctlModelChecker.cpp (was just there to make sure the corresponding h file is compiled, but is not necessary for that any more right now) --- src/modelChecker/DtmcPrctlModelChecker.cpp | 8 -------- 1 file changed, 8 deletions(-) delete mode 100644 src/modelChecker/DtmcPrctlModelChecker.cpp diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp deleted file mode 100644 index c2d52aa92..000000000 --- a/src/modelChecker/DtmcPrctlModelChecker.cpp +++ /dev/null @@ -1,8 +0,0 @@ -/* - * DtmcPrctlModelChecker.cpp - * - * Created on: 22.10.2012 - * Author: Thomas Heinemann - */ - -#include "DtmcPrctlModelChecker.h" From 1c088c1ca6a07ae92ad59ffc63f49bf019474c51 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 12:19:58 +0100 Subject: [PATCH 04/10] Added a probabilistic operator class that checks whether the probability that the path formula holds is equal to one single number, instead of comparing it to a lower and upper bound. --- src/formula/Formulas.h | 1 + src/formula/ProbabilisticIntervalOperator.h | 176 ++++++++++++++++++ src/formula/ProbabilisticOperator.h | 98 ++++------ src/modelChecker/DtmcPrctlModelChecker.h | 25 ++- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 2 +- 5 files changed, 229 insertions(+), 73 deletions(-) create mode 100644 src/formula/ProbabilisticIntervalOperator.h diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 58b679d8b..d37972987 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -18,6 +18,7 @@ #include "PCTLPathFormula.h" #include "PCTLStateFormula.h" #include "ProbabilisticOperator.h" +#include "ProbabilisticIntervalOperator.h" #include "Until.h" #endif /* FORMULAS_H_ */ diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h new file mode 100644 index 000000000..acc6f5b5f --- /dev/null +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -0,0 +1,176 @@ +/* + * ProbabilisticOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef PROBABILISTICINTERVALOPERATOR_H_ +#define PROBABILISTICINTERVALOPERATOR_H_ + +#include "PCTLStateFormula.h" +#include "PCTLPathFormula.h" +#include "utility/const_templates.h" + +namespace mrmc { + +namespace formula { + +/*! + * @brief + * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * If the probability interval consist just of one single value (i.e. it is [x,x] for some + * real number x), the class ProbabilisticOperator should be used instead. + * + * + * Has one PCTL path formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the probability that the path formula holds is inside the bounds + * specified in this operator + * + * 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 ProbabilisticOperator + * @see PCTLFormula + */ +template +class ProbabilisticIntervalOperator : public PCTLStateFormula { + +public: + /*! + * Empty constructor + */ + ProbabilisticIntervalOperator() { + upper = mrmc::utility::constGetZero(upper); + lower = mrmc::utility::constGetZero(lower); + pathFormula = NULL; + } + + /*! + * Constructor + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + * @param pathFormula The child node + */ + ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula& pathFormula) { + this->lower = lowerBound; + this->upper = upperBound; + this->pathFormula = &pathFormula; + } + + /*! + * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~ProbabilisticIntervalOperator() { + if (pathFormula != NULL) { + delete pathFormula; + } + } + + /*! + * @returns the child node (representation of a PCTL path formula) + */ + const PCTLPathFormula& getPathFormula () const { + return *pathFormula; + } + + /*! + * @returns the lower bound for the probability + */ + const T& getLowerBound() const { + return lower; + } + + /*! + * @returns the upper bound for the probability + */ + const T& getUpperBound() const { + return upper; + } + + /*! + * Sets the child node + * + * @param pathFormula the path formula that becomes the new child node + */ + void setPathFormula(PCTLPathFormula* pathFormula) { + this->pathFormula = pathFormula; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + */ + void setInterval(T lowerBound, T upperBound) { + this->lower = lowerBound; + this->upper = upperBound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "("; + result += " P["; + result += lower; + result += ";"; + result += upper; + result += "] "; + result += pathFormula->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() const { + ProbabilisticIntervalOperator* result = new ProbabilisticIntervalOperator(); + result->setInterval(lower, upper); + if (pathFormula != NULL) { + result->setPathFormula(pathFormula->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @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.checkProbabilisticIntervalOperator(this); + } + +private: + T lower; + T upper; + PCTLPathFormula* pathFormula; +}; + +} //namespace formula + +} //namespace mrmc + +#endif /* PROBABILISTICINTERVALOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 49e6530de..0e3876237 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -1,7 +1,7 @@ /* * ProbabilisticOperator.h * - * Created on: 19.10.2012 + * Created on: 07.12.2012 * Author: Thomas Heinemann */ @@ -9,53 +9,54 @@ #define PROBABILISTICOPERATOR_H_ #include "PCTLStateFormula.h" -#include "PCTLPathFormula.h" -#include "utility/const_templates.h" namespace mrmc { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator node as root. + * Class for a PCTL formula tree with a P (probablistic) operator node over a single real valued + * probability as root. + * + * If the probability interval consist just of one single value (i.e. it is [x,x] for some + * real number x), the class ProbabilisticOperator should be used instead. + * * * Has one PCTL path formula as sub formula/tree. * * @par Semantics - * The formula holds iff the probability that the path formula holds is inside the bounds specified in this operator + * The formula holds iff the probability that the path formula holds is equal to the probablility + * specified in this operator * * 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 ProbabilisticOperator * @see PCTLFormula */ template -class ProbabilisticOperator : public PCTLStateFormula { - +class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula { public: /*! * Empty constructor */ ProbabilisticOperator() { - upper = mrmc::utility::constGetZero(upper); - lower = mrmc::utility::constGetZero(lower); - pathFormula = NULL; + // TODO Auto-generated constructor stub + } /*! * Constructor * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability - * @param pathFormula The child node (can be omitted, is then set to NULL) + * @param bound The expected value for path formulas + * @param pathFormula The child node */ - ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { - this->lower = lowerBound; - this->upper = upperBound; - this->pathFormula = pathFormula; + ProbabilisticOperator(T bound, PCTLPathFormula& pathFormula) { + this->bound = bound; + this->pathFormula = &pathFormula; } /*! @@ -65,9 +66,7 @@ public: * (this behavior can be prevented by setting them to NULL before deletion) */ virtual ~ProbabilisticOperator() { - if (pathFormula != NULL) { - delete pathFormula; - } + // TODO Auto-generated destructor stub } /*! @@ -81,14 +80,7 @@ public: * @returns the lower bound for the probability */ const T& getLowerBound() const { - return lower; - } - - /*! - * @returns the upper bound for the probability - */ - const T& getUpperBound() const { - return upper; + return bound; } /*! @@ -101,29 +93,12 @@ public: } /*! - * Sets the interval in which the probability that the path formula holds may lie. + * Sets the expected probability that the path formula holds. * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param bound The bound for the probability */ - void setInterval(T lowerBound, T upperBound) { - this->lower = lowerBound; - this->upper = upperBound; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "("; - result += " P["; - result += lower; - result += ";"; - result += upper; - result += "] "; - result += pathFormula->toString(); - result += ")"; - return result; + void setInterval(T bound) { + this->bound = bound; } /*! @@ -131,11 +106,11 @@ public: * * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones * - * @returns a new AND-object that is identical the called object. + * @returns a new ProbabilisticOperator-object that is identical to the called object. */ virtual PCTLStateFormula* clone() const { ProbabilisticOperator* result = new ProbabilisticOperator(); - result->setInterval(lower, upper); + result->setBound(bound); if (pathFormula != NULL) { result->setPathFormula(pathFormula->clone()); } @@ -146,23 +121,22 @@ public: * Calls the model checker to check this formula. * Needed to infer the correct type of formula class. * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. + * @note This function should only be called in a generic check function of a model checker + * class. For other uses, the methods of the model checker should be used. * - * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + * @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 { + virtual mrmc::storage::BitVector *check( + const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkProbabilisticOperator(this); } private: - T lower; - T upper; + T bound; PCTLPathFormula* pathFormula; }; -} //namespace formula - -} //namespace mrmc - +} /* namespace formula */ +} /* namespace mrmc */ #endif /* PROBABILISTICOPERATOR_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index fcfb83cce..ba1b098c0 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -26,14 +26,7 @@ class DtmcPrctlModelChecker; #include "src/formula/PCTLPathFormula.h" #include "src/formula/PCTLStateFormula.h" -#include "src/formula/And.h" -#include "src/formula/AP.h" -#include "src/formula/BoundedUntil.h" -#include "src/formula/Next.h" -#include "src/formula/Not.h" -#include "src/formula/Or.h" -#include "src/formula/ProbabilisticOperator.h" -#include "src/formula/Until.h" +#include "src/formula/Formulas.h" #include "src/models/Dtmc.h" #include "src/storage/BitVector.h" @@ -163,12 +156,24 @@ public: } /*! - * The check method for a state formula with a probabilistic operator node as root in its formula tree + * The check method for a state formula with a probabilistic operator node as root in its + * formula tree * * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const = 0; + virtual mrmc::storage::BitVector* checkProbabilisticOperator( + const mrmc::formula::ProbabilisticOperator& formula) const = 0; + + /*! + * The check method for a state formula with a probabilistic interval operator node as root in + * its formula tree + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector* checkProbabilisticIntervalOperator( + const mrmc::formula::ProbabilisticIntervalOperator& formula) const = 0; /*! * The check method for a path formula; Will infer the actual type of formula and delegate it diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 696a86c1e..9192b7886 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -37,7 +37,7 @@ public: virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const { + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticIntervalOperator& formula) const { std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); From 851e3a631d9f265c65dec7663a56a888d49236c4 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 7 Dec 2012 13:09:43 +0100 Subject: [PATCH 05/10] Fixed CMakeLists.txt, made everything compile under Windows/MSVC Added popcnt for MSVC Fixed line ending detection in parser --- CMakeLists.txt | 35 ++++++++++++++++++++++++++--------- src/mrmc.cpp | 1 + src/parser/parser.cpp | 6 ++---- src/parser/parser.h | 5 ++++- src/parser/readLabFile.cpp | 4 ++++ src/storage/BitVector.h | 5 +++++ src/utility/osDetection.h | 13 ++++++++----- 7 files changed, 50 insertions(+), 19 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 99386c34b..77b790509 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -9,17 +9,32 @@ set (MRMC_CPP_VERSION_MINOR 0) # Set all GTest references to the version in the repository and show it as output set (GTEST_INCLUDE_DIR resources/3rdparty/gtest-1.6.0/include) -set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.a) -set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.a) +if(MSVC) + set (MRMC_LIB_SUFFIX lib) + set (GTEST_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest.${MRMC_LIB_SUFFIX}) + set (GTEST_MAIN_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest_main.${MRMC_LIB_SUFFIX}) + set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest.${MRMC_LIB_SUFFIX}) + set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest_main.${MRMC_LIB_SUFFIX}) + set (GTEST_LIBRARIES optimized ${GTEST_LIBRARY} debug ${GTEST_LIBRARY_DEBUG}) +else() + set (MRMC_LIB_SUFFIX a) + set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.${MRMC_LIB_SUFFIX}) + set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.${MRMC_LIB_SUFFIX}) + set (GTEST_LIBRARIES ${GTEST_LIBRARY}) # as we dont use FindGTest anymore +endif() message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}") message(STATUS "GTEST_LIBRARY is ${GTEST_LIBRARY}") message(STATUS "GTEST_MAIN_LIBRARY is ${GTEST_MAIN_LIBRARY}") # Set all log4cplus references the version in the repository set (LOG4CPLUS_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/include) -set (LOG4CPLUS_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.a) +if (MSVC) + set (LOG4CPLUS_LIBRARIES optimized ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Release/log4cplusS.${MRMC_LIB_SUFFIX} debug ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Debug/log4cplusSD.${MRMC_LIB_SUFFIX}) +else() + set (LOG4CPLUS_LIBRARIES ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.${MRMC_LIB_SUFFIX}) +endif() message(STATUS "LOG4CPLUS_INCLUDE_DIR is ${LOG4CPLUS_INCLUDE_DIR}") -message(STATUS "LOG4CPLUS_LIBRARY is ${LOG4CPLUS_LIBRARY}") +message(STATUS "LOG4CPLUS_LIBRARY is ${LOG4CPLUS_LIBRARIES}") # Set all Eigen references the version in the repository set(EIGEN3_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen) @@ -52,7 +67,8 @@ if(CMAKE_COMPILER_IS_GNUCC) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") endif(USE_POPCNT) elseif(MSVC) - + # required for GMM to compile, ugly error directive in their code + add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) # Set standard flags for GCC set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable") @@ -88,12 +104,13 @@ source_group(Headers FILES ${MRMC_TEST_HEADERS}) source_group(Sources FILES ${MRMC_TEST_SOURCES}) # Add base folder for better inclusion paths +include_directories("${PROJECT_SOURCE_DIR}") include_directories("${PROJECT_SOURCE_DIR}/src") # Set required external packages find_package(Threads REQUIRED) find_package(Doxygen REQUIRED) -#set(Boost_USE_STATIC_LIBS ON) +set(Boost_USE_STATIC_LIBS ON) set(Boost_USE_MULTITHREADED ON) set(Boost_USE_STATIC_RUNTIME OFF) find_package(Boost REQUIRED COMPONENTS program_options) @@ -141,7 +158,7 @@ if (GTEST_INCLUDE_DIR) enable_testing() include_directories(${GTEST_INCLUDE_DIR}) - target_link_libraries(mrmc-tests ${GTEST_LIBRARY} ${GTEST_MAIN_LIBRARY}) + target_link_libraries(mrmc-tests ${GTEST_LIBRARIES}) add_test(NAME mrmc-tests COMMAND mrmc-tests) if(MSVC) # VS2012 doesn't support correctly the tuples yet @@ -151,8 +168,8 @@ endif(GTEST_INCLUDE_DIR) if (LOG4CPLUS_INCLUDE_DIR) include_directories(${LOG4CPLUS_INCLUDE_DIR}) - target_link_libraries(mrmc ${LOG4CPLUS_LIBRARY}) - target_link_libraries(mrmc-tests ${LOG4CPLUS_LIBRARY}) + target_link_libraries(mrmc ${LOG4CPLUS_LIBRARIES}) + target_link_libraries(mrmc-tests ${LOG4CPLUS_LIBRARIES}) # On Linux, we have to link against librt if (UNIX AND NOT APPLE) target_link_libraries(mrmc rt) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index a63ea0f4e..c531102f5 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -12,6 +12,7 @@ * Description: Central part of the application containing the main() Method */ +#include "src/utility/osDetection.h" #include #include #include diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 403ff6fd9..9e5558291 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,15 +1,13 @@ #include "src/parser/parser.h" #if defined LINUX || defined MACOSX - #include +# include +# include #elif defined WINDOWS #endif #include #include -//#if defined MACOSX - #include -//#endif #include #include #include diff --git a/src/parser/parser.h b/src/parser/parser.h index b7819c7be..78b8dd890 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -11,8 +11,10 @@ #include "src/utility/osDetection.h" #if defined LINUX || defined MACOSX - #include +# include #elif defined WINDOWS +# include +# include #endif #include @@ -20,6 +22,7 @@ #include #include +#include #include "src/exceptions/file_IO_exception.h" #include "src/exceptions/wrong_file_format.h" diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index 42a7566e2..7bb020e5a 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -57,7 +57,11 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) /* * first run: obtain number of propositions */ +#ifdef WINDOWS + char separator[] = " \r\n\t"; +#else char separator[] = " \n\t"; +#endif bool foundDecl = false, foundEnd = false; uint_fast32_t proposition_count = 0; { diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index dca00e61d..a7c063eb4 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -10,6 +10,7 @@ #include "src/exceptions/invalid_argument.h" #include "src/exceptions/out_of_range.h" +#include "src/utility/osDetection.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -394,6 +395,10 @@ public: // Check if we are using g++ or clang++ and, if so, use the built-in function #if (defined (__GNUG__) || defined(__clang__)) result += __builtin_popcountll(this->bucketArray[i]); +#elif defined WINDOWS + #include + // if the target machine does not support SSE4, this will fail. + result += _mm_popcnt_u64(this->bucketArray[i]); #else uint_fast32_t cnt; uint_fast64_t bitset = this->bucketArray[i]; diff --git a/src/utility/osDetection.h b/src/utility/osDetection.h index da72a909f..a88e8354c 100644 --- a/src/utility/osDetection.h +++ b/src/utility/osDetection.h @@ -1,12 +1,15 @@ #pragma once #if defined __linux__ || defined __linux - #define LINUX +# define LINUX #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ - #define MACOSX - #define _DARWIN_USE_64_BIT_INODE +# define MACOSX +# define _DARWIN_USE_64_BIT_INODE #elif defined _WIN32 || defined _WIN64 - #define WINDOWS +# define WINDOWS +# define NOMINMAX +# include +# include #else - #error Could not detect Operating System +# error Could not detect Operating System #endif From 645ebe8b9e45b3cf9fef6b180bb2f62758c15e23 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 13:31:24 +0100 Subject: [PATCH 06/10] Changed functions of GmmxxDtmcPrctlModelChecker to fit to the changed interface. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 9192b7886..488b03c00 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -37,7 +37,12 @@ public: virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticIntervalOperator& formula) const { + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const { + //FIXME: Implementation needed + return NULL; + } + + virtual mrmc::storage::BitVector* checkProbabilisticIntervalOperator(const mrmc::formula::ProbabilisticIntervalOperator& formula) const { std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); From 667b60db8feddc3bc72094e1e5b142abbb6f28d8 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 7 Dec 2012 13:34:05 +0100 Subject: [PATCH 07/10] Added absolute path names for command line parameters for valgrind in make targets (by CMAKE variables), so it should work with out of source builds; and a dependency to the executables (so it is built automatically if that has not been done before) --- CMakeLists.txt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 77b790509..46518e999 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -189,5 +189,8 @@ configure_file ( "${PROJECT_BINARY_DIR}/mrmc-config.h" ) -add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ./mrmc examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab) -add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ./mrmc-tests) +add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/mrmc ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab + DEPENDS mrmc) +add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/mrmc-tests + DEPENDS mrmc-tests) + From 1f36724cc21589d74fddceeac603d33b3cdda904 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 7 Dec 2012 17:03:58 +0100 Subject: [PATCH 08/10] Refactored StringOutput to use std::to_string Fixed Reference/Pointer bugs in all formulas. Implemented EigenDtmcPrctlModelChecker Replaced uses of int32 with 64bits --- src/formula/And.h | 2 +- src/formula/BoundedUntil.h | 5 ++-- src/formula/Next.h | 2 +- src/formula/Not.h | 2 +- src/formula/Or.h | 2 +- src/formula/ProbabilisticIntervalOperator.h | 6 ++-- src/formula/ProbabilisticOperator.h | 17 ++++++++--- src/models/AtomicPropositionsLabeling.h | 30 +++++++++---------- src/models/Dtmc.h | 2 +- src/mrmc.cpp | 32 ++++++++++++++++++--- src/parser/readLabFile.cpp | 2 +- src/parser/readTraFile.cpp | 10 +++---- src/parser/readTraFile.h | 2 +- src/storage/SquareSparseMatrix.h | 4 +-- src/utility/vector.h | 9 ++++++ 15 files changed, 84 insertions(+), 43 deletions(-) diff --git a/src/formula/And.h b/src/formula/And.h index 742633f3b..7a42193b8 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -142,7 +142,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.checkAnd(this); + return modelChecker.checkAnd(*this); } private: diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 93355b7f3..51131602d 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -11,7 +11,6 @@ #include "PCTLPathFormula.h" #include "PCTLStateFormula.h" #include "boost/integer/integer_mask.hpp" -#include "boost/lexical_cast.hpp" #include namespace mrmc { @@ -131,7 +130,7 @@ public: std::string result = "("; result += left->toString(); result += " U<="; - result += boost::lexical_cast(bound); + result += std::to_string(bound); result += " "; result += right->toString(); result += ")"; @@ -168,7 +167,7 @@ public: * @returns A vector indicating the probability that the formula holds for each state. */ virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkBoundedUntil(this); + return modelChecker.checkBoundedUntil(*this); } private: diff --git a/src/formula/Next.h b/src/formula/Next.h index 1a5acb1ec..2eb00be05 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -113,7 +113,7 @@ public: * @returns A vector indicating the probability that the formula holds for each state. */ virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkNext(this); + return modelChecker.checkNext(*this); } private: diff --git a/src/formula/Not.h b/src/formula/Not.h index c816a827b..574d287a1 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -106,7 +106,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.checkNot(this); + return modelChecker.checkNot(*this); } private: diff --git a/src/formula/Or.h b/src/formula/Or.h index 78185b0d5..5a60d9770 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -141,7 +141,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.checkOr(this); + return modelChecker.checkOr(*this); } private: diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h index acc6f5b5f..8b50da26d 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -125,9 +125,9 @@ public: virtual std::string toString() const { std::string result = "("; result += " P["; - result += lower; + result += std::to_string(lower); result += ";"; - result += upper; + result += std::to_string(upper); result += "] "; result += pathFormula->toString(); result += ")"; @@ -160,7 +160,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.checkProbabilisticIntervalOperator(this); + return modelChecker.checkProbabilisticIntervalOperator(*this); } private: diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 0e3876237..43962d6d4 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -77,9 +77,9 @@ public: } /*! - * @returns the lower bound for the probability + * @returns the bound for the probability */ - const T& getLowerBound() const { + const T& getBound() const { return bound; } @@ -97,7 +97,7 @@ public: * * @param bound The bound for the probability */ - void setInterval(T bound) { + void setBound(T bound) { this->bound = bound; } @@ -129,9 +129,18 @@ public: */ virtual mrmc::storage::BitVector *check( const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkProbabilisticOperator(this); + return modelChecker.checkProbabilisticOperator(*this); } + /*! + * Returns a string representation of this PCTLStateFormula + * + * @returns a string representation of this PCTLStateFormula + */ + virtual std::string toString() const { + // TODO + return ""; + } private: T bound; PCTLPathFormula* pathFormula; diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 457d2f6a1..34c2da73b 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -33,10 +33,10 @@ public: * @param stateCount The number of states of the model. * @param apCountMax The number of atomic propositions. */ - AtomicPropositionsLabeling(const uint_fast32_t stateCount, const uint_fast32_t apCountMax) + AtomicPropositionsLabeling(const uint_fast64_t stateCount, const uint_fast64_t apCountMax) : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0) { this->singleLabelings = new mrmc::storage::BitVector*[apCountMax]; - for (uint_fast32_t i = 0; i < apCountMax; ++i) { + for (uint_fast64_t i = 0; i < apCountMax; ++i) { this->singleLabelings[i] = new mrmc::storage::BitVector(stateCount); } } @@ -53,7 +53,7 @@ public: apsCurrent(atomicPropositionsLabeling.apsCurrent), nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap) { this->singleLabelings = new mrmc::storage::BitVector*[apCountMax]; - for (uint_fast32_t i = 0; i < apCountMax; ++i) { + for (uint_fast64_t i = 0; i < apCountMax; ++i) { this->singleLabelings[i] = new mrmc::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]); } } @@ -64,7 +64,7 @@ public: */ virtual ~AtomicPropositionsLabeling() { // delete all the single atomic proposition labelings in the map - for (uint_fast32_t i = 0; i < apCountMax; ++i) { + for (uint_fast64_t i = 0; i < apCountMax; ++i) { delete this->singleLabelings[i]; this->singleLabelings[i] = NULL; } @@ -79,7 +79,7 @@ public: * @param ap The name of the atomic proposition to add. * @return The index of the new proposition. */ - uint_fast32_t addAtomicProposition(std::string ap) { + uint_fast64_t addAtomicProposition(std::string ap) { if (nameToLabelingMap.count(ap) != 0) { throw std::out_of_range("Atomic Proposition already exists."); } @@ -89,7 +89,7 @@ public: } nameToLabelingMap[ap] = apsCurrent; - uint_fast32_t returnValue = apsCurrent++; + uint_fast64_t returnValue = apsCurrent++; return returnValue; } @@ -107,7 +107,7 @@ public: * @param ap The name of the atomic proposition. * @param state The index of the state to label. */ - void addAtomicPropositionToState(std::string ap, const uint_fast32_t state) { + void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) { if (nameToLabelingMap.count(ap) == 0) { throw std::out_of_range("Atomic Proposition '" + ap + "' unknown."); } @@ -122,7 +122,7 @@ public: * @param state The index of a state * @returns The list of propositions for the given state */ - std::set getPropositionsForState(uint_fast32_t state) { + std::set getPropositionsForState(uint_fast64_t state) { if (state >= stateCount) { throw std::out_of_range("State index out of range."); } @@ -144,7 +144,7 @@ public: * @return True if the node is labeled with the atomic proposition, false * otherwise. */ - bool stateHasAtomicProposition(std::string ap, const uint_fast32_t state) { + bool stateHasAtomicProposition(std::string ap, const uint_fast64_t state) { return this->singleLabelings[nameToLabelingMap[ap]]->get(state); } @@ -153,7 +153,7 @@ public: * the initialization). * @return The number of atomic propositions. */ - uint_fast32_t getNumberOfAtomicPropositions() { + uint_fast64_t getNumberOfAtomicPropositions() { return apCountMax; } @@ -174,7 +174,7 @@ public: uint_fast64_t getSizeInMemory() { uint_fast64_t size = sizeof(*this); // Add sizes of all single labelings. - for (uint_fast32_t i = 0; i < apCountMax; i++) { + for (uint_fast64_t i = 0; i < apCountMax; i++) { size += this->singleLabelings[i]->getSizeInMemory(); } return size; @@ -197,24 +197,24 @@ public: private: /*! The number of states whose labels are to be stored by this object. */ - uint_fast32_t stateCount; + uint_fast64_t stateCount; /*! The number of different atomic propositions this object can store. */ - uint_fast32_t apCountMax; + uint_fast64_t apCountMax; /*! * The number of different atomic propositions currently associated with * this labeling. Used to prevent too many atomic propositions from being * added to this object. */ - uint_fast32_t apsCurrent; + uint_fast64_t apsCurrent; /*! * Associates a name of an atomic proposition to its corresponding labeling * by mapping the name to a specific index in the array of all * individual labelings. */ - std::unordered_map nameToLabelingMap; + std::unordered_map nameToLabelingMap; /*! * Stores all individual labelings. To find the labeling associated with diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 83bba3d6e..8fa263f54 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -102,7 +102,7 @@ public: /*! * */ - std::set getPropositionsForState(uint_fast32_t state) { + std::set getPropositionsForState(uint_fast64_t state) { return stateLabeling->getPropositionsForState(state); } diff --git a/src/mrmc.cpp b/src/mrmc.cpp index c531102f5..cb5510530 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -22,6 +22,7 @@ #include "src/models/Dtmc.h" #include "src/storage/SquareSparseMatrix.h" #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" @@ -106,14 +107,37 @@ int main(const int argc, const char* argv[]) { dtmc.printModelInformationToStream(std::cout); // Uncomment this if you want to see the first model checking procedure in action. :) - /* - mrmc::modelChecker::GmmxxDtmcPrctlModelChecker mc(dtmc); + mrmc::modelChecker::EigenDtmcPrctlModelChecker mc(dtmc); mrmc::formula::AP* trueFormula = new mrmc::formula::AP(std::string("true")); mrmc::formula::AP* ap = new mrmc::formula::AP(std::string("observe0Greater1")); mrmc::formula::Until* until = new mrmc::formula::Until(trueFormula, ap); - mc.checkPathFormula(*until); + std::vector* eigenResult = mc.checkPathFormula(*until); delete until; - */ + + mrmc::modelChecker::GmmxxDtmcPrctlModelChecker mcG(dtmc); + mrmc::formula::AP* trueFormulaG = new mrmc::formula::AP(std::string("true")); + mrmc::formula::AP* apG = new mrmc::formula::AP(std::string("observe0Greater1")); + mrmc::formula::Until* untilG = new mrmc::formula::Until(trueFormulaG, apG); + std::vector* gmmResult = mcG.checkPathFormula(*untilG); + delete untilG; + + if (eigenResult->size() != gmmResult->size()) { + LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results (Eigen: " << eigenResult->size() << ", Gmm: " << gmmResult->size() << ") in size!"); + } else { + LOG4CPLUS_INFO(logger, "Testing for different entries"); + for (int i = 0; i < eigenResult->size(); ++i) { + if (std::abs((eigenResult->at(i) - gmmResult->at(i))) > 0) { + LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results in entry " << i << " (Eigen: " << eigenResult->at(i) << ", Gmm: " << gmmResult->at(i) << ")!"); + } + } + } + + /* + LOG4CPLUS_INFO(logger, "Result: "); + LOG4CPLUS_INFO(logger, "Entry : EigenResult at Entry : GmmResult at Entry"); + for (int i = 0; i < eigenResult->size(); ++i) { + LOG4CPLUS_INFO(logger, i << " : " << eigenResult->at(i) << " : " << gmmResult->at(i)); + }*/ if (s != nullptr) { delete s; diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index 7bb020e5a..3ef488373 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -163,7 +163,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) /* * now parse node label assignments */ - uint_fast32_t node; + uint_fast64_t node; char proposition[128]; size_t cnt; /* diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp index 6a73bff0a..902259f54 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/readTraFile.cpp @@ -48,9 +48,9 @@ namespace parser{ * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode) +uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) { - uint_fast32_t non_zero = 0; + uint_fast64_t non_zero = 0; /* * check file header and extract number of transitions @@ -74,7 +74,7 @@ uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode) /* * check all transitions for non-zero diagonal entrys */ - uint_fast32_t row, col; + uint_fast64_t row, col; double val; maxnode = 0; char* tmp; @@ -134,8 +134,8 @@ TraParser::TraParser(const char * filename) /* * perform first pass, i.e. count entries that are not zero and not on the diagonal */ - uint_fast32_t maxnode; - uint_fast32_t non_zero = this->firstPass(file.data, maxnode); + uint_fast64_t maxnode; + uint_fast64_t non_zero = this->firstPass(file.data, maxnode); /* * if first pass returned zero, the file format was wrong */ diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h index c46167e37..cf2886b18 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/readTraFile.h @@ -30,7 +30,7 @@ class TraParser : Parser private: std::shared_ptr> matrix; - uint_fast32_t firstPass(char* buf, uint_fast32_t &maxnode); + uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode); }; diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 5f322de01..d57d9ddb6 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -509,7 +509,7 @@ public: rowEnd = rowIndications[row + 1]; while (rowStart < rowEnd) { if (valueStorage[rowStart] == 0) zeroCount++; - tripletList.push_back(IntTriplet(row, columnIndications[rowStart], valueStorage[rowStart])); + tripletList.push_back(IntTriplet(static_cast(row), static_cast(columnIndications[rowStart]), valueStorage[rowStart])); ++rowStart; } } @@ -517,7 +517,7 @@ public: // Then add the elements on the diagonal. for (uint_fast64_t i = 0; i < rowCount; ++i) { if (diagonalStorage[i] == 0) zeroCount++; - tripletList.push_back(IntTriplet(i, i, diagonalStorage[i])); + tripletList.push_back(IntTriplet(static_cast(i), static_cast(i), diagonalStorage[i])); } // Let Eigen create a matrix from the given list of triplets. diff --git a/src/utility/vector.h b/src/utility/vector.h index eff5f02b9..d744fdc35 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -8,6 +8,8 @@ #ifndef VECTOR_H_ #define VECTOR_H_ +#include "Eigen/src/Core/Matrix.h" + namespace mrmc { namespace utility { @@ -27,6 +29,13 @@ void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& pos } } +template +void setVectorValues(Eigen::Matrix* eigenVector, const mrmc::storage::BitVector& positions, T value) { + for (auto position : positions) { + (*vector)(position, 0) = value; + } +} + } //namespace utility } //namespace mrmc From b50d906ae30a8a57fa917e13acae10bed0717349 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 7 Dec 2012 19:05:02 +0100 Subject: [PATCH 09/10] Added missing EigenDtmcPrctlModelChecker.h Refactored solver to use iterative deepening for convergence :P --- src/exceptions/NoConvergence.h | 56 ++++ src/modelChecker/EigenDtmcPrctlModelChecker.h | 267 ++++++++++++++++++ src/mrmc.cpp | 14 +- 3 files changed, 336 insertions(+), 1 deletion(-) create mode 100644 src/exceptions/NoConvergence.h create mode 100644 src/modelChecker/EigenDtmcPrctlModelChecker.h diff --git a/src/exceptions/NoConvergence.h b/src/exceptions/NoConvergence.h new file mode 100644 index 000000000..1ae6a8eab --- /dev/null +++ b/src/exceptions/NoConvergence.h @@ -0,0 +1,56 @@ +#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 + InvalidSettings() : exception() { + iterations = -1; + maxIterations = -1; + } + InvalidSettings(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/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h new file mode 100644 index 000000000..b08a3ae92 --- /dev/null +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -0,0 +1,267 @@ +/* + * EigenDtmcPrctlModelChecker.h + * + * Created on: 07.12.2012 + * Author: + */ + +#ifndef EIGENDTMCPRCTLMODELCHECKER_H_ +#define EIGENDTMCPRCTLMODELCHECKER_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 "Eigen/Sparse" +#include "Eigen/src/IterativeLinearSolvers/BiCGSTAB.h" + +#include "gmm/gmm_matrix.h" +#include "gmm/gmm_iter_solvers.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace mrmc { + +namespace modelChecker { + +/* + * A model checking engine that makes use of the eigen backend. + */ +template +class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker { + +public: + explicit EigenDtmcPrctlModelChecker(mrmc::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } + + virtual ~EigenDtmcPrctlModelChecker() { } + + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const { + std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); + + mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + Type bound = formula.getBound(); + for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { + if ((*probabilisticResult)[i] == bound) result->set(i, true); + } + + delete probabilisticResult; + + return result; + } + + virtual mrmc::storage::BitVector* checkProbabilisticIntervalOperator(const mrmc::formula::ProbabilisticIntervalOperator& formula) const { + std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); + + mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + Type lower = formula.getLowerBound(); + Type upper = formula.getUpperBound(); + for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { + if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true); + } + + delete probabilisticResult; + + return result; + } + + virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + + // Copy the matrix before we make any changes. + mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); + + // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. + tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates); + + // Transform the transition probability matrix to the eigen format to use its arithmetic. + Eigen::SparseMatrix* eigenMatrix = tmpMatrix.toEigenSparseMatrix(); + + // Create the vector with which to multiply. + uint_fast64_t stateCount = this->getModel().getNumberOfStates(); + + typedef Eigen::Matrix VectorType; + typedef Eigen::Map MapType; + + std::vector* result = new std::vector(stateCount); + + // Dummy Type variable for const templates + Type dummy; + mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne(dummy)); + + Type *p = &((*result)[0]); // get the address storing the data for result + MapType vectorMap(p, result->size()); // vectorMap shares data + + + // Now perform matrix-vector multiplication as long as we meet the bound of the formula. + for (uint_fast64_t i = 0, bound = formula.getBound(); i < bound; ++i) { + vectorMap = (*eigenMatrix) * vectorMap; + } + + // Delete intermediate results. + delete leftStates; + delete rightStates; + delete eigenMatrix; + + return result; + } + + virtual std::vector* checkNext(const mrmc::formula::Next& formula) const { + // First, we need to compute the states that satisfy the sub-formula of the next-formula. + mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + Eigen::SparseMatrix* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix(); + + // Create the vector with which to multiply and initialize it correctly. + std::vector x(this->getModel().getNumberOfStates()); + Type dummy; + mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne(dummy)); + + // Delete not needed next states bit vector. + delete nextStates; + + typedef Eigen::Matrix VectorType; + typedef Eigen::Map MapType; + + Type *px = &(x[0]); // get the address storing the data for x + MapType vectorX(px, x.size()); // vectorX shares data + + // Create resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + + Type *pr = &((*result)[0]); // get the address storing the data for result + MapType vectorResult(px, result->size()); // vectorResult shares data + + // Perform the actual computation. + vectorResult = (*eigenMatrix) * vectorX; + + // Delete temporary matrix and return result. + delete eigenMatrix; + return result; + } + + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + + // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // all states that have probability 0 and 1 of satisfying the until-formula. + mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); + mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); + mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + notExistsPhiUntilPsiStates.complement(); + + delete leftStates; + delete rightStates; + + LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); + mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector and set values accordingly. + uint_fast64_t stateCount = this->getModel().getNumberOfStates(); + std::vector* result = new std::vector(stateCount); + + // Only try to solve system if there are states for which the probability is unknown. + if (maybeStates.getNumberOfSetBits() > 0) { + typedef Eigen::Matrix VectorType; + typedef Eigen::Map MapType; + + // Now we can eliminate the rows and columns from the original transition probability matrix. + mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + // Converting the matrix to the form needed for the equation system. That is, we go from + // x = A*x + b to (I-A)x = b. + submatrix->convertToEquationSystem(); + + // Transform the submatric matrix to the eigen format to use its solvers + Eigen::SparseMatrix* eigenSubMatrix = submatrix->toEigenSparseMatrix(); + + // Initialize the x vector with 0.5 for each element. This is the initial guess for + // the iterative solvers. It should be safe as for all 'maybe' states we know that the + // probability is strictly larger than 0. + std::vector x(maybeStates.getNumberOfSetBits(), Type(0.5)); + + // Map for x + Type *px = &(x[0]); // get the address storing the data for x + MapType vectorX(px, x.size()); // vectorX shares data + + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b(maybeStates.getNumberOfSetBits()); + + Type *pb = &(b[0]); // get the address storing the data for b + MapType vectorB(pb, b.size()); // vectorB shares data + + this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + + Eigen::BiCGSTAB> solver; + solver.compute(*eigenSubMatrix); + if(solver.info()!= Eigen::ComputationInfo::Success) { + // decomposition failed + LOG4CPLUS_ERROR(logger, "Decomposition of Submatrix failed!"); + } + + // Now do the actual solving. + LOG4CPLUS_INFO(logger, "Starting iterative solver."); + + solver.setTolerance(0.000001); + + bool hasConverged = false; + int turns = 6; + while (!hasConverged) { + vectorX = solver.solve(vectorB); + hasConverged = (solver.info() != Eigen::ComputationInfo::NoConvergence) || (turns <= 0); + if (!hasConverged) { + LOG4CPLUS_INFO(logger, "EigenDtmcPrctlModelChecker did not converge with " << solver.iterations() << " of max. " << solver.maxIterations() << "Iterations, restarting "); + solver.setMaxIterations(solver.maxIterations() * 2); + } + --turns; + } + + if(solver.info() == Eigen::ComputationInfo::InvalidInput) { + // solving failed + 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()); + } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { + // NumericalIssue + LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); + } else if(solver.info() == Eigen::ComputationInfo::Success) { + // solving Success + LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success"); + } + + // Set values of resulting vector according to result. + mrmc::utility::setVectorValues(result, maybeStates, x); + + // Delete temporary matrix. + delete eigenSubMatrix; + } + + // Dummy Type variable for const templates + Type dummy; + mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero(dummy)); + mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne(dummy)); + + return result; + } +}; + +} //namespace modelChecker + +} //namespace mrmc + +#endif /* EIGENDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index cb5510530..91e07b24d 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -30,6 +30,7 @@ #include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" #include "src/formula/Formulas.h" +#include "src/exceptions/NoConvergence.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -111,7 +112,15 @@ int main(const int argc, const char* argv[]) { mrmc::formula::AP* trueFormula = new mrmc::formula::AP(std::string("true")); mrmc::formula::AP* ap = new mrmc::formula::AP(std::string("observe0Greater1")); mrmc::formula::Until* until = new mrmc::formula::Until(trueFormula, ap); - std::vector* eigenResult = mc.checkPathFormula(*until); + + std::vector* eigenResult = NULL; + try { + eigenResult = mc.checkPathFormula(*until); + } catch (mrmc::exceptions::NoConvergence& nce) { + // solver did not converge + LOG4CPLUS_ERROR(logger, "EigenDtmcPrctlModelChecker did not converge with " << nce.getIterationCount() << " of max. " << nce.getMaxIterationCount() << "Iterations!"); + return -1; + } delete until; mrmc::modelChecker::GmmxxDtmcPrctlModelChecker mcG(dtmc); @@ -129,6 +138,9 @@ int main(const int argc, const char* argv[]) { if (std::abs((eigenResult->at(i) - gmmResult->at(i))) > 0) { LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results in entry " << i << " (Eigen: " << eigenResult->at(i) << ", Gmm: " << gmmResult->at(i) << ")!"); } + if (eigenResult->at(i) != 0.0) { + LOG4CPLUS_INFO(logger, "Non zero entry " << eigenResult->at(i) << " at " << i); + } } } From cbe162ab8478f60099532365d893d6fccf1c7b50 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 8 Dec 2012 11:31:27 +0100 Subject: [PATCH 10/10] Fixed some copy-paste errors. --- src/exceptions/NoConvergence.h | 4 ++-- src/utility/vector.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/exceptions/NoConvergence.h b/src/exceptions/NoConvergence.h index 1ae6a8eab..bd5b71af9 100644 --- a/src/exceptions/NoConvergence.h +++ b/src/exceptions/NoConvergence.h @@ -26,11 +26,11 @@ class NoConvergence : public std::exception this->maxIterations = maxIterations; } #else - InvalidSettings() : exception() { + NoConvergence() : exception() { iterations = -1; maxIterations = -1; } - InvalidSettings(const char * const s, int iterations, int maxIterations): exception() { + NoConvergence(const char * const s, int iterations, int maxIterations): exception() { this->iterations = iterations; this->maxIterations = maxIterations; } diff --git a/src/utility/vector.h b/src/utility/vector.h index d744fdc35..d872fc124 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -32,7 +32,7 @@ void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& pos template void setVectorValues(Eigen::Matrix* eigenVector, const mrmc::storage::BitVector& positions, T value) { for (auto position : positions) { - (*vector)(position, 0) = value; + (*eigenVector)(position, 0) = value; } }