From bb9aa0dfe2fe9640663a14fcda451ea2ead44416 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 5 Dec 2012 15:30:11 +0100 Subject: [PATCH] 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: