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

Adapted abstract formulas to new structure

main
Lanchid 12 years ago
parent
38652f44e4
commit
f1383964f0
20 changed files with 527 additions and 1126 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. 2
      src/formula/abstract/AbstractFormula.h
  2. 109
      src/formula/abstract/And.h
  3. 57
      src/formula/abstract/Ap.h
  4. 95
      src/formula/abstract/BoundedEventually.h
  5. 145
      src/formula/abstract/BoundedNaryUntil.h
  6. 130
      src/formula/abstract/BoundedUntil.h
  7. 92
      src/formula/abstract/Eventually.h
  8. 92
      src/formula/abstract/Globally.h
  9. 92
      src/formula/abstract/Next.h
  10. 91
      src/formula/abstract/Not.h
  11. 14
      src/formula/abstract/OptimizingOperator.h
  12. 125
      src/formula/abstract/Or.h
  13. 71
      src/formula/abstract/PathBoundOperator.h
  14. 97
      src/formula/abstract/PathNoBoundOperator.h
  15. 80
      src/formula/abstract/ProbabilisticBoundOperator.h
  16. 29
      src/formula/abstract/ProbabilisticNoBoundOperator.h
  17. 85
      src/formula/abstract/StateBoundOperator.h
  18. 61
      src/formula/abstract/StateNoBoundOperator.h
  19. 21
      src/formula/abstract/TimeBoundedOperator.h
  20. 123
      src/formula/abstract/Until.h

2
src/formula/abstract/AbstractFormula.h
View File

@ -32,7 +32,7 @@ namespace abstract {
* @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
* AbstractPathFormula and AbstractStateFormula offer the method clone().
* AbstractFormula and AbstractFormula offer the method clone().
* *
* This is the base class for every formula class in every logic. * This is the base class for every formula class in every logic.
*/ */

109
src/formula/abstract/And.h
View File

@ -15,26 +15,7 @@
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class And;
/*!
* @brief Interface class for model checkers that support And.
*
* All model checkers that support the formula class And must inherit
* this pure virtual class.
*/
template <class T>
class IAndModelChecker {
public:
/*!
* @brief Evaluates And formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -48,7 +29,7 @@ class IAndModelChecker {
* 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 AbstractStateFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
@ -91,12 +72,35 @@ public:
} }
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = "(";
result += left->toString();
result += " & ";
result += right->toString();
result += ")";
return result;
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
protected:
/*! /*!
* Sets the left child node. * Sets the left child node.
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(AbstractStateFormula<T>* newLeft) {
void setLeft(AbstractFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -105,82 +109,31 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(AbstractStateFormula<T>* newRight) {
void setRight(AbstractFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const AbstractStateFormula<T>& getLeft() const {
const AbstractFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const AbstractStateFormula<T>& getRight() const {
const AbstractFormula<T>& getRight() const {
return *right; return *right;
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
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 AbstractStateFormula<T>* clone() const {
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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
private: private:
AbstractFormula<T>* left; AbstractFormula<T>* left;
AbstractFormula<T>* right; AbstractFormula<T>* right;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm

57
src/formula/abstract/Ap.h
View File

@ -5,35 +5,16 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_AP_H_
#define STORM_FORMULA_AP_H_
#ifndef STORM_FORMULA_ABSTRACT_AP_H_
#define STORM_FORMULA_ABSTRACT_AP_H_
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class Ap;
/*!
* @brief Interface class for model checkers that support Ap.
*
* All model checkers that support the formula class Ap must inherit
* this pure virtual class.
*/
template <class T>
class IApModelChecker {
public:
/*!
* @brief Evaluates Ap formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -41,11 +22,11 @@ class IApModelChecker {
* *
* This class represents the leaves in the formula tree. * This class represents the leaves in the formula tree.
* *
* @see AbstractStateFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Ap : public AbstractStateFormula<T> {
class Ap : public AbstractFormula<T> {
public: public:
/*! /*!
@ -80,28 +61,6 @@ public:
return getAp(); return getAp();
} }
/*!
* Clones the called object.
*
* @returns a new Ap-object that is identical the called object.
*/
virtual AbstractStateFormula<T>* clone() const {
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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
/*! /*!
* @brief Checks if all subtrees conform to some logic. * @brief Checks if all subtrees conform to some logic.
* *
@ -118,8 +77,10 @@ private:
std::string ap; std::string ap;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_AP_H_ */
#endif /* STORM_FORMULA_ABSTRACT_ABSTRCT_AP_H_ */

95
src/formula/abstract/BoundedEventually.h
View File

@ -5,11 +5,10 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
@ -19,25 +18,7 @@ namespace storm {
namespace formula { namespace formula {
template <class T> class BoundedEventually;
/*!
* @brief Interface class for model checkers that support BoundedEventually.
*
* All model checkers that support the formula class BoundedEventually must inherit
* this pure virtual class.
*/
template <class T>
class IBoundedEventuallyModelChecker {
public:
/*!
* @brief Evaluates BoundedEventually formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -51,11 +32,11 @@ class IBoundedEventuallyModelChecker {
* 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 AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class BoundedEventually : public AbstractPathFormula<T> {
class BoundedEventually : public AbstractFormula<T> {
public: public:
/*! /*!
@ -72,7 +53,7 @@ public:
* @param child The child formula subtree * @param child The child formula subtree
* @param bound The maximal number of steps * @param bound The maximal number of steps
*/ */
BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) {
BoundedEventually(AbstractFormula<T>* child, uint_fast64_t bound) {
this->child = child; this->child = child;
this->bound = bound; this->bound = bound;
} }
@ -89,21 +70,6 @@ public:
} }
} }
/*!
* @returns the child node
*/
const AbstractStateFormula<T>& getChild() const {
return *child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
/*! /*!
* @returns the maximally allowed number of steps for the bounded until operator * @returns the maximally allowed number of steps for the bounded until operator
*/ */
@ -132,52 +98,41 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new BoundedUntil-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
BoundedEventually<T>* result = new BoundedEventually<T>();
result->setBound(bound);
if (child != nullptr) {
result->setChild(child->clone());
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
} }
protected:
/*! /*!
* 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.
* @returns the child node
*/ */
virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
const AbstractFormula<T>& getChild() const {
return *child;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
*
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* Sets the subtree
* @param child the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
void setChild(AbstractFormula<T>* child) {
this->child = child;
} }
private: private:
AbstractStateFormula<T>* child;
AbstractFormula<T>* child;
uint_fast64_t bound; uint_fast64_t bound;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_ */

145
src/formula/abstract/BoundedNaryUntil.h
View File

@ -5,11 +5,10 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_
#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_
#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
#define STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
#include <vector> #include <vector>
@ -19,26 +18,7 @@
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class BoundedNaryUntil;
/*!
* @brief Interface class for model checkers that support BoundedNaryUntil.
*
* All model checkers that support the formula class BoundedNaryUntil must inherit
* this pure virtual class.
*/
template <class T>
class IBoundedNaryUntilModelChecker {
public:
/*!
* @brief Evaluates BoundedNaryUntil formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -56,11 +36,11 @@ class IBoundedNaryUntilModelChecker {
* 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 AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class BoundedNaryUntil : public AbstractPathFormula<T> {
class BoundedNaryUntil : public AbstractFormula<T> {
public: public:
/*! /*!
@ -68,7 +48,7 @@ public:
*/ */
BoundedNaryUntil() { BoundedNaryUntil() {
this->left = nullptr; this->left = nullptr;
this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
this->right = new std::vector<std::tuple<AbstractFormula<T>*,T,T>>();
} }
/*! /*!
@ -77,7 +57,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
*/ */
BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) {
BoundedNaryUntil(AbstractFormula<T>* left, std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -97,43 +77,6 @@ public:
} }
} }
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
void setRight(std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newRight) {
right = newRight;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void addRight(AbstractStateFormula<T>* newRight, T upperBound, T lowerBound) {
this->right->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(newRight, upperBound, lowerBound));
}
/*!
* @returns a pointer to the left child node
*/
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child nodes.
*/
const std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>& getRight() const {
return *right;
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -148,61 +91,65 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if all subtrees conform to some logic.
* *
* @returns a new BoundedNaryUntil-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
bool res = checker.conforms(this->left);
for (auto it = this->right->begin(); it != this->right->end(); ++it) { for (auto it = this->right->begin(); it != this->right->end(); ++it) {
newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
res &= checker.conforms(std::get<0>(*it));
}
return res;
} }
result->setRight(newright);
protected:
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(AbstractFormula<T>* newLeft) {
left = newLeft;
} }
return result;
void setRight(std::vector<std::tuple<AbstractFormula<T>*,T,T>>* newRight) {
right = newRight;
} }
/*! /*!
* 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.
* Sets the right child node.
* *
* @returns A vector indicating the probability that the formula holds for each state.
* @param newRight the new right child.
*/ */
virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
void addRight(AbstractFormula<T>* newRight, T upperBound, T lowerBound) {
this->right->push_back(std::tuple<AbstractFormula<T>*,T,T>(newRight, upperBound, lowerBound));
} }
/*! /*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
* @returns a pointer to the left child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
bool res = checker.conforms(this->left);
for (auto it = this->right->begin(); it != this->right->end(); ++it) {
res &= checker.conforms(std::get<0>(*it));
const AbstractFormula<T>& getLeft() const {
return *left;
} }
return res;
/*!
* @returns a pointer to the right child nodes.
*/
const std::vector<std::tuple<AbstractFormula<T>*,T,T>>& getRight() const {
return *right;
} }
private: private:
AbstractStateFormula<T>* left;
std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right;
AbstractFormula<T>* left;
std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */
#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_ */

130
src/formula/abstract/BoundedUntil.h
View File

