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

Code style for formula classes

tempestpy_adaptions
Lanchid 12 years ago
parent
79761d0492
commit
350f1a0990
11 changed files with 914 additions and 893 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. 138
      src/formula/AP.h
  2. 229
      src/formula/And.h
  3. 275
      src/formula/BoundedUntil.h
  4. 170
      src/formula/Next.h
  5. 164
      src/formula/Not.h
  6. 230
      src/formula/Or.h
  7. 53
      src/formula/PCTLPathFormula.h
  8. 53
      src/formula/PCTLStateFormula.h
  9. 23
      src/formula/PCTLformula.h
  10. 247
      src/formula/ProbabilisticOperator.h
  11. 225
      src/formula/Until.h

138
src/formula/AP.h
View File

@ -25,74 +25,76 @@ namespace formula {
*/
template <class T>
class AP : public PCTLStateFormula<T> {
private:
std::string ap;
public:
/*!
* Constructor
*
* Creates a new atomic proposition leaf, with the label AP
*
* @param ap The string representing the atomic proposition
*/
AP(std::string ap) {
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...
*/
virtual ~AP() { }
/*!
* @returns the name of the atomic proposition
*/
std::string getAP() {
return ap;
}
/*!
* @returns a string representation of the leaf.
*
*/
virtual std::string toString() {
return getAP();
}
/*!
* Clones the called object.
*
* @returns a new AP-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
return new AP(ap);
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Constructor
*
* Creates a new atomic proposition leaf, with the label AP
*
* @param ap The string representing the atomic proposition
*/
AP(std::string ap) {
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...
*/
virtual ~AP() { }
/*!
* @returns the name of the atomic proposition
*/
std::string getAP() {
return ap;
}
/*!
* @returns a string representation of the leaf.
*
*/
virtual std::string toString() {
return getAP();
}
/*!
* Clones the called object.
*
* @returns a new AP-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
return new AP(ap);
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
std::string ap;
};
} //namespace formula

229
src/formula/And.h
View File

@ -32,121 +32,122 @@ namespace formula {
*/
template <class T>
class And : public PCTLStateFormula<T> {
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
public:
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
And() {
left = NULL;
right = NULL;
}
/*!
* Constructor.
* Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* The subtrees are deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~And() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " && ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
And<T>* result = new And();
if (this->left != NULL) {
result->setLeft(left->clone());
}
if (this->right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
And() {
left = NULL;
right = NULL;
}
/*!
* Constructor.
* Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* The subtrees are deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~And() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " && ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
And<T>* result = new And();
if (this->left != NULL) {
result->setLeft(left->clone());
}
if (this->right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
};
} //namespace formula

275
src/formula/BoundedUntil.h
View File

@ -36,142 +36,145 @@ namespace formula {
*/
template <class T>
class BoundedUntil : public PCTLPathFormula<T> {
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
uint_fast64_t bound;
public:
/*!
* Empty constructor
*/
BoundedUntil() {
this->left = NULL;
this->right = NULL;
bound = 0;
}
/*!
* Constructor
*
* @param left The left formula subtree
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
uint_fast64_t bound) {
this->left = left;
this->right = right;;
this->bound = bound;
}
/*!
* Destructor.
*
* Also deletes the subtrees.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~BoundedUntil() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns the maximally allowed number of steps for the bounded until operator
*/
uint_fast64_t getBound() {
return bound;
}
/*!
* Sets the maximally allowed number of steps for the bounded until operator
*
* @param bound the new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " U<=";
result += boost::lexical_cast<std::string>(bound);
result += " ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
BoundedUntil<T>* result = new BoundedUntil();
result->setBound(bound);
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor
*/
BoundedUntil() {
this->left = NULL;
this->right = NULL;
bound = 0;
}
/*!
* Constructor
*
* @param left The left formula subtree
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
uint_fast64_t bound) {
this->left = left;
this->right = right;;
this->bound = bound;
}
/*!
* Destructor.
*
* Also deletes the subtrees.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~BoundedUntil() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns the maximally allowed number of steps for the bounded until operator
*/
uint_fast64_t getBound() {
return bound;
}
/*!
* Sets the maximally allowed number of steps for the bounded until operator
*
* @param bound the new bound.
*/
void setBound(uint_fast64_t bound) {
this->bound = bound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " U<=";
result += boost::lexical_cast<std::string>(bound);
result += " ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
BoundedUntil<T>* result = new BoundedUntil();
result->setBound(bound);
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
uint_fast64_t bound;
};
} //namespace formula

170
src/formula/Next.h
View File

@ -32,90 +32,92 @@ namespace formula {
*/
template <class T>
class Next : public PCTLPathFormula<T> {
private:
PCTLStateFormula<T>* child;
public:
/*!
* Empty constructor
*/
Next() {
this->child = NULL;
}
/*!
* Constructor
*
* @param child The child node
*/
Next(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* Constructor.
*
* Also deletes the subtree.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Next() {
if (child != NULL) {
delete child;
}
}
/*!
* @returns the child node
*/
PCTLStateFormula<T>* getChild() {
return child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += " X ";
result += child->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor
*/
Next() {
this->child = NULL;
}
/*!
* Constructor
*
* @param child The child node
*/
Next(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* Constructor.
*
* Also deletes the subtree.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Next() {
if (child != NULL) {
delete child;
}
}
/*!
* @returns the child node
*/
PCTLStateFormula<T>* getChild() {
return child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += " X ";
result += child->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* child;
};
} //namespace formula

164
src/formula/Not.h
View File

@ -28,87 +28,89 @@ namespace formula {
*/
template <class T>
class Not : public PCTLStateFormula<T> {
private:
PCTLStateFormula<T>* child;
public:
/*!
* Empty constructor
*/
Not() {
this->child = NULL;
}
/*!
* Constructor
* @param child The child node
*/
Not(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* Destructor
*
* Also deletes the subtree
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Not() {
if (child != NULL) {
delete child;
}
}
/*!
* @returns The child node
*/
PCTLStateFormula<T>* getChild() {
return child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "!";
result += child->toString();
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child);
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor
*/
Not() {
this->child = NULL;
}
/*!
* Constructor
* @param child The child node
*/
Not(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* Destructor
*
* Also deletes the subtree
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Not() {
if (child != NULL) {
delete child;
}
}
/*!
* @returns The child node
*/
PCTLStateFormula<T>* getChild() {
return child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(PCTLStateFormula<T>* child) {
this->child = child;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "!";
result += child->toString();
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child);
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* child;
};
} //namespace formula

230
src/formula/Or.h
View File

@ -31,120 +31,122 @@ namespace formula {
*/
template <class T>
class Or : public PCTLStateFormula<T> {
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
public:
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
Or() {
left = NULL;
right = NULL;
}
/*!
* Constructor.
* Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* The subtrees are deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Or() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " || ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
Or<T>* result = new Or();
if (this->left != NULL) {
result->setLeft(left->clone());
}
if (this->right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
Or() {
left = NULL;
right = NULL;
}
/*!
* Constructor.
* Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* The subtrees are deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Or() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " || ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
Or<T>* result = new Or();
if (this->left != NULL) {
result->setLeft(left->clone());
}
if (this->right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
};
} //namespace formula

53
src/formula/PCTLPathFormula.h
View File

@ -27,34 +27,35 @@ namespace formula {
*/
template <class T>
class PCTLPathFormula : public PCTLFormula<T> {
public:
/*!
* empty destructor
*/
virtual ~PCTLPathFormula() { }
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @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;
public:
/*!
* empty destructor
*/
virtual ~PCTLPathFormula() { }
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @note This function is not implemented in this class.
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @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;
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @note This function is not implemented in this class.
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
};
} //namespace formula

53
src/formula/PCTLStateFormula.h
View File

@ -27,34 +27,35 @@ namespace formula {
*/
template <class T>
class PCTLStateFormula : public PCTLFormula<T> {
public:
/*!
* empty destructor
*/
virtual ~PCTLStateFormula() { }
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @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;
public:
/*!
* empty destructor
*/
virtual ~PCTLStateFormula() { }
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @note This function is not implemented in this class.
*
* @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;
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @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;
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @note This function is not implemented in this class.
*
* @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;
};
} //namespace formula

23
src/formula/PCTLformula.h
View File

@ -27,17 +27,18 @@ namespace formula {
*/
template <class T>
class PCTLFormula {
public:
/*!
* virtual destructor
*/
virtual ~PCTLFormula() { }
/*!
* @note This function is not implemented in this class.
* @returns a string representation of the formula
*/
virtual std::string toString() = 0;
public:
/*!
* virtual destructor
*/
virtual ~PCTLFormula() { }
/*!
* @note This function is not implemented in this class.
* @returns a string representation of the formula
*/
virtual std::string toString() = 0;
};
} //namespace formula

247
src/formula/ProbabilisticOperator.h
View File

@ -34,128 +34,131 @@ namespace formula {
*/
template<class T>
class ProbabilisticOperator : public PCTLStateFormula<T> {
T lower;
T upper;
PCTLPathFormula<T>* pathFormula;
public:
/*!
* Empty constructor
*/
ProbabilisticOperator() {
upper = mrmc::misc::constGetZero(&upper);
lower = mrmc::misc::constGetZero(&lower);
pathFormula = NULL;
}
/*!
* Constructor
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
* @param pathFormula The child node (can be omitted, is then set to NULL)
*/
ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
this->lower = lowerBound;
this->upper = upperBound;
this->pathFormula = pathFormula;
}
/*!
* Destructor
*
* The subtree is deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~ProbabilisticOperator() {
if (pathFormula != NULL) {
delete pathFormula;
}
}
/*!
* @returns the child node (representation of a PCTL path formula)
*/
PCTLPathFormula<T>* getPathFormula () {
return pathFormula;
}
/*!
* @returns the lower bound for the probability
*/
T getLowerBound() {
return lower;
}
/*!
* @returns the upper bound for the probability
*/
T getUpperBound() {
return upper;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
/*!
* Sets the interval in which the probability that the path formula holds may lie.
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
*/
void setInterval(T lowerBound, T upperBound) {
this->lower = lowerBound;
this->upper = upperBound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += " P[";
result += lower;
result += ";";
result += upper;
result += "] ";
result += pathFormula->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
result->setInterval(lower, upper);
if (pathFormula != NULL) {
result->setPathFormula(pathFormula->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor
*/
ProbabilisticOperator() {
upper = mrmc::misc::constGetZero(&upper);
lower = mrmc::misc::constGetZero(&lower);
pathFormula = NULL;
}
/*!
* Constructor
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
* @param pathFormula The child node (can be omitted, is then set to NULL)
*/
ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
this->lower = lowerBound;
this->upper = upperBound;
this->pathFormula = pathFormula;
}
/*!
* Destructor
*
* The subtree is deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~ProbabilisticOperator() {
if (pathFormula != NULL) {
delete pathFormula;
}
}
/*!
* @returns the child node (representation of a PCTL path formula)
*/
PCTLPathFormula<T>* getPathFormula () {
return pathFormula;
}
/*!
* @returns the lower bound for the probability
*/
T getLowerBound() {
return lower;
}
/*!
* @returns the upper bound for the probability
*/
T getUpperBound() {
return upper;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
/*!
* Sets the interval in which the probability that the path formula holds may lie.
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
*/
void setInterval(T lowerBound, T upperBound) {
this->lower = lowerBound;
this->upper = upperBound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += " P[";
result += lower;
result += ";";
result += upper;
result += "] ";
result += pathFormula->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() {
ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
result->setInterval(lower, upper);
if (pathFormula != NULL) {
result->setPathFormula(pathFormula->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
T lower;
T upper;
PCTLPathFormula<T>* pathFormula;
};
} //namespace formula

225
src/formula/Until.h
View File

@ -33,117 +33,120 @@ namespace formula {
*/
template <class T>
class Until : public PCTLPathFormula<T> {
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
public:
/*!
* Empty constructor
*/
Until() {
this->left = NULL;
this->right = NULL;
}
/*!
* Constructor
*
* @param left The left formula subtree
* @param right The left formula subtree
*/
Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* Also deletes the subtrees.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Until() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " U ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
Until<T>* result = new Until();
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
public:
/*!
* Empty constructor
*/
Until() {
this->left = NULL;
this->right = NULL;
}
/*!
* Constructor
*
* @param left The left formula subtree
* @param right The left formula subtree
*/
Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
this->left = left;
this->right = right;
}
/*!
* Destructor.
*
* Also deletes the subtrees.
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Until() {
if (left != NULL) {
delete left;
}
if (right != NULL) {
delete right;
}
}
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(PCTLStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(PCTLStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
PCTLStateFormula<T>* getLeft() {
return left;
}
/*!
* @returns a pointer to the right child node
*/
PCTLStateFormula<T>* getRight() {
return right;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() {
std::string result = "(";
result += left->toString();
result += " U ";
result += right->toString();
result += ")";
return result;
}
/*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PCTLPathFormula<T>* clone() {
Until<T>* result = new Until();
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
result->setRight(right->clone());
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
*
* @note This function should only be called in a generic check function of a model checker class. For other uses,
* the methods of the model checker should be used.
*
* @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);
}
private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
};
} //namespace formula

Write Preview
Loading…
Cancel
Save