From 091a7740a281970166dcd5eaea994b6ef812710c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 6 Dec 2012 18:01:13 +0100 Subject: [PATCH 1/5] Added a lot of consts to all methods provided by formula classes. --- src/formula/AP.h | 8 ++++---- src/formula/And.h | 10 +++++----- src/formula/BoundedUntil.h | 12 ++++++------ src/formula/Next.h | 8 ++++---- src/formula/Not.h | 8 ++++---- src/formula/Or.h | 10 +++++----- src/formula/PCTLPathFormula.h | 4 ++-- src/formula/PCTLStateFormula.h | 4 ++-- src/formula/PCTLformula.h | 2 +- src/formula/ProbabilisticOperator.h | 12 ++++++------ src/formula/Until.h | 10 +++++----- 11 files changed, 44 insertions(+), 44 deletions(-) diff --git a/src/formula/AP.h b/src/formula/AP.h index 3fa19a202..4b7d18011 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -59,7 +59,7 @@ public: /*! * @returns the name of the atomic proposition */ - const std::string& getAP() { + const std::string& getAP() const { return ap; } @@ -67,7 +67,7 @@ public: * @returns a string representation of the leaf. * */ - virtual std::string toString() { + virtual std::string toString() const { return getAP(); } @@ -76,7 +76,7 @@ public: * * @returns a new AP-object that is identical the called object. */ - virtual PCTLStateFormula* clone() { + virtual PCTLStateFormula* clone() const { return new AP(ap); } @@ -89,7 +89,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) { + virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkAP(this); } diff --git a/src/formula/And.h b/src/formula/And.h index de6821b8d..742633f3b 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -91,21 +91,21 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula& getLeft() { + const PCTLStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula& getRight() { + const PCTLStateFormula& getRight() const { return *right; } /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += left->toString(); result += " && "; @@ -121,7 +121,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() { + virtual PCTLStateFormula* clone() const { And* result = new And(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -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(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkAnd(this); } diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index f6c6b6d93..93355b7f3 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -97,21 +97,21 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula& getLeft() { + const PCTLStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula& getRight() { + const PCTLStateFormula& getRight() const { return *right; } /*! * @returns the maximally allowed number of steps for the bounded until operator */ - uint_fast64_t getBound() { + uint_fast64_t getBound() const { return bound; } @@ -127,7 +127,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += left->toString(); result += " U<="; @@ -145,7 +145,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() { + virtual PCTLPathFormula* clone() const { BoundedUntil* result = new BoundedUntil(); result->setBound(bound); if (left != NULL) { @@ -167,7 +167,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkBoundedUntil(this); } diff --git a/src/formula/Next.h b/src/formula/Next.h index d1647fee3..1a5acb1ec 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -65,7 +65,7 @@ public: /*! * @returns the child node */ - PCTLStateFormula& getChild() { + const PCTLStateFormula& getChild() const { return *child; } @@ -80,7 +80,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += " X "; result += child->toString(); @@ -95,7 +95,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() { + virtual PCTLPathFormula* clone() const { Next* result = new Next(); if (child != NULL) { result->setChild(child); @@ -112,7 +112,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkNext(this); } diff --git a/src/formula/Not.h b/src/formula/Not.h index 835c8844b..c816a827b 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -60,7 +60,7 @@ public: /*! * @returns The child node */ - PCTLStateFormula& getChild() { + const PCTLStateFormula& getChild() const { return *child; } @@ -75,7 +75,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "!"; result += child->toString(); return result; @@ -88,7 +88,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() { + virtual PCTLStateFormula* clone() const { Not* result = new Not(); if (child != NULL) { result->setChild(child); @@ -105,7 +105,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) { + virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkNot(this); } diff --git a/src/formula/Or.h b/src/formula/Or.h index a1e563e4f..78185b0d5 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -90,21 +90,21 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula& getLeft() { + const PCTLStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula& getRight() { + const PCTLStateFormula& getRight() const { return *right; } /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += left->toString(); result += " || "; @@ -120,7 +120,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() { + virtual PCTLStateFormula* clone() const { Or* result = new Or(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -140,7 +140,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) { + virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkOr(this); } diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h index 86812c902..a70a35f53 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PCTLPathFormula.h @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLPathFormula* clone() = 0; + virtual PCTLPathFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -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(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; }; } //namespace formula diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h index ac7c458eb..a8ca831c3 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PCTLStateFormula.h @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() = 0; + virtual PCTLStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -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(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; }; } //namespace formula diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h index b1e7bf0b9..add5c5198 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PCTLformula.h @@ -38,7 +38,7 @@ public: * @note This function is not implemented in this class. * @returns a string representation of the formula */ - virtual std::string toString() = 0; + virtual std::string toString() const = 0; }; } //namespace formula diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index e974feaaf..49e6530de 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -73,21 +73,21 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - PCTLPathFormula& getPathFormula () { + const PCTLPathFormula& getPathFormula () const { return *pathFormula; } /*! * @returns the lower bound for the probability */ - const T& getLowerBound() { + const T& getLowerBound() const { return lower; } /*! * @returns the upper bound for the probability */ - const T& getUpperBound() { + const T& getUpperBound() const { return upper; } @@ -114,7 +114,7 @@ public: /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += " P["; result += lower; @@ -133,7 +133,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() { + virtual PCTLStateFormula* clone() const { ProbabilisticOperator* result = new ProbabilisticOperator(); result->setInterval(lower, upper); if (pathFormula != NULL) { @@ -151,7 +151,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) { + virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkProbabilisticOperator(this); } diff --git a/src/formula/Until.h b/src/formula/Until.h index 86de81728..f6bf62a98 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -90,21 +90,21 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula& getLeft() { + const PCTLStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula& getRight() { + const PCTLStateFormula& getRight() const { return *right; } /*! * @returns a string representation of the formula */ - virtual std::string toString() { + virtual std::string toString() const { std::string result = "("; result += left->toString(); result += " U "; @@ -120,7 +120,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() { + virtual PCTLPathFormula* clone() const { Until* result = new Until(); if (left != NULL) { result->setLeft(left->clone()); @@ -140,7 +140,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) { + virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkUntil(this); } From 27ba61ff748eeb82775f0b13c71345d7e1753a37 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 6 Dec 2012 20:03:12 +0100 Subject: [PATCH 2/5] Fixed minor bugs here and there. Improved gmm++-based model checker. --- src/formula/AP.h | 14 +-- src/formula/Formulas.h | 23 +++++ src/formula/Until.h | 2 +- src/modelChecker/DtmcPrctlModelChecker.h | 39 ++++---- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 95 +++++++++++-------- src/mrmc.cpp | 12 +++ src/storage/SquareSparseMatrix.h | 17 ++-- src/utility/vector.h | 12 +-- 8 files changed, 132 insertions(+), 82 deletions(-) create mode 100644 src/formula/Formulas.h diff --git a/src/formula/AP.h b/src/formula/AP.h index 4b7d18011..990365ff0 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -38,18 +38,6 @@ public: this->ap = ap; } - /*! - * Constructor - * - * Creates a new atomic proposition leaf, with the label AP - * - * @param ap The string representing the atomic proposition - */ - AP(char* ap) { - //TODO: Does that really work? - this->ap = ap; - } - /*! * Destructor. * At this time, empty... @@ -90,7 +78,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.checkAP(this); + return modelChecker.checkAP(*this); } private: diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h new file mode 100644 index 000000000..58b679d8b --- /dev/null +++ b/src/formula/Formulas.h @@ -0,0 +1,23 @@ +/* + * Formulas.h + * + * Created on: 06.12.2012 + * Author: chris + */ + +#ifndef FORMULAS_H_ +#define FORMULAS_H_ + +#include "And.h" +#include "AP.h" +#include "BoundedUntil.h" +#include "Next.h" +#include "Not.h" +#include "Or.h" +#include "PCTLformula.h" +#include "PCTLPathFormula.h" +#include "PCTLStateFormula.h" +#include "ProbabilisticOperator.h" +#include "Until.h" + +#endif /* FORMULAS_H_ */ diff --git a/src/formula/Until.h b/src/formula/Until.h index f6bf62a98..1b492e68b 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -141,7 +141,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.checkUntil(this); + return modelChecker.checkUntil(*this); } private: diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 83e29e38b..7923f592d 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -103,8 +103,8 @@ 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) { - return formula.check(this); + virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { + return formula.check(*this); } /*! @@ -113,9 +113,9 @@ 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) { - mrmc::storage::BitVector* result = check(formula.getLeft()); - mrmc::storage::BitVector* right = check(formula.getRight()); + virtual 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); delete right; return result; @@ -127,7 +127,12 @@ 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) { + virtual 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) { + return new mrmc::storage::BitVector(model->getNumberOfStates()); + } return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP())); } @@ -137,8 +142,8 @@ 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) { - mrmc::storage::BitVector* result = check(formula.getChild()); + virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) const { + mrmc::storage::BitVector* result = checkStateFormula(formula.getChild()); result->complement(); return result; } @@ -149,9 +154,9 @@ 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) { - mrmc::storage::BitVector* result = check(formula.getLeft()); - mrmc::storage::BitVector* right = check(formula.getRight()); + virtual 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); delete right; return result; @@ -163,7 +168,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(const mrmc::formula::ProbabilisticOperator& formula); + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const = 0; /*! * The check method for a path formula; Will infer the actual type of formula and delegate it @@ -172,8 +177,8 @@ 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) { - return formula.check(this); + virtual std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { + return formula.check(*this); } /*! @@ -182,7 +187,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) = 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 @@ -190,7 +195,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) = 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 @@ -198,7 +203,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(const mrmc::formula::Until& formula) = 0; + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; private: mrmc::models::Dtmc* model; diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 0493cda1a..9d9c0aad2 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -11,6 +11,7 @@ #include "src/utility/vector.h" #include "src/models/dtmc.h" +#include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "gmm/gmm_matrix.h" @@ -19,7 +20,7 @@ #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" -log4cplus::Logger logger; +extern log4cplus::Logger logger; namespace mrmc { @@ -28,31 +29,46 @@ namespace modelChecker { /* * A model checking engine that makes use of the gmm++ backend. */ -template -class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { +template +class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(const mrmc::models::Dtmc* dtmc) : DtmcPrctlModelChecker(dtmc) { } + explicit GmmxxDtmcPrctlModelChecker(mrmc::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(mrmc::formula::BoundedUntil& formula) { + 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 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->check(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + 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(dtmc.getTransitionProbabilityMatrix()); + 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); + tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); // Create the vector with which to multiply. - std::vector* result = new st::vector(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValue(result, *rightStates, 1); + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { @@ -66,22 +82,22 @@ public: return result; } - virtual std::vector* checkNext(const mrmc::formula::Next& formula) { + 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->check(formula.getChild()); + mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = dtmc.getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); // Create the vector with which to multiply and initialize it correctly. - std::vector x(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValue(x, nextStates, 1); + std::vector x(this->getModel().getNumberOfStates()); + mrmc::utility::setVectorValues(&x, *nextStates, static_cast(1.0)); // Delete not needed next states bit vector. delete nextStates; // Create resulting vector. - std::vector* result = new std::vector(dtmc.getNumberOfStates()); + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Perform the actual computation. gmm::mult(*gmmxxMatrix, x, *result); @@ -91,17 +107,17 @@ public: return result; } - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) { + 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->check(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + 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(dtmc.getNumberOfStates()); - mrmc::storage::BitVector alwaysPhiUntilPsiStates(dtmc.getNumberOfStates()); - mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(dtmc, *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); - notExistsPhiUntilPsiStates->complement(); + 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; @@ -109,12 +125,15 @@ public: 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."); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector and set values accordingly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Only try to solve system if there are states for which the probability is unknown. if (maybeStates.getNumberOfSetBits() > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. - mrmc::storage::SquareSparseMatrix* submatrix = dtmc.getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + 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(); @@ -125,12 +144,12 @@ public: // 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 = new std::vector(maybeStates.getNumberOfSetBits(), 0.5); + std::vector x(maybeStates.getNumberOfSetBits(), Type(0.5)); // 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()); - dtmc.getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); // Set up the precondition of the iterative solver. gmm::ilu_precond> P(*gmmxxMatrix); @@ -139,24 +158,26 @@ public: gmm::iteration iter(0.000001); // Now do the actual solving. - LOG4CPLUS_INFO(logger, "Starting iterations..."); + LOG4CPLUS_INFO(logger, "Starting iterative solver."); gmm::bicgstab(*gmmxxMatrix, x, b, P, iter); - LOG4CPLUS_INFO(logger, "Done with iterations."); + LOG4CPLUS_INFO(logger, "Iterative solver converged."); - // Create resulting vector and set values accordingly. - std::vector* result = new std::vector(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValues>(result, maybeStates, x); + // Set values of resulting vector according to result. + mrmc::utility::setVectorValues(result, maybeStates, x); - // Delete temporary matrix and return result. - delete x; + // Delete temporary matrix. delete gmmxxMatrix; } - mrmc::utility::setVectorValue>(result, notExistsPhiUntilPsiStates, 0); - mrmc::utility::setVectorValue>(result, alwaysPhiUntilPsiStates, 1); + mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, static_cast(0)); + mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, static_cast(1.0)); return result; } }; +} //namespace modelChecker + +} //namespace mrmc + #endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index baa2f20d5..a63ea0f4e 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -21,11 +21,13 @@ #include "src/models/Dtmc.h" #include "src/storage/SquareSparseMatrix.h" #include "src/models/AtomicPropositionsLabeling.h" +#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/readLabFile.h" #include "src/parser/readTraFile.h" #include "src/parser/readPrctlFile.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" +#include "src/formula/Formulas.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -102,6 +104,16 @@ 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::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); + delete until; + */ + if (s != nullptr) { delete s; } diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index a81302b1c..4e433816a 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -71,8 +71,8 @@ public: * @param ssm A reference to the matrix to be copied. */ SquareSparseMatrix(const SquareSparseMatrix &ssm) - : internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow), - rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount) { + : rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount), + internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) { LOG4CPLUS_WARN(logger, "Invoking copy constructor."); // Check whether copying the matrix is safe. if (!ssm.hasError()) { @@ -454,7 +454,7 @@ public: * Checks whether the internal state of the matrix signals an error. * @return True iff the internal state of the matrix signals an error. */ - bool hasError() { + bool hasError() const { return (internalStatus == MatrixStatus::Error); } @@ -663,15 +663,16 @@ public: /*! * This function makes the rows given by the bit vector absorbing. + * @param rows A bit vector indicating which rows to make absorbing. + * @return True iff the operation was successful. */ bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) { + bool result = true; for (auto row : rows) { - makeRowAbsorbing(row); + 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; } /*! @@ -733,7 +734,7 @@ public: void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector* resultVector) { uint_fast64_t currentRowCount = 0; for (auto row : rowConstraint) { - resultVector[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); + (*resultVector)[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index 393151745..eff5f02b9 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -12,18 +12,18 @@ namespace mrmc { namespace utility { -template -void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, std::vector* values) { +template +void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, const std::vector values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { - vector[position] = values[oldPosition++]; + (*vector)[position] = values[oldPosition++]; } } -template -void setVectorValue(std::vector* vector, const mrmc::storage::BitVector& positions, T value) { +template +void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, T value) { for (auto position : positions) { - vector[position] = value; + (*vector)[position] = value; } } From 54e52b5ab7f9300e18eb3807ba3e7bd1c98a0f0c Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 6 Dec 2012 20:10:02 +0100 Subject: [PATCH 3/5] dtmc.h -> Dtmc.h --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 9d9c0aad2..696a86c1e 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -10,7 +10,7 @@ #include "src/utility/vector.h" -#include "src/models/dtmc.h" +#include "src/models/Dtmc.h" #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" From 8cbb7aa7d70a7fe0b499dbe2ca2c3b1dbb32d727 Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 6 Dec 2012 21:37:56 +0100 Subject: [PATCH 4/5] fixing toEigen conversion, making test case working :-) --- src/storage/SquareSparseMatrix.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 4e433816a..5f322de01 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -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(i, i, diagonalStorage[i])); } // Let Eigen create a matrix from the given list of triplets. From 4095e87282393e302b7e01238ca3ae39bae73288 Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 6 Dec 2012 21:39:00 +0100 Subject: [PATCH 5/5] changing pointer to std::shared_ptr parsers return some kind of object and it is not clear who owns this object, i.e. who is responsible to delete it. --- src/models/Dtmc.h | 19 ++++++------------- src/models/GraphTransitions.h | 7 ++++--- src/parser/readLabFile.cpp | 2 +- src/parser/readLabFile.h | 6 ++++-- src/parser/readTraFile.cpp | 2 +- src/parser/readTraFile.h | 6 ++++-- src/utility/ioUtility.cpp | 2 +- test/parser/read_lab_file_test.cpp | 7 ++++--- test/parser/read_tra_file_test.cpp | 4 +--- 9 files changed, 26 insertions(+), 29 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 8ac46ffee..83bba3d6e 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -9,6 +9,7 @@ #define DTMC_H_ #include +#include #include "AtomicPropositionsLabeling.h" #include "GraphTransitions.h" @@ -35,10 +36,8 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Dtmc(mrmc::storage::SquareSparseMatrix* probabilityMatrix, mrmc::models::AtomicPropositionsLabeling* stateLabeling) - : backwardTransitions(nullptr) { - this->probabilityMatrix = probabilityMatrix; - this->stateLabeling = stateLabeling; + Dtmc(std::shared_ptr> probabilityMatrix, std::shared_ptr stateLabeling) + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), backwardTransitions(nullptr) { } //! Copy Constructor @@ -58,12 +57,6 @@ public: * Destructor. Frees the matrix and labeling associated with this DTMC. */ ~Dtmc() { - if (this->probabilityMatrix != nullptr) { - delete this->probabilityMatrix; - } - if (this->stateLabeling != nullptr) { - delete this->stateLabeling; - } if (this->backwardTransitions != nullptr) { delete this->backwardTransitions; } @@ -102,7 +95,7 @@ public: * @return A pointer to the matrix representing the transition probability * function. */ - mrmc::storage::SquareSparseMatrix* getTransitionProbabilityMatrix() const { + std::shared_ptr> getTransitionProbabilityMatrix() const { return this->probabilityMatrix; } @@ -146,10 +139,10 @@ public: private: /*! A matrix representing the transition probability function of the DTMC. */ - mrmc::storage::SquareSparseMatrix* probabilityMatrix; + std::shared_ptr> probabilityMatrix; /*! The labeling of the states of the DTMC. */ - mrmc::models::AtomicPropositionsLabeling* stateLabeling; + std::shared_ptr stateLabeling; /*! * A data structure that stores the predecessors for all states. This is diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 7b60e92f3..4563bfc59 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -11,6 +11,7 @@ #include "src/storage/SquareSparseMatrix.h" #include +#include namespace mrmc { @@ -38,7 +39,7 @@ public: * @param forward If set to true, this objects will store the graph structure * of the backwards transition relation. */ - GraphTransitions(mrmc::storage::SquareSparseMatrix* transitionMatrix, bool forward) + GraphTransitions(std::shared_ptr> transitionMatrix, bool forward) : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { if (forward) { this->initializeForward(transitionMatrix); @@ -86,7 +87,7 @@ private: * Initializes this graph transitions object using the forward transition * relation given by means of a sparse matrix. */ - void initializeForward(mrmc::storage::SquareSparseMatrix* transitionMatrix) { + void initializeForward(std::shared_ptr> transitionMatrix) { this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; this->stateIndications = new uint_fast64_t[numberOfStates + 1]; @@ -108,7 +109,7 @@ private: * relation, whose forward transition relation is given by means of a sparse * matrix. */ - void initializeBackward(mrmc::storage::SquareSparseMatrix* transitionMatrix) { + void initializeBackward(std::shared_ptr> transitionMatrix) { this->successorList = new uint_fast64_t[numberOfNonZeroTransitions](); this->stateIndications = new uint_fast64_t[numberOfStates + 1](); diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index ebcacd099..42a7566e2 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -106,7 +106,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) /* * create labeling object with given node and proposition count */ - this->labeling = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count); + this->labeling = std::shared_ptr(new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count)); /* * second run: add propositions and node labels to labeling diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h index 67aec1178..5aa142d4d 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/readLabFile.h @@ -6,6 +6,8 @@ #include "src/parser/parser.h" +#include + namespace mrmc { namespace parser { @@ -20,13 +22,13 @@ class LabParser : Parser public: LabParser(uint_fast64_t node_count, const char* filename); - mrmc::models::AtomicPropositionsLabeling* getLabeling() + std::shared_ptr getLabeling() { return this->labeling; } private: - mrmc::models::AtomicPropositionsLabeling* labeling; + std::shared_ptr labeling; }; } // namespace parser diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp index 0871bfebd..6a73bff0a 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/readTraFile.cpp @@ -166,7 +166,7 @@ TraParser::TraParser(const char * filename) * non-zero elements has to be specified (which is non_zero, computed by make_first_pass) */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); - this->matrix = new mrmc::storage::SquareSparseMatrix(maxnode + 1); + this->matrix = std::shared_ptr>(new mrmc::storage::SquareSparseMatrix(maxnode + 1)); if (this->matrix == NULL) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h index 7ec735123..c46167e37 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/readTraFile.h @@ -5,6 +5,8 @@ #include "src/parser/parser.h" +#include + namespace mrmc { namespace parser { @@ -20,13 +22,13 @@ class TraParser : Parser public: TraParser(const char* filename); - mrmc::storage::SquareSparseMatrix* getMatrix() + std::shared_ptr> getMatrix() { return this->matrix; } private: - mrmc::storage::SquareSparseMatrix* matrix; + std::shared_ptr> matrix; uint_fast32_t firstPass(char* buf, uint_fast32_t &maxnode); diff --git a/src/utility/ioUtility.cpp b/src/utility/ioUtility.cpp index 6a9a0808f..01872a3c9 100644 --- a/src/utility/ioUtility.cpp +++ b/src/utility/ioUtility.cpp @@ -16,7 +16,7 @@ namespace mrmc { namespace utility { void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { - mrmc::storage::SquareSparseMatrix* matrix = dtmc->getTransitionProbabilityMatrix(); + std::shared_ptr> matrix(dtmc->getTransitionProbabilityMatrix()); double* diagonal_storage = matrix->getDiagonalStoragePointer(); std::ofstream file; diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp index 8a14c872a..24eb98356 100644 --- a/test/parser/read_lab_file_test.cpp +++ b/test/parser/read_lab_file_test.cpp @@ -12,6 +12,8 @@ #include "src/exceptions/file_IO_exception.h" #include "src/exceptions/wrong_file_format.h" +#include + TEST(ReadLabFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception); @@ -19,12 +21,12 @@ TEST(ReadLabFileTest, NonExistingFileTest) { TEST(ReadLabFileTest, ParseTest) { //This test is based on a test case from the original MRMC. - mrmc::models::AtomicPropositionsLabeling* labeling = NULL; + mrmc::parser::LabParser* parser; //Parsing the file ASSERT_NO_THROW(parser = new mrmc::parser::LabParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); - labeling = parser->getLabeling(); + std::shared_ptr labeling(parser->getLabeling()); //Checking whether all propositions are in the labelling @@ -77,7 +79,6 @@ TEST(ReadLabFileTest, ParseTest) { ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,11)); //Deleting the labeling - delete labeling; delete parser; } else { FAIL(); diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp index 5e8e230f8..509ea79d8 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/test/parser/read_tra_file_test.cpp @@ -22,10 +22,9 @@ TEST(ReadTraFileTest, NonExistingFileTest) { /* The following test case is based on one of the original MRMC test cases */ TEST(ReadTraFileTest, ParseFileTest1) { - mrmc::storage::SquareSparseMatrix *result = NULL; mrmc::parser::TraParser* parser; ASSERT_NO_THROW(parser = new mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra")); - result = parser->getMatrix(); + std::shared_ptr> result = parser->getMatrix(); if (result != NULL) { double val = 0; @@ -63,7 +62,6 @@ TEST(ReadTraFileTest, ParseFileTest1) { ASSERT_TRUE(result->getValue(4,4,&val)); ASSERT_EQ(val,0); - delete result; delete parser; } else { FAIL();