From bc698ffd202f8942a9e6f3c4d22cbe60d6bb487b Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 12 Dec 2012 15:55:14 +0100 Subject: [PATCH] Implemented probabilistic operator without specified bounds, including check method in the model checker. Also, the check methods for other the probabilistic operators are now in the base class (as they do not depend on the library). --- src/formula/Formulas.h | 1 + src/formula/ProbabilisticIntervalOperator.h | 1 + src/formula/ProbabilisticOperator.h | 3 +- src/modelChecker/DtmcPrctlModelChecker.h | 80 ++++++++++++++----- src/modelChecker/EigenDtmcPrctlModelChecker.h | 29 ------- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 20 ----- 6 files changed, 63 insertions(+), 71 deletions(-) diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index d37972987..5b8b4bffc 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 "ProbabilisticNoBoundsOperator.h" #include "ProbabilisticIntervalOperator.h" #include "Until.h" diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h index 8b50da26d..f61ec8af3 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -38,6 +38,7 @@ namespace formula { * @see PCTLStateFormula * @see PCTLPathFormula * @see ProbabilisticOperator + * @see ProbabilisticNoBoundsOperator * @see PCTLFormula */ template diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 43962d6d4..f1f6df24f 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -34,7 +34,8 @@ namespace formula { * * @see PCTLStateFormula * @see PCTLPathFormula - * @see ProbabilisticOperator + * @see ProbabilisticIntervalOperator + * @see ProbabilisticNoBoundsOperator * @see PCTLFormula */ template diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index ba1b098c0..fef616231 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -17,7 +17,7 @@ namespace modelChecker { * so the model checker class is declared here already. * */ -template +template class DtmcPrctlModelChecker; } @@ -45,7 +45,7 @@ namespace modelChecker { * * @attention This class is abstract. */ -template +template class DtmcPrctlModelChecker { public: /*! @@ -53,7 +53,7 @@ public: * * @param model The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) { + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) { this->model = &model; } @@ -62,8 +62,8 @@ public: * * @param modelChecker The model checker that is copied. */ - explicit DtmcPrctlModelChecker(const mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - this->model = new mrmc::models::Dtmc(modelChecker->getModel()); + explicit DtmcPrctlModelChecker(const mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + this->model = new mrmc::models::Dtmc(modelChecker->getModel()); } /*! @@ -77,7 +77,7 @@ public: /*! * @returns A reference to the dtmc of the model checker. */ - mrmc::models::Dtmc& getModel() const { + mrmc::models::Dtmc& getModel() const { return *(this->model); } @@ -85,7 +85,7 @@ public: * Sets the DTMC model which is checked * @param model */ - void setModel(mrmc::models::Dtmc& model) { + void setModel(mrmc::models::Dtmc& model) { this->model = &model; } @@ -96,7 +96,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { + mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { return formula.check(*this); } @@ -106,7 +106,7 @@ 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(const mrmc::formula::And& formula) const { + mrmc::storage::BitVector* checkAnd(const mrmc::formula::And& formula) const { mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) &= (*right); @@ -120,7 +120,7 @@ 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(const mrmc::formula::AP& formula) const { + mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) const { if (formula.getAP().compare("true") == 0) { return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); } else if (formula.getAP().compare("false") == 0) { @@ -135,7 +135,7 @@ 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(const mrmc::formula::Not& formula) const { + mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) const { mrmc::storage::BitVector* result = checkStateFormula(formula.getChild()); result->complement(); return result; @@ -147,7 +147,7 @@ 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(const mrmc::formula::Or& formula) const { + mrmc::storage::BitVector* checkOr(const mrmc::formula::Or& formula) const { mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) |= (*right); @@ -162,8 +162,20 @@ 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( - const mrmc::formula::ProbabilisticOperator& formula) const = 0; + 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; + } /*! * The check method for a state formula with a probabilistic interval operator node as root in @@ -172,8 +184,34 @@ 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* checkProbabilisticIntervalOperator( - const mrmc::formula::ProbabilisticIntervalOperator& formula) const = 0; + 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; + } + + + /*! + * The check method for a state formula with a probabilistic operator node without bounds 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 + */ + std::vector* checkProbabilisticOperator( + const mrmc::formula::ProbabilisticNoBoundsOperator& formula) const { + return formula.getPathFormula().check(this); + } /*! * The check method for a path formula; Will infer the actual type of formula and delegate it @@ -182,7 +220,7 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { + std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { return formula.check(*this); } @@ -192,7 +230,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(const mrmc::formula::BoundedUntil& formula) const = 0; + virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -200,7 +238,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(const mrmc::formula::Next& formula) const = 0; + virtual std::vector* checkNext(const mrmc::formula::Next& formula) const = 0; /*! * The check method for a path formula with an Until operator node as root in its formula tree @@ -208,10 +246,10 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; private: - mrmc::models::Dtmc* model; + mrmc::models::Dtmc* model; }; } //namespace modelChecker diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index deaebb9ef..7be98d772 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -42,35 +42,6 @@ public: 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()); diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 488b03c00..29057d95a 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -37,26 +37,6 @@ public: virtual ~GmmxxDtmcPrctlModelChecker() { } - 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()); - 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());