Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement

a "StateNoBoundOperator" now...

src/formula/NoBoundOperator.h → src/formula/PathNoBoundOperator.h

@@ -1,5 +1,5 @@
 /*
- * NoBoundOperator.h
+ * PathNoBoundOperator.h
  *
  *  Created on: 27.12.2012
  *      Author: Christian Dehnert
@@ -19,7 +19,7 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class NoBoundOperator;
+template <class T> class PathNoBoundOperator;
 
 /*!
  *  @brief Interface class for model checkers that support NoBoundOperator.
@@ -28,7 +28,7 @@ template <class T> class NoBoundOperator;
  *  this pure virtual class.
  */
 template <class T>
-class INoBoundOperatorModelChecker {
+class IPathNoBoundOperatorModelChecker {
     public:
 		/*!
          *  @brief Evaluates NoBoundOperator formula within a model checker.
@@ -36,7 +36,7 @@ class INoBoundOperatorModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
+        virtual std::vector<T>* checkPathNoBoundOperator(const PathNoBoundOperator<T>& obj) const = 0;
 };
 
 /*!
@@ -70,12 +70,12 @@ class INoBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class NoBoundOperator: public storm::formula::AbstractFormula<T>, public OptimizingOperator {
+class PathNoBoundOperator: public storm::formula::AbstractFormula<T>, public OptimizingOperator {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	NoBoundOperator() : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator() : optimalityOperator(false), minimumOperator(false) {
 		this->pathFormula = nullptr;
 	}
 
@@ -84,7 +84,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	NoBoundOperator(AbstractPathFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator(AbstractPathFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -95,7 +95,7 @@ public:
 	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a
 	 * maximizing operator.
 	 */
-	NoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+	PathNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
 		: optimalityOperator(true), minimumOperator(minimumOperator) {
 		this->pathFormula = pathFormula;
 	}
@@ -103,7 +103,7 @@ public:
 	/*!
 	 * Destructor
 	 */
-	virtual ~NoBoundOperator() {
+	virtual ~PathNoBoundOperator() {
 		if (pathFormula != NULL) {
 			delete pathFormula;
 		}
@@ -137,7 +137,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::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<INoBoundOperatorModelChecker>()->checkNoBoundOperator(*this);
+		return modelChecker.template as<IPathNoBoundOperatorModelChecker>()->checkPathNoBoundOperator(*this);
 	}
 
 	/*!

src/formula/ProbabilisticNoBoundOperator.h

@@ -10,7 +10,7 @@
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
-#include "NoBoundOperator.h"
+#include "PathNoBoundOperator.h"
 
 namespace storm {
 namespace formula {
@@ -46,12 +46,12 @@ namespace formula {
  * @see AbstractFormula
  */
 template <class T>
-class ProbabilisticNoBoundOperator: public NoBoundOperator<T> {
+class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticNoBoundOperator() : NoBoundOperator<T>(nullptr) {
+	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
 		// Intentionally left empty
 	}
 
@@ -60,7 +60,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -69,7 +69,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : NoBoundOperator<T>(pathFormula, minimumOperator) {
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -78,7 +78,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "P";
-		result += NoBoundOperator<T>::toString();
+		result += PathNoBoundOperator<T>::toString();
 		return result;
 	}
 };

src/formula/RewardNoBoundOperator.h

@@ -10,7 +10,7 @@
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
-#include "NoBoundOperator.h"
+#include "PathNoBoundOperator.h"
 
 namespace storm {
 namespace formula {
@@ -46,12 +46,12 @@ namespace formula {
  * @see AbstractFormula
  */
 template <class T>
-class RewardNoBoundOperator: public NoBoundOperator<T> {
+class RewardNoBoundOperator: public PathNoBoundOperator<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardNoBoundOperator() : NoBoundOperator<T>(nullptr) {
+	RewardNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
 		// Intentionally left empty
 	}
 
@@ -60,7 +60,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -69,7 +69,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : NoBoundOperator<T>(pathFormula, minimumOperator) {
+	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -78,7 +78,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "R";
-		result += NoBoundOperator<T>::toString();
+		result += PathNoBoundOperator<T>::toString();
 		return result;
 	}
 };

src/modelchecker/AbstractModelChecker.h

@@ -52,7 +52,7 @@ class AbstractModelChecker :
 	public virtual storm::formula::INextModelChecker<Type>,
 	public virtual storm::formula::IBoundedUntilModelChecker<Type>,
 	public virtual storm::formula::IBoundedEventuallyModelChecker<Type>,
-	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IPathNoBoundOperatorModelChecker<Type>,
 	public virtual storm::formula::IProbabilisticBoundOperatorModelChecker<Type>,
 	public virtual storm::formula::IRewardBoundOperatorModelChecker<Type>,
 	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
@@ -154,7 +154,7 @@ public:
 	 *
 	 * @param noBoundFormula The formula to be checked.
 	 */
-	void check(storm::formula::NoBoundOperator<Type> const& noBoundFormula) const {
+	void check(storm::formula::PathNoBoundOperator<Type> const& noBoundFormula) const {
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
 		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;

src/modelchecker/SparseDtmcPrctlModelChecker.h

@@ -64,7 +64,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	std::vector<Type>* checkNoBoundOperator(storm::formula::NoBoundOperator<Type> const& formula) const {
+	std::vector<Type>* checkPathNoBoundOperator(storm::formula::PathNoBoundOperator<Type> const& formula) const {
 		// Check if the operator was an optimality operator and report a warning in that case.
 		if (formula.isOptimalityOperator()) {
 			LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");

src/modelchecker/SparseMdpPrctlModelChecker.h

@@ -66,7 +66,7 @@ public:
 	 * @param formula The formula to check.
 	 * @returns The set of states satisfying the formula represented by a bit vector.
 	 */
-	std::vector<Type>* checkNoBoundOperator(const storm::formula::NoBoundOperator<Type>& formula) const {
+	std::vector<Type>* checkPathNoBoundOperator(const storm::formula::PathNoBoundOperator<Type>& formula) const {
 		// Check if the operator was an non-optimality operator and report an error in that case.
 		if (!formula.isOptimalityOperator()) {
 			LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");

src/parser/CslParser.cpp

@@ -148,9 +148,9 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 	qi::rule<Iterator, storm::formula::SteadyStateBoundOperator<double>*(), Skipper> steadyStateBoundOperator;
 	qi::rule<Iterator, storm::formula::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator;
 
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> noBoundOperator;
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> noBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
 
 	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula;
 	qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually;

src/parser/PrctlFileParser.cpp

@@ -67,7 +67,7 @@ void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractM
 			if (stateFormula != nullptr) {
 				modelChecker->check(*stateFormula);
 			}
-			storm::formula::NoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::formula::NoBoundOperator<double>*>(parser.getFormula());
+			storm::formula::PathNoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::formula::PathNoBoundOperator<double>*>(parser.getFormula());
 			if (noBoundFormula != nullptr) {
 				modelChecker->check(*noBoundFormula);
 			}

src/parser/PrctlParser.cpp

@@ -140,9 +140,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 	qi::rule<Iterator, storm::formula::ProbabilisticBoundOperator<double>*(), Skipper> probabilisticBoundOperator;
 	qi::rule<Iterator, storm::formula::RewardBoundOperator<double>*(), Skipper> rewardBoundOperator;
 
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> noBoundOperator;
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
-	qi::rule<Iterator, storm::formula::NoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> noBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> probabilisticNoBoundOperator;
+	qi::rule<Iterator, storm::formula::PathNoBoundOperator<double>*(), Skipper> rewardNoBoundOperator;
 
 	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula;
 	qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually;