From cdc0332fd7a17ece0f6b3cf10021d4a6fed31d53 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 11:43:02 +0100 Subject: [PATCH] Code style and fixing errors in doxygen code for model checker class --- src/modelChecker/DtmcPrctlModelChecker.h | 278 +++++++++++------------ 1 file changed, 139 insertions(+), 139 deletions(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 979d8d93d..3061dc75b 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -54,145 +54,145 @@ namespace modelChecker { */ template class DtmcPrctlModelChecker { - public: - /*! - * Constructor - * - * @parameter Dtmc The dtmc model which is checked. - */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); - - /*! - * Copy constructor - * - * @parameter modelChecker The model checker that is copied. - */ - explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); - - /*! - * Destructor - */ - virtual ~DtmcPrctlModelChecker(); - - /*! - * @returns A reference to the dtmc of the model checker. - */ - mrmc::models::Dtmc* getDtmc() const { - return this->dtmc; - } - - /*! - * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all - * other edges from these states) - * - * @param states A bit vector representing a set of states that should become absorbing. - */ - virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; - - /*! - * Returns all states that are labeled with a given atomic proposition. - * - * @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; - - /*! - * Multiplies the matrix with a given vector; the result again is a vector. - * - * @param vector The vector to multiply the matrix with. - * @returns The result of multiplying the transition probability matrix with vector. - */ - virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; - - /*! - * The check method for a state formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @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) { - return formula->check(this); - } - - /*! - * The check method for a state formula with an And node as root in its formula tree - * - * @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; - - /*! - * The check method for a formula with an AP node as root in its formula tree - * - * @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*) = 0; - - /*! - * The check method for a formula with a Not node as root in its formula tree - * - * @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*) = 0; - - /*! - * The check method for a state formula with an Or node as root in its formula tree - * - * @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*) = 0; - - /*! - * 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(mrmc::formula::ProbabilisticOperator*) = 0; - - /*! - * The check method for a path formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @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) { - return formula->check(this); - } - - /*! - * The check method for a path formula with a Bounded Until operator node as root in its formula tree - * - * @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*) = 0; - - /*! - * The check method for a path formula with a Next operator node as root in its formula tree - * - * @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*) = 0; - - /*! - * The check method for a path formula with an Until operator node as root in its formula tree - * - * @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*) = 0; - - private: - mrmc::models::Dtmc* dtmc; +public: + /*! + * Constructor + * + * @param Dtmc The dtmc model which is checked. + */ + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); + + /*! + * Copy constructor + * + * @param modelChecker The model checker that is copied. + */ + explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); + + /*! + * Destructor + */ + virtual ~DtmcPrctlModelChecker(); + + /*! + * @returns A reference to the dtmc of the model checker. + */ + mrmc::models::Dtmc* getDtmc() const { + return this->dtmc; + } + + /*! + * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all + * other edges from these states) + * + * @param states A bit vector representing a set of states that should become absorbing. + */ + virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; + + /*! + * Returns all states that are labeled with a given atomic proposition. + * + * @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; + + /*! + * Multiplies the matrix with a given vector; the result again is a vector. + * + * @param vector The vector to multiply the matrix with. + * @returns The result of multiplying the transition probability matrix with vector. + */ + virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; + + /*! + * The check method for a state formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @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) { + return formula->check(this); + } + + /*! + * The check method for a state formula with an And node as root in its formula tree + * + * @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; + + /*! + * The check method for a formula with an AP node as root in its formula tree + * + * @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; + + /*! + * The check method for a formula with a Not node as root in its formula tree + * + * @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; + + /*! + * The check method for a state formula with an Or node as root in its formula tree + * + * @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; + + /*! + * 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(mrmc::formula::ProbabilisticOperator* formula) = 0; + + /*! + * The check method for a path formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @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) { + return formula->check(this); + } + + /*! + * The check method for a path formula with a Bounded Until operator node as root in its formula tree + * + * @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; + + /*! + * The check method for a path formula with a Next operator node as root in its formula tree + * + * @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; + + /*! + * The check method for a path formula with an Until operator node as root in its formula tree + * + * @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; + +private: + mrmc::models::Dtmc* dtmc; }; } //namespace modelChecker