From 67b3888ba9423cf536b5afc5345a9c898e3f7b5c Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 5 Dec 2012 15:24:11 +0100 Subject: [PATCH 1/3] Implemented basic functions of the model checker --- src/modelChecker/DtmcPrctlModelChecker.cpp | 24 ---------- src/modelChecker/DtmcPrctlModelChecker.h | 54 ++++++++++++++++------ 2 files changed, 40 insertions(+), 38 deletions(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp index f5a884921..c2d52aa92 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.cpp +++ b/src/modelChecker/DtmcPrctlModelChecker.cpp @@ -6,27 +6,3 @@ */ #include "DtmcPrctlModelChecker.h" - -namespace mrmc { - -namespace modelChecker { - -template -DtmcPrctlModelChecker::DtmcPrctlModelChecker(mrmc::models::Dtmc* dtmc) { - this->dtmc = dtmc; -} - -template -DtmcPrctlModelChecker::~DtmcPrctlModelChecker() { - delete this->dtmc; -} - -template -DtmcPrctlModelChecker::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - this->dtmc = new mrmc::models::Dtmc(modelChecker->getDtmc()); -} - - -} //namespace modelChecker - -} //namespace mrmc diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 3061dc75b..edb5fd8a8 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -60,19 +60,25 @@ public: * * @param Dtmc The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* dtmc) { + this->dtmc = dtmc; + } /*! * Copy constructor * * @param modelChecker The model checker that is copied. */ - explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); + explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + this->dtmc = new mrmc::models::Dtmc(modelChecker->getDtmc()); + } /*! * Destructor */ - virtual ~DtmcPrctlModelChecker(); + virtual ~DtmcPrctlModelChecker() { + delete this->dtmc; + } /*! * @returns A reference to the dtmc of the model checker. @@ -95,7 +101,9 @@ public: * @param ap A string representing an atomic proposition. * @returns The set of states labeled with the atomic proposition ap. */ - virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0; + virtual mrmc::storage::BitVector* getStatesLabeledWith(std::string ap) { + return dtmc->getLabeledStates(ap); + } /*! * Multiplies the matrix with a given vector; the result again is a vector. @@ -112,7 +120,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { + virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula& formula) { return formula->check(this); } @@ -122,7 +130,13 @@ public: * @param formula The And formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And* formula) = 0; + virtual mrmc::storage::BitVector* checkAnd(mrmc::formula::And& formula) { + mrmc::storage::BitVector* result = check(formula.getLeft()); + mrmc::storage::BitVector* right = check(formula.getRight()); + (*result) &= (*right); + delete right; + return result; + } /*! * The check method for a formula with an AP node as root in its formula tree @@ -130,7 +144,9 @@ public: * @param formula The AP state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP* formula) = 0; + virtual mrmc::storage::BitVector* checkAP(mrmc::formula::AP& formula) { + return getStatesLabeledWith(formula.getAP()); + } /*! * The check method for a formula with a Not node as root in its formula tree @@ -138,7 +154,11 @@ public: * @param formula The Not state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not* formula) = 0; + virtual mrmc::storage::BitVector* checkNot(mrmc::formula::Not& formula) { + mrmc::storage::BitVector* result = check(formula.getChild()); + result->complement(); + return result; + } /*! * The check method for a state formula with an Or node as root in its formula tree @@ -146,7 +166,13 @@ public: * @param formula The Or state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or* formula) = 0; + virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or& formula) { + mrmc::storage::BitVector* result = check(formula.getLeft()); + mrmc::storage::BitVector* right = check(formula.getRight()); + (*result) |= (*right); + delete right; + return result; + } /*! * The check method for a state formula with a probabilistic operator node as root in its formula tree @@ -154,7 +180,7 @@ public: * @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(mrmc::formula::ProbabilisticOperator* formula) = 0; + virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator& formula); /*! * The check method for a path formula; Will infer the actual type of formula and delegate it @@ -163,7 +189,7 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { + virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula& formula) { return formula->check(this); } @@ -173,7 +199,7 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil* formula) = 0; + virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil& formula) = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -181,7 +207,7 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkNext(mrmc::formula::Next* formula) = 0; + virtual std::vector checkNext(mrmc::formula::Next& formula) = 0; /*! * The check method for a path formula with an Until operator node as root in its formula tree @@ -189,7 +215,7 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector checkUntil(mrmc::formula::Until* formula) = 0; + virtual std::vector checkUntil(mrmc::formula::Until& formula) = 0; private: mrmc::models::Dtmc* dtmc; From bb9aa0dfe2fe9640663a14fcda451ea2ead44416 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 5 Dec 2012 15:30:11 +0100 Subject: [PATCH 2/3] Changed check function in formula classes to use a reference of the model checker instead of a pointer. --- src/formula/AP.h | 4 ++-- src/formula/And.h | 4 ++-- src/formula/BoundedUntil.h | 4 ++-- src/formula/Next.h | 4 ++-- src/formula/Not.h | 4 ++-- src/formula/Or.h | 4 ++-- src/formula/PCTLPathFormula.h | 2 +- src/formula/PCTLStateFormula.h | 2 +- src/formula/ProbabilisticOperator.h | 4 ++-- src/formula/Until.h | 4 ++-- 10 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/formula/AP.h b/src/formula/AP.h index 8c9f7ad16..3fa19a202 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -89,8 +89,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkAP(this); + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkAP(this); } private: diff --git a/src/formula/And.h b/src/formula/And.h index 12d8d38da..de6821b8d 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -141,8 +141,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkAnd(this); + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkAnd(this); } private: diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 9d7cf65f3..f6c6b6d93 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -167,8 +167,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkBoundedUntil(this); + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkBoundedUntil(this); } private: diff --git a/src/formula/Next.h b/src/formula/Next.h index 98f5d9533..d1647fee3 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -112,8 +112,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkNext(this); + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkNext(this); } private: diff --git a/src/formula/Not.h b/src/formula/Not.h index 09782530a..835c8844b 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -105,8 +105,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkNot(this); + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkNot(this); } private: diff --git a/src/formula/Or.h b/src/formula/Or.h index a5072b02a..a1e563e4f 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -140,8 +140,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkOr(this); + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkOr(this); } private: diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h index b795244e3..86812c902 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PCTLPathFormula.h @@ -55,7 +55,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; + virtual std::vector* check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h index daf369510..ac7c458eb 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PCTLStateFormula.h @@ -55,7 +55,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 622c2effc..9be1dbebe 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -151,8 +151,8 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkProbabilisticOperator(this); + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkProbabilisticOperator(this); } private: diff --git a/src/formula/Until.h b/src/formula/Until.h index be02eb5d9..86de81728 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -140,8 +140,8 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkUntil(this); + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + return modelChecker.checkUntil(this); } private: From 13a2bd30570e5b3d8981ff33c0017cb200db4bb0 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 5 Dec 2012 15:49:00 +0100 Subject: [PATCH 3/3] Moved const_templates.h from "misc" to "utility" to be able to remove the former folder. Also, changed those templates to use references instead of pointers for easier code. Renamer "utility.h" and .cpp to "ioUtility.h/cpp", as utility code providing functionality not linked with IO has been put into other files. --- src/formula/ProbabilisticOperator.h | 6 ++--- src/storage/SquareSparseMatrix.h | 6 ++--- src/{misc => utility}/const_templates.h | 31 ++++++++++------------ src/utility/{utility.cpp => ioUtility.cpp} | 4 +-- src/utility/{utility.h => ioUtility.h} | 2 +- test/parser/parse_dtmc_test.cpp | 2 +- test/parser/read_tra_file_test.cpp | 2 +- 7 files changed, 25 insertions(+), 28 deletions(-) rename src/{misc => utility}/const_templates.h (66%) rename src/utility/{utility.cpp => ioUtility.cpp} (97%) rename src/utility/{utility.h => ioUtility.h} (98%) diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 622c2effc..4b87ce869 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -10,7 +10,7 @@ #include "PCTLStateFormula.h" #include "PCTLPathFormula.h" -#include "misc/const_templates.h" +#include "utility/const_templates.h" namespace mrmc { @@ -40,8 +40,8 @@ public: * Empty constructor */ ProbabilisticOperator() { - upper = mrmc::misc::constGetZero(&upper); - lower = mrmc::misc::constGetZero(&lower); + upper = mrmc::utility::constGetZero(upper); + lower = mrmc::utility::constGetZero(lower); pathFormula = NULL; } diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index fd9c0b904..02cdec904 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -12,7 +12,7 @@ #include "src/exceptions/file_IO_exception.h" #include "src/storage/BitVector.h" -#include "src/misc/const_templates.h" +#include "src/utility/const_templates.h" #include "Eigen/Sparse" #include "gmm/gmm_matrix.h" @@ -658,12 +658,12 @@ public: uint_fast64_t rowEnd = rowIndications[row + 1]; while (rowStart < rowEnd) { - valueStorage[rowStart] = mrmc::misc::constGetZero(valueStorage); + valueStorage[rowStart] = mrmc::utility::constGetZero(valueStorage[rowStart]); ++rowStart; } // Set the element on the diagonal to one. - diagonalStorage[row] = mrmc::misc::constGetOne(diagonalStorage); + diagonalStorage[row] = mrmc::utility::constGetOne(diagonalStorage[row]); return true; } diff --git a/src/misc/const_templates.h b/src/utility/const_templates.h similarity index 66% rename from src/misc/const_templates.h rename to src/utility/const_templates.h index aeedf7632..0261cdecc 100644 --- a/src/misc/const_templates.h +++ b/src/utility/const_templates.h @@ -10,7 +10,7 @@ namespace mrmc { -namespace misc { +namespace utility { /*! * Returns a constant value of 0 that is fit to the type it is being written to. @@ -19,20 +19,19 @@ namespace misc { * * Parameter * - * The parameter is a pointer which is used to infer the return type (So, if you want - * the return value to be of type double, the parameter has to be of type double*). - * In most cases, it is a good choice to use the address of the variable that is to be - * set. + * The parameter is a reference which is used to infer the return type (So, if you want + * the return value to be of type double, the parameter has to be a double variable). + * In most cases, it is a good choice to use the the variable that is to be set. */ template -static inline _Scalar constGetZero(_Scalar*) { +static inline _Scalar constGetZero(_Scalar&) { return _Scalar(0); } /*! @cond TEMPLATE_SPECIALIZATION * (exclude the specializations from the documentation) */ template <> -inline int_fast32_t constGetZero(int_fast32_t*) { +inline int_fast32_t constGetZero(int_fast32_t&) { return 0; } @@ -40,7 +39,7 @@ inline int_fast32_t constGetZero(int_fast32_t*) { * Specialization of constGetZero for int_fast32_t */ template <> -inline double constGetZero(double*) { +inline double constGetZero(double&) { return 0.0; } /*! @endcond */ @@ -52,30 +51,28 @@ inline double constGetZero(double*) { * * Parameter * - * The parameter is a pointer which is used to infer the return type (So, if you want - * the return value to be of type double, the parameter has to be of type double*). - * In most cases, it is a good choice to use the address of the variable that is to be - * set. - */ + * The parameter is a reference which is used to infer the return type (So, if you want + * the return value to be of type double, the parameter has to be a double variable). + * In most cases, it is a good choice to use the the variable that is to be set. */ template -static inline _Scalar constGetOne(_Scalar*) { +static inline _Scalar constGetOne(_Scalar&) { return _Scalar(1); } /*! @cond TEMPLATE_SPECIALIZATION * (exclude the specializations from the documentation) */ template<> -inline int_fast32_t constGetOne(int_fast32_t*) { +inline int_fast32_t constGetOne(int_fast32_t&) { return 1; } template<> -inline double constGetOne(double*) { +inline double constGetOne(double&) { return 1.0; } /*! @endcond */ -} //namespace misc +} //namespace utility } //namespace mrmc diff --git a/src/utility/utility.cpp b/src/utility/ioUtility.cpp similarity index 97% rename from src/utility/utility.cpp rename to src/utility/ioUtility.cpp index e2ef43833..6a9a0808f 100644 --- a/src/utility/utility.cpp +++ b/src/utility/ioUtility.cpp @@ -1,11 +1,11 @@ /* - * utility.cpp + * ioUtility.cpp * * Created on: 17.10.2012 * Author: Thomas Heinemann */ -#include "src/utility/utility.h" +#include "src/utility/ioUtility.h" #include "src/parser/readTraFile.h" #include "src/parser/readLabFile.h" diff --git a/src/utility/utility.h b/src/utility/ioUtility.h similarity index 98% rename from src/utility/utility.h rename to src/utility/ioUtility.h index ebfa964b7..04a389a1d 100644 --- a/src/utility/utility.h +++ b/src/utility/ioUtility.h @@ -1,5 +1,5 @@ /* - * utility.h + * ioUtility.h * * Created on: 17.10.2012 * Author: Thomas Heinemann diff --git a/test/parser/parse_dtmc_test.cpp b/test/parser/parse_dtmc_test.cpp index e89ec331e..239ba735f 100644 --- a/test/parser/parse_dtmc_test.cpp +++ b/test/parser/parse_dtmc_test.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "mrmc-config.h" -#include "src/utility/utility.h" +#include "src/utility/ioUtility.h" TEST(ParseDtmcTest, parseAndOutput) { mrmc::models::Dtmc* myDtmc; diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp index d8cf64c8e..5e8e230f8 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/test/parser/read_tra_file_test.cpp @@ -12,7 +12,7 @@ #include "src/exceptions/file_IO_exception.h" #include "src/exceptions/wrong_file_format.h" -#include "src/utility/utility.h" +#include "src/utility/ioUtility.h" TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)