From 67b3888ba9423cf536b5afc5345a9c898e3f7b5c Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 5 Dec 2012 15:24:11 +0100 Subject: [PATCH 1/2] 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/2] 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: