Mass-added Keyword "override"

src/formula/ComparisonType.h

@@ -2,7 +2,7 @@
  * ComparisonType.h
  *
  *  Created on: 17.04.2013
- *      Author: thomas
+ *      Author: Thomas Heinemann
  */
 
 #ifndef STORM_FORMULA_COMPARISONTYPE_H_

src/formula/Csl.h

@@ -2,7 +2,7 @@
  * Csl.h
  *
  *  Created on: 19.04.2013
- *      Author: thomas
+ *      Author: Thomas Heinemann
  */
 
 #ifndef STORM_FORMULA_CSL_H_
@@ -28,5 +28,4 @@
 
 #include "modelchecker/csl/AbstractModelChecker.h"
 
-
 #endif /* STORM_FORMULA_CSL_H_ */

src/formula/Csl/AbstractCslFormula.h

@@ -25,13 +25,6 @@ public:
 	}
 };
 
-/*!
- * @brief An encapsulation type for the Return Type of the CslParser. As a pure virtual Class can not be an r-value return type, it has to be encapsulated.
- * @see CslParser
- */
-template <typename T>
-using AbstractCslFormularRef_t = std::reference_wrapper<storm::property::csl::AbstractCslFormula<T>>;
-
 } /* namespace csl */
 } /* namespace property */
 } /* namespace storm */

src/formula/Csl/And.h

@@ -94,7 +94,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		And<T>* result = new And();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -114,7 +114,7 @@ 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::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 

src/formula/Csl/Ap.h

@@ -78,7 +78,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		return new Ap(this->getAp());
 	}
 
@@ -91,7 +91,7 @@ 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::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 

src/formula/Csl/Eventually.h

@@ -91,7 +91,7 @@ public:
 	 *
 	 * @returns a new Eventually-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Eventually<T>* result = new Eventually<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -108,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::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
 	}
 };

src/formula/Csl/Globally.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new Globally-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Globally<T>* result = new Globally<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -110,7 +110,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
 	}
 };

src/formula/Csl/Next.h

@@ -91,7 +91,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Next<T>* result = new Next<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -108,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::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
 	}
 };

src/formula/Csl/Not.h

@@ -87,7 +87,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		Not<T>* result = new Not<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -104,7 +104,7 @@ 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::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 };

src/formula/Csl/Or.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		Or<T>* result = new Or();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -113,7 +113,7 @@ 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::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 };

src/formula/Csl/ProbabilisticBoundOperator.h

@@ -92,7 +92,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
 		result->setComparisonOperator(this->getComparisonOperator());
 		result->setBound(this->getBound());
@@ -109,7 +109,7 @@ 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::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
 	}
 };

src/formula/Csl/ProbabilisticNoBoundOperator.h

@@ -84,7 +84,7 @@ public:
 		// Intentionally left empty
 	}
 
-	virtual AbstractNoBoundOperator<T>* clone() const {
+	virtual AbstractNoBoundOperator<T>* clone() const override {
 		ProbabilisticNoBoundOperator<T>* result = new ProbabilisticNoBoundOperator<T>();
 		if (this->pathFormulaIsSet()) {
 			result->setPathFormula(this->getPathFormula().clone());
@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };

src/formula/Csl/SteadyStateBoundOperator.h

@@ -90,7 +90,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		SteadyStateBoundOperator<T>* result = new SteadyStateBoundOperator<T>();
 		result->setStateFormula(this->getStateFormula().clone());
 		return result;
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*this);
 	}
 	

src/formula/Csl/SteadyStateNoBoundOperator.h

@@ -72,7 +72,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractNoBoundOperator <T>* clone() const {
+	virtual AbstractNoBoundOperator <T>* clone() const override {
 		SteadyStateNoBoundOperator<T>* result = new SteadyStateNoBoundOperator<T>();
 		result->setStateFormula(this->getStateFormula().clone());
 		return result;
@@ -87,7 +87,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>*  check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>*  check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
 		return modelChecker.template as<ISteadyStateNoBoundOperatorModelChecker>()->checkSteadyStateNoBoundOperator(*this);
 	}
 

src/formula/Csl/TimeBoundedEventually.h

@@ -68,7 +68,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		TimeBoundedEventually<T>* result = new TimeBoundedEventually<T>(this->getLowerBound(), this->getUpperBound());
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -85,7 +85,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
 	}
 };

src/formula/Csl/TimeBoundedUntil.h