@ -5,37 +5,17 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
#define STORM_FORMULA_BOUNDEDUNTIL_H_
#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
#define STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class BoundedUntil;
/*!
* @brief Interface class for model checkers that support BoundedUntil.
*
* All model checkers that support the formula class BoundedUntil must inherit
* this pure virtual class.
*/
template <class T>
class IBoundedUntilModelChecker {
public:
/*!
* @brief Evaluates BoundedUntil formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -50,11 +30,11 @@ class IBoundedUntilModelChecker {
* 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 AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class BoundedUntil : public AbstractPathFormula<T> {
class BoundedUntil : public AbstractFormula<T> {
public: public:
/*! /*!
@ -73,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(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
BoundedUntil(AbstractFormula<T>* left, AbstractFormula<T>* right,
uint_fast64_t bound) { uint_fast64_t bound) {
this->left = left; this->left = left;
this->right = right; this->right = right;
@ -95,38 +75,6 @@ public:
} }
} }
/*!
* Sets the left child node.
*
* @param newLeft the new left child.
*/
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
/*!
* Sets the right child node.
*
* @param newRight the new right child.
*/
void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const AbstractStateFormula<T>& getRight() const {
return *right;
}
/*! /*!
* @returns the maximally allowed number of steps for the bounded until operator * @returns the maximally allowed number of steps for the bounded until operator
*/ */
@ -156,56 +104,58 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if all subtrees conform to some logic.
* *
* @returns a new BoundedUntil-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil<T>();
result->setBound(bound);
if (left != NULL) {
result->setLeft(left->clone());
}
if (right != NULL) {
result->setRight(right->clone());
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
} }
protected:
/*! /*!
* 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.
* Sets the left child node.
* *
* @returns A vector indicating the probability that the formula holds for each state.
* @param newLeft the new left child.
*/ */
virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
void setLeft(AbstractFormula<T>* newLeft) {
left = newLeft;
} }
/*! /*!
* @brief Checks if all subtrees conform to some logic.
* Sets the right child node.
* *
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
* @param newRight the new right child.
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
void setRight(AbstractFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const AbstractFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const AbstractFormula<T>& getRight() const {
return *right;
} }
private: private:
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
AbstractFormula<T>* left;
AbstractFormula<T>* right;
uint_fast64_t bound; uint_fast64_t bound;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_ */

92
src/formula/abstract/Eventually.h
View File

@ -5,36 +5,17 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_EVENTUALLY_H_
#define STORM_FORMULA_EVENTUALLY_H_
#ifndef STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
#define STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class Eventually;
/*!
* @brief Interface class for model checkers that support Eventually.
*
* All model checkers that support the formula class Eventually must inherit
* this pure virtual class.
*/
template <class T>
class IEventuallyModelChecker {
public:
/*!
* @brief Evaluates Eventually formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -48,11 +29,11 @@ class IEventuallyModelChecker {
* 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 nullptr before deletion) * (this behavior can be prevented by setting them to nullptr before deletion)
* *
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Eventually : public AbstractPathFormula<T> {
class Eventually : public AbstractFormula<T> {
public: public:
/*! /*!
@ -67,7 +48,7 @@ public:
* *
* @param child The child node * @param child The child node
*/ */
Eventually(AbstractStateFormula<T>* child) {
Eventually(AbstractFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -83,21 +64,6 @@ public:
} }
} }
/*!
* @returns the child node
*/
const AbstractStateFormula<T>& getChild() const {
return *child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -108,49 +74,39 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new Eventually-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
Eventually<T>* result = new Eventually<T>();
if (child != nullptr) {
result->setChild(child);
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
} }
protected:
/*! /*!
* 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.
* @returns the child node
*/ */
virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
const AbstractFormula<T>& getChild() const {
return *child;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
*
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* Sets the subtree
* @param child the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
void setChild(AbstractFormula<T>* child) {
this->child = child;
} }
private: private:
AbstractStateFormula<T>* child;
AbstractFormula<T>* child;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_EVENTUALLY_H_ */
#endif /* STORM_FORMULA_ABSTRACT_EVENTUALLY_H_ */

92
src/formula/abstract/Globally.h
View File

@ -5,11 +5,10 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_GLOBALLY_H_
#define STORM_FORMULA_GLOBALLY_H_
#ifndef STORM_FORMULA_ABSTRACT_GLOBALLY_H_
#define STORM_FORMULA_ABSTRACT_GLOBALLY_H_
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
@ -17,25 +16,7 @@ namespace storm {
namespace formula { namespace formula {
template <class T> class Globally;
/*!
* @brief Interface class for model checkers that support Globally.
*
* All model checkers that support the formula class Globally must inherit
* this pure virtual class.
*/
template <class T>
class IGloballyModelChecker {
public:
/*!
* @brief Evaluates Globally formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -49,11 +30,11 @@ class IGloballyModelChecker {
* 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 nullptr before deletion) * (this behavior can be prevented by setting them to nullptr before deletion)
* *
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Globally : public AbstractPathFormula<T> {
class Globally : public AbstractFormula<T> {
public: public:
/*! /*!
@ -68,7 +49,7 @@ public:
* *
* @param child The child node * @param child The child node
*/ */
Globally(AbstractStateFormula<T>* child) {
Globally(AbstractFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -84,21 +65,6 @@ public:
} }
} }
/*!
* @returns the child node
*/
const AbstractStateFormula<T>& getChild() const {
return *child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -109,49 +75,39 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new Globally-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != nullptr) {
result->setChild(child);
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
} }
protected:
/*! /*!
* 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.
* @returns the child node
*/ */
virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
const AbstractFormula<T>& getChild() const {
return *child;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
*
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* Sets the subtree
* @param child the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
void setChild(AbstractFormula<T>* child) {
this->child = child;
} }
private: private:
AbstractStateFormula<T>* child;
AbstractFormula<T>* child;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_GLOBALLY_H_ */
#endif /* STORM_FORMULA_ABSTRACT_GLOBALLY_H_ */

92
src/formula/abstract/Next.h
View File

@ -5,36 +5,17 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_NEXT_H_
#define STORM_FORMULA_NEXT_H_
#ifndef STORM_FORMULA_ABSTRACT_NEXT_H_
#define STORM_FORMULA_ABSTRACT_NEXT_H_
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class Next;
/*!
* @brief Interface class for model checkers that support Next.
*
* All model checkers that support the formula class Next must inherit
* this pure virtual class.
*/
template <class T>
class INextModelChecker {
public:
/*!
* @brief Evaluates Next formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -48,11 +29,11 @@ class INextModelChecker {
* 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 AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Next : public AbstractPathFormula<T> {
class Next : public AbstractFormula<T> {
public: public:
/*! /*!
@ -67,7 +48,7 @@ public:
* *
* @param child The child node * @param child The child node
*/ */
Next(AbstractStateFormula<T>* child) {
Next(AbstractFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -83,21 +64,6 @@ public:
} }
} }
/*!
* @returns the child node
*/
const AbstractStateFormula<T>& getChild() const {
return *child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -110,49 +76,39 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new BoundedUntil-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
} }
protected:
/*! /*!
* 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.
* @returns the child node
*/ */
virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
const AbstractFormula<T>& getChild() const {
return *child;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
*
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* Sets the subtree
* @param child the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
void setChild(AbstractFormula<T>* child) {
this->child = child;
} }
private: private:
AbstractStateFormula<T>* child;
AbstractFormula<T>* child;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_NEXT_H_ */
#endif /* STORM_FORMULA_ABSTRACT_NEXT_H_ */

91
src/formula/abstract/Not.h
View File

@ -5,10 +5,10 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_NOT_H_
#define STORM_FORMULA_NOT_H_
#ifndef STORM_FORMULA_ABSTRACT_NOT_H_
#define STORM_FORMULA_ABSTRACT_NOT_H_
#include "AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
@ -16,25 +16,7 @@ namespace storm {
namespace formula { namespace formula {
template <class T> class Not;
/*!
* @brief Interface class for model checkers that support Not.
*
* All model checkers that support the formula class Not must inherit
* this pure virtual class.
*/
template <class T>
class INotModelChecker {
public:
/*!
* @brief Evaluates Not formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -45,11 +27,11 @@ class INotModelChecker {
* 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 AbstractStateFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Not : public AbstractStateFormula<T> {
class Not : public AbstractFormula<T> {
public: public:
/*! /*!
@ -63,7 +45,7 @@ public:
* Constructor * Constructor
* @param child The child node * @param child The child node
*/ */
Not(AbstractStateFormula<T>* child) {
Not(AbstractFormula<T>* child) {
this->child = child; this->child = child;
} }
@ -79,21 +61,6 @@ public:
} }
} }
/*!
* @returns The child node
*/
const AbstractStateFormula<T>& getChild() const {
return *child;
}
/*!
* Sets the subtree
* @param child the new child node
*/
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -104,49 +71,39 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new AND-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child->clone());
}
return result;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
} }
protected:
/*! /*!
* 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.
* @returns The child node
*/ */
virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
const AbstractFormula<T>& getChild() const {
return *child;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
*
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* Sets the subtree
* @param child the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
void setChild(AbstractFormula<T>* child) {
this->child = child;
} }
private: private:
AbstractStateFormula<T>* child;
AbstractFormula<T>* child;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_NOT_H_ */
#endif /* STORM_FORMULA_ABSTRACT_NOT_H_ */

14
src/formula/abstract/OptimizingOperator.h
View File

@ -1,10 +1,12 @@
#ifndef STORM_FORMULA_OPTIMIZINGOPERATOR_H_
#define STORM_FORMULA_OPTIMIZINGOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
namespace storm { namespace storm {
namespace formula { namespace formula {
namespace abstract {
class OptimizingOperator { class OptimizingOperator {
public: public:
/*! /*!
@ -49,8 +51,10 @@ private:
bool minimumOperator; bool minimumOperator;
}; };
} /* namespace formula */
} //namespace abstract
} //namespace formula
} /* namespace storm */
} //namespace storm
#endif /* STORM_FORMULA_OPTIMIZINGOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_ */

125
src/formula/abstract/Or.h
View File

@ -5,34 +5,15 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
#ifndef STORM_FORMULA_ABSTRACT_OR_H_
#define STORM_FORMULA_ABSTRACT_OR_H_
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class Or;
/*!
* @brief Interface class for model checkers that support Or.
*
* All model checkers that support the formula class Or must inherit
* this pure virtual class.
*/
template <class T>
class IOrModelChecker {
public:
/*!
* @brief Evaluates Or formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -46,11 +27,11 @@ class IOrModelChecker {
* 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 AbstractStateFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Or : public AbstractStateFormula<T> {
class Or : public AbstractFormula<T> {
public: public:
/*! /*!
@ -69,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
*/ */
Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
Or(AbstractFormula<T>* left, AbstractFormula<T>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -89,12 +70,35 @@ public:
} }
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = "(";
result += left->toString();
result += " | ";
result += right->toString();
result += ")";
return result;
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
protected:
/*! /*!
* Sets the left child node. * Sets the left child node.
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(AbstractStateFormula<T>* newLeft) {
void setLeft(AbstractFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -103,84 +107,33 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(AbstractStateFormula<T>* newRight) {
void setRight(AbstractFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const AbstractStateFormula<T>& getLeft() const {
const AbstractFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const AbstractStateFormula<T>& getRight() const {
const AbstractFormula<T>& getRight() const {
return *right; return *right;
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
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 AbstractStateFormula<T>* clone() const {
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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
private: private:
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
AbstractFormula<T>* left;
AbstractFormula<T>* right;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_OR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_OR_H_ */

71
src/formula/abstract/PathBoundOperator.h
View File

@ -5,14 +5,14 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_PATHBOUNDOPERATOR_H_
#define STORM_FORMULA_PATHBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/formula/OptimizingOperator.h"
#include "src/formula/abstract/OptimizingOperator.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
#include "src/utility/ConstTemplates.h" #include "src/utility/ConstTemplates.h"
@ -21,6 +21,8 @@ namespace storm {
namespace formula { namespace formula {
namespace abstract {
template <class T> class PathBoundOperator; template <class T> class PathBoundOperator;
/*! /*!
@ -38,14 +40,14 @@ template <class T> class PathBoundOperator;
* (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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator * @see ProbabilisticNoBoundsOperator
* @see AbstractFormula * @see AbstractFormula
*/ */
template<class T> template<class T>
class PathBoundOperator : public AbstractStateFormula<T>, public OptimizingOperator {
class PathBoundOperator : public AbstractFormula<T>, public OptimizingOperator {
public: public:
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@ -57,7 +59,7 @@ public:
* @param bound The bound for the probability * @param bound The bound for the probability
* @param pathFormula The child node * @param pathFormula The child node
*/ */
PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
// Intentionally left empty // Intentionally left empty
} }
@ -70,7 +72,7 @@ public:
* @param pathFormula The child node * @param pathFormula The child node
* @param minimumOperator Indicator, if operator should be minimum or maximum operator. * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
*/ */
PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) { : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) {
// Intentionally left empty // Intentionally left empty
} }
@ -87,22 +89,6 @@ public:
} }
} }
/*!
* @returns the child node (representation of a Abstract path formula)
*/
const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
/*! /*!
* @returns the comparison relation * @returns the comparison relation
*/ */
@ -159,15 +145,6 @@ public:
} }
} }
/*!
* 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 AbstractStateFormula<T>* clone() const = 0;
/*! /*!
* @brief Checks if the subtree conforms to some logic. * @brief Checks if the subtree conforms to some logic.
* *
@ -178,14 +155,34 @@ public:
return checker.conforms(this->pathFormula); return checker.conforms(this->pathFormula);
} }
protected:
/*!
* @returns the child node (representation of a Abstract path formula)
*/
const AbstractFormula<T>& getPathFormula () const {
return *pathFormula;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(AbstractFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
private: private:
ComparisonType comparisonOperator; ComparisonType comparisonOperator;
T bound; T bound;
AbstractPathFormula<T>* pathFormula;
AbstractFormula<T>* pathFormula;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_PATHBOUNDOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_ */

97
src/formula/abstract/PathNoBoundOperator.h
View File

@ -5,13 +5,13 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
#define STORM_FORMULA_NOBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
#include "src/formula/AbstractFormula.h"
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/formula/OptimizingOperator.h"
#include "src/formula/abstract/OptimizingOperator.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
@ -19,26 +19,7 @@ namespace storm {
namespace formula { namespace formula {
template <class T> class PathNoBoundOperator;
/*!
* @brief Interface class for model checkers that support PathNoBoundOperator.
*
* All model checkers that support the formula class NoBoundOperator must inherit
* this pure virtual class.
*/
template <class T>
class IPathNoBoundOperatorModelChecker {
public:
/*!
* @brief Evaluates NoBoundOperator formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkPathNoBoundOperator(const PathNoBoundOperator<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
* Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
@ -63,8 +44,8 @@ class IPathNoBoundOperatorModelChecker {
* (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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator * @see ProbabilisticIntervalOperator
* @see AbstractFormula * @see AbstractFormula
@ -84,7 +65,7 @@ public:
* *
* @param pathFormula The child node. * @param pathFormula The child node.
*/ */
PathNoBoundOperator(AbstractPathFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
PathNoBoundOperator(AbstractFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
this->pathFormula = pathFormula; this->pathFormula = pathFormula;
} }
@ -95,7 +76,7 @@ public:
* @param minimumOperator A flag indicating whether this operator is a minimizing or a * @param minimumOperator A flag indicating whether this operator is a minimizing or a
* maximizing operator. * maximizing operator.
*/ */
PathNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
PathNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator)
: optimalityOperator(true), minimumOperator(minimumOperator) { : optimalityOperator(true), minimumOperator(minimumOperator) {
this->pathFormula = pathFormula; this->pathFormula = pathFormula;
} }
@ -109,37 +90,6 @@ public:
} }
} }
/*!
* @returns the child node (representation of a Abstract path formula)
*/
const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
/*!
* 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 all states that satisfy the formula represented by the called object.
*/
virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IPathNoBoundOperatorModelChecker>()->checkPathNoBoundOperator(*this);
}
/*! /*!
* @returns a string representation of the formula * @returns a string representation of the formula
*/ */
@ -186,8 +136,25 @@ public:
return optimalityOperator && minimumOperator; return optimalityOperator && minimumOperator;
} }
protected:
/*!
* @returns the child node (representation of a Abstract path formula)
*/
const AbstractFormula<T>& getPathFormula () const {
return *pathFormula;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(AbstractFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
private: private:
AbstractPathFormula<T>* pathFormula;
AbstractFormula<T>* pathFormula;
// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
// over a nondeterministic model. // over a nondeterministic model.
@ -198,8 +165,10 @@ private:
bool minimumOperator; bool minimumOperator;
}; };
} /* namespace formula */
} //namespace abstract
} //namespace formula
} /* namespace storm */
} //namespace storm
#endif /* STORM_FORMULA_NOBOUNDOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_ */

80
src/formula/abstract/ProbabilisticBoundOperator.h
View File

@ -5,31 +5,17 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
#include "AbstractStateFormula.h"
#include "AbstractPathFormula.h"
#include "src/formula/PathBoundOperator.h"
#include "src/formula/OptimizingOperator.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/abstract/PathBoundOperator.h"
#include "src/formula/abstract/OptimizingOperator.h"
#include "utility/ConstTemplates.h" #include "utility/ConstTemplates.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class ProbabilisticBoundOperator;
/*!
* @brief Interface class for model checkers that support ProbabilisticBoundOperator.
*
* All model checkers that support the formula class PathBoundOperator must inherit
* this pure virtual class.
*/
template <class T>
class IProbabilisticBoundOperatorModelChecker {
public:
virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -46,8 +32,8 @@ class IProbabilisticBoundOperatorModelChecker {
* (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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator * @see ProbabilisticNoBoundsOperator
* @see AbstractFormula * @see AbstractFormula
@ -73,56 +59,44 @@ public:
* @param pathFormula The child node * @param pathFormula The child node
*/ */
ProbabilisticBoundOperator( ProbabilisticBoundOperator(
typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula)
: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) { : PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
// Intentionally left empty // Intentionally left empty
} }
/*!
* Constructor
*
* @param comparisonRelation
* @param bound
* @param pathFormula
* @param minimumOperator
*/
ProbabilisticBoundOperator( ProbabilisticBoundOperator(
typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){ : PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
// Intentionally left empty // Intentionally left empty
} }
/*! /*!
* @returns a string representation of the formula
* Destructor
*/ */
virtual std::string toString() const {
std::string result = "P ";
result += PathBoundOperator<T>::toString();
return result;
virtual ~ProbabilisticBoundOperator() {
// Intentionally left empty
} }
/*! /*!
* 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.
* @returns a string representation of the formula
*/ */
virtual AbstractStateFormula<T>* clone() const {
ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
result->setComparisonOperator(this->getComparisonOperator());
result->setBound(this->getBound());
result->setPathFormula(this->getPathFormula().clone());
virtual std::string toString() const {
std::string result = "P ";
result += PathBoundOperator<T>::toString();
return result; 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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
}
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_ */

29
src/formula/abstract/ProbabilisticNoBoundOperator.h
View File

@ -5,15 +5,16 @@
* Author: thomas * Author: thomas
*/ */
#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
#include "AbstractFormula.h" #include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "PathNoBoundOperator.h" #include "PathNoBoundOperator.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
namespace abstract {
/*! /*!
* @brief * @brief
@ -39,8 +40,8 @@ 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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator * @see ProbabilisticIntervalOperator
* @see AbstractFormula * @see AbstractFormula
@ -60,7 +61,14 @@ public:
* *
* @param pathFormula The child node. * @param pathFormula The child node.
*/ */
ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}
/*!
* Destructor
*/
virtual ~ProbabilisticNoBoundOperator() {
// Intentionally left empty // Intentionally left empty
} }
@ -69,7 +77,7 @@ public:
* *
* @param pathFormula The child node. * @param pathFormula The child node.
*/ */
ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
// Intentionally left empty // Intentionally left empty
} }
@ -83,7 +91,8 @@ public:
} }
}; };
} /* namespace formula */
} /* namespace storm */
} //namespace abstract
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_ */

