Made bound/no-bound operators more consistent to reduce similar code. Changed bound operators to have a single bound and a comparison operator instead of an interval.

CMakeLists.txt

@@ -60,12 +60,13 @@ endif()
 
 if(CMAKE_COMPILER_IS_GNUCC)
     # Set standard flags for GCC
+    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
     set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic")
     # -Werror is atm removed as this gave some problems with existing code
     # May be re-set later
     # (Thomas Heinemann, 2012-12-21)
     
-    # Turn on popcnt instruction if possible (yes by default)
+    # Turn on popcnt instruction if desired (yes by default)
     if (USE_POPCNT)
         set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
     endif(USE_POPCNT)
@@ -73,7 +74,8 @@ elseif(MSVC)
 	# required for GMM to compile, ugly error directive in their code
 	add_definitions(/D_SCL_SECURE_NO_DEPRECATE)
 else(CLANG)
-    # Set standard flags for GCC
+    # Set standard flags for clang
+    set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
     set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable")
     
     # Turn on popcnt instruction if desired (yes by default)

src/formula/ProbabilisticIntervalOperator.h → src/formula/BoundOperator.h

@@ -1,12 +1,12 @@
 /*
- * ProbabilisticOperator.h
+ * BoundOperator.h
  *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
+ *  Created on: 27.12.2012
+ *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
+#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
+#define STORM_FORMULA_BOUNDOPERATOR_H_
 
 #include "PctlStateFormula.h"
 #include "PctlPathFormula.h"
@@ -38,17 +38,10 @@ namespace formula {
  * @see PctlFormula
  */
 template<class T>
-class ProbabilisticIntervalOperator : public PctlStateFormula<T> {
+class BoundOperator : public PctlStateFormula<T> {
 
 public:
-	/*!
-	 * Empty constructor
-	 */
-	ProbabilisticIntervalOperator() {
-		upper = storm::utility::constGetZero<T>();
-		lower = storm::utility::constGetZero<T>();
-		pathFormula = NULL;
-	}
+	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
 
 	/*!
 	 * Constructor
@@ -57,10 +50,9 @@ public:
 	 * @param upperBound The upper bound for the probability
 	 * @param pathFormula The child node
 	 */
-	ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) {
-		this->lower = lowerBound;
-		this->upper = upperBound;
-		this->pathFormula = &pathFormula;
+	BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula<T>* pathFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -69,8 +61,8 @@ public:
 	 * The subtree is deleted with the object
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
-	virtual ~ProbabilisticIntervalOperator() {
-	 if (pathFormula != NULL) {
+	virtual ~BoundOperator() {
+	 if (pathFormula != nullptr) {
 		 delete pathFormula;
 	 }
 	}
@@ -82,20 +74,6 @@ public:
 		return *pathFormula;
 	}
 
-	/*!
-	 * @returns the lower bound for the probability
-	 */
-	const T& getLowerBound() const {
-		return lower;
-	}
-
-	/*!
-	 * @returns the upper bound for the probability
-	 */
-	const T& getUpperBound() const {
-		return upper;
-	}
-
 	/*!
 	 * Sets the child node
 	 *
@@ -105,31 +83,50 @@ public:
 		this->pathFormula = pathFormula;
 	}
 
+	/*!
+	 * @returns the bound for the measure
+	 */
+	const T& getBound() const {
+		return bound;
+	}
+
 	/*!
 	 * Sets the interval in which the probability that the path formula holds may lie in.
 	 *
-	 * @param lowerBound The lower bound for the probability
-	 * @param upperBound The upper bound for the probability
+	 * @param bound The bound for the measure
 	 */
-	void setInterval(T lowerBound, T upperBound) {
-		this->lower = lowerBound;
-		this->upper = upperBound;
+	void setBound(T bound) {
+		this->bound = bound;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "P[";
-		result += std::to_string(lower);
-		result += ";";
-		result += std::to_string(upper);
-		result += "] (";
+		std::string result = "P ";
+		switch (comparisonOperator) {
+		case LESS: result += "<"; break;
+		case LESS_EQUAL: result += "<="; break;
+		case GREATER: result += ">"; break;
+		case GREATER_EQUAL: result += ">="; break;
+		}
+		result += std::to_string(bound);
+		result += " [";
 		result += pathFormula->toString();
-		result += ")";
+		result += "]";
 		return result;
 	}
 
+	bool meetsBound(T value) {
+		switch (comparisonOperator) {
+		case LESS: return value < bound; break;
+		case LESS_EQUAL: return value <= bound; break;
+		case GREATER: return value > bound; break;
+		case GREATER_EQUAL: return value >= bound; break;
+		default: return false;
+		}
+	}
+
 	/*!
 	 * Clones the called object.
 	 *
@@ -137,14 +134,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PctlStateFormula<T>* clone() const {
-		ProbabilisticIntervalOperator<T>* result = new ProbabilisticIntervalOperator<T>();
-		result->setInterval(lower, upper);
-		if (pathFormula != NULL) {
-			result->setPathFormula(pathFormula->clone());
-		}
-		return result;
-	}
+	virtual PctlStateFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -156,12 +146,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 {
-	  return modelChecker.checkProbabilisticIntervalOperator(*this);
+	  return modelChecker.checkBoundOperator(*this);
 	}
 
 private:
-	T lower;
-	T upper;
+	ComparisonType comparisonOperator;
+	T bound;
 	PctlPathFormula<T>* pathFormula;
 };
 
@@ -169,4 +159,4 @@ private:
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ */
+#endif /* STORM_FORMULA_BOUNDOPERATOR_H_ */

src/formula/Formulas.h

@@ -17,8 +17,8 @@
 #include "PctlFormula.h"
 #include "PctlPathFormula.h"
 #include "PctlStateFormula.h"
-#include "ProbabilisticNoBoundsOperator.h"
-#include "ProbabilisticIntervalOperator.h"
+#include "ProbabilisticNoBoundOperator.h"
+#include "ProbabilisticBoundOperator.h"
 #include "Until.h"
 #include "Eventually.h"
 #include "Globally.h"
@@ -27,7 +27,7 @@
 #include "InstantaneousReward.h"
 #include "CumulativeReward.h"
 #include "ReachabilityReward.h"
-#include "RewardIntervalOperator.h"
-#include "RewardNoBoundsOperator.h"
+#include "RewardBoundOperator.h"
+#include "RewardNoBoundOperator.h"
 
 #endif /* STORM_FORMULA_FORMULAS_H_ */

src/formula/ProbabilisticNoBoundsOperator.h → src/formula/NoBoundOperator.h

@@ -1,17 +1,18 @@
 /*
- * ProbabilisticNoBoundsOperator.h
+ * NoBoundOperator.h
  *
- *  Created on: 12.12.2012
- *      Author: thomas
+ *  Created on: 27.12.2012
+ *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
+#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
+#define STORM_FORMULA_NOBOUNDOPERATOR_H_
 
 #include "PctlFormula.h"
 #include "PctlPathFormula.h"
 
 namespace storm {
+
 namespace formula {
 
 /*!
@@ -32,7 +33,7 @@ namespace formula {
  * 	This class does not contain a check() method like the other formula classes.
  * 	The check method should only be called by the model checker to infer the correct check function for sub
  * 	formulas. As this operator can only appear at the root, the method is not useful here.
- * 	Use the checkProbabilisticNoBoundsOperator method from the DtmcPrctlModelChecker class instead.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
  *
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
@@ -45,12 +46,12 @@ namespace formula {
  * @see PctlFormula
  */
 template <class T>
-class ProbabilisticNoBoundsOperator: public storm::formula::PctlFormula<T> {
+class NoBoundOperator: public storm::formula::PctlFormula<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticNoBoundsOperator() {
+	NoBoundOperator() {
 		this->pathFormula = NULL;
 	}
 
@@ -59,14 +60,14 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundsOperator(PctlPathFormula<T>* pathFormula) {
+	NoBoundOperator(PctlPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
 	/*!
 	 * Destructor
 	 */
-	virtual ~ProbabilisticNoBoundsOperator() {
+	virtual ~NoBoundOperator() {
 		if (pathFormula != NULL) {
 			delete pathFormula;
 		}
@@ -89,20 +90,31 @@ public:
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * 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::string toString() const {
-		std::string result = " P=? (";
-		result += pathFormula->toString();
-		result += ")";
-		return result;
+	virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+		return modelChecker.checkNoBoundOperator(*this);
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const = 0;
+
 private:
 	PctlPathFormula<T>* pathFormula;
 };
 
 } /* namespace formula */
+
 } /* namespace storm */
 
-#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */
+#endif /* STORM_FORMULA_NOBOUNDOPERATOR_H_ */

src/formula/ProbabilisticBoundOperator.h

@@ -0,0 +1,96 @@
+/*
+ * ProbabilisticBoundOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+
+#include "PctlStateFormula.h"
+#include "PctlPathFormula.h"
+#include "BoundOperator.h"
+#include "utility/ConstTemplates.h"
+
+namespace storm {
+
+namespace formula {
+
+/*!
+ * @brief
+ * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
+ * as root.
+ *
+ * Has one PCTL path formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the probability that the path formula holds is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see PctlStateFormula
+ * @see PctlPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see PctlFormula
+ */
+template<class T>
+class ProbabilisticBoundOperator : public BoundOperator<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @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) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "P [";
+		result += std::to_string(this->getLowerBound());
+		result += ",";
+		result += std::to_string(this->getUpperBound());
+		result += "] (";
+		result += this->getPathFormula()->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PctlStateFormula<T>* clone() const {
+		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
+		result->setInterval(this->getLowerBound(), this->getUpperBound());
+		result->setPathFormula(this->getPathFormula()->clone());
+		return result;
+	}
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */

src/formula/ProbabilisticNoBoundOperator.h

@@ -0,0 +1,83 @@
+/*
+ * ProbabilisticNoBoundOperator.h
+ *
+ *  Created on: 12.12.2012
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+
+#include "PctlFormula.h"
+#include "PctlPathFormula.h"
+#include "NoBoundOperator.h"
+
+namespace storm {
+
+namespace formula {
+
+/*!
+ * @brief
+ * Class for a PCTL 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.
+ *
+ * @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.
+ *
+ * @note
+ * 	This class does not contain a check() method like the other formula classes.
+ * 	The check method should only be called by the model checker to infer the correct check function for sub
+ * 	formulas. As this operator can only appear at the root, the method is not useful here.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see PctlStateFormula
+ * @see PctlPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticIntervalOperator
+ * @see PctlFormula
+ */
+template <class T>
+class ProbabilisticNoBoundOperator: public NoBoundOperator<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticNoBoundOperator() : NoBoundOperator<T>(nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = " P=? [";
+		result += this->getPathFormula().toString();
+		result += "]";
+		return result;
+	}
+};
+
+} /* namespace formula */
+
+} /* namespace storm */
+
+#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/RewardBoundOperator.h

@@ -0,0 +1,95 @@
+/*
+ * RewardBoundOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_
+#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_
+
+#include "PctlStateFormula.h"
+#include "PctlPathFormula.h"
+#include "BoundOperator.h"
+#include "utility/ConstTemplates.h"
+
+namespace storm {
+
+namespace formula {
+
+/*!
+ * @brief
+ * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root.
+ *
+ * Has a reward path formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the reward of the reward path formula is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see PctlStateFormula
+ * @see PctlPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see PctlFormula
+ */
+template<class T>
+class RewardBoundOperator : public BoundOperator<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	RewardBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @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) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "R [";
+		result += std::to_string(this->getLowerBound());
+		result += ", ";
+		result += std::to_string(this->getUpperBound());
+		result += "] [";
+		result += this->getPathFormula()->toString();
+		result += "]";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PctlStateFormula<T>* clone() const {
+		RewardBoundOperator<T>* result = new RewardBoundOperator<T>();
+		result->setBound(this->getLowerBound(), this->getUpperBound());
+		result->setPathFormula(this->getPathFormula()->clone());
+		return result;
+	}
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */

src/formula/RewardIntervalOperator.h

@@ -1,171 +0,0 @@
-/*
- * ProbabilisticOperator.h
- *
- *  Created on: 19.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_REWARDINTERVALOPERATOR_H_
-#define STORM_FORMULA_REWARDINTERVALOPERATOR_H_
-
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
-#include "utility/ConstTemplates.h"
-
-namespace storm {
-
-namespace formula {
-
-/*!
- * @brief
- * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root.
- *
- * Has a reward path formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the reward of the reward path formula is inside the bounds
- * 	  specified in this operator
- *
- * The subtree is seen as part of the object and deleted with it
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- *
- * @see PctlStateFormula
- * @see PctlPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
- */
-template<class T>
-class RewardIntervalOperator : public PctlStateFormula<T> {
-
-public:
-	/*!
-	 * Empty constructor
-	 */
-	RewardIntervalOperator() {
-		upper = storm::utility::constGetZero<T>();
-		lower = storm::utility::constGetZero<T>();
-		pathFormula = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 *
-	 * @param lowerBound The lower bound for the probability
-	 * @param upperBound The upper bound for the probability
-	 * @param pathFormula The child node
-	 */
-	RewardIntervalOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) {
-		this->lower = lowerBound;
-		this->upper = upperBound;
-		this->pathFormula = &pathFormula;
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * The subtree is deleted with the object
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~RewardIntervalOperator() {
-	 if (pathFormula != nullptr) {
-		 delete pathFormula;
-	 }
-	}
-
-	/*!
-	 * @returns the child node (representation of a PCTL path formula)
-	 */
-	const PctlPathFormula<T>& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * @returns the lower bound for the probability
-	 */
-	const T& getLowerBound() const {
-		return lower;
-	}
-
-	/*!
-	 * @returns the upper bound for the probability
-	 */
-	const T& getUpperBound() const {
-		return upper;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(PctlPathFormula<T>* pathFormula) {
-		this->pathFormula = pathFormula;
-	}
-
-	/*!
-	 * Sets the interval in which the probability that the path formula holds may lie in.
-	 *
-	 * @param lowerBound The lower bound for the probability
-	 * @param upperBound The upper bound for the probability
-	 */
-	void setInterval(T lowerBound, T upperBound) {
-		this->lower = lowerBound;
-		this->upper = upperBound;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = "R [";
-		result += std::to_string(lower);
-		result += ", ";
-		result += std::to_string(upper);
-		result += "] [";
-		result += pathFormula->toString();
-		result += "]";
-		return result;
-	}
-
-	/*!
-	 * Clones the called object.
-	 *
-	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-	 *
-	 * @returns a new AND-object that is identical the called object.
-	 */
-	virtual PctlStateFormula<T>* clone() const {
-		RewardIntervalOperator<T>* result = new RewardIntervalOperator<T>();
-		result->setInterval(lower, upper);
-		if (pathFormula != nullptr) {
-			result->setPathFormula(pathFormula->clone());
-		}
-		return result;
-	}
-
-	/*!
-	 * Calls the model checker to check this formula.
-	 * Needed to infer the correct type of formula class.
-	 *
-	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
-	 *       the methods of the model checker should be used.
-	 *
-	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-	 */
-	virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkRewardIntervalOperator(*this);
-	}
-
-private:
-	T lower;
-	T upper;
-	PctlPathFormula<T>* pathFormula;
-};
-
-} //namespace formula
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_REWARDINTERVALOPERATOR_H_ */

src/formula/RewardNoBoundsOperator.h → src/formula/RewardNoBoundOperator.h

@@ -1,15 +1,16 @@
 /*
- * RewardNoBoundsOperator.h
+ * RewardNoBoundOperator.h
  *
- *  Created on: 12.12.2012
- *      Author: thomas
+ *  Created on: 25.12.2012
+ *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_
-#define STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_
+#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
 
 #include "PctlFormula.h"
 #include "PctlPathFormula.h"
+#include "NoBoundOperator.h"
 
 namespace storm {
 
@@ -33,7 +34,7 @@ namespace formula {
  * 	This class does not contain a check() method like the other formula classes.
  * 	The check method should only be called by the model checker to infer the correct check function for sub
  * 	formulas. As this operator can only appear at the root, the method is not useful here.
- * 	Use the checkRewardNoBoundsOperator method from the DtmcPrctlModelChecker class instead.
+ * 	Use the checkRewardNoBoundOperator method from the DtmcPrctlModelChecker class instead.
  *
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
@@ -46,13 +47,13 @@ namespace formula {
  * @see PctlFormula
  */
 template <class T>
-class RewardNoBoundsOperator: public storm::formula::PctlFormula<T> {
+class RewardNoBoundOperator: public NoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardNoBoundsOperator() {
-		this->pathFormula = nullptr;
+	RewardNoBoundOperator() : NoBoundOperator<T>(nullptr) {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -60,33 +61,8 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundsOperator(PctlPathFormula<T>* pathFormula) {
-		this->pathFormula = pathFormula;
-	}
-
-	/*!
-	 * Destructor
-	 */
-	virtual ~RewardNoBoundsOperator() {
-		if (pathFormula != nullptr) {
-			delete pathFormula;
-		}
-	}
-
-	/*!
-	 * @returns the child node (representation of a PCTL path formula)
-	 */
-	const PctlPathFormula<T>& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(PctlPathFormula<T>* pathFormula) {
-		this->pathFormula = pathFormula;
+	RewardNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -94,17 +70,14 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = " R=? [";
-		result += pathFormula->toString();
+		result += this->getPathFormula().toString();
 		result += "]";
 		return result;
 	}
-
-private:
-	PctlPathFormula<T>* pathFormula;
 };
 
 } /* namespace formula */
 
 } /* namespace storm */
 
-#endif /* STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_ */
+#endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */

src/modelChecker/DtmcPrctlModelChecker.h

@@ -124,17 +124,17 @@ public:
 	}
 
 	/*!
-	 * Checks the given probabilistic operator (with no bound) on the DTMC and prints the result
-	 * (probability) for all initial states.
-	 * @param probabilisticNoBoundsFormula The formula to be checked.
+	 * Checks the given operator (with no bound) on the DTMC and prints the result
+	 * (probability/rewards) for all initial states.
+	 * @param probabilisticNoBoundFormula The formula to be checked.
 	 */
-	void check(const storm::formula::ProbabilisticNoBoundsOperator<Type>& probabilisticNoBoundsFormula) const {
+	void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
 		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << probabilisticNoBoundsFormula.toString());
-		std::cout << "Model checking formula:\t" << probabilisticNoBoundsFormula.toString() << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
+		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
 		std::vector<Type>* result = nullptr;
 		try {
-			result = checkProbabilisticNoBoundsOperator(probabilisticNoBoundsFormula);
+			result = noBoundFormula.check(*this);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
 			for (auto initialState : *this->getModel().getLabeledStates("init")) {
@@ -152,37 +152,6 @@ public:
 		storm::utility::printSeparationLine(std::cout);
 	}
 
-	/*!
-	 * Checks the given reward operator (with no bound) on the DTMC and prints the result
-	 * (reward values) for all initial states.
-	 * @param rewardNoBoundsFormula The formula to be checked.
-	 */
-	void check(const storm::formula::RewardNoBoundsOperator<Type>& rewardNoBoundsFormula) {
-		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << rewardNoBoundsFormula.toString());
-		std::cout << "Model checking formula:\t" << rewardNoBoundsFormula.toString() << std::endl;
-		std::vector<Type>* result = nullptr;
-		try {
-			result = checkRewardNoBoundsOperator(rewardNoBoundsFormula);
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : *this->getModel().getLabeledStates("init")) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
-			}
-			std::cout << std::endl;
-			storm::utility::printSeparationLine(std::cout);
-			delete result;
-		} catch (std::exception& e) {
-			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
-		}
-		std::cout << std::endl;
-		storm::utility::printSeparationLine(std::cout);
-	}
-
 	/*!
 	 * The check method for a state formula; Will infer the actual type of formula and delegate it
 	 * to the specialized method
@@ -255,60 +224,29 @@ public:
 	}
 
 	/*!
-	 * The check method for a state formula with a probabilistic interval operator node as root in
+	 * The check method for a state formula with a bound operator node as root in
 	 * its formula tree
 	 *
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	storm::storage::BitVector* checkProbabilisticIntervalOperator(
-			const storm::formula::ProbabilisticIntervalOperator<Type>& formula) const {
+	storm::storage::BitVector* checkBoundOperator(const storm::formula::BoundOperator<Type>& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
-		std::vector<Type>* probabilisticResult = this->checkPathFormula(formula.getPathFormula());
+		std::vector<Type>* quantitativeResult = this->checkPathFormula(formula.getPathFormula());
 
 		// Create resulting bit vector, which will hold the yes/no-answer for every state.
 		storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates());
 
-		// Now, we can compute which states meet the bound specified in this operator, i.e.
-		// lie in the interval that was given along with this operator, and set the corresponding bits
-		// to true in the resulting vector.
-		Type lower = formula.getLowerBound();
-		Type upper = formula.getUpperBound();
+		// Now, we can compute which states meet the bound specified in this operator and set the
+		// corresponding bits to true in the resulting vector.
 		for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) {
-			if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true);
+			if (formula.meetsBound((*quantitativeResult)[i])) {
+				result->set(i, true);
+			}
 		}
 
 		// Delete the probabilities computed for the states and return result.
-		delete probabilisticResult;
-		return result;
-	}
-
-	/*!
-	 * The check method for a state formula with a reward interval operator node as root in
-	 * its formula tree
-	 *
-	 * @param formula The state formula to check
-	 * @returns The set of states satisfying the formula, represented by a bit vector
-	 */
-	storm::storage::BitVector* checkRewardIntervalOperator(
-			const storm::formula::RewardIntervalOperator<Type>& formula) const {
-		// First, we need to compute the probability for satisfying the path formula for each state.
-		std::vector<Type>* rewardResult = this->checkPathFormula(formula.getPathFormula());
-
-		// Create resulting bit vector, which will hold the yes/no-answer for every state.
-		storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates());
-
-		// Now, we can compute which states meet the bound specified in this operator, i.e.
-		// lie in the interval that was given along with this operator, and set the corresponding bits
-		// to true in the resulting vector.
-		Type lower = formula.getLowerBound();
-		Type upper = formula.getUpperBound();
-		for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) {
-			if ((*rewardResult)[i] >= lower && (*rewardResult)[i] <= upper) result->set(i, true);
-		}
-
-		// Delete the reward values computed for the states and return result.
-		delete rewardResult;
+		delete quantitativeResult;
 		return result;
 	}
 