@@ -78,7 +78,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		TimeBoundedUntil<T>* result = new TimeBoundedUntil<T>(this->getLowerBound(), this->getUpperBound());
 		if (this->leftIsSet()) {
 			result->setLeft(this->getLeft().clone());
@@ -99,7 +99,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
 	}
 };

src/formula/Csl/Until.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Until<T>* result = new Until();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
 	}
 };

src/formula/Ltl.h

@@ -2,7 +2,7 @@
  * Ltl.h
  *
  *  Created on: 22.04.2013
- *      Author: thomas
+ *      Author: Thomas Heinemann
  */
 
 #ifndef STORM_FORMULA_LTL_H_

src/formula/Ltl/AbstractLtlFormula.h

@@ -82,9 +82,6 @@ public:
 	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
 };
 
-template <typename T>
-using AbstractLtlFormularSharedPtr_t = std::shared_ptr<T>;
-
 } /* namespace ltl */
 } /* namespace property */
 } /* namespace storm */

src/formula/Ltl/And.h

@@ -111,7 +111,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		And<T>* result = new And();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -131,7 +131,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 

src/formula/Ltl/Ap.h

@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
@@ -114,7 +114,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		return new Ap(this->getAp());
 	}
 

src/formula/Ltl/BoundedEventually.h

@@ -111,7 +111,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		BoundedEventually<T>* result = new BoundedEventually<T>();
 		result->setBound(this->getBound());
 		if (this->childIsSet()) {
@@ -130,7 +130,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 

src/formula/Ltl/BoundedUntil.h

@@ -125,7 +125,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		BoundedUntil<T>* result = new BoundedUntil<T>();
 		result->setBound(this->getBound());
 		if (this->leftIsSet()) {

src/formula/Ltl/Eventually.h

@@ -107,7 +107,7 @@ public:
 	 *
 	 * @returns a new Eventually-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Eventually<T>* result = new Eventually<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());

src/formula/Ltl/Globally.h

@@ -109,7 +109,7 @@ public:
 	 *
 	 * @returns a new Globally-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Globally<T>* result = new Globally<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());

src/formula/Ltl/Next.h

@@ -107,7 +107,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Next<T>* result = new Next<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());

src/formula/Ltl/Not.h

@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Not<T>* result = new Not<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
 

src/formula/Ltl/Or.h

@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Or<T>* result = new Or();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -125,7 +125,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 

src/formula/Ltl/Until.h

@@ -121,7 +121,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractLtlFormula<T>* clone() const {
+	virtual AbstractLtlFormula<T>* clone() const override {
 		Until<T>* result = new Until();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());

src/formula/Prctl.h

@@ -2,7 +2,7 @@
  * Prctl.h
  *
  *  Created on: 06.12.2012
- *      Author: chris
+ *      Author: Christian Dehnert
  */
 
 #ifndef STORM_FORMULA_PRCTL_H_

src/formula/Prctl/And.h

@@ -94,7 +94,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		And<T>* result = new And();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -114,7 +114,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 

src/formula/Prctl/Ap.h

@@ -78,7 +78,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		return new Ap(this->getAp());
 	}
 
@@ -91,7 +91,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 

src/formula/Prctl/BoundedEventually.h

@@ -95,7 +95,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		BoundedEventually<T>* result = new BoundedEventually<T>();
 		result->setBound(this->getBound());
 		if (this->childIsSet()) {
@@ -114,7 +114,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
 	}
 };

src/formula/Prctl/BoundedNaryUntil.h

@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns a new BoundedNaryUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
 		if (this->leftIsSet()) {
 			result->setLeft(this->getLeft().clone());
@@ -128,7 +128,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
 	}
 

src/formula/Prctl/BoundedUntil.h

@@ -97,7 +97,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		BoundedUntil<T>* result = new BoundedUntil<T>();
 		result->setBound(this->getBound());
 		if (this->leftIsSet()) {
@@ -119,7 +119,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
 	}
 };

src/formula/Prctl/CumulativeReward.h

@@ -84,7 +84,7 @@ public:
 	 *
 	 * @returns a new CumulativeReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		return new CumulativeReward(this->getBound());
 	}
 
@@ -98,7 +98,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this, qualitative);
 	}
 };

src/formula/Prctl/Eventually.h

@@ -91,7 +91,7 @@ public:
 	 *
 	 * @returns a new Eventually-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Eventually<T>* result = new Eventually<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -108,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::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
 	}
 };