85
src/formula/abstract/StateBoundOperator.h
View File

@ -5,31 +5,18 @@
* Author: Christian Dehnert * Author: Christian Dehnert
*/ */
#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_
#define STORM_FORMULA_STATEBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/AbstractModelChecker.h" #include "src/modelchecker/AbstractModelChecker.h"
#include "src/utility/ConstTemplates.h" #include "src/utility/ConstTemplates.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class StateBoundOperator;
/*!
* @brief Interface class for model checkers that support StateBoundOperator.
*
* All model checkers that support the formula class StateBoundOperator must inherit
* this pure virtual class.
*/
template <class T>
class IStateBoundOperatorModelChecker {
public:
virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -46,14 +33,14 @@ class IStateBoundOperatorModelChecker {
* (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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see ProbabilisticOperator * @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator * @see ProbabilisticNoBoundsOperator
* @see AbstractFormula * @see AbstractFormula
*/ */
template<class T> template<class T>
class StateBoundOperator : public AbstractStateFormula<T> {
class StateBoundOperator : public AbstractFormula<T> {
public: public:
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@ -65,7 +52,7 @@ public:
* @param bound The bound for the probability * @param bound The bound for the probability
* @param stateFormula The child node * @param stateFormula The child node
*/ */
StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula)
StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* stateFormula)
: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
// Intentionally left empty // Intentionally left empty
} }
@ -82,22 +69,6 @@ public:
} }
} }
/*!
* @returns the child node (representation of a Abstract state formula)
*/
const AbstractStateFormula<T>& getStateFormula () const {
return *stateFormula;
}
/*!
* Sets the child node
*
* @param stateFormula the state formula that becomes the new child node
*/
void setStateFormula(AbstractStateFormula<T>* stateFormula) {
this->stateFormula = stateFormula;
}
/*! /*!
* @returns the comparison relation * @returns the comparison relation
*/ */
@ -154,44 +125,40 @@ public:
} }
/*! /*!
* Clones the called object.
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
* @brief Checks if the subtree conforms to some logic.
* *
* @returns a new AND-object that is identical the called object.
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
*/ */
virtual AbstractStateFormula<T>* clone() const = 0;
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->stateFormula);
}
protected:
/*! /*!
* 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.
* @returns the child node (representation of a Abstract state formula)
*/ */
virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this);
const AbstractFormula<T>& getStateFormula () const {
return *stateFormula;
} }
/*! /*!
* @brief Checks if the subtree conforms to some logic.
* Sets the child node
* *
* @param checker Formula checker object.
* @return true iff the subtree conforms to some logic.
* @param stateFormula the state formula that becomes the new child node
*/ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->stateFormula);
void setStateFormula(AbstractFormula<T>* stateFormula) {
this->stateFormula = stateFormula;
} }
private: private:
ComparisonType comparisonOperator; ComparisonType comparisonOperator;
T bound; T bound;
AbstractStateFormula<T>* stateFormula;
AbstractFormula<T>* stateFormula;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */
#endif /* STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_ */

61
src/formula/abstract/StateNoBoundOperator.h
View File

@ -5,38 +5,17 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_
#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
#include "src/formula/AbstractFormula.h"
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h" #include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class StateNoBoundOperator;
/*!
* @brief Interface class for model checkers that support PathNoBoundOperator.
*
* All model checkers that support the formula class NoBoundOperator must inherit
* this pure virtual class.
*/
template <class T>
class IStateNoBoundOperatorModelChecker {
public:
/*!
* @brief Evaluates NoBoundOperator formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkStateNoBoundOperator(const StateNoBoundOperator<T>& obj) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -62,8 +41,8 @@ class IStateNoBoundOperatorModelChecker {
* (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 AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see SteadyStateNoBoundOperator * @see SteadyStateNoBoundOperator
* @see AbstractFormula * @see AbstractFormula
*/ */
@ -80,7 +59,7 @@ public:
/*! /*!
* Constructor * Constructor
*/ */
StateNoBoundOperator(AbstractStateFormula<T>* stateFormula) {
StateNoBoundOperator(AbstractFormula<T>* stateFormula) {
this->stateFormula = stateFormula; this->stateFormula = stateFormula;
} }
@ -95,14 +74,6 @@ public:
} }
} }
const AbstractStateFormula<T>& getStateFormula() const {
return *(this->stateFormula);
}
void setStateFormula(AbstractStateFormula<T>* stateFormula) {
this->stateFormula = stateFormula;
}
/*! /*!
* Calls the model checker to check this formula. * Calls the model checker to check this formula.
* Needed to infer the correct type of formula class. * Needed to infer the correct type of formula class.
@ -139,10 +110,20 @@ public:
return checker.conforms(this->stateFormula); return checker.conforms(this->stateFormula);
} }
protected:
const AbstractFormula<T>& getStateFormula() const {
return *(this->stateFormula);
}
void setStateFormula(AbstractFormula<T>* stateFormula) {
this->stateFormula = stateFormula;
}
private: private:
AbstractStateFormula<T>* stateFormula;
AbstractFormula<T>* stateFormula;
}; };
} /* namespace formula */
} /* namespace storm */
#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */
} //namespace abstract
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ */

21
src/formula/abstract/TimeBoundedOperator.h
View File

@ -5,16 +5,17 @@
* Author: thomas * Author: thomas
*/ */
#ifndef TIMEBOUNDEDOPERATOR_H_
#define TIMEBOUNDEDOPERATOR_H_
#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
#include <limits> #include <limits>
#include "AbstractPathFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "exceptions/InvalidArgumentException.h" #include "exceptions/InvalidArgumentException.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
namespace abstract {
/*! /*!
* @brief * @brief
@ -24,12 +25,12 @@ namespace formula {
* This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class. * This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class.
* *
* *
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template<class T> template<class T>
class TimeBoundedOperator: public storm::formula::AbstractPathFormula<T> {
class TimeBoundedOperator: public storm::formula::AbstractFormula<T> {
public: public:
/** /**
* Constructor * Constructor
@ -104,6 +105,8 @@ private:
T lowerBound, upperBound; T lowerBound, upperBound;
}; };
} /* namespace formula */
} /* namespace storm */
#endif /* TIMEBOUNDEDOPERATOR_H_ */
} //namespace abstract
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_ */

123
src/formula/abstract/Until.h
View File

@ -5,35 +5,16 @@
* Author: Thomas Heinemann * Author: Thomas Heinemann
*/ */
#ifndef STORM_FORMULA_UNTIL_H_
#define STORM_FORMULA_UNTIL_H_
#ifndef STORM_FORMULA_ABSTRACT_UNTIL_H_
#define STORM_FORMULA_ABSTRACT_UNTIL_H_
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/abstract/AbstractFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
namespace storm { namespace storm {
namespace formula { namespace formula {
template <class T> class Until;
/*!
* @brief Interface class for model checkers that support Until.
*
* All model checkers that support the formula class Until must inherit
* this pure virtual class.
*/
template <class T>
class IUntilModelChecker {
public:
/*!
* @brief Evaluates Until formula within a model checker.
*
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
};
namespace abstract {
/*! /*!
* @brief * @brief
@ -48,11 +29,11 @@ class IUntilModelChecker {
* 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 AbstractPathFormula
* @see AbstractFormula
* @see AbstractFormula * @see AbstractFormula
*/ */
template <class T> template <class T>
class Until : public AbstractPathFormula<T> {
class Until : public AbstractFormula<T> {
public: public:
/*! /*!
@ -69,7 +50,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(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
Until(AbstractFormula<T>* left, AbstractFormula<T>* right) {
this->left = left; this->left = left;
this->right = right; this->right = right;
} }
@ -89,12 +70,33 @@ public:
} }
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = left->toString();
result += " U ";
result += right->toString();
return result;
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
protected:
/*! /*!
* Sets the left child node. * Sets the left child node.
* *
* @param newLeft the new left child. * @param newLeft the new left child.
*/ */
void setLeft(AbstractStateFormula<T>* newLeft) {
void setLeft(AbstractFormula<T>* newLeft) {
left = newLeft; left = newLeft;
} }
@ -103,82 +105,33 @@ public:
* *
* @param newRight the new right child. * @param newRight the new right child.
*/ */
void setRight(AbstractStateFormula<T>* newRight) {
void setRight(AbstractFormula<T>* newRight) {
right = newRight; right = newRight;
} }
/*! /*!
* @returns a pointer to the left child node * @returns a pointer to the left child node
*/ */
const AbstractStateFormula<T>& getLeft() const {
const AbstractFormula<T>& getLeft() const {
return *left; return *left;
} }
/*! /*!
* @returns a pointer to the right child node * @returns a pointer to the right child node
*/ */
const AbstractStateFormula<T>& getRight() const {
const AbstractFormula<T>& getRight() const {
return *right; return *right;
} }
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = left->toString();
result += " U ";
result += right->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 BoundedUntil-object that is identical the called object.
*/
virtual AbstractPathFormula<T>* clone() const {
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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
}
/*!
* @brief Checks if all subtrees conform to some logic.
*
* @param checker Formula checker object.
* @return true iff all subtrees conform to some logic.
*/
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
private: private:
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
AbstractFormula<T>* left;
AbstractFormula<T>* right;
}; };
} //namespace abstract
} //namespace formula } //namespace formula
} //namespace storm } //namespace storm
#endif /* STORM_FORMULA_UNTIL_H_ */
#endif /* STORM_FORMULA_ABSTRACT_UNTIL_H_ */
Write Preview
Loading…
Cancel
Save