@@ -319,20 +257,7 @@ public:
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	std::vector<Type>* checkProbabilisticNoBoundsOperator(
-			const storm::formula::ProbabilisticNoBoundsOperator<Type>& formula) const {
-		return formula.getPathFormula().check(*this);
-	}
-
-	/*!
-	 * The check method for a state formula with a reward operator node without bounds as root
-	 * in its formula tree
-	 *
-	 * @param formula The state formula to check
-	 * @returns The set of states satisfying the formula, represented by a bit vector
-	 */
-	std::vector<Type>* checkRewardNoBoundsOperator(
-			const storm::formula::RewardNoBoundsOperator<Type>& formula) const {
+	std::vector<Type>* checkNoBoundOperator(const storm::formula::NoBoundOperator<Type>& formula) const {
 		return formula.getPathFormula().check(*this);
 	}
 

src/storm.cpp

@@ -141,11 +141,11 @@ void cleanUp() {
 void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
 	storm::formula::Ap<double>* oneFormula = new storm::formula::Ap<double>("one");
 	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
-	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
 	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
-	storm::formula::RewardNoBoundsOperator<double>* rewardFormula = new storm::formula::RewardNoBoundsOperator<double>(reachabilityRewardFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
@@ -159,7 +159,7 @@ void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
 void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
 	storm::formula::Ap<double>* observe0Greater1Formula = new storm::formula::Ap<double>("observe0Greater1");
 	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(observe0Greater1Formula);
-	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
@@ -167,14 +167,14 @@ void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
 
 	storm::formula::Ap<double>* observeIGreater1Formula = new storm::formula::Ap<double>("observeIGreater1");
 	eventuallyFormula = new storm::formula::Eventually<double>(observeIGreater1Formula);
-	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
 
 	storm::formula::Ap<double>* observeOnlyTrueSenderFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
 	eventuallyFormula = new storm::formula::Eventually<double>(observeOnlyTrueSenderFormula);
-	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	mc->check(*probFormula);
 	delete probFormula;
@@ -185,7 +185,7 @@ void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
 void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast64_t n) {
 	storm::formula::Ap<double>* electedFormula = new storm::formula::Ap<double>("elected");
 	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(eventuallyFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
 
 	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	mc->check(*probFormula);
@@ -193,7 +193,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 
 	electedFormula = new storm::formula::Ap<double>("elected");
 	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), electedFormula, 1);
-	probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(boundedUntilFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
 
 	for (uint_fast64_t L = 1; L < 5; ++L) {
 		boundedUntilFormula->setBound(L*(n + 1));
@@ -203,7 +203,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 
 	electedFormula = new storm::formula::Ap<double>("elected");
 	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
-	storm::formula::RewardNoBoundsOperator<double>* rewardFormula = new storm::formula::RewardNoBoundsOperator<double>(reachabilityRewardFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
 
 	mc->check(*rewardFormula);
 	delete rewardFormula;
@@ -221,7 +221,7 @@ void testChecking() {
 
 	dtmc->printModelInformationToStream(std::cout);
 
-	testCheckingDie(*dtmc);
+	// testCheckingDie(*dtmc);
 	// testCheckingCrowds(*dtmc);
 	// testCheckingSynchronousLeader(*dtmc, 4);
 }