src/formula/Prctl/Globally.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new Globally-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Globally<T>* result = new Globally<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -110,7 +110,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
 	}
 };

src/formula/Prctl/InstantaneousReward.h

@@ -85,7 +85,7 @@ public:
 	 *
 	 * @returns a new InstantaneousReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		return new InstantaneousReward(this->getBound());
 	}
 
@@ -99,7 +99,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
 	}
 };

src/formula/Prctl/Next.h

@@ -91,7 +91,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Next<T>* result = new Next<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -108,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::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
 	}
 };

src/formula/Prctl/Not.h

@@ -87,7 +87,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		Not<T>* result = new Not<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -104,7 +104,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 };

src/formula/Prctl/Or.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		Or<T>* result = new Or();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -113,7 +113,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 };

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -110,7 +110,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
 		result->setComparisonOperator(this->getComparisonOperator());
 		result->setBound(this->getBound());
@@ -127,7 +127,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
 	}
 };

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -84,7 +84,7 @@ public:
 		// Intentionally left empty
 	}
 
-	virtual AbstractNoBoundOperator<T>* clone() const {
+	virtual AbstractNoBoundOperator<T>* clone() const override {
 		ProbabilisticNoBoundOperator<T>* result = new ProbabilisticNoBoundOperator<T>();
 		if (this->pathFormulaIsSet()) {
 			result->setPathFormula(this->getPathFormula().clone());
@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };

src/formula/Prctl/ReachabilityReward.h

@@ -88,7 +88,7 @@ public:
 	 *
 	 * @returns a new ReachabilityReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		ReachabilityReward<T>* result = new ReachabilityReward<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
 	}
 };

src/formula/Prctl/RewardBoundOperator.h

@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
+	virtual AbstractStateFormula<T>* clone() const override {
 		RewardBoundOperator<T>* result = new RewardBoundOperator<T>();
 		result->setComparisonOperator(this->getComparisonOperator());
 		result->setBound(this->getBound());
@@ -120,7 +120,7 @@ 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::prctl::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
 		return modelChecker.template as<IRewardBoundOperatorModelChecker>()->checkRewardBoundOperator(*this);
 	}
 };

src/formula/Prctl/RewardNoBoundOperator.h

@@ -77,7 +77,7 @@ public:
 		// Intentionally left empty
 	}
 
-	virtual AbstractNoBoundOperator<T>* clone() const {
+	virtual AbstractNoBoundOperator<T>* clone() const override {
 		RewardNoBoundOperator<T>* result = new RewardNoBoundOperator<T>();
 		if (this->pathFormulaIsSet()) {
 			result->setPathFormula(this->getPathFormula().clone());
@@ -96,7 +96,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };

src/formula/Prctl/SteadyStateReward.h

@@ -67,7 +67,7 @@ public:
 	 *
 	 * @returns a new SteadyState-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		return new SteadyStateReward<T>();
 	}
 
@@ -80,7 +80,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
 	}
 };

src/formula/Prctl/Until.h

@@ -93,7 +93,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
+	virtual AbstractPathFormula<T>* clone() const override {
 		Until<T>* result = new Until();
 		if (this->leftIsSet()) {
 		  result->setLeft(this->getLeft().clone());
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
 	}
 };

src/formula/abstract/And.h

@@ -130,7 +130,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "(";
 		result += left->toString();
 		result += " & ";
@@ -145,7 +145,7 @@ public:
 	 *	@param checker Formula checker object.
 	 *	@return true iff all subtrees conform to some logic.
 	 */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->left) && checker.validate(this->right);
     }
 

src/formula/abstract/Ap.h

@@ -55,7 +55,7 @@ public:
 	 * @returns a string representation of the leaf.
 	 *
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		return getAp();
 	}
 	
@@ -67,7 +67,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return true;
 	}
 

src/formula/abstract/BoundedEventually.h

@@ -118,7 +118,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "F<=";
 		result += std::to_string(bound);
 		result += " ";
@@ -132,7 +132,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->child);
 	}
 

src/formula/abstract/BoundedNaryUntil.h

@@ -138,7 +138,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::stringstream result;
 		result << "( " << left->toString();
 		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
@@ -154,7 +154,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff all subtrees conform to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		bool res = checker.validate(this->left);
 		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
 			res &= checker.validate(std::get<0>(*it));

src/formula/abstract/BoundedUntil.h

@@ -148,7 +148,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = left->toString();
 		result += " U<=";
 		result += std::to_string(bound);
@@ -163,7 +163,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff all subtrees conform to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 

src/formula/abstract/CumulativeReward.h

@@ -72,7 +72,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "C <= ";
 		result += std::to_string(bound);
 		return result;
@@ -86,7 +86,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true
      */	
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return true;
 	}
 

src/formula/abstract/Eventually.h

@@ -96,7 +96,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "F ";
 		result += child->toString();
 		return result;
@@ -108,7 +108,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->child);
 	}
 

src/formula/abstract/Globally.h

@@ -97,7 +97,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "G ";
 		result += child->toString();
 		return result;
@@ -109,7 +109,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->child);
 	}
 

src/formula/abstract/InstantaneousReward.h

@@ -72,7 +72,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "I=";
 		result += std::to_string(bound);
 		return result;
@@ -86,7 +86,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return true;
 	}
 

src/formula/abstract/Next.h

@@ -97,7 +97,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "(";
 		result += " X ";
 		result += child->toString();
@@ -111,7 +111,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->child);
     }
 

src/formula/abstract/Not.h

@@ -93,7 +93,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "!";
 		result += child->toString();
 		return result;
@@ -105,7 +105,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->child);
 	}
 

src/formula/abstract/Or.h

@@ -128,7 +128,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "(";
 		result += left->toString();
 		result += " | ";
@@ -143,7 +143,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff all subtrees conform to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->left) && checker.validate(this->right);
     }
 

src/formula/abstract/PathBoundOperator.h

@@ -143,7 +143,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "";
 		switch (comparisonOperator) {
 		case LESS: result += "<"; break;
@@ -175,7 +175,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->pathFormula);
     }
 

src/formula/abstract/PathNoBoundOperator.h

@@ -122,7 +122,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result;
 		if (this->isOptimalityOperator()) {
 			if (this->isMinimumOperator()) {
@@ -143,7 +143,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->pathFormula);
 	}
 

src/formula/abstract/ProbabilisticBoundOperator.h

@@ -100,7 +100,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "P ";
 		result += PathBoundOperator<T, FormulaType>::toString();
 		return result;

src/formula/abstract/ProbabilisticNoBoundOperator.h

@@ -90,7 +90,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "P";
 		result += PathNoBoundOperator<T, FormulaType>::toString();
 		return result;

src/formula/abstract/RewardBoundOperator.h

@@ -92,7 +92,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "R ";
 		result += PathBoundOperator<T, FormulaType>::toString();
 		return result;

src/formula/abstract/RewardNoBoundOperator.h

@@ -89,7 +89,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "R";
 		result += PathNoBoundOperator<T, FormulaType>::toString();
 		return result;

src/formula/abstract/StateBoundOperator.h

@@ -126,7 +126,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = " ";
 		switch (comparisonOperator) {
 		case LESS: result += "< "; break;
@@ -157,7 +157,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->stateFormula);
     }
 

src/formula/abstract/StateNoBoundOperator.h

@@ -98,7 +98,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result;
 		result += " = ? [";
 		result += this->getStateFormula().toString();
@@ -112,7 +112,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->stateFormula);
 	}
 

src/formula/abstract/SteadyStateBoundOperator.h

@@ -65,7 +65,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		return "S" + StateBoundOperator<T, FormulaType>::toString();
 	}
 };

src/formula/abstract/SteadyStateNoBoundOperator.h

@@ -63,7 +63,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		return "S" + StateNoBoundOperator<T, FormulaType>::toString();
 	}
 

src/formula/abstract/SteadyStateReward.h

@@ -39,7 +39,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		return "S";
 	}
 
@@ -51,7 +51,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return true;
 	}
 };

src/formula/abstract/TimeBoundedEventually.h

@@ -78,7 +78,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "F";
 		result += TimeBoundedOperator<T>::toString();
 		result += " ";
@@ -92,7 +92,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->child);
 	}
 

src/formula/abstract/TimeBoundedOperator.h

@@ -87,7 +87,7 @@ public:
 	 * @returns a string representation of the Interval of the formula
 	 * 			May be used in subclasses to simplify string output.
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = "";
 		if (upperBound == std::numeric_limits<double>::infinity()) {
 			result = ">=" + std::to_string(lowerBound);

src/formula/abstract/TimeBoundedUntil.h

@@ -118,7 +118,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = left->toString();
 		result += " U";
 		result += TimeBoundedOperator<T>::toString();
@@ -133,7 +133,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff the subtree conforms to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
 		return checker.validate(this->left) && checker.validate(this->right);
 	}
 

