Removed const declarations for the vistor callbacks, as the visitor

should be able to store information on the formulas during the process.

src/formula/Ltl/AbstractLtlFormula.h

@@ -79,7 +79,7 @@ public:
 	 *	@param visitor The visitor object.
 	 *	@return true iff all subtrees are valid.
 	 */
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const = 0;
 };
 
 } /* namespace ltl */

src/formula/Ltl/And.h

@@ -53,7 +53,7 @@ class IAndVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitAnd(const And<T>& obj) const = 0;
+		virtual void visitAnd(const And<T>& obj) = 0;
 };
 
 /*!
@@ -135,7 +135,7 @@ public:
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IAndVisitor>()->visitAnd(*this);
 	}
 

src/formula/Ltl/Ap.h

@@ -51,7 +51,7 @@ class IApVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitAp(const Ap<T>& obj) const = 0;
+		virtual void visitAp(const Ap<T>& obj) = 0;
 };
 
 /*!
@@ -118,7 +118,7 @@ public:
 		return new Ap(this->getAp());
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IApVisitor>()->visitAp(*this);
 	}
 };

src/formula/Ltl/BoundedEventually.h

@@ -54,7 +54,7 @@ class IBoundedEventuallyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitBoundedEventually(const BoundedEventually<T>& obj) const = 0;
+		virtual void visitBoundedEventually(const BoundedEventually<T>& obj) = 0;
 };
 
 /*!
@@ -134,7 +134,7 @@ public:
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IBoundedEventuallyVisitor>()->visitBoundedEventually(*this);
 	}
 };

src/formula/Ltl/BoundedUntil.h

@@ -53,7 +53,7 @@ class IBoundedUntilVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitBoundedUntil(const BoundedUntil<T>& obj) const = 0;
+		virtual void visitBoundedUntil(const BoundedUntil<T>& obj) = 0;
 };
 
 /*!
@@ -151,7 +151,7 @@ public:
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IBoundedUntilVisitor>()->visitBoundedUntil(*this);
 	}
 };

src/formula/Ltl/Eventually.h

@@ -51,7 +51,7 @@ class IEventuallyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitEventually(const Eventually<T>& obj) const = 0;
+		virtual void visitEventually(const Eventually<T>& obj) = 0;
 };
 
 /*!
@@ -128,7 +128,7 @@ public:
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IEventuallyVisitor>()->visitEventually(*this);
 	}
 };

src/formula/Ltl/Globally.h

@@ -52,7 +52,7 @@ class IGloballyVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitGlobally(const Globally<T>& obj) const = 0;
+		virtual void visitGlobally(const Globally<T>& obj) = 0;
 };
 
 /*!
@@ -130,7 +130,7 @@ public:
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IGloballyVisitor>()->visitGlobally(*this);
 	}
 };

src/formula/Ltl/Next.h

@@ -51,7 +51,7 @@ class INextVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitNext(const Next<T>& obj) const = 0;
+		virtual void visitNext(const Next<T>& obj) = 0;
 };
 
 /*!
@@ -128,7 +128,7 @@ public:
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<INextVisitor>()->visitNext(*this);
 	}
 };

src/formula/Ltl/Not.h

@@ -51,7 +51,7 @@ class INotVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitNot(const Not<T>& obj) const = 0;
+		virtual void visitNot(const Not<T>& obj) = 0;
 };
 
 /*!
@@ -124,7 +124,7 @@ public:
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<INotVisitor>()->visitNot(*this);
 	}
 };

src/formula/Ltl/Or.h

@@ -50,7 +50,7 @@ class IOrVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitOr(const Or<T>& obj) const = 0;
+		virtual void visitOr(const Or<T>& obj) = 0;
 };
 
 /*!
@@ -129,7 +129,7 @@ public:
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IOrVisitor>()->visitOr(*this);
 	}
 

src/formula/Ltl/Until.h

@@ -51,7 +51,7 @@ class IUntilVisitor {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual void visitUntil(const Until<T>& obj) const = 0;
+		virtual void visitUntil(const Until<T>& obj) = 0;
 };
 
 /*!
@@ -145,7 +145,7 @@ public:
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 
-	virtual void visit(const visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
+	virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const {
 		visitor.template as<IUntilVisitor>()->visitUntil(*this);
 	}
 };

src/formula/Ltl/visitor/AbstractLtlFormulaVisitor.h

@@ -49,9 +49,9 @@ public:
 	 * If the model checker is not of the requested type, type casting will fail and result in an exception.
 	 */
 	template <template <class Type> class Target>
-	const Target<T>* as() const {
+	Target<T>* as() {
 		try {
-			const Target<T>* target = dynamic_cast<const Target<T>*>(this);
+			Target<T>* target = dynamic_cast<Target<T>*>(this);
 			return target;
 		} catch (std::bad_cast& bc) {
 			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<T>).name() << ".");