Browse Source

Changed check function in formula classes to use a reference of the

model checker instead of a pointer.
tempestpy_adaptions
Lanchid 12 years ago
parent
commit
bb9aa0dfe2
  1. 4
      src/formula/AP.h
  2. 4
      src/formula/And.h
  3. 4
      src/formula/BoundedUntil.h
  4. 4
      src/formula/Next.h
  5. 4
      src/formula/Not.h
  6. 4
      src/formula/Or.h
  7. 2
      src/formula/PCTLPathFormula.h
  8. 2
      src/formula/PCTLStateFormula.h
  9. 4
      src/formula/ProbabilisticOperator.h
  10. 4
      src/formula/Until.h

4
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<T>* modelChecker) {
return modelChecker->checkAP(this);
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkAP(this);
}
private:

4
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<T>* modelChecker) {
return modelChecker->checkAnd(this);
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkAnd(this);
}
private:

4
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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
return modelChecker->checkBoundedUntil(this);
virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkBoundedUntil(this);
}
private:

4
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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
return modelChecker->checkNext(this);
virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkNext(this);
}
private:

4
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<T>* modelChecker) {
return modelChecker->checkNot(this);
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkNot(this);
}
private:

4
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<T>* modelChecker) {
return modelChecker->checkOr(this);
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkOr(this);
}
private:

2
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<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
};
} //namespace formula

2
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<T>* modelChecker) = 0;
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
};
} //namespace formula

4
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<T>* modelChecker) {
return modelChecker->checkProbabilisticOperator(this);
virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkProbabilisticOperator(this);
}
private:

4
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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
return modelChecker->checkUntil(this);
virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
return modelChecker.checkUntil(this);
}
private:

Loading…
Cancel
Save