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

Further naming scheme enforcement.

tempestpy_adaptions
PBerger 12 years ago
parent
96c7dd9a79
commit
9e5b69b211
17 changed files with 148 additions and 148 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 24
      src/formula/And.h
  2. 28
      src/formula/Ap.h
  3. 26
      src/formula/BoundedUntil.h
  4. 8
      src/formula/Formulas.h
  5. 20
      src/formula/Next.h
  6. 18
      src/formula/Not.h
  7. 24
      src/formula/Or.h
  8. 8
      src/formula/PctlFormula.h
  9. 10
      src/formula/PctlPathFormula.h
  10. 10
      src/formula/PctlStateFormula.h
  11. 22
      src/formula/ProbabilisticIntervalOperator.h
  12. 22
      src/formula/ProbabilisticNoBoundsOperator.h
  13. 24
      src/formula/ProbabilisticOperator.h
  14. 26
      src/formula/Until.h
  15. 18
      src/modelChecker/DtmcPrctlModelChecker.h
  16. 2
      src/parser/PrctlParser.cpp
  17. 6
      src/parser/PrctlParser.h

24
src/formula/And.h
View File

@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_AND_H_ #ifndef MRMC_FORMULA_AND_H_
#define MRMC_FORMULA_AND_H_ #define MRMC_FORMULA_AND_H_
#include "PCTLStateFormula.h"
#include "PctlStateFormula.h"
#include <string> #include <string>
namespace mrmc { namespace mrmc {
@ -27,11 +27,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object * The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLStateFormula
* @see PCTLFormula
* @see PctlStateFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class And : public PCTLStateFormula<T> {
class And : public PctlStateFormula<T> {
public: public:
/*! /*!
@ -50,7 +50,7 @@ public:
* @param left The left sub formula * @param left The left sub formula
* @param right The right sub formula * @param right The right sub formula
*/ */
And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
And(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -75,7 +75,7 @@ public:
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(PCTLStateFormula<T>* newLeft) {
void setLeft(PctlStateFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -84,21 +84,21 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(PCTLStateFormula<T>* newRight) {
void setRight(PctlStateFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const PCTLStateFormula<T>& getLeft() const {
const PctlStateFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const PCTLStateFormula<T>& getRight() const {
const PctlStateFormula<T>& getRight() const {
return *right; return *right;
} }
@ -121,7 +121,7 @@ public:
* *
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
virtual PctlStateFormula<T>* clone() const {
And<T>* result = new And(); And<T>* result = new And();
if (this->left != NULL) { if (this->left != NULL) {
result->setLeft(left->clone()); result->setLeft(left->clone());
@ -146,8 +146,8 @@ public:
} }
private: private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
}; };
} //namespace formula } //namespace formula

28
src/formula/AP.h → src/formula/Ap.h
View File

@ -1,5 +1,5 @@
/* /*
* AP.h
* Ap.h
* *
* Created on: 19.10.2012 * Created on: 19.10.2012
* Author: Thomas Heinemann * Author: Thomas Heinemann
@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_AP_H_ #ifndef MRMC_FORMULA_AP_H_
#define MRMC_FORMULA_AP_H_ #define MRMC_FORMULA_AP_H_
#include "PCTLStateFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
@ -20,21 +20,21 @@ namespace formula {
* *
* This class represents the leaves in the formula tree. * This class represents the leaves in the formula tree.
* *
* @see PCTLStateFormula
* @see PCTLFormula
* @see PctlStateFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class AP : public PCTLStateFormula<T> {
class Ap : public PctlStateFormula<T> {
public: public:
/*! /*!
* Constructor * Constructor
* *
* Creates a new atomic proposition leaf, with the label AP
* Creates a new atomic proposition leaf, with the label Ap
* *
* @param ap The string representing the atomic proposition * @param ap The string representing the atomic proposition
*/ */
AP(std::string ap) {
Ap(std::string ap) {
this->ap = ap; this->ap = ap;
} }
@ -42,12 +42,12 @@ public:
* Destructor. * Destructor.
* At this time, empty... * At this time, empty...
*/ */
virtual ~AP() { }
virtual ~Ap() { }
/*! /*!
* @returns the name of the atomic proposition * @returns the name of the atomic proposition
*/ */
const std::string& getAP() const {
const std::string& getAp() const {
return ap; return ap;
} }
@ -56,16 +56,16 @@ public:
* *
*/ */
virtual std::string toString() const { virtual std::string toString() const {
return getAP();
return getAp();
} }
/*! /*!
* Clones the called object. * Clones the called object.
* *
* @returns a new AP-object that is identical the called object.
* @returns a new Ap-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
return new AP(ap);
virtual PctlStateFormula<T>* clone() const {
return new Ap(ap);
} }
/*! /*!
@ -78,7 +78,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object. * @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<T>& modelChecker) const { virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkAP(*this);
return modelChecker.checkAp(*this);
} }
private: private:

26
src/formula/BoundedUntil.h
View File

@ -8,8 +8,8 @@
#ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_ #ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_
#define MRMC_FORMULA_BOUNDEDUNTIL_H_ #define MRMC_FORMULA_BOUNDEDUNTIL_H_
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
@ -30,11 +30,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object * The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLPathFormula
* @see PCTLFormula
* @see PctlPathFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class BoundedUntil : public PCTLPathFormula<T> {
class BoundedUntil : public PctlPathFormula<T> {
public: public:
/*! /*!
@ -53,7 +53,7 @@ public:
* @param right The left formula subtree * @param right The left formula subtree
* @param bound The maximal number of steps * @param bound The maximal number of steps
*/ */
BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
BoundedUntil(PctlStateFormula<T>* left, PctlStateFormula<T>* right,
uint_fast64_t bound) { uint_fast64_t bound) {
this->left = left; this->left = left;
this->right = right;; this->right = right;;
@ -80,7 +80,7 @@ public:
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(PCTLStateFormula<T>* newLeft) {
void setLeft(PctlStateFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -89,21 +89,21 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(PCTLStateFormula<T>* newRight) {
void setRight(PctlStateFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const PCTLStateFormula<T>& getLeft() const {
const PctlStateFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const PCTLStateFormula<T>& getRight() const {
const PctlStateFormula<T>& getRight() const {
return *right; return *right;
} }
@ -144,7 +144,7 @@ public:
* *
* @returns a new BoundedUntil-object that is identical the called object. * @returns a new BoundedUntil-object that is identical the called object.
*/ */
virtual PCTLPathFormula<T>* clone() const {
virtual PctlPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil(); BoundedUntil<T>* result = new BoundedUntil();
result->setBound(bound); result->setBound(bound);
if (left != NULL) { if (left != NULL) {
@ -171,8 +171,8 @@ public:
} }
private: private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
uint_fast64_t bound; uint_fast64_t bound;
}; };

8
src/formula/Formulas.h
View File

@ -9,14 +9,14 @@
#define MRMC_FORMULA_FORMULAS_H_ #define MRMC_FORMULA_FORMULAS_H_
#include "And.h" #include "And.h"
#include "AP.h"
#include "Ap.h"
#include "BoundedUntil.h" #include "BoundedUntil.h"
#include "Next.h" #include "Next.h"
#include "Not.h" #include "Not.h"
#include "Or.h" #include "Or.h"
#include "PCTLformula.h"
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "PctlFormula.h"
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "ProbabilisticOperator.h" #include "ProbabilisticOperator.h"
#include "ProbabilisticNoBoundsOperator.h" #include "ProbabilisticNoBoundsOperator.h"
#include "ProbabilisticIntervalOperator.h" #include "ProbabilisticIntervalOperator.h"

20
src/formula/Next.h
View File

@ -8,8 +8,8 @@
#ifndef MRMC_FORMULA_NEXT_H_ #ifndef MRMC_FORMULA_NEXT_H_
#define MRMC_FORMULA_NEXT_H_ #define MRMC_FORMULA_NEXT_H_
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
@ -27,11 +27,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object * The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLPathFormula
* @see PCTLFormula
* @see PctlPathFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class Next : public PCTLPathFormula<T> {
class Next : public PctlPathFormula<T> {
public: public:
/*! /*!
@ -46,7 +46,7 @@ public:
* *
* @param child The child node * @param child The child node
*/ */
Next(PCTLStateFormula<T>* child) {
Next(PctlStateFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -65,7 +65,7 @@ public:
/*! /*!
* @returns the child node * @returns the child node
*/ */
const PCTLStateFormula<T>& getChild() const {
const PctlStateFormula<T>& getChild() const {
return *child; return *child;
} }
@ -73,7 +73,7 @@ public:
* Sets the subtree * Sets the subtree
* @param child the new child node * @param child the new child node
*/ */
void setChild(PCTLStateFormula<T>* child) {
void setChild(PctlStateFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -95,7 +95,7 @@ public:
* *
* @returns a new BoundedUntil-object that is identical the called object. * @returns a new BoundedUntil-object that is identical the called object.
*/ */
virtual PCTLPathFormula<T>* clone() const {
virtual PctlPathFormula<T>* clone() const {
Next<T>* result = new Next<T>(); Next<T>* result = new Next<T>();
if (child != NULL) { if (child != NULL) {
result->setChild(child); result->setChild(child);
@ -117,7 +117,7 @@ public:
} }
private: private:
PCTLStateFormula<T>* child;
PctlStateFormula<T>* child;
}; };
} //namespace formula } //namespace formula

18
src/formula/Not.h
View File

@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_NOT_H_ #ifndef MRMC_FORMULA_NOT_H_
#define MRMC_FORMULA_NOT_H_ #define MRMC_FORMULA_NOT_H_
#include "PCTLStateFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
@ -23,11 +23,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object * The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLStateFormula
* @see PCTLFormula
* @see PctlStateFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class Not : public PCTLStateFormula<T> {
class Not : public PctlStateFormula<T> {
public: public:
/*! /*!
@ -41,7 +41,7 @@ public:
* Constructor * Constructor
* @param child The child node * @param child The child node
*/ */
Not(PCTLStateFormula<T>* child) {
Not(PctlStateFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -60,7 +60,7 @@ public:
/*! /*!
* @returns The child node * @returns The child node
*/ */
const PCTLStateFormula<T>& getChild() const {
const PctlStateFormula<T>& getChild() const {
return *child; return *child;
} }
@ -68,7 +68,7 @@ public:
* Sets the subtree * Sets the subtree
* @param child the new child node * @param child the new child node
*/ */
void setChild(PCTLStateFormula<T>* child) {
void setChild(PctlStateFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -88,7 +88,7 @@ public:
* *
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
virtual PctlStateFormula<T>* clone() const {
Not<T>* result = new Not<T>(); Not<T>* result = new Not<T>();
if (child != NULL) { if (child != NULL) {
result->setChild(child); result->setChild(child);
@ -110,7 +110,7 @@ public:
} }
private: private:
PCTLStateFormula<T>* child;
PctlStateFormula<T>* child;
}; };
} //namespace formula } //namespace formula

24
src/formula/Or.h
View File

@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_OR_H_ #ifndef MRMC_FORMULA_OR_H_
#define MRMC_FORMULA_OR_H_ #define MRMC_FORMULA_OR_H_
#include "PCTLStateFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
@ -26,11 +26,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object * The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLStateFormula
* @see PCTLFormula
* @see PctlStateFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class Or : public PCTLStateFormula<T> {
class Or : public PctlStateFormula<T> {
public: public:
/*! /*!
@ -49,7 +49,7 @@ public:
* @param left The left sub formula * @param left The left sub formula
* @param right The right sub formula * @param right The right sub formula
*/ */
Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
Or(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -74,7 +74,7 @@ public:
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(PCTLStateFormula<T>* newLeft) {
void setLeft(PctlStateFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -83,21 +83,21 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(PCTLStateFormula<T>* newRight) {
void setRight(PctlStateFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const PCTLStateFormula<T>& getLeft() const {
const PctlStateFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const PCTLStateFormula<T>& getRight() const {
const PctlStateFormula<T>& getRight() const {
return *right; return *right;
} }
@ -120,7 +120,7 @@ public:
* *
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
virtual PctlStateFormula<T>* clone() const {
Or<T>* result = new Or(); Or<T>* result = new Or();
if (this->left != NULL) { if (this->left != NULL) {
result->setLeft(left->clone()); result->setLeft(left->clone());
@ -145,8 +145,8 @@ public:
} }
private: private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
}; };
} //namespace formula } //namespace formula

8
src/formula/PCTLformula.h → src/formula/PctlFormula.h
View File

@ -1,5 +1,5 @@
/* /*
* PCTLformula.h
* Pctlformula.h
* *
* Created on: 19.10.2012 * Created on: 19.10.2012
* Author: Thomas Heinemann * Author: Thomas Heinemann
@ -23,16 +23,16 @@ namespace formula {
* @attention This class is abstract. * @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
* PCTLPathFormula and PCTLStateFormula offer the method clone().
* PctlPathFormula and PctlStateFormula offer the method clone().
*/ */
template <class T> template <class T>
class PCTLFormula {
class PctlFormula {
public: public:
/*! /*!
* virtual destructor * virtual destructor
*/ */
virtual ~PCTLFormula() { }
virtual ~PctlFormula() { }
/*! /*!
* @note This function is not implemented in this class. * @note This function is not implemented in this class.

10
src/formula/PCTLPathFormula.h → src/formula/PctlPathFormula.h
View File

@ -1,5 +1,5 @@
/* /*
* PCTLPathFormula.h
* PctlPathFormula.h
* *
* Created on: 19.10.2012 * Created on: 19.10.2012
* Author: Thomas Heinemann * Author: Thomas Heinemann
@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_ #ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_
#define MRMC_FORMULA_PCTLPATHFORMULA_H_ #define MRMC_FORMULA_PCTLPATHFORMULA_H_
#include "PCTLformula.h"
#include "PctlFormula.h"
#include "modelChecker/DtmcPrctlModelChecker.h" #include "modelChecker/DtmcPrctlModelChecker.h"
#include <vector> #include <vector>
@ -26,13 +26,13 @@ namespace formula {
* clone(). * clone().
*/ */
template <class T> template <class T>
class PCTLPathFormula : public PCTLFormula<T> {
class PctlPathFormula : public PctlFormula<T> {
public: public:
/*! /*!
* empty destructor * empty destructor
*/ */
virtual ~PCTLPathFormula() { }
virtual ~PctlPathFormula() { }
/*! /*!
* Clones the called object. * Clones the called object.
@ -42,7 +42,7 @@ public:
* @note This function is not implemented in this class. * @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLPathFormula<T>* clone() const = 0;
virtual PctlPathFormula<T>* clone() const = 0;
/*! /*!
* Calls the model checker to check this formula. * Calls the model checker to check this formula.

10
src/formula/PCTLStateFormula.h → src/formula/PctlStateFormula.h
View File

@ -1,5 +1,5 @@
/* /*
* PCTLStateFormula.h
* PctlStateFormula.h
* *
* Created on: 19.10.2012 * Created on: 19.10.2012
* Author: Thomas Heinemann * Author: Thomas Heinemann
@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_ #ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_
#define MRMC_FORMULA_PCTLSTATEFORMULA_H_ #define MRMC_FORMULA_PCTLSTATEFORMULA_H_
#include "PCTLformula.h"
#include "PctlFormula.h"
#include "storage/BitVector.h" #include "storage/BitVector.h"
#include "modelChecker/DtmcPrctlModelChecker.h" #include "modelChecker/DtmcPrctlModelChecker.h"
@ -26,13 +26,13 @@ namespace formula {
* clone(). * clone().
*/ */
template <class T> template <class T>
class PCTLStateFormula : public PCTLFormula<T> {
class PctlStateFormula : public PctlFormula<T> {
public: public:
/*! /*!
* empty destructor * empty destructor
*/ */
virtual ~PCTLStateFormula() { }
virtual ~PctlStateFormula() { }
/*! /*!
* Clones the called object. * Clones the called object.
@ -42,7 +42,7 @@ public:
* @note This function is not implemented in this class. * @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const = 0;
virtual PctlStateFormula<T>* clone() const = 0;
/*! /*!
* Calls the model checker to check this formula. * Calls the model checker to check this formula.

22
src/formula/ProbabilisticIntervalOperator.h
View File

@ -8,8 +8,8 @@
#ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ #ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
#define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
#include "PCTLStateFormula.h"
#include "PCTLPathFormula.h"
#include "PctlStateFormula.h"
#include "PctlPathFormula.h"
#include "utility/ConstTemplates.h" #include "utility/ConstTemplates.h"
namespace mrmc { namespace mrmc {
@ -35,14 +35,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* *
* @see PCTLStateFormula
* @see PCTLPathFormula
* @see PctlStateFormula
* @see PctlPathFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator * @see ProbabilisticNoBoundsOperator
* @see PCTLFormula
* @see PctlFormula
*/ */
template<class T> template<class T>
class ProbabilisticIntervalOperator : public PCTLStateFormula<T> {
class ProbabilisticIntervalOperator : public PctlStateFormula<T> {
public: public:
/*! /*!
@ -61,7 +61,7 @@ public:
* @param upperBound The upper bound for the probability * @param upperBound The upper bound for the probability
* @param pathFormula The child node * @param pathFormula The child node
*/ */
ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula<T>& pathFormula) {
ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) {
this->lower = lowerBound; this->lower = lowerBound;
this->upper = upperBound; this->upper = upperBound;
this->pathFormula = &pathFormula; this->pathFormula = &pathFormula;
@ -82,7 +82,7 @@ public:
/*! /*!
* @returns the child node (representation of a PCTL path formula) * @returns the child node (representation of a PCTL path formula)
*/ */
const PCTLPathFormula<T>& getPathFormula () const {
const PctlPathFormula<T>& getPathFormula () const {
return *pathFormula; return *pathFormula;
} }
@ -105,7 +105,7 @@ public:
* *
* @param pathFormula the path formula that becomes the new child node * @param pathFormula the path formula that becomes the new child node
*/ */
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
void setPathFormula(PctlPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula; this->pathFormula = pathFormula;
} }
@ -141,7 +141,7 @@ public:
* *
* @returns a new AND-object that is identical the called object. * @returns a new AND-object that is identical the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
virtual PctlStateFormula<T>* clone() const {
ProbabilisticIntervalOperator<T>* result = new ProbabilisticIntervalOperator<T>(); ProbabilisticIntervalOperator<T>* result = new ProbabilisticIntervalOperator<T>();
result->setInterval(lower, upper); result->setInterval(lower, upper);
if (pathFormula != NULL) { if (pathFormula != NULL) {
@ -166,7 +166,7 @@ public:
private: private:
T lower; T lower;
T upper; T upper;
PCTLPathFormula<T>* pathFormula;
PctlPathFormula<T>* pathFormula;
}; };
} //namespace formula } //namespace formula

22
src/formula/ProbabilisticNoBoundsOperator.h
View File

@ -8,8 +8,8 @@
#ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ #ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
#define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
#include "PCTLformula.h"
#include "PCTLPathFormula.h"
#include "PctlFormula.h"
#include "PctlPathFormula.h"
namespace mrmc { namespace mrmc {
namespace formula { namespace formula {
@ -26,20 +26,20 @@ namespace formula {
* *
* @note * @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator. * This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from PCTLformula.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
* *
* The subtree is seen as part of the object and deleted with it * The subtree is seen as part of the object and deleted with it
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* *
* @see PCTLStateFormula
* @see PCTLPathFormula
* @see PctlStateFormula
* @see PctlPathFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator * @see ProbabilisticIntervalOperator
* @see PCTLFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class ProbabilisticNoBoundsOperator: public mrmc::formula::PCTLFormula<T> {
class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula<T> {
public: public:
/*! /*!
* Empty constructor * Empty constructor
@ -54,7 +54,7 @@ public:
* *
* @param pathFormula The child node. * @param pathFormula The child node.
*/ */
ProbabilisticNoBoundsOperator(PCTLPathFormula<T> &pathFormula) {
ProbabilisticNoBoundsOperator(PctlPathFormula<T> &pathFormula) {
this->pathFormula = &pathFormula; this->pathFormula = &pathFormula;
} }
@ -68,7 +68,7 @@ public:
/*! /*!
* @returns the child node (representation of a PCTL path formula) * @returns the child node (representation of a PCTL path formula)
*/ */
const PCTLPathFormula<T>& getPathFormula () const {
const PctlPathFormula<T>& getPathFormula () const {
return *pathFormula; return *pathFormula;
} }
@ -77,7 +77,7 @@ public:
* *
* @param pathFormula the path formula that becomes the new child node * @param pathFormula the path formula that becomes the new child node
*/ */
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
void setPathFormula(PctlPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula; this->pathFormula = pathFormula;
} }
@ -92,7 +92,7 @@ public:
} }
private: private:
PCTLPathFormula<T>* pathFormula;
PctlPathFormula<T>* pathFormula;
}; };
} /* namespace formula */ } /* namespace formula */

24
src/formula/ProbabilisticOperator.h
View File

@ -8,7 +8,7 @@
#ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_ #ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_
#define MRMC_FORMULA_PROBABILISTICOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICOPERATOR_H_
#include "PCTLStateFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
namespace formula { namespace formula {
@ -32,14 +32,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* *
* @see PCTLStateFormula
* @see PCTLPathFormula
* @see PctlStateFormula
* @see PctlPathFormula
* @see ProbabilisticIntervalOperator * @see ProbabilisticIntervalOperator
* @see ProbabilisticNoBoundsOperator * @see ProbabilisticNoBoundsOperator
* @see PCTLFormula
* @see PctlFormula
*/ */
template<class T> template<class T>
class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula<T> {
class ProbabilisticOperator : public mrmc::formula::PctlStateFormula<T> {
public: public:
/*! /*!
* Empty constructor * Empty constructor
@ -55,7 +55,7 @@ public:
* @param bound The expected value for path formulas * @param bound The expected value for path formulas
* @param pathFormula The child node * @param pathFormula The child node
*/ */
ProbabilisticOperator(T bound, PCTLPathFormula<T>& pathFormula) {
ProbabilisticOperator(T bound, PctlPathFormula<T>& pathFormula) {
this->bound = bound; this->bound = bound;
this->pathFormula = &pathFormula; this->pathFormula = &pathFormula;
} }
@ -73,7 +73,7 @@ public:
/*! /*!
* @returns the child node (representation of a PCTL path formula) * @returns the child node (representation of a PCTL path formula)
*/ */
const PCTLPathFormula<T>& getPathFormula () const {
const PctlPathFormula<T>& getPathFormula () const {
return *pathFormula; return *pathFormula;
} }
@ -89,7 +89,7 @@ public:
* *
* @param pathFormula the path formula that becomes the new child node * @param pathFormula the path formula that becomes the new child node
*/ */
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
void setPathFormula(PctlPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula; this->pathFormula = pathFormula;
} }
@ -109,7 +109,7 @@ public:
* *
* @returns a new ProbabilisticOperator-object that is identical to the called object. * @returns a new ProbabilisticOperator-object that is identical to the called object.
*/ */
virtual PCTLStateFormula<T>* clone() const {
virtual PctlStateFormula<T>* clone() const {
ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>(); ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
result->setBound(bound); result->setBound(bound);
if (pathFormula != NULL) { if (pathFormula != NULL) {
@ -134,9 +134,9 @@ public:
} }
/*! /*!
* Returns a string representation of this PCTLStateFormula
* Returns a string representation of this PctlStateFormula
* *
* @returns a string representation of this PCTLStateFormula
* @returns a string representation of this PctlStateFormula
*/ */
virtual std::string toString() const { virtual std::string toString() const {
std::string result = " P="; std::string result = " P=";
@ -148,7 +148,7 @@ public:
} }
private: private:
T bound; T bound;
PCTLPathFormula<T>* pathFormula;
PctlPathFormula<T>* pathFormula;
}; };
} /* namespace formula */ } /* namespace formula */

26
src/formula/Until.h
View File

@ -8,8 +8,8 @@
#ifndef MRMC_FORMULA_UNTIL_H_ #ifndef MRMC_FORMULA_UNTIL_H_
#define MRMC_FORMULA_UNTIL_H_ #define MRMC_FORMULA_UNTIL_H_
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
namespace mrmc { namespace mrmc {
@ -28,11 +28,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object * The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion) * (this behavior can be prevented by setting them to NULL before deletion)
* *
* @see PCTLPathFormula
* @see PCTLFormula
* @see PctlPathFormula
* @see PctlFormula
*/ */
template <class T> template <class T>
class Until : public PCTLPathFormula<T> {
class Until : public PctlPathFormula<T> {
public: public:
/*! /*!
@ -49,7 +49,7 @@ public:
* @param left The left formula subtree * @param left The left formula subtree
* @param right The left formula subtree * @param right The left formula subtree
*/ */
Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
Until(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -74,7 +74,7 @@ public:
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(PCTLStateFormula<T>* newLeft) {
void setLeft(PctlStateFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -83,21 +83,21 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(PCTLStateFormula<T>* newRight) {
void setRight(PctlStateFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const PCTLStateFormula<T>& getLeft() const {
const PctlStateFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const PCTLStateFormula<T>& getRight() const {
const PctlStateFormula<T>& getRight() const {
return *right; return *right;
} }
@ -120,7 +120,7 @@ public:
* *
* @returns a new BoundedUntil-object that is identical the called object. * @returns a new BoundedUntil-object that is identical the called object.
*/ */
virtual PCTLPathFormula<T>* clone() const {
virtual PctlPathFormula<T>* clone() const {
Until<T>* result = new Until(); Until<T>* result = new Until();
if (left != NULL) { if (left != NULL) {
result->setLeft(left->clone()); result->setLeft(left->clone());
@ -145,8 +145,8 @@ public:
} }
private: private:
PCTLStateFormula<T>* left;
PCTLStateFormula<T>* right;
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
}; };
} //namespace formula } //namespace formula

18
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -23,8 +23,8 @@ class DtmcPrctlModelChecker;
} }
#include "src/formula/PCTLPathFormula.h"
#include "src/formula/PCTLStateFormula.h"
#include "src/formula/PctlPathFormula.h"
#include "src/formula/PctlStateFormula.h"
#include "src/formula/Formulas.h" #include "src/formula/Formulas.h"
@ -96,7 +96,7 @@ public:
* @param formula The state formula to check * @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector * @returns The set of states satisfying the formula, represented by a bit vector
*/ */
mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula<Type>& formula) const {
mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PctlStateFormula<Type>& formula) const {
return formula.check(*this); return formula.check(*this);
} }
@ -117,16 +117,16 @@ public:
/*! /*!
* The check method for a formula with an AP node as root in its formula tree * The check method for a formula with an AP node as root in its formula tree
* *
* @param formula The AP state formula to check
* @param formula The Ap state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector * @returns The set of states satisfying the formula, represented by a bit vector
*/ */
mrmc::storage::BitVector* checkAP(const mrmc::formula::AP<Type>& formula) const {
if (formula.getAP().compare("true") == 0) {
mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap<Type>& formula) const {
if (formula.getAp().compare("true") == 0) {
return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); return new mrmc::storage::BitVector(model->getNumberOfStates(), 1);
} else if (formula.getAP().compare("false") == 0) {
} else if (formula.getAp().compare("false") == 0) {
return new mrmc::storage::BitVector(model->getNumberOfStates()); return new mrmc::storage::BitVector(model->getNumberOfStates());
} }
return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP()));
return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAp()));
} }
/*! /*!
@ -226,7 +226,7 @@ public:
* @param formula The path formula to check * @param formula The path formula to check
* @returns for each state the probability that the path formula holds. * @returns for each state the probability that the path formula holds.
*/ */
std::vector<Type>* checkPathFormula(const mrmc::formula::PCTLPathFormula<Type>& formula) const {
std::vector<Type>* checkPathFormula(const mrmc::formula::PctlPathFormula<Type>& formula) const {
return formula.check(*this); return formula.check(*this);
} }

2
src/parser/PrctlParser.cpp
View File

@ -58,7 +58,7 @@ namespace
/*! /*!
* @brief Resulting formula. * @brief Resulting formula.
*/ */
mrmc::formula::PCTLFormula<double>* result;
mrmc::formula::PctlFormula<double>* result;
struct dump struct dump
{ {

6
src/parser/PrctlParser.h
View File

@ -1,7 +1,7 @@
#ifndef MRMC_PARSER_PRCTLPARSER_H_ #ifndef MRMC_PARSER_PRCTLPARSER_H_
#define MRMC_PARSER_PRCTLPARSER_H_ #define MRMC_PARSER_PRCTLPARSER_H_
#include "src/formula/PCTLformula.h"
#include "src/formula/PctlFormula.h"
#include "src/parser/Parser.h" #include "src/parser/Parser.h"
namespace mrmc { namespace mrmc {
@ -18,13 +18,13 @@ class PrctlParser : Parser
/*! /*!
* @brief return formula object parsed from file. * @brief return formula object parsed from file.
*/ */
mrmc::formula::PCTLFormula<double>* getFormula()
mrmc::formula::PctlFormula<double>* getFormula()
{ {
return this->formula; return this->formula;
} }
private: private:
mrmc::formula::PCTLFormula<double>* formula;
mrmc::formula::PctlFormula<double>* formula;
}; };
} // namespace parser } // namespace parser

Write Preview
Loading…
Cancel
Save