diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
new file mode 100644
index 000000000..8bd8b8782
--- /dev/null
+++ b/src/formula/AbstractFormula.h
@@ -0,0 +1,65 @@
+/*
+ * Abstractformula.h
+ *
+ * Created on: 19.10.2012
+ * Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_AbstractFORMULA_H_
+#define STORM_FORMULA_AbstractFORMULA_H_
+
+#include <string>
+
+namespace storm { namespace formula {
+template <class T> class AbstractFormula;
+}}
+
+#include "src/modelChecker/AbstractModelChecker.h"
+
+namespace storm {
+namespace formula {
+
+
+//abstract
+/*!
+ * @brief
+ * Abstract base class for Abstract formulas in general.
+ *
+ * @attention This class is abstract.
+ * @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
+ * AbstractPathFormula and AbstractStateFormula offer the method clone().
+ */
+template <class T>
+class AbstractFormula {
+
+public:
+ /*!
+ * virtual destructor
+ */
+ virtual ~AbstractFormula() { }
+
+ /*!
+ * @note This function is not implemented in this class.
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const = 0;
+
+ template <template <class Type> class MC>
+ const MC<T>* cast(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ try {
+ const MC<T>& mc = dynamic_cast<const MC<T>&>(modelChecker);
+ return &mc;
+ } catch (std::bad_cast& bc) {
+ std::cerr << "Bad cast: tried to cast " << typeid(modelChecker).name() << " to " << typeid(MC<T>).name() << std::endl;
+
+ }
+ return nullptr;
+ }
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_AbstractFORMULA_H_ */
diff --git a/src/formula/PctlPathFormula.h b/src/formula/AbstractPathFormula.h
similarity index 60%
rename from src/formula/PctlPathFormula.h
rename to src/formula/AbstractPathFormula.h
index f929c642a..cba3425fa 100644
--- a/src/formula/PctlPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -1,16 +1,23 @@
/*
- * PctlPathFormula.h
+ * AbstractPathFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_PCTLPATHFORMULA_H_
-#define STORM_FORMULA_PCTLPATHFORMULA_H_
+#ifndef STORM_FORMULA_AbstractPATHFORMULA_H_
+#define STORM_FORMULA_AbstractPATHFORMULA_H_
-#include "PctlFormula.h"
-#include "modelChecker/DtmcPrctlModelChecker.h"
+namespace storm { namespace formula {
+template <class T> class AbstractPathFormula;
+}}
+
+#include "src/formula/AbstractFormula.h"
+
+#include "modelChecker/AbstractModelChecker.h"
#include <vector>
+#include <iostream>
+#include <typeinfo>
namespace storm {
@@ -18,7 +25,7 @@ namespace formula {
/*!
* @brief
- * Abstract base class for PCTL path formulas.
+ * Abstract base class for Abstract path formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@@ -26,13 +33,13 @@ namespace formula {
* clone().
*/
template <class T>
-class PctlPathFormula : public PctlFormula<T> {
+class AbstractPathFormula : public virtual AbstractFormula<T> {
public:
/*!
* empty destructor
*/
- virtual ~PctlPathFormula() { }
+ virtual ~AbstractPathFormula() { }
/*!
* Clones the called object.
@@ -42,7 +49,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const = 0;
+ virtual AbstractPathFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -55,11 +62,14 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
+ virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+ return nullptr;
+ }
};
} //namespace formula
} //namespace storm
-#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_AbstractPATHFORMULA_H_ */
diff --git a/src/formula/PctlStateFormula.h b/src/formula/AbstractStateFormula.h
similarity index 63%
rename from src/formula/PctlStateFormula.h
rename to src/formula/AbstractStateFormula.h
index bfd035e4d..f17f7eda0 100644
--- a/src/formula/PctlStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -1,16 +1,20 @@
/*
- * PctlStateFormula.h
+ * AbstractStateFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_
-#define STORM_FORMULA_PCTLSTATEFORMULA_H_
+#ifndef STORM_FORMULA_AbstractSTATEFORMULA_H_
+#define STORM_FORMULA_AbstractSTATEFORMULA_H_
-#include "PctlFormula.h"
-#include "storage/BitVector.h"
-#include "modelChecker/DtmcPrctlModelChecker.h"
+namespace storm { namespace formula {
+template <class T> class AbstractStateFormula;
+}}
+
+#include "AbstractFormula.h"
+#include "src/storage/BitVector.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -18,7 +22,7 @@ namespace formula {
/*!
* @brief
- * Abstract base class for PCTL state formulas.
+ * Abstract base class for Abstract state formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@@ -26,13 +30,13 @@ namespace formula {
* clone().
*/
template <class T>
-class PctlStateFormula : public PctlFormula<T> {
+class AbstractStateFormula : public AbstractFormula<T> {
public:
/*!
* empty destructor
*/
- virtual ~PctlStateFormula() { }
+ virtual ~AbstractStateFormula() { }
/*!
* Clones the called object.
@@ -42,7 +46,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const = 0;
+ virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -55,7 +59,10 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+ return nullptr;
+ }
};
} //namespace formula
@@ -63,4 +70,4 @@ public:
} //namespace storm
-#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */
+#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */
diff --git a/src/formula/And.h b/src/formula/And.h
index d166fd7c5..33e69ee1d 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -8,18 +8,25 @@
#ifndef STORM_FORMULA_AND_H_
#define STORM_FORMULA_AND_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
#include <string>
namespace storm {
-
namespace formula {
+template <class T> class And;
+
+template <class T>
+class IAndModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with AND node as root.
+ * Class for a Abstract formula tree with AND node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* As AND is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@@ -27,11 +34,11 @@ namespace formula {
* 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)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class And : public PctlStateFormula<T> {
+class And : public AbstractStateFormula<T> {
public:
/*!
@@ -50,7 +57,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
- And(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -75,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -84,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -121,7 +128,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
And<T>* result = new And();
if (this->left != NULL) {
result->setLeft(left->clone());
@@ -141,13 +148,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IAndModelChecker<T>& modelChecker) const {
return modelChecker.checkAnd(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index e479d0c61..8eb4dbe5b 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -8,23 +8,32 @@
#ifndef STORM_FORMULA_AP_H_
#define STORM_FORMULA_AP_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
+template <class T> class Ap;
+
+template <class T>
+class IApModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with atomic proposition as root.
+ * Class for a Abstract formula tree with atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Ap : public PctlStateFormula<T> {
+class Ap : public AbstractStateFormula<T> {
public:
/*!
@@ -64,7 +73,7 @@ public:
*
* @returns a new Ap-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
return new Ap(ap);
}
@@ -77,8 +86,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkAp(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IApModelChecker>(modelChecker)->checkAp(*this);
}
private:
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 0d0abedbd..2333897e7 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -8,20 +8,28 @@
#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
#define STORM_FORMULA_BOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "utility/ConstTemplates.h"
namespace storm {
namespace formula {
+template <class T> class BoundUntil;
+
+template <class T>
+class IBoundUntilModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkBoundUntil(const BoundUntil<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@@ -31,14 +39,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
-class BoundOperator : public PctlStateFormula<T> {
+class BoundOperator : public AbstractStateFormula<T> {
public:
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -50,7 +58,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula<T>* pathFormula)
+ BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
// Intentionally left empty
}
@@ -68,9 +76,9 @@ public:
}
/*!
- * @returns the child node (representation of a PCTL path formula)
+ * @returns the child node (representation of a Abstract path formula)
*/
- const PctlPathFormula<T>& getPathFormula () const {
+ const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@@ -79,7 +87,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
- void setPathFormula(PctlPathFormula<T>* pathFormula) {
+ void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -134,7 +142,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const = 0;
+ virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -145,14 +153,14 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IBoundUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundOperator(*this);
}
private:
ComparisonType comparisonOperator;
T bound;
- PctlPathFormula<T>* pathFormula;
+ AbstractPathFormula<T>* pathFormula;
};
} //namespace formula
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 0a66f6b83..bb7585ff9 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,11 +17,19 @@ namespace storm {
namespace formula {
+template <class T> class BoundedEventually;
+
+template <class T>
+class IBoundedEventuallyModelChecker {
+ public:
+ virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a BoundedEventually node as root.
+ * Class for a Abstract (path) formula tree with a BoundedEventually node as root.
*
- * Has one PCTL state formulas as sub formula/tree.
+ * Has one Abstract state formulas as sub formula/tree.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e child holds.
@@ -29,11 +37,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class BoundedEventually : public PctlPathFormula<T> {
+class BoundedEventually : public AbstractPathFormula<T> {
public:
/*!
@@ -50,7 +58,7 @@ public:
* @param child The child formula subtree
* @param bound The maximal number of steps
*/
- BoundedEventually(PctlStateFormula<T>* child, uint_fast64_t bound) {
+ BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) {
this->child = child;
this->bound = bound;
}
@@ -70,7 +78,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -78,7 +86,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -116,7 +124,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
BoundedEventually<T>* result = new BoundedEventually<T>();
result->setBound(bound);
if (child != nullptr) {
@@ -135,12 +143,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IBoundedEventuallyModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedEventually(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
uint_fast64_t bound;
};
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 675138e27..90d5ca10b 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
#define STORM_FORMULA_BOUNDEDUNTIL_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,11 +17,19 @@ namespace storm {
namespace formula {
+template <class T> class BoundedUntil;
+
+template <class T>
+class IBoundedUntilModelChecker {
+ public:
+ virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
+ * Class for a Abstract (path) formula tree with a BoundedUntil node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
@@ -30,11 +38,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class BoundedUntil : public PctlPathFormula<T> {
+class BoundedUntil : public AbstractPathFormula<T> {
public:
/*!
@@ -53,7 +61,7 @@ public:
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
- BoundedUntil(PctlStateFormula<T>* left, PctlStateFormula<T>* right,
+ BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
uint_fast64_t bound) {
this->left = left;
this->right = right;
@@ -80,7 +88,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -89,21 +97,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -144,7 +152,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil<T>();
result->setBound(bound);
if (left != NULL) {
@@ -166,13 +174,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IBoundedUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedUntil(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
uint_fast64_t bound;
};
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index cbbf1e18b..2587390ea 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_CUMULATIVEREWARD_H_
#define STORM_FORMULA_CUMULATIVEREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,18 +17,26 @@ namespace storm {
namespace formula {
+template <class T> class CumulativeReward;
+
+template <class T>
+class ICumulativeRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Cumulative Reward node as root.
+ * Class for a Abstract (path) formula tree with a Cumulative Reward node as root.
*
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class CumulativeReward : public PctlPathFormula<T> {
+class CumulativeReward : public AbstractPathFormula<T> {
public:
/*!
@@ -84,9 +92,9 @@ public:
*
* 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.
+ * @returns a new CumulativeReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
return new CumulativeReward(bound);
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const ICumulativeRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkCumulativeReward(*this);
}
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 1a781fbb7..32e6d126a 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -8,18 +8,27 @@
#ifndef STORM_FORMULA_EVENTUALLY_H_
#define STORM_FORMULA_EVENTUALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
+template <class T> class Eventually;
+
+template <class T>
+class IEventuallyModelChecker {
+ public:
+ virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Eventually node as root.
+ * Class for a Abstract (path) formula tree with an Eventually node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff eventually \e child holds.
@@ -27,11 +36,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Eventually : public PctlPathFormula<T> {
+class Eventually : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +55,7 @@ public:
*
* @param child The child node
*/
- Eventually(PctlStateFormula<T>* child) {
+ Eventually(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +74,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +82,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -91,9 +100,9 @@ public:
*
* 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.
+ * @returns a new Eventually-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Eventually<T>* result = new Eventually<T>();
if (child != nullptr) {
result->setChild(child);
@@ -110,12 +119,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkEventually(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IEventuallyModelChecker>(modelChecker)->checkEventually(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 70ed03c75..09de1acf0 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -8,15 +8,16 @@
#ifndef STORM_FORMULA_FORMULAS_H_
#define STORM_FORMULA_FORMULAS_H_
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+
#include "And.h"
#include "Ap.h"
#include "BoundedUntil.h"
#include "Next.h"
#include "Not.h"
#include "Or.h"
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
#include "ProbabilisticNoBoundOperator.h"
#include "ProbabilisticBoundOperator.h"
#include "Until.h"
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 02a18b884..115d96673 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_GLOBALLY_H_
#define STORM_FORMULA_GLOBALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Globally;
+
+template <class T>
+class IGloballyModelChecker {
+ public:
+ virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Globally node as root.
+ * Class for a Abstract (path) formula tree with a Globally node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff globally \e child holds.
@@ -27,11 +35,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Globally : public PctlPathFormula<T> {
+class Globally : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
- Globally(PctlStateFormula<T>* child) {
+ Globally(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -91,9 +99,9 @@ public:
*
* 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.
+ * @returns a new Globally-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != nullptr) {
result->setChild(child);
@@ -110,12 +118,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IGloballyModelChecker<T>& modelChecker) const {
return modelChecker.checkGlobally(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index d6067d344..319e38f49 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_INSTANTANEOUSREWARD_H_
#define STORM_FORMULA_INSTANTANEOUSREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,18 +17,26 @@ namespace storm {
namespace formula {
+template <class T> class InstantaneousReward;
+
+template <class T>
+class IInstantaneousRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Instantaneous Reward node as root.
+ * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root.
*
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class InstantaneousReward : public PctlPathFormula<T> {
+class InstantaneousReward : public AbstractPathFormula<T> {
public:
/*!
@@ -84,9 +92,9 @@ public:
*
* 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.
+ * @returns a new InstantaneousReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
return new InstantaneousReward(bound);
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IInstantaneousRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkInstantaneousReward(*this);
}
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 7b8214757..501277bba 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_NEXT_H_
#define STORM_FORMULA_NEXT_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Next;
+
+template <class T>
+class INextModelChecker {
+ public:
+ virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Next node as root.
+ * Class for a Abstract (path) formula tree with a Next node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in the next step, \e child holds
@@ -27,11 +35,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Next : public PctlPathFormula<T> {
+class Next : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
- Next(PctlStateFormula<T>* child) {
+ Next(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -95,7 +103,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
@@ -112,12 +120,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const INextModelChecker<T>& modelChecker) const {
return modelChecker.checkNext(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index 204c102a8..eeb8d2c54 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
#define STORM_FORMULA_NOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
namespace storm {
namespace formula {
+template <class T> class NoBoundOperator;
+
+template <class T>
+class INoBoundOperatorModelChecker {
+ public:
+ virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL 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
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* 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 AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -39,14 +47,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
-class NoBoundOperator: public storm::formula::PctlFormula<T> {
+class NoBoundOperator: public storm::formula::AbstractFormula<T> {
public:
/*!
* Empty constructor
@@ -60,7 +68,7 @@ public:
*
* @param pathFormula The child node.
*/
- NoBoundOperator(PctlPathFormula<T>* pathFormula) {
+ NoBoundOperator(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -74,9 +82,9 @@ public:
}
/*!
- * @returns the child node (representation of a PCTL path formula)
+ * @returns the child node (representation of a Abstract path formula)
*/
- const PctlPathFormula<T>& getPathFormula () const {
+ const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@@ -85,7 +93,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
- void setPathFormula(PctlPathFormula<T>* pathFormula) {
+ void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T>* check(const INoBoundOperatorModelChecker<T>& modelChecker) const {
return modelChecker.checkNoBoundOperator(*this);
}
@@ -110,7 +118,7 @@ public:
virtual std::string toString() const = 0;
private:
- PctlPathFormula<T>* pathFormula;
+ AbstractPathFormula<T>* pathFormula;
};
} /* namespace formula */
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 03d5cf572..9e211084d 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOT_H_
#define STORM_FORMULA_NOT_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Not;
+
+template <class T>
+class INotModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with NOT node as root.
+ * Class for a Abstract formula tree with NOT node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* 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)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Not : public PctlStateFormula<T> {
+class Not : public AbstractStateFormula<T> {
public:
/*!
@@ -41,7 +49,7 @@ public:
* Constructor
* @param child The child node
*/
- Not(PctlStateFormula<T>* child) {
+ Not(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -60,7 +68,7 @@ public:
/*!
* @returns The child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -68,7 +76,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -88,7 +96,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child);
@@ -105,12 +113,12 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const INotModelChecker<T>& modelChecker) const {
return modelChecker.checkNot(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 524ca58e7..79e30cdab 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -8,17 +8,24 @@
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
-
namespace formula {
+template <class T> class Or;
+
+template <class T>
+class IOrModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with OR node as root.
+ * Class for a Abstract formula tree with OR node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* As OR is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@@ -26,11 +33,11 @@ namespace formula {
* 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)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Or : public PctlStateFormula<T> {
+class Or : public AbstractStateFormula<T> {
public:
/*!
@@ -49,7 +56,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
- Or(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -74,7 +81,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -83,21 +90,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -120,7 +127,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
Or<T>* result = new Or();
if (this->left != NULL) {
result->setLeft(left->clone());
@@ -130,7 +137,7 @@ public:
}
return result;
}
-
+
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
@@ -140,13 +147,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IOrModelChecker<T>& modelChecker) const {
return modelChecker.checkOr(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/PctlFormula.h b/src/formula/PctlFormula.h
deleted file mode 100644
index 394e3cfa2..000000000
--- a/src/formula/PctlFormula.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*
- * Pctlformula.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_PCTLFORMULA_H_
-#define STORM_FORMULA_PCTLFORMULA_H_
-
-#include <string>
-
-namespace storm {
-
-namespace formula {
-
-
-//abstract
-/*!
- * @brief
- * Abstract base class for PCTL formulas in general.
- *
- * @attention This class is abstract.
- * @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
- * PctlPathFormula and PctlStateFormula offer the method clone().
- */
-template <class T>
-class PctlFormula {
-
-public:
- /*!
- * virtual destructor
- */
- virtual ~PctlFormula() { }
-
- /*!
- * @note This function is not implemented in this class.
- * @returns a string representation of the formula
- */
- virtual std::string toString() const = 0;
-};
-
-} //namespace formula
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_PCTLFORMULA_H_ */
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index e541619c1..37fe7858d 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@@ -19,10 +19,10 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@@ -32,11 +32,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
class ProbabilisticBoundOperator : public BoundOperator<T> {
@@ -56,7 +56,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
+ ProbabilisticBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@@ -81,7 +81,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
result->setInterval(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());
diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h
index ad4ab4851..bfe6f92db 100644
--- a/src/formula/ProbabilisticNoBoundOperator.h
+++ b/src/formula/ProbabilisticNoBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL 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
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* 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 AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
class ProbabilisticNoBoundOperator: public NoBoundOperator<T> {
@@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
- ProbabilisticNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+ ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 9f5d6ee43..6fdfb4733 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -8,27 +8,35 @@
#ifndef STORM_FORMULA_REACHABILITYREWARD_H_
#define STORM_FORMULA_REACHABILITYREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class ReachabilityReward;
+
+template <class T>
+class IReachabilityRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Reachability Reward node as root.
+ * Class for a Abstract (path) formula tree with an Reachability Reward node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class ReachabilityReward : public PctlPathFormula<T> {
+class ReachabilityReward : public AbstractPathFormula<T> {
public:
/*!
@@ -43,7 +51,7 @@ public:
*
* @param child The child node
*/
- ReachabilityReward(PctlStateFormula<T>* child) {
+ ReachabilityReward(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -62,7 +70,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -70,7 +78,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -88,9 +96,9 @@ public:
*
* 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.
+ * @returns a new ReachabilityReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
ReachabilityReward<T>* result = new ReachabilityReward<T>();
if (child != nullptr) {
result->setChild(child);
@@ -107,12 +115,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IReachabilityRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkReachabilityReward(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index 8118fdbe2..26f6ae7aa 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@@ -19,7 +19,7 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root.
+ * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
*
* Has a reward path formula as sub formula/tree.
*
@@ -31,11 +31,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
class RewardBoundOperator : public BoundOperator<T> {
@@ -55,7 +55,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
+ RewardBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@@ -80,7 +80,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
RewardBoundOperator<T>* result = new RewardBoundOperator<T>();
result->setBound(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());
diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h
index 3362ff136..3752b381a 100644
--- a/src/formula/RewardNoBoundOperator.h
+++ b/src/formula/RewardNoBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a R (reward) operator without declaration of reward values
+ * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values
* as root.
*
* Checking a formula with this operator as root returns the reward for the reward path formula for
* each state
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* 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 AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
class RewardNoBoundOperator: public NoBoundOperator<T> {
@@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
- RewardNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+ RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}
diff --git a/src/formula/Until.h b/src/formula/Until.h
index be86a1153..94f917a60 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_UNTIL_H_
#define STORM_FORMULA_UNTIL_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Until;
+
+template <class T>
+class IUntilModelChecker {
+ public:
+ virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Until node as root.
+ * Class for a Abstract (path) formula tree with an Until node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
@@ -28,11 +36,11 @@ namespace formula {
* 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)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Until : public PctlPathFormula<T> {
+class Until : public AbstractPathFormula<T> {
public:
/*!
@@ -49,7 +57,7 @@ public:
* @param left The left formula subtree
* @param right The left formula subtree
*/
- Until(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -74,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -83,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -120,7 +128,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Until<T>* result = new Until();
if (left != NULL) {
result->setLeft(left->clone());
@@ -140,13 +148,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkUntil(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelChecker/AbstractModelChecker.h
new file mode 100644
index 000000000..6bac47a04
--- /dev/null
+++ b/src/modelChecker/AbstractModelChecker.h
@@ -0,0 +1,43 @@
+/*
+ * DtmcPrctlModelChecker.h
+ *
+ * Created on: 22.10.2012
+ * Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
+#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
+
+namespace storm { namespace modelChecker {
+template <class Type> class AbstractModelChecker;
+}}
+
+//#include "src/formula/Formulas.h"
+#include "src/formula/Or.h"
+#include "src/formula/Ap.h"
+#include "src/storage/BitVector.h"
+
+namespace storm {
+namespace modelChecker {
+
+/*!
+ * @brief
+ * Interface for model checker classes.
+ *
+ * This class provides basic functions that are the same for all subclasses, but mainly only declares
+ * abstract methods that are to be implemented in concrete instances.
+ *
+ * @attention This class is abstract.
+ */
+template<class Type>
+class AbstractModelChecker :
+ public virtual storm::formula::IOrModelChecker<Type>,
+ public virtual storm::formula::IApModelChecker<Type>
+ {
+};
+
+} //namespace modelChecker
+
+} //namespace storm
+
+#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index f443a2ead..16fdc913f 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -23,15 +23,13 @@ class DtmcPrctlModelChecker;
}
-#include "src/formula/PctlPathFormula.h"
-#include "src/formula/PctlStateFormula.h"
-
#include "src/formula/Formulas.h"
#include "src/models/Dtmc.h"
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/utility/Vector.h"
+#include "src/modelChecker/AbstractModelChecker.h"
#include <vector>
#include "log4cplus/logger.h"
@@ -53,7 +51,11 @@ namespace modelChecker {
* @attention This class is abstract.
*/
template<class Type>
-class DtmcPrctlModelChecker {
+class DtmcPrctlModelChecker :
+ public virtual AbstractModelChecker<Type>,
+ public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+ public virtual storm::formula::IEventuallyModelChecker<Type>
+ {
public:
/*!
* Constructor
@@ -100,7 +102,7 @@ public:
* states.
* @param stateFormula The formula to be checked.
*/
- void check(const storm::formula::PctlStateFormula<Type>& stateFormula) const {
+ void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
@@ -160,7 +162,7 @@ public:
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
- storm::storage::BitVector* checkStateFormula(const storm::formula::PctlStateFormula<Type>& formula) const {
+ storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula<Type>& formula) const {
return formula.check(*this);
}
@@ -216,7 +218,7 @@ public:
* @param formula The Or state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
- storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
+ virtual storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
storm::storage::BitVector* result = checkStateFormula(formula.getLeft());
storm::storage::BitVector* right = checkStateFormula(formula.getRight());
(*result) |= (*right);
@@ -269,7 +271,7 @@ public:
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
- std::vector<Type>* checkPathFormula(const storm::formula::PctlPathFormula<Type>& formula) const {
+ std::vector<Type>* checkPathFormula(const storm::formula::AbstractPathFormula<Type>& formula) const {
return formula.check(*this);
}
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 9c0850ca5..f7288f3fe 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -58,7 +58,7 @@ namespace
/*!
* @brief Resulting formula.
*/
- storm::formula::PctlFormula<double>* result;
+ //storm::formula::PctlFormula<double>* result;
struct dump
{
@@ -141,7 +141,7 @@ storm::parser::PrctlParser::PrctlParser(const char* filename)
std::cout << "File was parsed" << std::endl;
std::string rest(data, file.dataend);
std::cout << "Rest: " << rest << std::endl;
- this->formula = p.result;
+ //this->formula = p.result;
}
- else this->formula = NULL;
+ //else this->formula = NULL;
}
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 79c2e81c7..70a7da0db 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -1,7 +1,7 @@
#ifndef STORM_PARSER_PRCTLPARSER_H_
#define STORM_PARSER_PRCTLPARSER_H_
-#include "src/formula/PctlFormula.h"
+// #include "src/formula/PctlFormula.h"
#include "src/parser/Parser.h"
namespace storm {
@@ -18,13 +18,14 @@ class PrctlParser : Parser
/*!
* @brief return formula object parsed from file.
*/
- storm::formula::PctlFormula<double>* getFormula()
+/* storm::formula::PctlFormula<double>* getFormula()
{
return this->formula;
}
private:
storm::formula::PctlFormula<double>* formula;
+*/
};
} // namespace parser