src/formula/abstract/Until.h

@@ -128,7 +128,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() const {
+	virtual std::string toString() const override {
 		std::string result = left->toString();
 		result += " U ";
 		result += right->toString();
@@ -141,7 +141,7 @@ public:
      *  @param checker Formula checker object.
      *  @return true iff all subtrees conform to some logic.
      */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const {
+	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
         return checker.validate(this->left) && checker.validate(this->right);
     }
 

src/ir/expressions/BooleanLiteral.h

@@ -0,0 +1,62 @@
+/*
+ * BooleanLiteral.h
+ *
+ *  Created on: 03.01.2013
+ *      Author: chris
+ */
+
+#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_
+#define STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_
+
+#include "src/ir/expressions/BaseExpression.h"
+
+namespace storm {
+namespace ir {
+namespace expressions {
+
+class BooleanLiteral : public BaseExpression {
+public:
+	bool value;
+
+	BooleanLiteral(bool value) : BaseExpression(bool_), value(value) {
+
+	}
+
+	virtual ~BooleanLiteral() {
+
+	}
+
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
+		return std::shared_ptr<BaseExpression>(new BooleanLiteral(this->value));
+	}
+
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
+		return value;
+	}
+
+	virtual void accept(ExpressionVisitor* visitor) override {
+		visitor->visit(this);
+	}
+
+	virtual std::string toString() const override {
+		if (value) {
+			return std::string("true");
+		} else {
+			return std::string("false");
+		}
+	}
+	
+	virtual std::string dump(std::string prefix) const override {
+		std::stringstream result;
+		result << prefix << "BooleanLiteral " << this->toString() << std::endl;
+		return result.str();
+	}
+};
+
+}
+
+}
+
+}
+
+#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ */

src/ir/expressions/DoubleLiteral.h

@@ -0,0 +1,62 @@
+/*
+ * DoubleLiteral.h
+ *
+ *  Created on: 03.01.2013
+ *      Author: chris
+ */
+
+#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_
+#define STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_
+
+#include "src/ir/expressions/BaseExpression.h"
+
+#include "boost/lexical_cast.hpp"
+
+namespace storm {
+
+namespace ir {
+
+namespace expressions {
+
+class DoubleLiteral : public BaseExpression {
+public:
+	double value;
+
+	DoubleLiteral(double value) : BaseExpression(double_), value(value) {
+
+	}
+
+	virtual ~DoubleLiteral() {
+
+	}
+
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
+		return std::shared_ptr<BaseExpression>(new DoubleLiteral(this->value));
+	}
+
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
+		return value;
+	}
+
+	virtual void accept(ExpressionVisitor* visitor) override {
+		visitor->visit(this);
+	}
+
+	virtual std::string toString() const override {
+		return boost::lexical_cast<std::string>(value);
+	}
+	
+	virtual std::string dump(std::string prefix) const override {
+		std::stringstream result;
+		result << prefix << "DoubleLiteral " << this->toString() << std::endl;
+		return result.str();
+	}
+};
+
+}
+
+}
+
+}
+
+#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ */

src/ir/expressions/IntegerLiteral.h

@@ -0,0 +1,58 @@
+/*
+ * IntegerLiteral.h
+ *
+ *  Created on: 03.01.2013
+ *      Author: chris
+ */
+
+#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_
+#define STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_
+
+#include "src/ir/expressions/BaseExpression.h"
+
+namespace storm {
+
+namespace ir {
+
+namespace expressions {
+
+class IntegerLiteral : public BaseExpression {
+public:
+	int_fast64_t value;
+
+	IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) {
+	}
+
+	virtual ~IntegerLiteral() {
+	}
+
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) override {
+		return std::shared_ptr<BaseExpression>(new IntegerLiteral(this->value));
+	}
+
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override {
+		return value;
+	}
+
+	virtual void accept(ExpressionVisitor* visitor) override {
+		visitor->visit(this);
+	}
+	
+	virtual std::string toString() const override {
+		return boost::lexical_cast<std::string>(value);
+	}
+
+	virtual std::string dump(std::string prefix) const override {
+		std::stringstream result;
+		result << prefix << "IntegerLiteral " << this->toString() << std::endl;
+		return result.str();
+	}
+};
+
+}
+
+}
+
+}
+
+#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ */