sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added a lot of consts to all methods provided by formula classes.

main
dehnert 13 years ago
parent
223f5a5c60
commit
091a7740a2
11 changed files with 44 additions and 44 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/formula/AP.h
  2. 10
      src/formula/And.h
  3. 12
      src/formula/BoundedUntil.h
  4. 8
      src/formula/Next.h
  5. 8
      src/formula/Not.h
  6. 10
      src/formula/Or.h
  7. 4
      src/formula/PCTLPathFormula.h
  8. 4
      src/formula/PCTLStateFormula.h
  9. 2
      src/formula/PCTLformula.h
  10. 12
      src/formula/ProbabilisticOperator.h
  11. 10
      src/formula/Until.h

8
src/formula/AP.h
View File

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

10
src/formula/And.h
View File

@ -91,21 +91,21 @@ public:
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>& getLeft() {
const PCTLStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>& getRight() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLStateFormula<T>* clone() const {
And<T>* 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<T>& modelChecker) {
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkAnd(this);
}

12
src/formula/BoundedUntil.h
View File

@ -97,21 +97,21 @@ public:
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>& getLeft() {
const PCTLStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>& getRight() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLPathFormula<T>* clone() const {
BoundedUntil<T>* 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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedUntil(this);
}

8
src/formula/Next.h
View File

@ -65,7 +65,7 @@ public:
/*!
* @returns the child node
*/
PCTLStateFormula<T>& getChild() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkNext(this);
}

8
src/formula/Not.h
View File

@ -60,7 +60,7 @@ public:
/*!
* @returns The child node
*/
PCTLStateFormula<T>& getChild() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
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<T>& modelChecker) {
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkNot(this);
}

10
src/formula/Or.h
View File

@ -90,21 +90,21 @@ public:
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>& getLeft() {
const PCTLStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>& getRight() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLStateFormula<T>* clone() const {
Or<T>* 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<T>& modelChecker) {
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkOr(this);
}

4
src/formula/PCTLPathFormula.h
View File

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

4
src/formula/PCTLStateFormula.h
View File

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

2
src/formula/PCTLformula.h
View File

@ -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

12
src/formula/ProbabilisticOperator.h
View File

@ -73,21 +73,21 @@ public:
/*!
* @returns the child node (representation of a PCTL path formula)
*/
PCTLPathFormula<T>& getPathFormula () {
const PCTLPathFormula<T>& 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<T>* clone() {
virtual PCTLStateFormula<T>* clone() const {
ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
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<T>& modelChecker) {
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkProbabilisticOperator(this);
}

10
src/formula/Until.h
View File

@ -90,21 +90,21 @@ public:
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>& getLeft() {
const PCTLStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>& getRight() {
const PCTLStateFormula<T>& 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<T>* clone() {
virtual PCTLPathFormula<T>* clone() const {
Until<T>* 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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkUntil(this);
}

Write Preview
Loading…
Cancel
Save