Removed actions and filters and old logic classes.

Former-commit-id: cd487fd3b3

src/properties/AbstractFilter.h

@@ -1,231 +0,0 @@
-#ifndef STORM_PROPERTIES_ABSTRACTFILTER_H_
-#define STORM_PROPERTIES_ABSTRACTFILTER_H_
-
-#include <vector>
-#include <string>
-#include "src/properties/AbstractFormula.h"
-#include "src/properties/actions/AbstractAction.h"
-
-namespace storm {
-	namespace properties {
-
-		/*!
-		 * This enum contains value indicating which kind of scheduler is to be used
-		 * for path formulas, i.e. probability or reward queries on nondeterministic models.
-		 */
-		enum OptimizingOperator {MINIMIZE, MAXIMIZE, UNDEFINED};
-
-		/*!
-		 * This is the base class for the logic specific filter classes.
-		 * It provides the logic independent functionality concerning the organization of actions and the optimization operator.
-		 *
-		 * The general role of the filter is to twofold.
-		 *
-		 * On the one hand it is meant to be the interface between the control and the formulas and modelchecker.
-		 * It sits one level above the root of the formula tree which is represented by it.
-		 * This gives a distinct class that can be moved through the control functions, thus encapsulating the formula tree and all its classes.
-		 *
-		 * On the other hand, as all modelchecking is initiated through its interface it opens up the opportunity to manipulate the output generated by the modelchecker.
-		 * The manipulation is done by a series of filter actions which are evaluated after the modelchecker has finished.
-		 * Each action has a distinct function that ranges from state selection to sorting.
-		 * The input for the first filter action consists mainly of the modelckecking result.
-		 * Thereafter, the result of each filter action is used as input for the next filter action until all actions have been executed.
-		 * The final result is then used to generate the output.
-		 */
-		template <class T>
-		class AbstractFilter {
-
-		public:
-
-			/*!
-			 * Constructs an empty AbstractFilter.
-			 * If a value for the optimization operator is given it will be set accordingly.
-			 * Otherwise, it will be undefined. The undefined value is intended for deterministic
-			 * models, as the do not need a scheduler resolving the nondeterminism.
-			 *
-			 * @note If a query is executed on a nondeterministic model using an undefined optimization operator
-			 *       the modelchecker will throw an exception.
-			 *
-			 * @param opt The value of the optimization operator.
-			 */
-			AbstractFilter(OptimizingOperator opt = UNDEFINED) : opt(opt) {
-				// Intentionally left empty.
-			}
-
-			/*!
-			 * Constructs an AbstractFilter containing only the specified action.
-			 *
-			 * @note If the shared_ptr to the action is empty (contains a nullptr) the Abstract filter will be created empty.
-			 *
-			 * @param action The action to be executed during evaluation.
-			 * @param opt The value of the optimization operator.
-			 */
-			AbstractFilter(std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : opt(opt) {
-				if(action.get() != nullptr) {
-					actions.push_back(action);
-				}
-			}
-
-			/*!
-			 * Constructs an AbstractFilter containing the given vector of actions as action list.
-			 * The actions will be executed in ascending order of index.
-			 *
-			 * @note Any vector entry containing an empty shared_ptr will be ignored. Thus, giving a
-			 *       vector of five actions with two empty shared_ptr will result in a AbstractFilter containing three actions.
-			 *
-			 * @param actions A vector of shared_ptr to the actions to be executed during evaluation.
-			 * @param opt The value of the optimization operator.
-			 */
-			AbstractFilter(std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) {
-				// Filter out all nullptr actions.
-				// First detect that there is at least one.
-				uint_fast64_t emptyCount = 0;
-				for(uint_fast64_t i = 0; i < actions.size(); i++) {
-					if (actions[i].get() == nullptr) {
-						emptyCount++;
-					}
-				}
-
-				if(emptyCount > 0) {
-					// There is at least one nullptr action.
-					// Allocate space for the non null actions.
-					this->actions.reserve(actions.size() - emptyCount);
-
-					// Fill the vector. Note: For most implementations of the standard there will be no reallocation in the vector while doing this.
-					for(auto action : actions) {
-						if(action.get() != nullptr) {
-							this->actions.push_back(action);
-						}
-					}
-				} else {
-					this->actions = actions;
-				}
-
-				this->opt = opt;
-			}
-
-			/*!
-			 * The virtual destructor.
-			 */
-			virtual ~AbstractFilter() {
-				// Intentionally left empty.
-			}
-
-			/*!
-			 * Returns a string representation of the filter.
-			 *
-			 * @returns A string representing the filter.
-			 */
-			virtual std::string toString() const {
-				std::string desc = "filter(";
-
-				for(auto action : actions) {
-					desc += action->toString();
-					desc += ", ";
-				}
-
-				// Remove the last ", ".
-				if(!actions.empty()) {
-					desc.pop_back();
-					desc.pop_back();
-				}
-
-				desc += ")";
-
-				return desc;
-			}
-
-			/*!
-			 * Appends the given action to the list of actions to be executed during evaluation.
-			 *
-			 * @note If the argument is an empty shared_ptr nothing will happen.
-			 *
-			 * @param action A shared pointer to the action to be appended.
-			 */
-			void addAction(std::shared_ptr<action::AbstractAction<T>> const & action) {
-				if(action.get() != nullptr) {
-					actions.push_back(action);
-				}
-			}
-
-			/*!
-			 * Removes the last action.
-			 */
-			void removeAction() {
-				actions.pop_back();
-			}
-
-			/*!
-			 * Returns the action at the specified position.
-			 *
-			 * @param position The position of the action to be returned within the action list.
-			 * @returns A shared pointer to the specified action.
-			 */
-			std::shared_ptr<action::AbstractAction<T>> getAction(uint_fast64_t position) {
-				// Make sure the chosen position is not beyond the end of the vector.
-				// If it is so return the last element.
-				if(position < actions.size()) {
-					return actions[position];
-				} else {
-					return actions[actions.size()-1];
-				}
-			}
-
-			/*!
-			 * Returns the number of actions to be executed during evaluation.
-			 *
-			 * @returns The number of actions in the action list.
-			 */
-			uint_fast64_t getActionCount() const {
-				return actions.size();
-			}
-
-			/*!
-			 * Sets whether a minimizing or a maximizing scheduler is to be used for
-			 * modelchecking of path formulas, i.e. probability and reward queries.
-			 *
-			 * @param opt The new operator specifying the scheduler to be used for path formulas.
-			 */
-			void setOptimizingOperator(OptimizingOperator opt) {
-				this->opt = opt;
-			}
-
-			/*!
-			 * Returns the current optimization operator.
-			 *
-			 * @return The optimization operator.
-			 */
-			OptimizingOperator getOptimizingOperator() const {
-				return opt;
-			}
-
-		protected:
-
-			//! The vector containing the actions to be executed during evaluation.
-			std::vector<std::shared_ptr<action::AbstractAction<T>>> actions;
-
-			//! The optimization operator specifying if and which kind of scheduler is to be used during modelchecking of path formulas on nondeterministic models.
-			OptimizingOperator opt;
-		};
-
-		/*!
-		 * Overloads the stream operator for AbstractFilter and thus all filter classes.
-		 *
-		 * @param os The output stream to which the string representation of the filter is to be appended.
-		 * @param filter The filter whose string representation is to be appended to the given output stream.
-		 * @returns A reference to an output stream containing the contents of the output stream given as input,
-		 *          appended with the string representation of the given filter.
-		 */
-		template <class T>
-		std::ostream & operator<<(std::ostream& os, AbstractFilter<T> const & filter) {
-
-			os << filter.toString();
-			return os;
-		}
-
-	} // namespace properties
-} // namespace storm
-
-
-
-#endif /* STORM_PROPERTIES_ABSTRACTFILTER_H_ */

src/properties/AbstractFormula.h

@@ -1,75 +0,0 @@
-#ifndef STORM_PROPERTIES_ABSTRACTFORMULA_H_
-#define STORM_PROPERTIES_ABSTRACTFORMULA_H_
-
-#include <string>
-#include <memory>
-
-namespace storm {
-	namespace properties {
-
-		// Forward declaration.
-		template <class T> class AbstractFormula;
-
-		/*!
-		 * This is the abstract base class for every formula class in every logic.
-		 *
-		 * There are currently three implemented logics Ltl, Csl and Pctl.
-		 * The implementation of these logics can be found in the namespaces storm::properties::<logic>
-		 * where <logic> is one of ltl, pctl and csl.
-		 *
-		 * @note While formula classes do have copy constructors using a copy constructor
-		 *       will yield a formula objects whose formula subtree consists of the same objects
-		 *       as the original formula. The ownership of the formula tree will be shared between
-		 *       the original and the copy.
-		 */
-		template <class T>
-		class AbstractFormula {
-
-		public:
-
-			/*!
-			 * The virtual destructor.
-			 */
-			virtual ~AbstractFormula() {
-				// Intentionally left empty.
-			}
-
-			/*!
-			 *	Return string representation of this formula.
-			 *
-			 *	@note Every subclass must implement this method.
-			 *
-			 *	@returns A string representation of the formula.
-			 */
-			virtual std::string toString() const = 0;
-
-			/*!
-			 * Returns whether the formula is a propositional logic formula.
-			 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-			 *
-			 * @return True iff this is a propositional logic formula.
-			 */
-			virtual bool isPropositional() const {
-				return false;
-			}
-		};
-
-		/*!
-		 * Overloads the stream operator for AbstractFormulas and thus all formula classes.
-		 *
-		 * @param os The output stream to which the string representation of the formula is to be appended.
-		 * @param formula The formula whose string representation is to be appended to the given output stream.
-		 * @returns A reference to an output stream containing the contents of the output stream given as input,
-		 *          appended with the string representation of the given formula.
-		 */
-		template <class T>
-		std::ostream & operator<<(std::ostream& os, AbstractFormula<T> const & formula) {
-
-			os << formula.toString();
-			return os;
-		}
-
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ABSTRACTFORMULA_H_ */

src/properties/ComparisonType.h

@@ -1,18 +0,0 @@
-#ifndef STORM_PROPERTIES_COMPARISONTYPE_H_
-#define STORM_PROPERTIES_COMPARISONTYPE_H_
-
-namespace storm {
-	namespace properties {
-
-		/*!
-		 * An enum representing the greater- and less-than operators in both
-		 * the strict (<, >) and the non strict (<=, >=) variant.
-		 * It is mainly used to represent upper and lower bounds.
-		 */
-		enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
-
-	}
-}
-
-
-#endif /* STORM_PROPERTIES_COMPARISONTYPE_H_ */

src/properties/Csl.h

@@ -1,22 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_H_
-#define STORM_PROPERTIES_CSL_H_
-
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-#include "csl/And.h"
-#include "csl/Ap.h"
-#include "csl/Next.h"
-#include "csl/Not.h"
-#include "csl/Or.h"
-#include "csl/ProbabilisticBoundOperator.h"
-#include "csl/SteadyStateBoundOperator.h"
-
-#include "csl/Until.h"
-#include "csl/Eventually.h"
-#include "csl/Globally.h"
-#include "csl/TimeBoundedEventually.h"
-#include "csl/TimeBoundedUntil.h"
-
-#include "modelchecker/csl/AbstractModelChecker.h"
-
-#endif /* STORM_PROPERTIES_CSL_H_ */

src/properties/Ltl.h

@@ -1,19 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_H_
-#define STORM_PROPERTIES_LTL_H_
-
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-
-#include "ltl/And.h"
-#include "ltl/Ap.h"
-#include "ltl/BoundedEventually.h"
-#include "ltl/BoundedUntil.h"
-#include "ltl/Eventually.h"
-#include "ltl/Globally.h"
-#include "ltl/Next.h"
-#include "ltl/Not.h"
-#include "ltl/Or.h"
-#include "ltl/Until.h"
-
-#include "modelchecker/ltl/AbstractModelChecker.h"
-
-#endif /* STORM_PROPERTIES_LTL_H_ */

src/properties/Prctl.h

@@ -1,33 +0,0 @@
-#ifndef STORM_PROPERTIES_PRCTL_H_
-#define STORM_PROPERTIES_PRCTL_H_
-
-#include "modelchecker/prctl/ForwardDeclarations.h"
-
-#include "prctl/And.h"
-#include "prctl/Ap.h"
-#include "prctl/BoundedUntil.h"
-#include "prctl/BoundedNaryUntil.h"
-#include "prctl/Next.h"
-#include "prctl/Not.h"
-#include "prctl/Or.h"
-#include "prctl/ProbabilisticBoundOperator.h"
-
-#include "prctl/Until.h"
-#include "prctl/Eventually.h"
-#include "prctl/Globally.h"
-#include "prctl/BoundedEventually.h"
-
-#include "prctl/InstantaneousReward.h"
-#include "prctl/CumulativeReward.h"
-#include "prctl/ReachabilityReward.h"
-#include "prctl/RewardBoundOperator.h"
-#include "prctl/SteadyStateReward.h"
-
-#include "prctl/AbstractPrctlFormula.h"
-#include "prctl/AbstractStateFormula.h"
-#include "prctl/AbstractPathFormula.h"
-#include "prctl/AbstractRewardPathFormula.h"
-
-#include "modelchecker/prctl/AbstractModelChecker.h"
-
-#endif /* STORM_PROPERTIES_PRCTL_H_ */

src/properties/actions/AbstractAction.h

@@ -1,140 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_ABSTRACTACTION_H_
-#define STORM_PROPERTIES_ACTION_ABSTRACTACTION_H_
-
-#include <vector>
-#include <utility>
-#include "src/storage/BitVector.h"
-#include "src/modelchecker/prctl/AbstractModelChecker.h"
-#include "src/modelchecker/csl/AbstractModelChecker.h"
-#include "src/modelchecker/ltl/AbstractModelChecker.h"
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * This is the abstract base class for all filter actions.
-			 *
-			 * Each action implements a distinct function which executed each time evaluate() is called.
-			 * The input and output for each action is an instance of the Result struct.
-			 * Thus the action is able to manipulate both the selection of output states and the order in which they are returned.
-			 */
-			template <class T>
-			class AbstractAction {
-
-			public:
-
-				/*!
-				 * This is the struct used by all actions to pass along information.
-				 *
-				 * It contains fields for the two possible data structures containing the modelchecking results.
-				 * A value vector for path formulas and a bit vector for state formulas.
-				 * The two other fields are used to describe a selection as well as an ordering of states within the modelchecking results.
-				 *
-				 * @note For each formula the modelchecker will return either a BitVector or a std::vector.
-				 *       Thus, either the state- or the pathResult should be set to be empty.
-				 *       If both contain a value for at least one state the pathResult will be used.
-				 *
-				 * @note The four vectors should always have the same number of entries.
-				 */
-				struct Result {
-
-					/*!
-					 * Constructs an empty Result.
-					 */
-					Result() : selection(), stateMap(), pathResult(), stateResult(){
-						// Intentionally left empty.
-					}
-
-					/*!
-					 * Copy constructs a Result.
-					 *
-					 * @param other The Result from which the fields are copied.
-					 */
-					Result(Result const & other) : selection(other.selection), stateMap(other.stateMap), pathResult(other.pathResult), stateResult(other.stateResult) {
-						// Intentionally left empty.
-					}
-
-					/*!
-					 * Constructs a Result using values for each field.
-					 *
-					 * @param selection A BitVector describing which states are currently selected.
-					 * @param stateMap A vector representing an ordering on the states within the modelchecking results.
-					 * @param pathResult The modelchecking result for a path formula.
-					 * @param stateResult The modelchecking result for a state formula.
-					 */
-					Result(storm::storage::BitVector const & selection, std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & pathResult, storm::storage::BitVector const & stateResult) : selection(selection), stateMap(stateMap), pathResult(pathResult), stateResult(stateResult) {
-						// Intentionally left empty.
-					}
-
-					//! A BitVector describing which states are currently selected.
-					//! For state i the i-th bit is true iff state i is selected.
-					storm::storage::BitVector selection;
-
-					//! A vector representing an ordering on the states within the modelchecking results.
-					//! The first value of the vector is the index of the state to be returned first.
-					//! Thus, stateMap[i] is the index of the state that is to be returned at position i.
-					std::vector<uint_fast64_t> stateMap;
-
-					//! The modelchecking result for a path formula.
-					std::vector<T> pathResult;
-
-					//! The modelchecking result for a state formula.
-					storm::storage::BitVector stateResult;
-				};
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~AbstractAction() {
-					//Intentionally left empty
-				}
-
-				/*!
-				 * Evaluate the action for a Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const {
-					return Result();
-				}
-
-				/*!
-				 * Evaluate the action for a Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const {
-					return Result();
-				}
-
-				/*!
-				 * Evaluate the action for an Ltl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const {
-					return Result();
-				}
-
-				/*!
-				 * Returns a string representation of the action.
-				 *
-				 * @returns A string representing the action.
-				 */
-				virtual std::string toString() const = 0;
-
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ACTION_ABSTRACTACTION_H_ */

src/properties/actions/BoundAction.h

@@ -1,205 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_BOUNDACTION_H_
-#define STORM_PROPERTIES_ACTION_BOUNDACTION_H_
-
-#include "src/properties/actions/AbstractAction.h"
-#include "src/properties/ComparisonType.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * The bound action deselects all states whose modelchecking values do not satisfy the given bound.
-			 *
-			 * Strict and non strict upper and lower bounds can be represented.
-			 * For modelchecking results of state formulas the value is taken to be 1 iff true and 0 otherwise.
-			 */
-			template <class T>
-			class BoundAction : public AbstractAction<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename AbstractAction<T>::Result Result;
-
-			public:
-
-				/*!
-				 * Constructs an empty BoundAction.
-				 * The bound is set to >= 0. Thus, all states will be selected by the action.
-				 */
-				BoundAction() : comparisonOperator(storm::properties::GREATER_EQUAL), bound(0) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * Constructs a BoundAction using the given values for the comparison operator and the bound.
-				 *
-				 * @param comparisonOperator The operator used to make the comparison between the bound and the modelchecking values for each state.
-				 * @param bound The bound to compare the modelchecking values against.
-				 */
-				BoundAction(storm::properties::ComparisonType comparisonOperator, T bound) : comparisonOperator(comparisonOperator), bound(bound) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~BoundAction() {
-					//Intentionally left empty
-				}
-
-				/*!
-				 * Evaluate the action for an Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for an Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for an Ltl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Returns a string representation of this action.
-				 *
-				 * @returns A string representing this action.
-				 */
-				virtual std::string toString() const override {
-					std::string out = "bound(";
-					switch (comparisonOperator) {
-						case LESS:
-							out += "<";
-							break;
-						case LESS_EQUAL:
-							out += "<=";
-							break;
-						case GREATER:
-							out += ">";
-							break;
-						case GREATER_EQUAL:
-							out += ">=";
-							break;
-						default:
-							LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-							throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
-							break;
-					}
-					out += ", ";
-					out += std::to_string(bound);
-					out += ")";
-					return out;
-				}
-
-			private:
-
-				/*!
-				 * Evaluate the action.
-				 *
-				 * As the BoundAction does not depend on the model or the formula for which the modelchecking result was computed,
-				 * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
-				 * modelchecking result as input.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result) const {
-
-					//Initialize the new selection vector.
-					storm::storage::BitVector out(result.selection.size());
-
-					if(result.pathResult.size() != 0) {
-
-						if(result.stateResult.size() != 0) {
-							LOG4CPLUS_WARN(logger, "Both pathResult and stateResult are set. The filter action is applied using only the pathResult.");
-							std::cout << "Both pathResult and stateResult are set. The filter action is applied using only the pathResult." << std::endl;
-						}
-
-						//Fill the selection by comparing the values for all previously selected states with the given bound using the comparison operator.
-						for(uint_fast64_t i = 0; i < result.pathResult.size(); i++) {
-							if(result.selection[i]) {
-								switch(comparisonOperator) {
-									case storm::properties::GREATER_EQUAL:
-										out.set(i, result.pathResult[i] >= bound);
-										break;
-									case storm::properties::GREATER:
-										out.set(i, result.pathResult[i] > bound);
-										break;
-									case storm::properties::LESS_EQUAL:
-										out.set(i, result.pathResult[i] <= bound);
-										break;
-									case storm::properties::LESS:
-										out.set(i, result.pathResult[i] < bound);
-										break;
-									default:
-										LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-										throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
-										break;
-								}
-							}
-						}
-					} else {
-						// Fill the selection by comparing the values of all previously selected states with the given bound using the comparison operator.
-						for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-							if(result.selection[i]) {
-								switch(comparisonOperator) {
-									case storm::properties::GREATER_EQUAL:
-										out.set(i, result.stateResult[i] >= bound);
-										break;
-									case storm::properties::GREATER:
-										out.set(i, result.stateResult[i] > bound);
-										break;
-									case storm::properties::LESS_EQUAL:
-										out.set(i, result.stateResult[i] <= bound);
-										break;
-									case storm::properties::LESS:
-										out.set(i, result.stateResult[i] < bound);
-										break;
-									default:
-										LOG4CPLUS_ERROR(logger, "Unknown comparison operator of value " << comparisonOperator << ".");
-										throw storm::exceptions::InvalidArgumentException() << "Unknown comparison operator of value " << comparisonOperator << ".";
-										break;
-								}
-							}
-						}
-					}
-
-					return Result(out, result.stateMap, result.pathResult, result.stateResult);
-				}
-
-				// The operator used to make the comparison between the bound and the modelchecking values for each state at time of evaluation.
-				storm::properties::ComparisonType comparisonOperator;
-
-				// The bound to compare the modelchecking values against during evaluation.
-				T bound;
-
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-
-#endif /* STORM_PROPERTIES_ACTION_BOUNDACTION_H_ */

src/properties/actions/FormulaAction.h

@@ -1,132 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_FORMULAACTION_H_
-#define STORM_PROPERTIES_ACTION_FORMULAACTION_H_
-
-#include "src/properties/actions/AbstractAction.h"
-#include "src/properties/prctl/AbstractStateFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-
-#include <string>
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * The Formula action deselects all states that do not satisfy the given state formula.
-			 *
-			 * @note Since there is no modelchecker implemented for Ltl formulas (except the abstract base class)
-			 *       the formula action currently only supports Prctl and Csl state formulas.
-			 */
-			template <class T>
-			class FormulaAction : public AbstractAction<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename AbstractAction<T>::Result Result;
-
-			public:
-
-
-				/*!
-				 * Constructs an empty FormulaAction.
-				 *
-				 * The evaluation will do nothing and return the Result as it was put in.
-				 */
-				FormulaAction() : prctlFormula(nullptr), cslFormula(nullptr) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * Constructs a FormulaAction using the given Prctl formula.
-				 *
-				 * @param prctlFormula The Prctl state formula used to filter the selection during evaluation.
-				 */
-				FormulaAction(std::shared_ptr<storm::properties::prctl::AbstractStateFormula<T>> const & prctlFormula) : prctlFormula(prctlFormula), cslFormula(nullptr) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * Constructs a FormulaAction using the given Csl formula.
-				 *
-				 * @param cslFormula The Csl state formula used to filter the selection during evaluation.
-				 */
-				FormulaAction(std::shared_ptr<storm::properties::csl::AbstractStateFormula<T>> const & cslFormula) : prctlFormula(nullptr), cslFormula(cslFormula) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~FormulaAction() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Evaluate the action for an Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
-
-					storm::storage::BitVector selection(result.selection);
-
-					//Compute the modelchecking results of the actions state formula and deselect all states that do not satisfy it.
-					if(prctlFormula.get() != nullptr) {
-						selection = selection & prctlFormula->check(mc);
-					}
-
-					return Result(selection, result.stateMap, result.pathResult, result.stateResult);
-				}
-
-				/*!
-				 * Evaluate the action for an Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
-
-					storm::storage::BitVector selection(result.selection);
-
-					//Compute the modelchecking results of the actions state formula and deselect all states that do not satisfy it.
-					if(cslFormula.get() != nullptr) {
-						selection = selection & cslFormula->check(mc);
-					}
-
-					return Result(selection, result.stateMap, result.pathResult, result.stateResult);
-				}
-
-				/*!
-				 * Returns a string representation of this action.
-				 *
-				 * @returns A string representing this action.
-				 */
-				virtual std::string toString() const override {
-					std::string out = "formula(";
-					if(prctlFormula.get() != nullptr) {
-						out += prctlFormula->toString();
-					} else if(cslFormula.get() != nullptr) {
-						out += cslFormula->toString();
-					}
-					out += ")";
-					return out;
-				}
-
-			private:
-
-				// The Prctl state formula used during evaluation.
-				std::shared_ptr<storm::properties::prctl::AbstractStateFormula<T>> prctlFormula;
-
-				// The Csl state formula used during evaluation.
-				std::shared_ptr<storm::properties::csl::AbstractStateFormula<T>> cslFormula;
-
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ACTION_FORMULAACTION_H_ */

src/properties/actions/InvertAction.h

@@ -1,102 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_INVERTACTION_H_
-#define STORM_PROPERTIES_ACTION_INVERTACTION_H_
-
-#include "src/properties/actions/AbstractAction.h"
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * The InvertAction inverts the selection, selecting precisely the unselected states.
-			 */
-			template <class T>
-			class InvertAction : public AbstractAction<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename AbstractAction<T>::Result Result;
-
-			public:
-
-				/*!
-				 * Constructs an InvertAction.
-				 *
-				 * As the simple inversion of the selection does not need any parameters, the empty constructor is the only one needed.
-				 */
-				InvertAction() {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~InvertAction() {
-					//Intentionally left empty
-				}
-
-				/*!
-				 * Evaluate the action for a Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Ltl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Returns a string representation of this action.
-				 *
-				 * @returns A string representing this action.
-				 */
-				virtual std::string toString() const override {
-					return "invert";
-				}
-
-			private:
-
-				/*!
-				 * Evaluate the action.
-				 *
-				 * As the InvertAction does not depend on the model or the formula for which the modelchecking result was computed,
-				 * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
-				 * modelchecking result as input.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result) const {
-					storm::storage::BitVector out(result.selection);
-					return Result(~out, result.stateMap, result.pathResult, result.stateResult);
-				}
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ACTION_INVERTACTION_H_ */

src/properties/actions/RangeAction.h

@@ -1,148 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_RANGEACTION_H_
-#define STORM_PROPERTIES_ACTION_RANGEACTION_H_
-
-#include "src/properties/actions/AbstractAction.h"
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * The RangeAction deselects all states that are not within the given range.
-			 *
-			 * The bounds of the range given are indices in the result ordering.
-			 * Thus, if the lower bound is 0 and the upper bound is 5 then all states that are not
-			 * at index 0 through 5 (including) in the state ordering will be deselected.
-			 * This action is thought to be used in connection with the SortAction.
-			 */
-			template <class T>
-			class RangeAction : public AbstractAction<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename AbstractAction<T>::Result Result;
-
-			public:
-
-				/*!
-				 *  Construct a RangeAction using the given values.
-				 *
-				 *  If no values are given they default to [0,UINT_FAST64_MAX] thus deselecting no state at evaluation.
-				 *
-				 *	@note The interval bounds are included in the interval.
-				 */
-				RangeAction(uint_fast64_t from = 0, uint_fast64_t to = UINT_FAST64_MAX) : from(from), to(to) {
-					if(from > to) {
-						throw storm::exceptions::IllegalArgumentValueException() << "The end of the range is lower than its beginning";
-					}
-				}
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~RangeAction() {
-					//Intentionally left empty
-				}
-
-				/*!
-				 * Evaluate the action for a Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Ltl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Returns a string representation of this action.
-				 *
-				 * @returns A string representing this action.
-				 */
-				virtual std::string toString() const override {
-					std::string out = "range(";
-					out += std::to_string(from);
-					out += ", ";
-					out += std::to_string(to);
-					out += ")";
-					return out;
-				}
-
-			private:
-
-				/*!
-				 * Evaluate the action.
-				 *
-				 * As the RangeAction does not depend on the model or the formula for which the modelchecking result was computed,
-				 * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
-				 * modelchecking result as input.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result) const {
-					//Initialize the output vector.
-					storm::storage::BitVector out(result.selection.size());
-
-					uint_fast64_t end = to - from;
-
-					// Safety check for access bounds.
-					if(from >= result.stateMap.size()) {
-						LOG4CPLUS_WARN(logger, "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected.");
-						std::cout << "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected." << std::endl;
-
-						return Result(out, result.stateMap, result.pathResult, result.stateResult);
-					}
-
-					if(to >= result.stateMap.size()) {
-
-						end = result.selection.size() - from - 1;
-
-						LOG4CPLUS_WARN(logger, "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state.");
-						std::cout << "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state." << std::endl;
-					}
-
-					//Fill the output vector.
-					for(uint_fast64_t i=0; i <= end; i++) {
-						out.set(result.stateMap[from + i], result.selection[result.stateMap[from + i]]);
-					}
-
-					return Result(out, result.stateMap, result.pathResult, result.stateResult);
-				}
-
-				// The lower bound of the interval of states not deselected.
-				uint_fast64_t from;
-
-				// The upper bound of the interval of states not deselected.
-				uint_fast64_t to;
-
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ACTION_RANGEACTION_H_ */

src/properties/actions/SortAction.h

@@ -1,224 +0,0 @@
-#ifndef STORM_PROPERTIES_ACTION_SORTACTION_H_
-#define STORM_PROPERTIES_ACTION_SORTACTION_H_
-
-#include "src/properties/actions/AbstractAction.h"
-#include <cctype>
-
-namespace storm {
-	namespace properties {
-		namespace action {
-
-			/*!
-			 * This action manipulates the state ordering by sorting the states by some category.
-			 *
-			 * Currently the states can be sorted either by index or by value; ascending or descending.
-			 * This is done using the standard libraries sort function, thus the action evaluates in O(n*log n) where n is the number of states.
-			 */
-			template <class T>
-			class SortAction : public AbstractAction<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename AbstractAction<T>::Result Result;
-
-			public:
-
-				//! Enum defining the categories in relation to which the states can be sorted.
-				enum SortingCategory {INDEX, VALUE};
-
-				/*!
-				 * Construct a SortAction using the given values.
-				 *
-				 * If no values are given the action will sort by ascending state index.
-				 *
-				 * @param category An enum value identifying the category by which the states are to be ordered.
-				 * @param ascending Determines whether the values are to be sorted in ascending or descending order.
-				 *                  The parameter is to be set to true iff the values are to be sorted in ascending order.
-				 */
-				SortAction(SortingCategory category = INDEX, bool ascending = true) : category(category), ascending(ascending) {
-					//Intentionally left empty.
-				}
-
-				/*!
-				 * The virtual destructor.
-				 * To ensure that the right destructor is called.
-				 */
-				virtual ~SortAction() {
-					//Intentionally left empty
-				}
-
-				/*!
-				 * Evaluate the action for a Prctl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Prctl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Csl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Csl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Evaluate the action for a Ltl formula.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @param mc The Ltl modelchecker that computed the path- or stateResult contained in the Result struct.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				virtual Result evaluate(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & mc) const override {
-					return evaluate(result);
-				}
-
-				/*!
-				 * Returns a string representation of this action.
-				 *
-				 * @returns A string representing this action.
-				 */
-				virtual std::string toString() const override {
-					std::string out = "sort(";
-					switch (category) {
-						case INDEX:
-							out += "index";
-							break;
-						case VALUE:
-							out += "value";
-							break;
-						default:
-							LOG4CPLUS_INFO(logger, "Unknown sorting category of value " << category << ".");
-							std::cout << "Unknown sorting category of value " << category << "." << std::endl;
-							break;
-					}
-					out += ", ";
-					out += ascending ? "ascending)" : "descending)";
-					return out;
-				}
-
-
-			private:
-
-				/*!
-				 * Evaluate the action.
-				 *
-				 * As the SortAction does not depend on the model or the formula for which the modelchecking result was computed,
-				 * it does not depend on the modelchecker at all. This internal version of the evaluate method therefore only needs the
-				 * modelchecking result as input.
-				 *
-				 * @param result The Result struct on which the action is to be evaluated.
-				 * @returns A Result struct containing the output of the action.
-				 */
-				Result evaluate(Result const & result) const {
-
-					if(category == VALUE) {
-						//TODO
-
-						if(result.pathResult.size() != 0) {
-							return Result(result.selection, sort(result.stateMap, result.pathResult), result.pathResult, result.stateResult);
-						} else {
-							return Result(result.selection, sort(result.stateMap, result.stateResult), result.pathResult, result.stateResult);
-						}
-
-					} else {
-						return Result(result.selection, sort(result.stateMap.size()), result.pathResult, result.stateResult);
-					}
-				}
-
-				/*!
-				 * This method returns a vector of the given length filled with the numbers 0 to length-1 in ascending or descending order,
-				 * depending on the value of the member variable ascending. Thus it sorts by state index.
-				 *
-				 * @param length The length of the generated vector.
-				 * @returns A vector of unsigned integers from 0 to length-1 in ascending or descending order.
-				 */
-				std::vector<uint_fast64_t> sort(uint_fast64_t length) const {
-
-					// Project the vector down to its first component.
-					std::vector<uint_fast64_t> outMap(length);
-
-					// Sort the combined vector.
-					if(ascending) {
-						for(uint_fast64_t i = 0; i < length; i++) {
-							outMap[i] = i;
-						}
-					} else {
-						for(uint_fast64_t i = 0; i < length; i++) {
-							outMap[i] = length - i - 1;
-						}
-					}
-
-					return outMap;
-				}
-
-				/*!
-				 * Sort the stateMap vector representing the current state ordering by the values in the values vector.
-				 *
-				 * Here the entries in the values vector are assumed to be the modelchecking results of a path formula.
-				 * Hence, the value at index i is associated with state i, i.e the value i in the stateMap.
-				 * The ordering direction (ascending/decending) is given by the member variable ascending, set in the constructor.
-				 *
-				 * @param stateMap A vector representing the current state ordering.
-				 * @param values A vector containing the values by which the stateMap is to be ordered.
-				 * @returns A vector containing the reordered entries of the stateMap.
-				 */
-				std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, std::vector<T> const & values) const {
-
-					// Prepare the new state map.
-					std::vector<uint_fast64_t> outMap(stateMap);
-
-					// Sort the state map.
-					if(ascending) {
-						std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] < values[b]; });
-					} else {
-						std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] > values[b]; });
-					}
-
-					return outMap;
-				}
-
-				/*!
-				 * Sort the stateMap vector representing the current state ordering by the values in the values vector.
-				 *
-				 * Here the entries in the values vector are assumed to be the modelchecking results of a state formula.
-				 * Hence, the value at index i is associated with state i, i.e the value i in the stateMap.
-				 * The ordering direction (ascending/decending) is given by the member variable ascending, set in the constructor.
-				 *
-				 * @param stateMap A vector representing the current state ordering.
-				 * @param values A vector containing the values by which the stateMap is to be ordered.
-				 * @returns A vector containing the reordered entries of the stateMap.
-				 */
-				std::vector<uint_fast64_t> sort(std::vector<uint_fast64_t> const & stateMap, storm::storage::BitVector const & values) const {
-
-					// Prepare the new state map.
-					std::vector<uint_fast64_t> outMap(stateMap);
-
-					// Sort the state map.
-					if(ascending) {
-						std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] < values[b]; });
-					} else {
-						std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] > values[b]; });
-					}
-
-					return outMap;
-				}
-
-				// The category by which the states are to be ordered.
-				SortingCategory category;
-
-				// Determines whether the values are to be sorted in ascending or descending order.
-				bool ascending;
-			};
-
-		} // namespace action
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_ACTION_SORTACTION_H_ */

src/properties/csl/AbstractCslFormula.h

@@ -1,73 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_ABSTRACTCSLFORMULA_H_
-#define STORM_PROPERTIES_CSL_ABSTRACTCSLFORMULA_H_
-
-#include "src/properties/AbstractFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declarations.
-			template <class T> class ProbabilisticBoundOperator;
-			template <class T> class Eventually;
-			template <class T> class Until;
-
-			/*!
-			 * This is the abstract base class for all Csl formulas.
-			 *
-			 * @note While formula classes do have copy constructors using a copy constructor
-			 *       will yield a formula objects whose formula subtree consists of the same objects
-			 *       as the original formula. The ownership of the formula tree will be shared between
-			 *       the original and the copy.
-			 */
-			template <class T>
-			class AbstractCslFormula : public virtual storm::properties::AbstractFormula<T>{
-			public:
-
-				/*!
-				 * The virtual destructor.
-				 */
-				virtual ~AbstractCslFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Checks whether the formula is a probabilistic bound reachability formula.
-				 * Returns true iff the formula conforms to the following pattern.
-				 * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
-				 * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
-				 * (denoting some set of atomic propositions).
-				 *
-				 * @return True iff this is a probabilistic bound reachability formula.
-				 */
-				bool isProbEventuallyAP() const {
-
-					// Test if a probabilistic bound operator is at the root.
-					if(dynamic_cast<storm::properties::csl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
-						return false;
-					}
-
-					auto probFormula = dynamic_cast<storm::properties::csl::ProbabilisticBoundOperator<T> const *>(this);
-
-					// Check if the direct subformula of the probabilistic bound operator is an eventually or until formula.
-					if(std::dynamic_pointer_cast<storm::properties::csl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
-
-						// Get the subformula and check if its subformulas are propositional.
-						auto eventuallyFormula = std::dynamic_pointer_cast<storm::properties::csl::Eventually<T>>(probFormula->getChild());
-						return eventuallyFormula->getChild()->isPropositional();
-					} else if(std::dynamic_pointer_cast<storm::properties::csl::Until<T>>(probFormula->getChild()).get() != nullptr) {
-
-						// Get the subformula and check if its subformulas are propositional.
-						auto untilFormula = std::dynamic_pointer_cast<storm::properties::csl::Until<T>>(probFormula->getChild());
-						return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
-					}
-
-					return false;
-				}
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_ABSTRACTCSLFORMULA_H_ */

src/properties/csl/AbstractPathFormula.h

@@ -1,62 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_ABSTRACTPATHFORMULA_H_
-#define STORM_PROPERTIES_CSL_ABSTRACTPATHFORMULA_H_
-
-#include "src/properties/csl/AbstractCslFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-#include <vector>
-#include <iostream>
-#include <typeinfo>
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			/*!
-			 * Abstract base class for Csl path formulas.
-			 *
-			 * @note Differing from the formal definitions of PRCTL a path formula may be the root of a PRCTL formula.
-			 *       The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model.
-			 */
-			template <class T>
-			class AbstractPathFormula : public virtual storm::properties::csl::AbstractCslFormula<T> {
-
-			public:
-
-				/*!
-				 * The virtual destructor.
-				 */
-				virtual ~AbstractPathFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
-				 *
-				 * @note This function is not implemented in this class.
-				 *
-				 * @returns A deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const = 0;
-
-				/*!
-				 * 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 the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const = 0;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_ABSTRACTPATHFORMULA_H_ */

src/properties/csl/AbstractStateFormula.h

@@ -1,56 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_ABSTRACTSTATEFORMULA_H_
-#define STORM_PROPERTIES_CSL_ABSTRACTSTATEFORMULA_H_
-
-#include "src/properties/csl/AbstractCslFormula.h"
-#include "src/storage/BitVector.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			/*!
-			 * Abstract base class for Csl state formulas.
-			 */
-			template <class T>
-			class AbstractStateFormula : public storm::properties::csl::AbstractCslFormula<T> {
-
-			public:
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~AbstractStateFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-				 *
-				 * @note This function is not implemented in this class.
-				 *
-				 * @returns A deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const = 0;
-
-				/*!
-				 * 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 bit vector indicating all states that satisfy the formula represented by the called object.
-				 */
-				virtual storm::storage::BitVector check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const = 0;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_AbstractSTATEFORMULA_H_ */

src/properties/csl/And.h

@@ -1,207 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_AND_H_
-#define STORM_PROPERTIES_CSL_AND_H_
-
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-#include <string>
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class And;
-
-			/*!
-			 * Interface class for model checkers that support And.
-			 *
-			 * All model checkers that support the formula class And must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IAndModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IAndModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates an And formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual storm::storage::BitVector checkAnd(And<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl formula tree with an And node as root.
-			 *
-			 * Has two Csl state formulas as sub formulas/trees.
-			 *
-			 * As And is commutative, the order is \e theoretically not important, but will influence the order in which
-			 * the model checker works.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractStateFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class And : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an And node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				And() : left(nullptr), right(nullptr){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an And node with the parameters as subtrees.
-				 *
-				 * @param left The left sub formula.
-				 * @param right The right sub formula.
-				 */
-				And(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~And() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * 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 a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<And<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(right->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(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "(";
-					result += left->toString();
-					result += " & ";
-					result += right->toString();
-					result += ")";
-					return result;
-				}
-
-				/*! Returns whether the formula is a propositional logic formula.
-				 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 *  @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return left->isPropositional() && right->isPropositional();
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractStateFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractStateFormula<T>> right;
-
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_AND_H_ */

src/properties/csl/Ap.h

@@ -1,132 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_AP_H_
-#define STORM_PROPERTIES_CSL_AP_H_
-
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Ap;
-
-			/*!
-			 * Interface class for model checkers that support Ap.
-			 *
-			 * All model checkers that support the formula class Ap must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IApModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IApModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates an Ap formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual storm::storage::BitVector checkAp(Ap<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl formula tree with an atomic proposition as root.
-			 *
-			 * This class represents the leaves in the formula tree.
-			 *
-			 * @see AbstractCslFormula
-			 * @see AbstractStateFormula
-			 */
-			template <class T>
-			class Ap : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a new atomic proposition leaf, with the given label.
-				 *
-				 * @param ap A string representing the atomic proposition.
-				 */
-				Ap(std::string ap) : ap(ap) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Ap() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * 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 Ap object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<Ap<T>>(this->getAp());
-					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(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IApModelChecker>()->checkAp(*this);
-				}
-
-				/*!
-				 * A string representing the atomic proposition.
-				 *
-				 * @returns A string representing the leaf.
-				 */
-				virtual std::string toString() const override {
-					return getAp();
-				}
-
-				/*! Returns whether the formula is a propositional logic formula.
-				 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 *  @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return true;
-				}
-
-				/*!
-				 * Gets the name of the atomic proposition.
-				 *
-				 * @returns The name of the atomic proposition.
-				 */
-				std::string const & getAp() const {
-					return ap;
-				}
-
-			private:
-
-				// The atomic proposition referenced by this leaf.
-				std::string ap;
-
-			};
-
-		} // namespace abstract
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_AP_H_ */

src/properties/csl/CslFilter.h

@@ -1,407 +0,0 @@
-#ifndef STORM_PROPERTIES_PRCTL_CSLFILTER_H_
-#define STORM_PROPERTIES_PRCTL_CSLFILTER_H_
-
-#include "src/properties/AbstractFilter.h"
-#include "src/properties/csl/AbstractCslFormula.h"
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/AbstractModelChecker.h"
-
-#include "src/properties/actions/AbstractAction.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			/*!
-			 * This is the Csl specific filter.
-			 *
-			 * It maintains a Csl formula which can be checked against a given model by either calling evaluate() or check().
-			 * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output.
-			 */
-			template <class T>
-			class CslFilter : public storm::properties::AbstractFilter<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename storm::properties::action::AbstractAction<T>::Result Result;
-
-			public:
-
-				/*!
-				 * Creates an empty CslFilter, maintaining no Csl formula.
-				 *
-				 * Calling check or evaluate will return an empty result.
-				 */
-				CslFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr), steadyStateQuery(false) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a CslFilter maintaining a Csl formula but containing no actions.
-				 *
-				 * The modelchecking result will be returned or printed as is.
-				 *
-				 * @param child The Csl formula to be maintained.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 * @param steadyStateQuery A flag indicating whether this is a steady state query.
-				 */
-				CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(opt), child(child), steadyStateQuery(steadyStateQuery) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a CslFilter maintaining a Csl formula and containing a single action.
-				 *
-				 * The given action will be applied to the modelchecking result during evaluation.
-				 * Further actions can be added later.
-				 *
-				 * @param child The Csl formula to be maintained.
-				 * @param action The single action to be executed during evaluation.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 * @param steadyStateQuery A flag indicating whether this is a steady state query.
-				 */
-				CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(action, opt), child(child), steadyStateQuery(steadyStateQuery) {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Creates a CslFilter using the given parameters.
-				 *
-				 * The given actions will be applied to the modelchecking result in ascending index order during evaluation.
-				 * Further actions can be added later.
-				 *
-				 * @param child The Csl formula to be maintained.
-				 * @param actions A vector conatining the actions that are to be executed during evaluation.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 * @param steadyStateQuery A flag indicating whether this is a steady state query.
-				 */
-				CslFilter(std::shared_ptr<AbstractCslFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED, bool steadyStateQuery = false) : AbstractFilter<T>(actions, opt), child(child), steadyStateQuery(steadyStateQuery) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~CslFilter() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and prints out the result.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 */
-				void check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
-
-					// Write out the formula to be checked.
-					std::cout << std::endl;
-					LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
-					std::cout << "Model checking formula:\t" << this->toString() << std::endl;
-
-					writeOut(evaluate(modelchecker), modelchecker);
-
-				}
-
-				/*!
-				 * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and returns the result.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 * @returns The result of the sequential application of the filter actions to the modelchecking result.
-				 */
-				Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
-					Result result;
-
-					try {
-						if(std::dynamic_pointer_cast<AbstractStateFormula<T>>(child).get() != nullptr) {
-							result = evaluate(modelchecker, std::dynamic_pointer_cast<AbstractStateFormula<T>>(child));
-						} else if (std::dynamic_pointer_cast<AbstractPathFormula<T>>(child).get() != nullptr) {
-							result = evaluate(modelchecker, std::dynamic_pointer_cast<AbstractPathFormula<T>>(child));
-						}
-					} catch (std::exception& e) {
-						std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
-						LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
-					}
-
-					return result;
-				}
-
-				/*!
-				 * Returns a textual representation of the filter.
-				 *
-				 * That includes the actions as well as the maintained formula.
-				 *
-				 * @returns A string representing the filter.
-				 */
-				virtual std::string toString() const override {
-					std::string desc = "";
-
-					if(!std::dynamic_pointer_cast<AbstractStateFormula<T>>(child)) {
-
-						// The formula is not a state formula so we have a probability query.
-						if(this->actions.empty()){
-
-							// Since there are no actions given we do legacy support.
-
-							desc += "P ";
-							switch(this->opt) {
-								case MINIMIZE:
-									desc += "min ";
-									break;
-								case MAXIMIZE:
-									desc += "max ";
-									break;
-								default:
-									break;
-							}
-							desc += "= ? ";
-
-						} else {
-							desc = "filter[";
-
-							switch(this->opt) {
-								case MINIMIZE:
-									desc += "min; ";
-									break;
-								case MAXIMIZE:
-									desc += "max; ";
-									break;
-								default:
-									break;
-							}
-
-							for(auto action : this->actions) {
-								desc += action->toString();
-								desc += "; ";
-							}
-
-							// Remove the last "; ".
-							desc.pop_back();
-							desc.pop_back();
-
-							desc += "]";
-						}
-
-					} else {
-
-						if(this->actions.empty()) {
-
-							if(steadyStateQuery) {
-
-								// Legacy support for the steady state query.
-								desc += "S = ? ";
-
-							} else {
-
-								// There are no filter actions but only the raw state formula. So just print that.
-								return child->toString();
-							}
-						} else {
-
-							desc = "filter[";
-
-							for(auto action : this->actions) {
-								desc += action->toString();
-								desc += "; ";
-							}
-
-							// Remove the last "; ".
-							desc.pop_back();
-							desc.pop_back();
-
-							desc += "]";
-						}
-					}
-
-					desc += "(";
-					desc += child->toString();
-					desc += ")";
-
-					return desc;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractCslFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractCslFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				/*!
-				 * Calls the modelchecker for a state formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
-				 *
-				 * This an internal version of the evaluate method overloading it for the different Csl formula types.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 * @param formula The state formula for which the modelchecker will be called.
-				 * @returns The result of the sequential application of the filter actions to the modelchecking result.
-				 */
-				Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractStateFormula<T>> const & formula) const {
-					// First, get the model checking result.
-					Result result;
-
-					//TODO: Once a modelchecker supporting steady state formulas is implemented, call it here in case steadyStateQuery is set.
-
-					if(this->opt != UNDEFINED) {
-						// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-						result.stateResult = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false);
-					} else {
-						result.stateResult = formula->check(modelchecker);
-					}
-
-
-					// Now apply all filter actions and return the result.
-					return evaluateActions(result, modelchecker);
-				}
-
-				/*!
-				 * Calls the modelchecker for a path formula, retrieves the modelchecking result, applies the filter action one by one and returns the result.
-				 *
-				 * This an internal version of the evaluate method overloading it for the different Csl formula types.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 * @param formula The path formula for which the modelchecker will be called.
-				 * @returns The result of the sequential application of the filter actions to the modelchecking result.
-				 */
-				Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractPathFormula<T>> const & formula) const {
-					// First, get the model checking result.
-					Result result;
-
-					if(this->opt != UNDEFINED) {
-						// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
-						result.pathResult = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false);
-					} else {
-						result.pathResult = formula->check(modelchecker, false);
-					}
-
-					// Now apply all filter actions and return the result.
-					return evaluateActions(result, modelchecker);
-				}
-
-				/*!
-				 * Evaluates the filter actions by calling them one by one using the output of each action as the input for the next one.
-				 *
-				 * @param input The modelchecking result in form of a Result struct.
-				 * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed by some actions.
-				 * @returns The result of the sequential application of the filter actions to the modelchecking result.
-				 */
-				Result evaluateActions(Result result, storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
-
-					// Init the state selection and state map vectors.
-					uint_fast64_t size = result.stateResult.size() == 0 ? result.pathResult.size() : result.stateResult.size();
-					result.selection = storm::storage::BitVector(size, true);
-					result.stateMap = std::vector<uint_fast64_t>(size);
-					for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
-						result.stateMap[i] = i;
-					}
-
-					// Now apply all filter actions and return the result.
-					for(auto action : this->actions) {
-						result = action->evaluate(result, modelchecker);
-					}
-					return result;
-				}
-
-				/*!
-				 * Writes out the given result.
-				 *
-				 * @param result The result of the sequential application of the filter actions to a modelchecking result.
-				 * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed for legacy support.
-				 */
-				void writeOut(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {
-
-					// Test if there is anything to write out.
-					// The selection size should only be 0 if an error occurred during the evaluation (since a model with 0 states is invalid).
-					if(result.selection.size() == 0) {
-						std::cout << std::endl << "-------------------------------------------" << std::endl;
-						return;
-					}
-
-					// Test for the kind of result. Values or states.
-					if(!result.pathResult.empty()) {
-
-						// Write out the selected value results in the order given by the stateMap.
-						if(this->actions.empty()) {
-
-							// There is no filter action given. So provide legacy support:
-							// Return the results for all states labeled with "init".
-							LOG4CPLUS_INFO(logger, "Result for initial states:");
-							std::cout << "Result for initial states:" << std::endl;
-							for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
-								LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result.pathResult[initialState]);
-								std::cout << "\t" << initialState << ": " << result.pathResult[initialState] << std::endl;
-							}
-						} else {
-							LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
-							std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
-
-							for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-								if(result.selection.get(result.stateMap[i])) {
-									LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]]);
-									std::cout << "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]] << std::endl;
-								}
-							}
-						}
-
-					} else {
-
-						// Write out the selected state results in the order given by the stateMap.
-						if(this->actions.empty()) {
-
-							// There is no filter action given. So provide legacy support:
-							// Return the results for all states labeled with "init".
-							LOG4CPLUS_INFO(logger, "Result for initial states:");
-							std::cout << "Result for initial states:" << std::endl;
-							for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
-								LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.stateResult[initialState] ? "satisfied" : "not satisfied"));
-								std::cout << "\t" << initialState << ": " << result.stateResult[initialState] << std::endl;
-							}
-						} else {
-							LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
-							std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
-
-							for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-								if(result.selection.get(result.stateMap[i])) {
-									LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << (result.stateResult[result.stateMap[i]] ? "satisfied" : "not satisfied"));
-									std::cout << "\t" << result.stateMap[i] << ": " << (result.stateResult[result.stateMap[i]] ? "satisfied" : "not satisfied") << std::endl;
-								}
-							}
-						}
-					}
-
-					std::cout << std::endl << "-------------------------------------------" << std::endl;
-				}
-
-				// The Csl formula maintained by this filter.
-				std::shared_ptr<AbstractCslFormula<T>> child;
-
-				// A flag indicating whether this is a steady state query.
-				bool steadyStateQuery;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_CSLFILTER_H_ */

src/properties/csl/Eventually.h

@@ -1,163 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_EVENTUALLY_H_
-#define STORM_PROPERTIES_CSL_EVENTUALLY_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Eventually;
-
-			/*!
-			 * Interface class for model checkers that support Eventually.
-			 *
-			 * All model checkers that support the formula class Eventually must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IEventuallyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IEventuallyModelChecker() {
-						// Intentionally left empty.
-					}
-
-					/*!
-					 * Evaluates an Eventually formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkEventually(Eventually<T> const & obj, bool qualitative) const = 0;
-			};
-
-			/*!
-			 * @brief
-			 * Class for a Csl (path) formula tree with an Eventually node as root.
-			 *
-			 * Has one Csl state formula as sub formula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff eventually formula \e child holds.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Eventually : public AbstractPathFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Eventually node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Eventually() : child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Eventually node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Eventually(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Eventually() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Eventually object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<Eventually<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "F ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_EVENTUALLY_H_ */

src/properties/csl/Globally.h

@@ -1,162 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_GLOBALLY_H_
-#define STORM_PROPERTIES_CSL_GLOBALLY_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Globally;
-
-			/*!
-			 * Interface class for model checkers that support Globally.
-			 *
-			 * All model checkers that support the formula class Globally must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IGloballyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IGloballyModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a Globally formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkGlobally(Globally<T> const & obj, bool qualitative) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl (path) formula tree with a Globally node as root.
-			 *
-			 * Has one Csl state formula as sub formula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff globally \e child holds.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Globally : public AbstractPathFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Globally node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Globally() : child(nullptr){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Globally node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Globally(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Globally() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Globally object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<Globally<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "G ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				AbstractStateFormula<T> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_GLOBALLY_H_ */

src/properties/csl/Next.h

@@ -1,161 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_NEXT_H_
-#define STORM_PROPERTIES_CSL_NEXT_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Next;
-
-			/*!
-			 * Interface class for model checkers that support Next.
-			 *
-			 * All model checkers that support the formula class Next must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class INextModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~INextModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Next formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return Result of the formula for every node.
-					 */
-					virtual std::vector<T> checkNext(Next<T> const & obj, bool qualitative) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl (path) formula tree with a Next node as root.
-			 *
-			 * Has two Csl state formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff in the next step, \e child holds
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Next : public AbstractPathFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Next node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Next() : child(nullptr){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Next node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Next(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Next() {
-					// Intetionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Next object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<Next<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "X ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_NEXT_H_ */

src/properties/csl/Not.h

@@ -1,165 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_NOT_H_
-#define STORM_PROPERTIES_CSL_NOT_H_
-
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/modelchecker/csl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Not;
-
-			/*!
-			 * Interface class for model checkers that support Not.
-			 *
-			 * All model checkers that support the formula class Not must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class INotModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~INotModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Not formulas within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return Result of the formula for every node.
-					 */
-					virtual storm::storage::BitVector checkNot(Not<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl formula tree with Not node as root.
-			 *
-			 * Has one Csl state formula as sub formula/tree.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractStateFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Not : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Not node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Not() : child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Not node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Not(std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Not() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Not object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<Not<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<INotModelChecker>()->checkNot(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "!";
-					result += child->toString();
-					return result;
-				}
-
-				/*! Returns whether the formula is a propositional logic formula.
-				 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 *  @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return child->isPropositional();
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_NOT_H_ */

src/properties/csl/Or.h

@@ -1,205 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_OR_H_
-#define STORM_PROPERTIES_CSL_OR_H_
-
-#include "src/properties/csl/AbstractStateFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Or;
-
-			/*!
-			 * Interface class for model checkers that support Or.
-			 *
-			 * All model checkers that support the formula class Or must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IOrModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IOrModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Or formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return Result of the formula for every node.
-					 */
-					virtual storm::storage::BitVector checkOr(Or<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Csl formula tree with an Or node as root.
-			 *
-			 * Has two state formulas as sub formulas/trees.
-			 *
-			 * As Or is commutative, the order is \e theoretically not important, but will influence the order in which
-			 * the model checker works.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractStateFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Or : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Or node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Or() : left(nullptr), right(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Or node with the parameters as subtrees.
-				 *
-				 * @param left The left sub formula.
-				 * @param right The right sub formula.
-				 */
-				Or(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Or() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * 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 Or object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<Or<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(right->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(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "(";
-					result += left->toString();
-					result += " | ";
-					result += right->toString();
-					result += ")";
-					return result;
-				}
-
-				/*! Returns whether the formula is a propositional logic formula.
-				 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 *  @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return left->isPropositional() && right->isPropositional();
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left right is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractStateFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractStateFormula<T>> right;
-
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_OR_H_ */

src/properties/csl/ProbabilisticBoundOperator.h

@@ -1,234 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_PROBABILISTICBOUNDOPERATOR_H_
-#define STORM_PROPERTIES_CSL_PROBABILISTICBOUNDOPERATOR_H_
-
-#include "src/properties/csl/AbstractStateFormula.h"
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/ComparisonType.h"
-#include "utility/constants.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class ProbabilisticBoundOperator;
-
-			/*!
-			 * Interface class for model checkers that support ProbabilisticBoundOperator.
-			 *
-			 * All model checkers that support the formula class PathBoundOperator must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IProbabilisticBoundOperatorModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IProbabilisticBoundOperatorModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a ProbabilisticBoundOperator within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual storm::storage::BitVector checkProbabilisticBoundOperator(ProbabilisticBoundOperator<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl formula tree with a P (probablistic) bound operator node as root.
-			 *
-			 * Has one path formula as sub formula/tree.
-			 *
-			 * @par Semantics
-			 * 	  The formula holds iff the probability that the path formula holds meets the bound
-			 * 	  specified in this operator
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractStateFormula
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template<class T>
-			class ProbabilisticBoundOperator : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a ProbabilisticBoundOperator node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a ProbabilisticBoundOperator node using the given parameters.
-				 *
-				 * @param comparisonOperator The relation for the bound.
-				 * @param bound The bound for the probability.
-				 * @param child The child formula subtree.
-				 */
-				ProbabilisticBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
-					: comparisonOperator(comparisonOperator), bound(bound), child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~ProbabilisticBoundOperator() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new ProbabilisticBoundOperator object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<ProbabilisticBoundOperator<T>>();
-					result->setComparisonOperator(comparisonOperator);
-					result->setBound(bound);
-					result->setChild(child->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(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					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 += " ";
-					result += std::to_string(bound);
-					result += " (";
-					result += child->toString();
-					result += ")";
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractPathFormula<T>> const & getChild () const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractPathFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-				/*!
-				 * Gets the comparison operator.
-				 *
-				 * @returns An enum value representing the comparison relation.
-				 */
-				storm::properties::ComparisonType const getComparisonOperator() const {
-					return comparisonOperator;
-				}
-
-				/*!
-				 * Sets the comparison operator.
-				 *
-				 * @param comparisonOperator An enum value representing the new comparison relation.
-				 */
-				void setComparisonOperator(storm::properties::ComparisonType comparisonOperator) {
-					this->comparisonOperator = comparisonOperator;
-				}
-
-				/*!
-				 * Gets the bound which the probability that the path formula holds has to obey.
-				 *
-				 * @returns The probability bound.
-				 */
-				T const & getBound() const {
-					return bound;
-				}
-
-				/*!
-				 * Sets the bound which the probability that the path formula holds has to obey.
-				 *
-				 * @param bound The new probability bound.
-				 */
-				void setBound(T const & bound) {
-					this->bound = bound;
-				}
-
-				/*!
-				 * Checks if the bound is met by the given value.
-				 *
-				 * @param value The value to test against the bound.
-				 * @returns True iff value <comparisonOperator> bound holds.
-				 */
-				bool meetsBound(T const & value) const {
-					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;
-					}
-				}
-
-			private:
-
-				// The operator used to indicate the kind of bound that is to be met.
-				storm::properties::ComparisonType comparisonOperator;
-
-				// The probability bound.
-				T bound;
-
-				// The path formula for which the probability to be satisfied has to meet the bound.
-				std::shared_ptr<AbstractPathFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_PROBABILISTICBOUNDOPERATOR_H_ */

src/properties/csl/SteadyStateBoundOperator.h

@@ -1,227 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_STEADYSTATEOPERATOR_H_
-#define STORM_PROPERTIES_CSL_STEADYSTATEOPERATOR_H_
-
-#include "AbstractStateFormula.h"
-#include "src/properties/ComparisonType.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class SteadyStateBoundOperator;
-
-			/*!
-			 * Interface class for model checkers that support SteadyStateOperator.
-			 *
-			 * All model checkers that support the formula class SteadyStateOperator must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class ISteadyStateBoundOperatorModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~ISteadyStateBoundOperatorModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a SteadyStateOperator formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual storm::storage::BitVector checkSteadyStateBoundOperator(SteadyStateBoundOperator<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl formula tree with a SteadyStateOperator node as root.
-			 *
-			 * Has two state formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff the long-run probability of being in a state satisfying \e child meets the \e bound specified in this operator.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class SteadyStateBoundOperator : public AbstractStateFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a SteadyStateBoundOperator node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				SteadyStateBoundOperator() : comparisonOperator(LESS), bound(storm::utility::constantZero<T>()), child(nullptr) {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Creates a SteadyStateBoundOperator node using the given parameters.
-				 *
-				 * @param comparisonOperator The relation for the bound.
-				 * @param bound The bound for the probability.
-				 * @param child The child formula subtree.
-				 */
-				SteadyStateBoundOperator(storm::properties::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractStateFormula<T>> const & child)
-					: comparisonOperator(comparisonOperator), bound(bound), child(child) {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~SteadyStateBoundOperator() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new SteadyStateBoundOperator object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractStateFormula<T>> clone() const override {
-					auto result = std::make_shared<SteadyStateBoundOperator<T>>();
-					result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual storm::storage::BitVector check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "S ";
-					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 += child->toString();
-					result += ")";
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getChild () const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-				/*!
-				 * Gets the comparison operator.
-				 *
-				 * @returns An enum value representing the comparison relation.
-				 */
-				ComparisonType const getComparisonOperator() const {
-					return comparisonOperator;
-				}
-
-				/*!
-				 * Sets the comparison operator.
-				 *
-				 * @param comparisonOperator An enum value representing the new comparison relation.
-				 */
-				void setComparisonOperator(ComparisonType comparisonOperator) {
-					this->comparisonOperator = comparisonOperator;
-				}
-
-				/*!
-				 * Gets the bound which the steady state probability has to obey.
-				 *
-				 * @returns The probability bound.
-				 */
-				T const & getBound() const {
-					return bound;
-				}
-
-				/*!
-				 * Sets the bound which the steady state probability has to obey.
-				 *
-				 * @param bound The new probability bound.
-				 */
-				void setBound(T const & bound) {
-					this->bound = bound;
-				}
-
-				/*!
-				 * Checks if the bound is met by the given value.
-				 *
-				 * @param value The value to test against the bound.
-				 * @returns True iff value <comparisonOperator> bound holds.
-				 */
-				bool meetsBound(T value) const {
-					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;
-					}
-				}
-
-			private:
-
-				// The operator used to indicate the kind of bound that is to be met.
-				ComparisonType comparisonOperator;
-
-				// The probability bound.
-				T bound;
-
-				// The state formula for whose state the long-run probability has to meet the bound.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_STEADYSTATEOPERATOR_H_ */

src/properties/csl/TimeBoundedEventually.h

@@ -1,212 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_TIMEBOUNDEDEVENTUALLY_H_
-#define STORM_PROPERTIES_CSL_TIMEBOUNDEDEVENTUALLY_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template<class T> class TimeBoundedEventually;
-
-			/*!
-			 * Interface class for model checkers that support TimeBoundedEventually.
-			 *
-			 * All model checkers that support the formula class TimeBoundedEventually must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class ITimeBoundedEventuallyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~ITimeBoundedEventuallyModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a TimeBoundedEventually formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkTimeBoundedEventually(TimeBoundedEventually<T> const & obj, bool qualitative) const = 0;
-			};
-
-			/*!
-			 * Class for a Csl (path) formula tree with a TimeBoundedEventually node as root.
-			 *
-			 * Has one state formula as subformula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff formula \e child holds within the given time interval [lowerBound, upperBound].
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template<class T>
-			class TimeBoundedEventually: public AbstractPathFormula<T> {
-			public:
-
-				/*!
-				 * Creates a TimeBoundedEventually node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				TimeBoundedEventually() : child(nullptr), lowerBound(0), upperBound(0) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a TimeBoundedEventually node using the given parameters.
-				 *
-				 * @param lowerBound The lower bound of the admissable time interval.
-				 * @param upperBound The upper bound of the admissable time interval.
-				 * @param child The child formula subtree.
-				 */
-				TimeBoundedEventually(T lowerBound, T upperBound, std::shared_ptr<AbstractStateFormula<T>> const & child) : child(child) {
-					setInterval(lowerBound, upperBound);
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~TimeBoundedEventually() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new TimeBoundedEventually object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<TimeBoundedEventually<T>>();
-					result->setInterval(lowerBound, upperBound);
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "F";
-					if (upperBound == std::numeric_limits<double>::infinity()) {
-						result += ">=" + std::to_string(lowerBound);
-					} else {
-						result += "[";
-						result += std::to_string(lowerBound);
-						result += ",";
-						result += std::to_string(upperBound);
-						result += "]";
-					}
-					result += " ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractStateFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-				/*!
-				 * Get the lower time bound.
-				 *
-				 * @return The lower time bound.
-				 */
-				T const & getLowerBound() const {
-					return lowerBound;
-				}
-
-				/*!
-				 * Get the upper time bound.
-				 *
-				 * @return The upper time bound.
-				 */
-				T const & getUpperBound() const {
-					return upperBound;
-				}
-
-				/*!
-				 * Set the time interval for the time bounded operator.
-				 *
-				 * @param lowerBound The new lower time bound.
-				 * @param upperBound The new upper time bound.
-				 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
-				 */
-				void setInterval(T lowerBound, T upperBound) {
-					if (lowerBound > upperBound) {
-						throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound");
-					}
-					this->lowerBound = lowerBound;
-					this->upperBound = upperBound;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractStateFormula<T>> child;
-
-				// The lower time bound.
-				T lowerBound;
-
-				// The upper time bound.
-				T upperBound;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_TIMEBOUNDEDEVENTUALLY_H_ */

src/properties/csl/TimeBoundedUntil.h

@@ -1,249 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_TIMEBOUNDEDUNTIL_H_
-#define STORM_PROPERTIES_CSL_TIMEBOUNDEDUNTIL_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class TimeBoundedUntil;
-
-			/*!
-			 * Interface class for model checkers that support TimeBoundedUntil.
-			 *
-			 * All model checkers that support the formula class TimeBoundedUntil must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class ITimeBoundedUntilModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~ITimeBoundedUntilModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a TimeBoundedUntil formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkTimeBoundedUntil(TimeBoundedUntil<T> const & obj, bool qualitative) const = 0;
-			};
-
-
-			/*!
-			 * Class for a Csl (path) formula tree with a TimeBoundedUntil node as root.
-			 *
-			 * Has two state formulas as subformulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff formula \e right holds within the given time interval [lowerBound, upperBound] and \e left holds
-			 * in each point in time before that.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class TimeBoundedUntil: public AbstractPathFormula<T> {
-			public:
-
-				/*!
-				 * Creates a TimeBoundedUntil node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				TimeBoundedUntil() : left(nullptr), right(nullptr), lowerBound(0), upperBound(0) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a TimeBoundedUntil node using the given parameters.
-				 *
-				 * @param lowerBound The lower bound of the admissable time interval.
-				 * @param upperBound The upper bound of the admissable time interval.
-				 * @param child The child formula subtree.
-				 */
-				TimeBoundedUntil(T lowerBound, T upperBound, std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right) {
-					setInterval(lowerBound, upperBound);
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~TimeBoundedUntil() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new TimeBoundedUntil object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<TimeBoundedUntil<T>>();
-					result->setInterval(lowerBound, upperBound);
-					if (this->isLeftSet()) {
-						result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-						result->setRight(right->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = left->toString();
-					result += " U";
-					if (upperBound == std::numeric_limits<double>::infinity()) {
-						result += ">=" + std::to_string(lowerBound);
-					} else {
-						result += "[";
-						result += std::to_string(lowerBound);
-						result += ",";
-						result += std::to_string(upperBound);
-						result += "]";
-					}
-					result += " ";
-					result += right->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-				/*!
-				 * Get the lower time bound.
-				 *
-				 * @return The lower time bound.
-				 */
-				T const & getLowerBound() const {
-					return lowerBound;
-				}
-
-				/*!
-				 * Get the upper time bound.
-				 *
-				 * @return The upper time bound.
-				 */
-				T const & getUpperBound() const {
-					return upperBound;
-				}
-
-				/**
-				 * Set the time interval for the time bounded operator
-				 *
-				 * @param lowerBound The new lower time bound.
-				 * @param upperBound The new upper time bound.
-				 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
-				 */
-				void setInterval(T lowerBound, T upperBound) {
-					if (lowerBound > upperBound) {
-						throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound");
-					}
-					this->lowerBound = lowerBound;
-					this->upperBound = upperBound;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractStateFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractStateFormula<T>> right;
-
-				// The lower time bound.
-				T lowerBound;
-
-				// The upper time bound.
-				T upperBound;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_TIMEBOUNDEDUNTIL_H_ */

src/properties/csl/Until.h

@@ -1,198 +0,0 @@
-#ifndef STORM_PROPERTIES_CSL_UNTIL_H_
-#define STORM_PROPERTIES_CSL_UNTIL_H_
-
-#include "src/properties/csl/AbstractPathFormula.h"
-#include "src/properties/csl/AbstractStateFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace csl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Until;
-
-			/*!
-			 * Interface class for model checkers that support Until.
-			 *
-			 * All model checkers that support the formula class Until must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IUntilModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IUntilModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates an Until formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-					 *                    results are only compared against the bounds 0 and 1.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkUntil(Until<T> const & obj, bool qualitative) const = 0;
-			};
-
-			/*!
-			 * @brief
-			 * Class for a Csl (path) formula tree with an Until node as root.
-			 *
-			 * Has two state formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
-			 * \e left holds always.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractPathFormula
-			 * @see AbstractCslFormula
-			 */
-			template <class T>
-			class Until : public AbstractPathFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Until node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Until() : left(nullptr), right(nullptr){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Until node using the given parameters.
-				 *
-				 * @param left The left formula subtree.
-				 * @param right The right formula subtree.
-				 */
-				Until(std::shared_ptr<AbstractStateFormula<T>> const & left, std::shared_ptr<AbstractStateFormula<T>> const & right) : left(left), right(right){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Until() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Until object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const override {
-					auto result = std::make_shared<Until<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(left->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const override {
-					return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = left->toString();
-					result += " U ";
-					result += right->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractStateFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractStateFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractStateFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractStateFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractStateFormula<T>> right;
-			};
-
-		} // namespace csl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_CSL_UNTIL_H_ */

src/properties/logic/AtomicExpressionFormula.cpp

@@ -0,0 +1,18 @@
+#include "src/properties/logic/AtomicExpressionFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool AtomicExpressionFormula::isAtomicExpressionFormula() const {
+            return true;
+        }
+        
+        storm::expressions::Expression const& AtomicExpressionFormula::getExpression() const {
+            return expression;
+        }
+        
+        std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
+            out << expression;
+            return out;
+        }
+    }
+}

src/properties/logic/AtomicExpressionFormula.h

@@ -2,11 +2,25 @@
 #define STORM_LOGIC_ATOMICEXPRESSIONFORMULA_H_
 
 #include "src/properties/logic/StateFormula.h"
+#include "src/storage/expressions/Expression.h"
 
 namespace storm {
     namespace logic {
         class AtomicExpressionFormula : public StateFormula {
+        public:
+            virtual ~AtomicExpressionFormula() {
+                // Intentionally left empty.
+            }
             
+            virtual bool isAtomicExpressionFormula() const override;
+            
+            storm::expressions::Expression const& getExpression() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            // The atomic expression represented by this node in the formula tree.
+            storm::expressions::Expression expression;
         };
     }
 }

src/properties/logic/AtomicLabelFormula.cpp

@@ -0,0 +1,18 @@
+#include "src/properties/logic/AtomicLabelFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool AtomicLabelFormula::isAtomicLabelFormula() const {
+            return true;
+        }
+        
+        std::string const& AtomicLabelFormula::getLabel() const {
+            return label;
+        }
+        
+        std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out) const {
+            out << "\"" << label << "\"";
+            return out;
+        }
+    }
+}

src/properties/logic/AtomicLabelFormula.h

@@ -1,12 +1,26 @@
 #ifndef STORM_LOGIC_ATOMICLABELFORMULA_H_
 #define STORM_LOGIC_ATOMICLABELFORMULA_H_
 
+#include <string>
+
 #include "src/properties/logic/StateFormula.h"
 
 namespace storm {
     namespace logic {
         class AtomicLabelFormula : public StateFormula {
+        public:
+            virtual ~AtomicLabelFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isAtomicLabelFormula() const override;
+
+            std::string const& getLabel() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
             
+        private:
+            std::string label;
         };
     }
 }

src/properties/logic/BinaryBooleanStateFormula.cpp

@@ -0,0 +1,25 @@
+#include "src/properties/logic/BinaryBooleanStateFormula.h"
+
+namespace storm {
+    namespace logic {
+        BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<StateFormula> const& leftSubformula, std::shared_ptr<StateFormula> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
+            // Intentionally left empty.
+        }
+        
+        bool BinaryBooleanStateFormula::isBinaryBooleanStateFormula() const {
+            return true;
+        }
+        
+        std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
+            out << "(";
+            this->getLeftSubformula().writeToStream(out);
+            switch (operatorType) {
+                case OperatorType::And: out << " & "; break;
+                case OperatorType::Or: out << " | "; break;
+            }
+            this->getRightSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}

src/properties/logic/BinaryBooleanStateFormula.h

@@ -6,7 +6,21 @@
 namespace storm {
     namespace logic {
         class BinaryBooleanStateFormula : public BinaryStateFormula {
+        public:
+            enum class OperatorType {And, Or};
+
+            BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<StateFormula> const& leftSubformula, std::shared_ptr<StateFormula> const& rightSubformula);
+            
+            virtual ~BinaryBooleanStateFormula() {
+                // Intentionally left empty.
+            };
+            
+            virtual bool isBinaryBooleanStateFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
             
+        private:
+            OperatorType operatorType;
         };
     }
 }

src/properties/logic/BinaryPathFormula.cpp

@@ -0,0 +1,29 @@
+#include "src/properties/logic/BinaryPathFormula.h"
+
+namespace storm {
+    namespace logic {
+        BinaryPathFormula::BinaryPathFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) {
+            // Intentionally left empty.
+        }
+
+        bool BinaryPathFormula::isBinaryPathFormula() const {
+            return true;
+        }
+        
+        Formula& BinaryPathFormula::getLeftSubformula() {
+            return *leftSubformula;
+        }
+        
+        Formula const& BinaryPathFormula::getLeftSubformula() const {
+            return *leftSubformula;
+        }
+        
+        Formula& BinaryPathFormula::getRightSubformula() {
+            return *rightSubformula;
+        }
+        
+        Formula const& BinaryPathFormula::getRightSubformula() const {
+            return *rightSubformula;
+        }
+    }
+}

src/properties/logic/BinaryPathFormula.h

@@ -1,12 +1,31 @@
 #ifndef STORM_LOGIC_BINARYPATHFORMULA_H_
 #define STORM_LOGIC_BINARYPATHFORMULA_H_
 
+#include <memory>
+
 #include "src/properties/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
         class BinaryPathFormula : public PathFormula {
+        public:
+            BinaryPathFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula);
+            
+            virtual ~BinaryPathFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isBinaryPathFormula() const override;
+            
+            Formula& getLeftSubformula();
+            Formula const& getLeftSubformula() const;
+            
+            Formula& getRightSubformula();
+            Formula const& getRightSubformula() const;
             
+        private:
+            std::shared_ptr<Formula> leftSubformula;
+            std::shared_ptr<Formula> rightSubformula;
         };
     }
 }

src/properties/logic/BinaryStateFormula.cpp

@@ -0,0 +1,29 @@
+#include "src/properties/logic/BinaryStateFormula.h"
+
+namespace storm {
+    namespace logic {
+        BinaryStateFormula::BinaryStateFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula) : leftSubformula(leftSubformula), rightSubformula(rightSubformula) {
+            // Intentionally left empty.
+        }
+        
+        bool BinaryStateFormula::isBinaryStateFormula() const {
+            return true;
+        }
+        
+        Formula& BinaryStateFormula::getLeftSubformula() {
+            return *leftSubformula;
+        }
+        
+        Formula const& BinaryStateFormula::getLeftSubformula() const {
+            return *leftSubformula;
+        }
+        
+        Formula& BinaryStateFormula::getRightSubformula() {
+            return *rightSubformula;
+        }
+        
+        Formula const& BinaryStateFormula::getRightSubformula() const {
+            return *rightSubformula;
+        }
+    }
+}

src/properties/logic/BinaryStateFormula.h

@@ -6,7 +6,24 @@
 namespace storm {
     namespace logic {
         class BinaryStateFormula : public StateFormula {
+        public:
+            BinaryStateFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula);
             
+            virtual ~BinaryStateFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isBinaryStateFormula() const override;
+
+            Formula& getLeftSubformula();
+            Formula const& getLeftSubformula() const;
+            
+            Formula& getRightSubformula();
+            Formula const& getRightSubformula() const;
+            
+        private:
+            std::shared_ptr<Formula> leftSubformula;
+            std::shared_ptr<Formula> rightSubformula;
         };
     }
 }

src/properties/logic/BooleanLiteralFormula.cpp

@@ -0,0 +1,26 @@
+#include "src/properties/logic/BooleanLiteralFormula.h"
+
+namespace storm {
+    namespace logic {
+        BooleanLiteralFormula::BooleanLiteralFormula(bool value) : value(value) {
+            // Intenionally left empty.
+        }
+        
+        bool BooleanLiteralFormula::isTrue() const {
+            return value;
+        }
+        
+        bool BooleanLiteralFormula::isFalse() const {
+            return !value;
+        }
+        
+        std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const {
+            if (value) {
+                out << "true";
+            } else {
+                out << "false";
+            }
+            return out;
+        }
+    }
+}

src/properties/logic/BooleanLiteralFormula.h

@@ -6,7 +6,20 @@
 namespace storm {
     namespace logic {
         class BooleanLiteralFormula : public StateFormula {
+        public:
+            BooleanLiteralFormula(bool value);
             
+            virtual ~BooleanLiteralFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isTrue() const;
+            virtual bool isFalse() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            bool value;
         };
     }
 }

src/properties/logic/BoundedUntilFormula.cpp

@@ -0,0 +1,48 @@
+#include "src/properties/logic/BoundedUntilFormula.h"
+
+namespace storm {
+    namespace logic {
+        BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) {
+            // Intentionally left empty.
+        }
+        
+        BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula, uint_fast64_t upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(upperBound) {
+            // Intentionally left empty.
+        }
+        
+        bool BoundedUntilFormula::isBoundedUntilFormula() const {
+            return true;
+        }
+        
+        bool BoundedUntilFormula::isIntervalBounded() const {
+            return bounds.which() == 1;
+        }
+        
+        bool BoundedUntilFormula::isIntegerUpperBounded() const {
+            return bounds.which() == 0;
+        }
+        
+        std::pair<double, double> const& BoundedUntilFormula::getIntervalBounds() const {
+            return boost::get<std::pair<double, double>>(bounds);
+        }
+        
+        uint_fast64_t BoundedUntilFormula::getUpperBound() const {
+            return boost::get<uint_fast64_t>(bounds);
+        }
+        
+        std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
+            this->getLeftSubformula().writeToStream(out);
+            
+            out << " U";
+            if (this->isIntervalBounded()) {
+                std::pair<double, double> const& intervalBounds = getIntervalBounds();
+                out << "[" << intervalBounds.first << "," << intervalBounds.second << "] ";
+            } else {
+                out << "<=" << getUpperBound() << " ";
+            }
+            
+            this->getRightSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/BoundedUntilFormula.h

@@ -1,12 +1,29 @@
 #ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
 #define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
 
+#include <boost/variant.hpp>
+
 #include "src/properties/logic/BinaryPathFormula.h"
 
 namespace storm {
     namespace logic {
         class BoundedUntilFormula : public BinaryPathFormula {
+        public:
+            BoundedUntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula, double lowerBound, double upperBound);
+            BoundedUntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula, uint_fast64_t upperBound);
+            
+            virtual bool isBoundedUntilFormula() const override;
+
+            bool isIntervalBounded() const;
+            bool isIntegerUpperBounded() const;
+            
+            std::pair<double, double> const& getIntervalBounds() const;
+            uint_fast64_t getUpperBound() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
             
+        private:
+            boost::variant<uint_fast64_t, std::pair<double, double>> bounds;
         };
     }
 }

src/properties/logic/ComparisonType.cpp

@@ -0,0 +1,15 @@
+#include "src/properties/logic/ComparisonType.h"
+
+namespace storm {
+    namespace logic {
+        std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType) {
+            switch (comparisonType) {
+                case Less: out << "<"; break;
+                case LessEqual: out << "<="; break;
+                case Greater: out << ">"; break;
+                case GreaterEqual: out << ">="; break;
+            }
+            return out;
+        }
+    }
+}

src/properties/logic/ComparisonType.h

@@ -0,0 +1,14 @@
+#ifndef STORM_LOGIC_COMPARISONTYPE_H_
+#define STORM_LOGIC_COMPARISONTYPE_H_
+
+#include <iostream>
+
+namespace storm {
+	namespace logic {
+		enum ComparisonType { Less, LessEqual, Greater, GreaterEqual };
+        
+        std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
+	}
+}
+
+#endif /* STORM_LOGIC_COMPARISONTYPE_H_ */

src/properties/logic/ConditionalPathFormula.cpp

@@ -0,0 +1,20 @@
+#include "src/properties/logic/ConditionalPathFormula.h"
+
+namespace storm {
+    namespace logic {
+        ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) {
+            // Intentionally left empty.
+        }
+        
+        bool ConditionalPathFormula::isConditionalPathFormula() const {
+            return true;
+        }
+        
+        std::ostream& ConditionalPathFormula::writeToStream(std::ostream& out) const {
+            this->getLeftSubformula().writeToStream(out);
+            out << " | ";
+            this->getRightSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/ConditionalPathFormula.h

@@ -6,7 +6,16 @@
 namespace storm {
     namespace logic {
         class ConditionalPathFormula : public BinaryPathFormula {
+        public:
+            ConditionalPathFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula);
             
+            virtual ~ConditionalPathFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isConditionalPathFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
 }

src/properties/logic/CumulativeRewardFormula.cpp

@@ -0,0 +1,18 @@
+#include "src/properties/logic/CumulativeRewardFormula.h"
+
+namespace storm {
+    namespace logic {
+        CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t stepBound) : stepBound(stepBound) {
+            // Intentionally left empty.
+        }
+        
+        bool CumulativeRewardFormula::isCumulativeRewardFormula() const {
+            return true;
+        }
+        
+        std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
+            out << "C<=" << stepBound;
+            return out;
+        }
+    }
+}

src/properties/logic/CumulativeRewardFormula.h

@@ -6,7 +6,19 @@
 namespace storm {
     namespace logic {
         class CumulativeRewardFormula : public PathRewardFormula {
+        public:
+            CumulativeRewardFormula(uint_fast64_t stepBound);
             
+            virtual ~CumulativeRewardFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isCumulativeRewardFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            uint_fast64_t stepBound;
         };
     }
 }

src/properties/logic/EventuallyFormula.cpp

@@ -0,0 +1,19 @@
+#include "src/properties/logic/EventuallyFormula.h"
+
+namespace storm {
+    namespace logic {
+        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula> const& subformula) : UnaryPathFormula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool EventuallyFormula::isEventuallyFormula() const {
+            return true;
+        }
+        
+        std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {
+            out << "F ";
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/EventuallyFormula.h

@@ -6,7 +6,16 @@
 namespace storm {
     namespace logic {
         class EventuallyFormula : public UnaryPathFormula {
+        public:
+            EventuallyFormula(std::shared_ptr<Formula> const& subformula);
             
+            virtual ~EventuallyFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isEventuallyFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
 }

src/properties/logic/Formula.cpp

@@ -2,10 +2,6 @@
 
 namespace storm {
     namespace logic {
-        Formula::~Formula() {
-            // Intentionally left empty.
-        }
-        
         bool Formula::isPathFormula() const {
             return false;
         }
@@ -34,6 +30,14 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isTrue() const {
+            return false;
+        }
+        
+        bool Formula::isFalse() const {
+            return false;
+        }
+        
         bool Formula::isAtomicExpressionFormula() const {
             return false;
         }
@@ -94,7 +98,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isProbabilisticOperator() const {
+        bool Formula::isProbabilityOperator() const {
             return false;
         }
         
@@ -102,6 +106,18 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isPctlPathFormula() const {
+            return false;
+        }
+        
+        bool Formula::isPctlStateFormula() const {
+            return false;
+        }
+        
+        bool Formula::isPltlFormula() const {
+            return false;
+        }
+        
         PathFormula& Formula::asPathFormula() {
             return dynamic_cast<PathFormula&>(*this);
         }
@@ -293,5 +309,9 @@ namespace storm {
         RewardOperatorFormula const& Formula::asRewardOperatorFormula() const {
             return dynamic_cast<RewardOperatorFormula const&>(*this);
         }
+        
+        std::ostream& operator<<(std::ostream& out, Formula const& formula) {
+            return formula.writeToStream(out);
+        }
     }
 }

src/properties/logic/Formula.h

@@ -2,6 +2,7 @@
 #define STORM_LOGIC_FORMULA_H_
 
 #include <memory>
+#include <iostream>
 
 #include "src/modelchecker/CheckResult.h"
 
@@ -39,7 +40,11 @@ namespace storm {
         class Formula {
         public:
             // Make the destructor virtual to allow deletion of objects of subclasses via a pointer to this class.
-            virtual ~Formula();
+            virtual ~Formula() {
+                // Intentionally left empty.
+            };
+            
+            friend std::ostream& operator<<(std::ostream& out, Formula const& formula);
             
             // Methods for querying the exact formula type.
             virtual bool isPathFormula() const;
@@ -49,6 +54,8 @@ namespace storm {
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
             virtual bool isBooleanLiteralFormula() const;
+            virtual bool isTrue() const;
+            virtual bool isFalse() const;
             virtual bool isAtomicExpressionFormula() const;
             virtual bool isAtomicLabelFormula() const;
             virtual bool isUntilFormula() const;
@@ -64,9 +71,13 @@ namespace storm {
             virtual bool isCumulativeRewardFormula() const;
             virtual bool isInstantaneousRewardFormula() const;
             virtual bool isReachabilityRewardFormula() const;
-            virtual bool isProbabilisticOperator() const;
+            virtual bool isProbabilityOperator() const;
             virtual bool isRewardOperator() const;
 
+            virtual bool isPctlPathFormula() const;
+            virtual bool isPctlStateFormula() const;
+            virtual bool isPltlFormula() const;
+            
             PathFormula& asPathFormula();
             PathFormula const& asPathFormula() const;
         
@@ -139,9 +150,13 @@ namespace storm {
             RewardOperatorFormula& asRewardOperatorFormula();
             RewardOperatorFormula const& asRewardOperatorFormula() const;
             
+            virtual std::ostream& writeToStream(std::ostream& out) const = 0;
+            
         private:
             // Currently empty.
         };
+        
+        std::ostream& operator<<(std::ostream& out, Formula const& formula);
     }
 }
 

src/properties/logic/Formulas.h

@@ -22,6 +22,8 @@
 #include "src/properties/logic/UnaryStateFormula.h"
 #include "src/properties/logic/UntilFormula.h"
 #include "src/properties/logic/ConditionalPathFormula.h"
+#include "src/properties/logic/ProbabilityOperatorFormula.h"
+#include "src/properties/logic/RewardOperatorFormula.h"
 
 
 

src/properties/logic/GloballyFormula.cpp

@@ -0,0 +1,19 @@
+#include "src/properties/logic/GloballyFormula.h"
+
+namespace storm {
+    namespace logic {
+        GloballyFormula::GloballyFormula(std::shared_ptr<Formula> const& subformula) : UnaryPathFormula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool GloballyFormula::isGloballyFormula() const {
+            return true;
+        }
+        
+        std::ostream& GloballyFormula::writeToStream(std::ostream& out) const {
+            out << "G ";
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/GloballyFormula.h

@@ -6,7 +6,16 @@
 namespace storm {
     namespace logic {
         class GloballyFormula : public UnaryPathFormula {
+        public:
+            GloballyFormula(std::shared_ptr<Formula> const& subformula);
             
+            virtual ~GloballyFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isGloballyFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
 }

src/properties/logic/InstantaneousRewardFormula.cpp

@@ -0,0 +1,18 @@
+#include "src/properties/logic/InstantaneousRewardFormula.h"
+
+namespace storm {
+    namespace logic {
+        InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t stepCount) : stepCount(stepCount) {
+            // Intentionally left empty.
+        }
+        
+        bool InstantaneousRewardFormula::isInstantaneousRewardFormula() const {
+            return true;
+        }
+        
+        std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const {
+            out << "I=" << stepCount;
+            return out;
+        }
+    }
+}

src/properties/logic/InstantaneousRewardFormula.h

@@ -6,7 +6,19 @@
 namespace storm {
     namespace logic {
         class InstantaneousRewardFormula : public PathRewardFormula {
+        public:
+            InstantaneousRewardFormula(uint_fast64_t stepCount);
             
+            virtual ~InstantaneousRewardFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isInstantaneousRewardFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            uint_fast64_t stepCount;
         };
     }
 }

src/properties/logic/NextFormula.cpp

@@ -0,0 +1,19 @@
+#include "src/properties/logic/NextFormula.h"
+
+namespace storm {
+    namespace logic {
+        NextFormula::NextFormula(std::shared_ptr<Formula> const& subformula) : UnaryPathFormula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool NextFormula::isNextFormula() const {
+            return true;
+        }
+        
+        std::ostream& NextFormula::writeToStream(std::ostream& out) const {
+            out << "X ";
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/NextFormula.h

@@ -6,7 +6,16 @@
 namespace storm {
     namespace logic {
         class NextFormula : public UnaryPathFormula {
+        public:
+            NextFormula(std::shared_ptr<Formula> const& subformula);
             
+            virtual ~NextFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isNextFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
 }

src/properties/logic/OperatorFormula.cpp

@@ -0,0 +1,44 @@
+#include "src/properties/logic/OperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        OperatorFormula::OperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) {
+            // Intentionally left empty.
+        }
+        
+        bool OperatorFormula::hasBound() const {
+            return static_cast<bool>(bound);
+        }
+        
+        ComparisonType const& OperatorFormula::getComparisonType() const {
+            return comparisonType.get();
+        }
+        
+        double OperatorFormula::getBound() const {
+            return bound.get();
+        }
+        
+        bool OperatorFormula::hasOptimalityType() const {
+            return static_cast<bool>(optimalityType);
+        }
+        
+        OptimalityType const& OperatorFormula::getOptimalityType() const {
+            return optimalityType.get();
+        }
+        
+        std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
+            if (hasOptimalityType()) {
+                out << getOptimalityType();
+            }
+            if (hasBound()) {
+                out << getComparisonType() << getBound();
+            } else {
+                out << "=?";
+            }
+            out << " [";
+            this->getSubformula().writeToStream(out);
+            out << "]";
+            return out;
+        }
+    }
+}

src/properties/logic/OperatorFormula.h

@@ -0,0 +1,37 @@
+#ifndef STORM_LOGIC_OPERATORFORMULA_H_
+#define STORM_LOGIC_OPERATORFORMULA_H_
+
+#include <boost/optional.hpp>
+
+#include "src/properties/logic/UnaryStateFormula.h"
+#include "src/properties/logic/OptimalityType.h"
+#include "src/properties/logic/ComparisonType.h"
+
+namespace storm {
+    namespace logic {
+        class OperatorFormula : public UnaryStateFormula {
+        public:
+            OperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
+            
+            virtual ~OperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            bool hasBound() const;
+            ComparisonType const& getComparisonType() const;
+            double getBound() const;
+            bool hasOptimalityType() const;
+            OptimalityType const& getOptimalityType() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            std::string operatorSymbol;
+            boost::optional<ComparisonType> comparisonType;
+            boost::optional<double> bound;
+            boost::optional<OptimalityType> optimalityType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_OPERATORFORMULA_H_ */

src/properties/logic/OptimalityType.cpp

@@ -0,0 +1,13 @@
+#include "src/properties/logic/OptimalityType.h"
+
+namespace storm {
+    namespace logic {
+        std::ostream& operator<<(std::ostream& out, OptimalityType const& optimalityType) {
+            switch (optimalityType) {
+                case Maximize: out << "max"; break;
+                case Minimize: out << "min"; break;
+            }
+            return out;
+        }
+    }
+}

src/properties/logic/OptimalityType.h

@@ -0,0 +1,14 @@
+#ifndef STORM_LOGIC_OPTIMALITYTYPE_H_
+#define STORM_LOGIC_OPTIMALITYTYPE_H_
+
+#include <iostream>
+
+namespace storm {
+	namespace logic {
+		enum OptimalityType { Minimize, Maximize };
+        
+        std::ostream& operator<<(std::ostream& out, OptimalityType const& optimalityType);
+	}
+}
+
+#endif /* STORM_LOGIC_OPTIMALITYTYPE_H_ */

src/properties/logic/PathFormula.cpp

@@ -0,0 +1,9 @@
+#include "src/properties/logic/PathFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool PathFormula::isPathFormula() const {
+            return true;
+        }
+    }
+}

src/properties/logic/PathFormula.h

@@ -6,7 +6,12 @@
 namespace storm {
     namespace logic {
         class PathFormula : public Formula {
+        public:
+            virtual ~PathFormula() {
+                // Intentionally left empty.
+            };
             
+            virtual bool isPathFormula() const override;
         };
     }
 }

src/properties/logic/PathRewardFormula.cpp

@@ -0,0 +1,9 @@
+#include "src/properties/logic/PathRewardFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool PathRewardFormula::isPathRewardFormula() const {
+            return true;
+        }
+    }
+}

src/properties/logic/PathRewardFormula.h

@@ -6,7 +6,12 @@
 namespace storm {
     namespace logic {
         class PathRewardFormula : public PathFormula {
+        public:
+            virtual ~PathRewardFormula() {
+                // Intentionally left empty.
+            }
             
+            virtual bool isPathRewardFormula() const override;
         };
     }
 }

src/properties/logic/ProbabilityOperatorFormula.cpp

@@ -0,0 +1,35 @@
+#include "src/properties/logic/ProbabilityOperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : ProbabilityOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool ProbabilityOperatorFormula::isProbabilityOperator() const {
+            return true;
+        }
+        
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) {
+            // Intentionally left empty.
+        }
+        
+        std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "P";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/ProbabilityOperatorFormula.h

@@ -1,12 +1,27 @@
 #ifndef STORM_LOGIC_PROBABILITYOPERATORFORMULA_H_
 #define STORM_LOGIC_PROBABILITYOPERATORFORMULA_H_
 
-#include "src/properties/logic/PathRewardFormula.h"
+#include "src/properties/logic/OperatorFormula.h"
 
 namespace storm {
     namespace logic {
-        class ProbabilityOperatorFormula : public Formula {
+        class ProbabilityOperatorFormula : public OperatorFormula {
+        public:
+            ProbabilityOperatorFormula(std::shared_ptr<Formula> const& subformula);
+            ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
+            ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            ProbabilityOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
             
+            virtual ~ProbabilityOperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isProbabilityOperator() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            ProbabilityOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
         };
     }
 }

src/properties/logic/ReachabilityRewardFormula.cpp

@@ -0,0 +1,27 @@
+#include "src/properties/logic/ReachabilityRewardFormula.h"
+
+namespace storm {
+    namespace logic {
+        ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr<StateFormula> const& subformula) : subformula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool ReachabilityRewardFormula::isReachabilityRewardFormula() const {
+            return true;
+        }
+        
+        StateFormula& ReachabilityRewardFormula::getSubformula() {
+            return *subformula;
+        }
+        
+        StateFormula const& ReachabilityRewardFormula::getSubformula() const {
+            return *subformula;
+        }
+        
+        std::ostream& ReachabilityRewardFormula::writeToStream(std::ostream& out) const {
+            out << "F ";
+            this->getSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/ReachabilityRewardFormula.h

@@ -1,12 +1,30 @@
 #ifndef STORM_LOGIC_REACHABILITYREWARDFORMULA_H_
 #define STORM_LOGIC_REACHABILITYREWARDFORMULA_H_
 
+#include <memory>
+
 #include "src/properties/logic/PathRewardFormula.h"
+#include "src/properties/logic/StateFormula.h"
 
 namespace storm {
     namespace logic {
         class ReachabilityRewardFormula : public PathRewardFormula {
+        public:
+            ReachabilityRewardFormula(std::shared_ptr<StateFormula> const& subformula);
+            
+            virtual ~ReachabilityRewardFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isReachabilityRewardFormula() const override;
+            
+            StateFormula& getSubformula();
+            StateFormula const& getSubformula() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
             
+        private:
+            std::shared_ptr<StateFormula> const& subformula;
         };
     }
 }

src/properties/logic/RewardOperatorFormula.cpp

@@ -0,0 +1,35 @@
+#include "src/properties/logic/RewardOperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        RewardOperatorFormula::RewardOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        RewardOperatorFormula::RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : RewardOperatorFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool RewardOperatorFormula::isRewardOperator() const {
+            return true;
+        }
+        
+        RewardOperatorFormula::RewardOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) {
+            // Intentionally left empty.
+        }
+        
+        std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "R";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/RewardOperatorFormula.h

@@ -1,12 +1,27 @@
 #ifndef STORM_LOGIC_REWARDOPERATORFORMULA_H_
 #define STORM_LOGIC_REWARDOPERATORFORMULA_H_
 
-#include "src/properties/logic/PathRewardFormula.h"
+#include "src/properties/logic/OperatorFormula.h"
 
 namespace storm {
     namespace logic {
-        class RewardOperatorFormula : public Formula {
+        class RewardOperatorFormula : public OperatorFormula {
+        public:
+            RewardOperatorFormula(std::shared_ptr<Formula> const& subformula);
+            RewardOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
+            RewardOperatorFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            RewardOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
             
+            virtual ~RewardOperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isRewardOperator() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            RewardOperatorFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
         };
     }
 }

src/properties/logic/StateFormula.cpp

@@ -0,0 +1,9 @@
+#include "src/properties/logic/StateFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool StateFormula::isStateFormula() const {
+            return true;
+        }
+    }
+}

src/properties/logic/StateFormula.h

@@ -6,7 +6,12 @@
 namespace storm {
     namespace logic {
         class StateFormula : public Formula {
+        public:
+            virtual ~StateFormula() {
+                // Intentionally left empty.
+            };
             
+            virtual bool isStateFormula() const override;
         };
     }
 }

src/properties/logic/SteadyStateFormula.cpp

@@ -0,0 +1,35 @@
+#include "src/properties/logic/SteadyStateFormula.h"
+
+namespace storm {
+    namespace logic {
+        SteadyStateFormula::SteadyStateFormula(std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateFormula::SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        SteadyStateFormula::SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula) : SteadyStateFormula(boost::optional<ComparisonType>(), boost::optional<double>(), boost::optional<OptimalityType>(optimalityType), subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool SteadyStateFormula::isSteadyStateFormula() const {
+            return true;
+        }
+        
+        SteadyStateFormula::SteadyStateFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula) : OperatorFormula(comparisonType, bound, optimalityType, subformula) {
+            // Intentionally left empty.
+        }
+        
+        std::ostream& SteadyStateFormula::writeToStream(std::ostream& out) const {
+            out << "S";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/SteadyStateFormula.h

@@ -1,12 +1,27 @@
 #ifndef STORM_LOGIC_STEADYSTATEFORMULA_H_
 #define STORM_LOGIC_STEADYSTATEFORMULA_H_
 
-#include "src/properties/logic/UnaryStateFormula.h"
+#include "src/properties/logic/OperatorFormula.h"
 
 namespace storm {
     namespace logic {
-        class SteadyStateFormula : public UnaryStateFormula {
+        class SteadyStateFormula : public OperatorFormula {
+        public:
+            SteadyStateFormula(std::shared_ptr<Formula> const& subformula);
+            SteadyStateFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula> const& subformula);
+            SteadyStateFormula(ComparisonType comparisonType, double bound, OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
+            SteadyStateFormula(OptimalityType optimalityType, std::shared_ptr<Formula> const& subformula);
             
+            virtual ~SteadyStateFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isSteadyStateFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            SteadyStateFormula(boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, boost::optional<OptimalityType> optimalityType, std::shared_ptr<Formula> const& subformula);
         };
     }
 }

src/properties/logic/UnaryBooleanStateFormula.cpp

@@ -0,0 +1,9 @@
+#include "src/properties/logic/UnaryBooleanStateFormula.h"
+
+namespace storm {
+    namespace logic {
+        bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const {
+            return true;
+        }
+    }
+}

src/properties/logic/UnaryBooleanStateFormula.h

@@ -6,7 +6,12 @@
 namespace storm {
     namespace logic {
         class UnaryBooleanStateFormula : public UnaryStateFormula {
+        public:
+            virtual ~UnaryBooleanStateFormula() {
+                // Intentionally left empty.
+            };
             
+            virtual bool isUnaryBooleanStateFormula() const override;
         };
     }
 }

src/properties/logic/UnaryPathFormula.cpp

@@ -0,0 +1,21 @@
+#include "src/properties/logic/UnaryPathFormula.h"
+
+namespace storm {
+    namespace logic {
+        UnaryPathFormula::UnaryPathFormula(std::shared_ptr<Formula> const& subformula) : subformula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool UnaryPathFormula::isUnaryPathFormula() const {
+            return true;
+        }
+        
+        Formula& UnaryPathFormula::getSubformula() {
+            return *subformula;
+        }
+        
+        Formula const& UnaryPathFormula::getSubformula() const {
+            return *subformula;
+        }
+    }
+}

src/properties/logic/UnaryPathFormula.h

@@ -1,12 +1,27 @@
 #ifndef STORM_LOGIC_UNARYPATHFORMULA_H_
 #define STORM_LOGIC_UNARYPATHFORMULA_H_
 
+#include <memory>
+
 #include "src/properties/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
         class UnaryPathFormula : public PathFormula {
+        public:
+            UnaryPathFormula(std::shared_ptr<Formula> const& subformula);
+            
+            virtual ~UnaryPathFormula() {
+                // Intentionally left empty.
+            }
+
+            virtual bool isUnaryPathFormula() const override;
+            
+            Formula& getSubformula();
+            Formula const& getSubformula() const;
             
+        private:
+            std::shared_ptr<Formula> subformula;
         };
     }
 }

src/properties/logic/UnaryStateFormula.cpp

@@ -0,0 +1,21 @@
+#include "src/properties/logic/UnaryStateFormula.h"
+
+namespace storm {
+    namespace logic {
+        UnaryStateFormula::UnaryStateFormula(std::shared_ptr<Formula> subformula) : subformula(subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool UnaryStateFormula::isUnaryStateFormula() const {
+            return true;
+        }
+        
+        Formula& UnaryStateFormula::getSubformula() {
+            return *subformula;
+        }
+        
+        Formula const& UnaryStateFormula::getSubformula() const {
+            return *subformula;
+        }
+    }
+}

src/properties/logic/UnaryStateFormula.h

@@ -6,7 +6,20 @@
 namespace storm {
     namespace logic {
         class UnaryStateFormula : public StateFormula {
+        public:
+            UnaryStateFormula(std::shared_ptr<Formula> subformula);
             
+            virtual ~UnaryStateFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isUnaryStateFormula() const override;
+            
+            Formula& getSubformula();
+            Formula const& getSubformula() const;
+            
+        private:
+            std::shared_ptr<Formula> subformula;
         };
     }
 }

src/properties/logic/UntilFormula.cpp

@@ -0,0 +1,20 @@
+#include "src/properties/logic/UntilFormula.h"
+
+namespace storm {
+    namespace logic {
+        UntilFormula::UntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) {
+            // Intentionally left empty.
+        }
+        
+        bool UntilFormula::isUntilFormula() const {
+            return true;
+        }
+        
+        std::ostream& UntilFormula::writeToStream(std::ostream& out) const {
+            this->getLeftSubformula().writeToStream(out);
+            out << " U ";
+            this->getRightSubformula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/properties/logic/UntilFormula.h

@@ -6,7 +6,16 @@
 namespace storm {
     namespace logic {
         class UntilFormula : public BinaryPathFormula {
+        public:
+            UntilFormula(std::shared_ptr<Formula> const& leftSubformula, std::shared_ptr<Formula> const& rightSubformula);
             
+            virtual ~UntilFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isUntilFormula() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
 }

src/properties/ltl/AbstractLtlFormula.h

@@ -1,58 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_ABSTRACTLTLFORMULA_H_
-#define STORM_PROPERTIES_LTL_ABSTRACTLTLFORMULA_H_
-
-#include <vector>
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-#include "src/properties/AbstractFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			/*!
-			 * This is the abstract base class for all Ltl formulas.
-			 *
-			 * @note While formula classes do have copy constructors using a copy constructor
-			 *       will yield a formula objects whose formula subtree consists of the same objects
-			 *       as the original formula. The ownership of the formula tree will be shared between
-			 *       the original and the copy.
-			 */
-			template <class T>
-			class AbstractLtlFormula : public virtual storm::properties::AbstractFormula<T> {
-			public:
-
-				/*!
-				 * The virtual destructor.
-				 */
-				virtual ~AbstractLtlFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-				 *
-				 * @returns A deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const = 0;
-
-				/*!
-				 * 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 the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const = 0;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_ABSTRACTLTLFORMULA_H_ */

src/properties/ltl/And.h

@@ -1,207 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_AND_H_
-#define STORM_PROPERTIES_LTL_AND_H_
-
-#include "AbstractLtlFormula.h"
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-#include <string>
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class And;
-
-			/*!
-			 * Interface class for model checkers that support And.
-			 *
-			 * All model checkers that support the formula class And must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IAndModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IAndModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 *	@brief Evaluates And formula within a model checker.
-					 *
-					 *	@param obj Formula object with subformulas.
-					 *	@return Result of the formula for every node.
-					 */
-					virtual std::vector<T> checkAnd(And<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with And node as root.
-			 *
-			 * Has two Ltl formulas as sub formulas/trees.
-			 *
-			 * As And is commutative, the order is \e theoretically not important, but will influence the order in which
-			 * the model checker works.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class And : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an And node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				And() : left(nullptr), right(nullptr){
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an And node with the parameters as subtrees.
-				 *
-				 * @param left The left sub formula.
-				 * @param right The right sub formula.
-				 */
-				And(std::shared_ptr<AbstractLtlFormula<T>> left, std::shared_ptr<AbstractLtlFormula<T>> right) : left(left), right(right) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~And() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * 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 a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<And<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(right->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 std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "(";
-					result += left->toString();
-					result += " & ";
-					result += right->toString();
-					result += ")";
-					return result;
-				}
-
-				/*!
-				 * Returns whether the formula is a propositional logic formula.
-				 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 * @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return left->isPropositional() && right->isPropositional();
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractLtlFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractLtlFormula<T>> right;
-
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_AND_H_ */

src/properties/ltl/Ap.h

@@ -1,130 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_AP_H_
-#define STORM_PROPERTIES_LTL_AP_H_
-
-#include "AbstractLtlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Ap;
-
-			/*!
-			 * Interface class for model checkers that support Ap.
-			 *
-			 * All model checkers that support the formula class Ap must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IApModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IApModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates an Ap formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkAp(Ap<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with an atomic proposition as root.
-			 *
-			 * This class represents the leaves in the formula tree.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Ap: public storm::properties::ltl::AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a new atomic proposition leaf, with the given label.
-				 *
-				 * @param ap A string representing the atomic proposition.
-				 */
-				Ap(std::string ap) : ap(ap) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Ap() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * 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 Ap object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Ap<T>>(this->getAp());
-					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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IApModelChecker>()->checkAp(*this);
-				}
-
-				/*!
-				 * A string representing the atomic proposition.
-				 *
-				 * @returns A string representing the leaf.
-				 */
-				virtual std::string toString() const override {
-					return getAp();
-				}
-
-				/*!
-				 * Returns whether the formula is a propositional logic formula.
-				 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 * @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return true;
-				}
-
-				/*!
-				 * Gets the name of the atomic proposition.
-				 *
-				 * @returns The name of the atomic proposition.
-				 */
-				std::string const & getAp() const {
-					return ap;
-				}
-
-			private:
-
-				// The atomic proposition referenced by this leaf.
-				std::string ap;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_AP_H_ */

src/properties/ltl/BoundedEventually.h

@@ -1,189 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_BOUNDEDEVENTUALLY_H_
-#define STORM_PROPERTIES_LTL_BOUNDEDEVENTUALLY_H_
-
-#include "AbstractLtlFormula.h"
-#include <cstdint>
-#include <string>
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class BoundedEventually;
-
-			/*!
-			 * Interface class for model checkers that support BoundedEventually.
-			 *
-			 * All model checkers that support the formula class BoundedEventually must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IBoundedEventuallyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IBoundedEventuallyModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a BoundedEventually formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkBoundedEventually(BoundedEventually<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for a Ltl formula tree with a BoundedEventually node as root.
-			 *
-			 * Has one Ltl formula as subformula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff in at most \e bound steps, formula \e child holds.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class BoundedEventually : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a BoundedEventually node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				BoundedEventually() : child(nullptr), bound(0) {
-					//  Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a BoundedEventually node using the given parameters.
-				 *
-				 * @param child The child formula subtree.
-				 * @param bound The maximal number of steps within which the subformula must hold.
-				 */
-				BoundedEventually(std::shared_ptr<AbstractLtlFormula<T>> child, uint_fast64_t bound) : child(child), bound(bound) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~BoundedEventually() {
-					// Intentionally left empty.
-				}
-
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new BoundedEventually object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<BoundedEventually<T>>();
-					result->setBound(bound);
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "F<=";
-					result += std::to_string(bound);
-					result += " ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-				/*!
-				 * Gets the maximally allowed number of steps for the bounded eventually operator.
-				 *
-				 * @returns The bound.
-				 */
-				uint_fast64_t getBound() const {
-					return bound;
-				}
-
-				/*!
-				 * Sets the maximally allowed number of steps for the bounded eventually operator.
-				 *
-				 * @param bound The new bound.
-				 */
-				void setBound(uint_fast64_t bound) {
-					this->bound = bound;
-				}
-
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-
-				// The maximal number of steps within which the subformula must hold.
-				uint_fast64_t bound;
-
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_BOUNDEDUNTIL_H_ */

src/properties/ltl/BoundedUntil.h

@@ -1,222 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_BOUNDEDUNTIL_H_
-#define STORM_PROPERTIES_LTL_BOUNDEDUNTIL_H_
-
-#include "src/properties/ltl/AbstractLtlFormula.h"
-#include <cstdint>
-#include <string>
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class BoundedUntil;
-
-			/*!
-			 * Interface class for model checkers that support BoundedUntil.
-			 *
-			 * All model checkers that support the formula class BoundedUntil must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IBoundedUntilModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IBoundedUntilModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a BoundedUntil formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkBoundedUntil(BoundedUntil<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with a BoundedUntil node as root.
-			 *
-			 * Has two Ltl formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
-			 * \e left holds.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class BoundedUntil : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a BoundedUntil node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				BoundedUntil() : left(nullptr), right(nullptr), bound(0) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a BoundedUntil node using the given parameters.
-				 *
-				 * @param left The left formula subtree.
-				 * @param right The right formula subtree.
-				 * @param bound The maximal number of steps within which the right subformula must hold.
-				 */
-				BoundedUntil(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right, uint_fast64_t bound) : left(left), right(right), bound(bound) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~BoundedUntil() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new BoundedUntil object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<BoundedUntil<T>>();
-					result->setBound(bound);
-					if (this->isLeftSet()) {
-						result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-						result->setRight(right->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const {
-					return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "(" + left->toString();
-					result += " U<=";
-					result += std::to_string(bound);
-					result += " ";
-					result += right->toString() + ")";
-					return result;
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-				/*!
-				 * Gets the maximally allowed number of steps for the bounded until operator.
-				 *
-				 * @returns The bound.
-				 */
-				uint_fast64_t getBound() const {
-					return bound;
-				}
-
-				/*!
-				 * Sets the maximally allowed number of steps for the bounded until operator.
-				 *
-				 * @param bound The new bound.
-				 */
-				void setBound(uint_fast64_t bound) {
-					this->bound = bound;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractLtlFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractLtlFormula<T>> right;
-
-				// The maximal number of steps within which the subformulas must hold.
-				uint_fast64_t bound;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_BOUNDEDUNTIL_H_ */

src/properties/ltl/Eventually.h

@@ -1,158 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_EVENTUALLY_H_
-#define STORM_PROPERTIES_LTL_EVENTUALLY_H_
-
-#include "src/properties/ltl/AbstractLtlFormula.h"
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Eventually;
-
-			/*!
-			 * Interface class for model checkers that support Eventually.
-			 *
-			 * All model checkers that support the formula class Eventually must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IEventuallyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IEventuallyModelChecker() {
-						// Intentionally left empty.
-					}
-
-					/*!
-					 * Evaluates an Eventually formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkEventually(Eventually<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with an Eventually node as root.
-			 *
-			 * Has one Abstract Ltl formula as sub formula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff eventually \e child holds.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Eventually : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Eventually node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Eventually() : child(nullptr) {
-					//  Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Eventually node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Eventually(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Eventually() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Eventually object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Eventually<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
-					return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "F ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_EVENTUALLY_H_ */

src/properties/ltl/Globally.h

@@ -1,158 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_GLOBALLY_H_
-#define STORM_PROPERTIES_LTL_GLOBALLY_H_
-
-#include "AbstractLtlFormula.h"
-#include "src/modelchecker/ltl/ForwardDeclarations.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Globally;
-
-			/*!
-			 * Interface class for model checkers that support Globally.
-			 *
-			 * All model checkers that support the formula class Globally must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IGloballyModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IGloballyModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates a Globally formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkGlobally(Globally<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with a Globally node as root.
-			 *
-			 * Has one Ltl formula as sub formula/tree.
-			 *
-			 * @par Semantics
-			 * The formula holds iff always formula \e child holds.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Globally : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Globally node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Globally() : child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Globally node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Globally(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Globally() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Globally object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Globally<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
-					return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "G ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return *child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_GLOBALLY_H_ */

src/properties/ltl/LtlFilter.h

@@ -1,273 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_LTLFILTER_H_
-#define STORM_PROPERTIES_LTL_LTLFILTER_H_
-
-#include "src/properties/AbstractFilter.h"
-#include "src/modelchecker/ltl/AbstractModelChecker.h"
-#include "src/properties/ltl/AbstractLtlFormula.h"
-#include "src/properties/actions/AbstractAction.h"
-#include "src/exceptions/NotImplementedException.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			/*!
-			 * This is the Ltl specific filter.
-			 *
-			 * It maintains a Ltl formula which can be checked against a given model by either calling evaluate() or check().
-			 * Additionally it maintains a list of filter actions that are used to further manipulate the modelchecking results and prepare them for output.
-			 */
-			template <class T>
-			class LtlFilter : public storm::properties::AbstractFilter<T> {
-
-				// Convenience typedef to make the code more readable.
-				typedef typename storm::properties::action::AbstractAction<T>::Result Result;
-
-			public:
-
-				/*!
-				 * Creates an empty LtlFilter, maintaining no Ltl formula.
-				 *
-				 * Calling check or evaluate will return an empty result.
-				 */
-				LtlFilter() : AbstractFilter<T>(UNDEFINED), child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an LtlFilter maintaining an Ltl formula but containing no actions.
-				 *
-				 * The modelchecking result will be returned or printed as is.
-				 *
-				 * @param child The Ltl formula to be maintained.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 */
-				LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(opt), child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an LtlFilter maintaining a Ltl formula and containing a single action.
-				 *
-				 * The given action will be applied to the modelchecking result during evaluation.
-				 * Further actions can be added later.
-				 *
-				 * @param child The Ltl formula to be maintained.
-				 * @param action The single action to be executed during evaluation.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 */
-				LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an LtlFilter using the given parameters.
-				 *
-				 * The given actions will be applied to the modelchecking result in ascending index order during evaluation.
-				 * Further actions can be added later.
-				 *
-				 * @param child The Ltl formula to be maintained.
-				 * @param actions A vector conatining the actions that are to be executed during evaluation.
-				 * @param opt An enum value indicating which kind of scheduler shall be used for path formulas on nondeterministic models.
-				 */
-				LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~LtlFilter() {
-					// Intentionally left empty.
-				}
-
-
-				/*!
-				 * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and prints out the result.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 */
-				void check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
-
-					// Write out the formula to be checked.
-					std::cout << std::endl;
-					LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
-					std::cout << "Model checking formula:\t" << this->toString() << std::endl;
-
-					Result result;
-
-					try {
-						result = evaluate(modelchecker);
-					} catch (std::exception& e) {
-						std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
-						LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
-						std::cout << std::endl << "-------------------------------------------" << std::endl;
-
-						return;
-					}
-
-					writeOut(result, modelchecker);
-
-				}
-
-				/*!
-				 * Calls the modelchecker, retrieves the modelchecking result, applies the filter action one by one and returns the result.
-				 *
-				 * @param modelchecker The modelchecker to be called.
-				 * @returns The result of the sequential application of the filter actions to the modelchecking result.
-				 */
-				Result evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
-					// First, get the model checking result.
-					Result result;
-
-					if(this->opt != UNDEFINED) {
-						// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
-						LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.");
-						throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.";
-					} else {
-						result.pathResult = child->check(modelchecker);
-					}
-
-					// Now apply all filter actions and return the result.
-
-					// Init the state selection and state map vectors.
-					result.selection = storm::storage::BitVector(result.stateResult.size(), true);
-					result.stateMap = std::vector<uint_fast64_t>(result.selection.size());
-					for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
-						result.stateMap[i] = i;
-					}
-
-					// Now apply all filter actions and return the result.
-					for(auto action : this->actions) {
-						result = action->evaluate(result, modelchecker);
-					}
-
-					return result;
-				}
-
-				/*!
-				 * Returns a textual representation of the filter.
-				 *
-				 * That includes the actions as well as the maintained formula.
-				 *
-				 * @returns A string representing the filter.
-				 */
-				std::string toString() const override {
-					std::string desc = "";
-
-					if(this->actions.empty()){
-						// There are no filter actions but only the raw state formula. So just print that.
-						return child->toString();
-					}
-
-					desc = "filter[";
-
-					switch(this->opt) {
-						case MINIMIZE:
-							desc += "min; ";
-							break;
-						case MAXIMIZE:
-							desc += "max; ";
-							break;
-						default:
-							break;
-					}
-
-					for(auto action : this->actions) {
-						desc += action->toString();
-						desc += "; ";
-					}
-
-					// Remove the last "; ".
-					desc.pop_back();
-					desc.pop_back();
-
-					desc += "]";
-
-					desc += "(";
-					desc += child->toString();
-					desc += ")";
-
-					return desc;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				/*!
-				 * Writes out the given result.
-				 *
-				 * @param result The result of the sequential application of the filter actions to a modelchecking result.
-				 * @param modelchecker The modelchecker that was called to generate the modelchecking result. Needed for legacy support.
-				 */
-				void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
-
-					// Test for the kind of result. Values or states.
-					if(!result.pathResult.empty()) {
-
-						// Write out the selected value results in the order given by the stateMap.
-						if(this->actions.empty()) {
-
-							// There is no filter action given. So provide legacy support:
-							// Return the results for all states labeled with "init".
-							LOG4CPLUS_INFO(logger, "Result for initial states:");
-							std::cout << "Result for initial states:" << std::endl;
-							for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
-								LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result.pathResult[initialState]);
-								std::cout << "\t" << initialState << ": " << result.pathResult[initialState] << std::endl;
-							}
-						} else {
-							LOG4CPLUS_INFO(logger, "Result for " << result.selection.getNumberOfSetBits() << " selected states:");
-							std::cout << "Result for " << result.selection.getNumberOfSetBits() << " selected states:" << std::endl;
-
-							for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) {
-								if(result.selection.get(result.stateMap[i])) {
-									LOG4CPLUS_INFO(logger, "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]]);
-									std::cout << "\t" << result.stateMap[i] << ": " << result.pathResult[result.stateMap[i]] << std::endl;
-								}
-							}
-						}
-
-					} else {
-						LOG4CPLUS_WARN(logger, "No results could be computed.");
-						std::cout << "No results could be computed." << std::endl;
-					}
-
-					std::cout << std::endl << "-------------------------------------------" << std::endl;
-				}
-
-				// The Ltl formula maintained by this filter.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_LTLFILTER_H_ */

src/properties/ltl/Next.h

@@ -1,157 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_NEXT_H_
-#define STORM_PROPERTIES_LTL_NEXT_H_
-
-#include "AbstractLtlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Next;
-
-			/*!
-			 * Interface class for model checkers that support Next.
-			 *
-			 * All model checkers that support the formula class Next must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class INextModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~INextModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Next formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return Result of the formula for every node.
-					 */
-					virtual std::vector<T> checkNext(Next<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with a Next node as root.
-			 *
-			 * Has two LTL formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff in the next step, formula \e child holds
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Next : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Next node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Next() : child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Next node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Next(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Next() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Next object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Next<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const {
-					return modelChecker.template as<INextModelChecker>()->checkNext(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "X ";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_NEXT_H_ */

src/properties/ltl/Not.h

@@ -1,164 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_NOT_H_
-#define STORM_PROPERTIES_LTL_NOT_H_
-
-#include "AbstractLtlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Not;
-
-			/*!
-			 * Interface class for model checkers that support Not.
-			 *
-			 * All model checkers that support the formula class Not must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class INotModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~INotModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Not formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return Result of the formula for every node.
-					 */
-					virtual std::vector<T> checkNot(Not<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with a Not node as root.
-			 *
-			 * Has one Ltl formula as sub formula/tree.
-			 *
-			 * The object has shared ownership of its subtree. If this object is deleted and no other object has a shared
-			 * ownership of the subtree it will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Not : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates a Not node without a subnode.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Not() : child(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates a Not node using the given parameter.
-				 *
-				 * @param child The child formula subtree.
-				 */
-				Not(std::shared_ptr<AbstractLtlFormula<T>> const & child) : child(child) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Not() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Not object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Not<T>>();
-					if (this->isChildSet()) {
-						result->setChild(child->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 std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<INotModelChecker>()->checkNot(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "!";
-					result += child->toString();
-					return result;
-				}
-
-				/*!
-				 * Returns whether the formula is a propositional logic formula.
-				 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 * @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return child->isPropositional();
-				}
-
-				/*!
-				 * Gets the child node.
-				 *
-				 * @returns The child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getChild() const {
-					return child;
-				}
-
-				/*!
-				 * Sets the subtree.
-				 *
-				 * @param child The new child.
-				 */
-				void setChild(std::shared_ptr<AbstractLtlFormula<T>> const & child) {
-					this->child = child;
-				}
-
-				/*!
-				 * Checks if the child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the child is set.
-				 */
-				bool isChildSet() const {
-					return child.get() != nullptr;
-				}
-
-			private:
-
-				// The child node.
-				std::shared_ptr<AbstractLtlFormula<T>> child;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_NOT_H_ */

src/properties/ltl/Or.h

@@ -1,204 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_OR_H_
-#define STORM_PROPERTIES_LTL_OR_H_
-
-#include "AbstractLtlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Or;
-
-			/*!
-			 * Interface class for model checkers that support Or.
-			 *
-			 * All model checkers that support the formula class Or must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IOrModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IOrModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates Or formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return Result of the formula for every node.
-					 */
-					virtual std::vector<T> checkOr(Or<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an abstract formula tree with an Or node as root.
-			 *
-			 * Has two Ltl formulas as sub formulas/trees.
-			 *
-			 * As Or is commutative, the order is \e theoretically not important, but will influence the order in which
-			 * the model checker works.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Or: public storm::properties::ltl::AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Or node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Or() : left(nullptr), right(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Or node with the parameters as subtrees.
-				 *
-				 * @param left The left sub formula.
-				 * @param right The right sub formula.
-				 */
-				Or(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right) : left(left), right(right) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Or() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * 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 Or object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Or<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(right->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 std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const override {
-					return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const override {
-					std::string result = "(";
-					result += left->toString();
-					result += " | ";
-					result += right->toString();
-					result += ")";
-					return result;
-				}
-
-				/*!
-				 * Returns whether the formula is a propositional logic formula.
-				 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
-				 *
-				 * @return True iff this is a propositional logic formula.
-				 */
-				virtual bool isPropositional() const override {
-					return left->isPropositional() && right->isPropositional();
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left right is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractLtlFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractLtlFormula<T>> right;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_OR_H_ */

src/properties/ltl/Until.h

@@ -1,193 +0,0 @@
-#ifndef STORM_PROPERTIES_LTL_UNTIL_H_
-#define STORM_PROPERTIES_LTL_UNTIL_H_
-
-#include "AbstractLtlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace ltl {
-
-			// Forward declaration for the interface class.
-			template <class T> class Until;
-
-			/*!
-			 * Interface class for model checkers that support Until.
-			 *
-			 * All model checkers that support the formula class Until must inherit
-			 * this pure virtual class.
-			 */
-			template <class T>
-			class IUntilModelChecker {
-				public:
-
-					/*!
-					 * Empty virtual destructor.
-					 */
-					virtual ~IUntilModelChecker() {
-						// Intentionally left empty
-					}
-
-					/*!
-					 * Evaluates an Until formula within a model checker.
-					 *
-					 * @param obj Formula object with subformulas.
-					 * @return The modelchecking result of the formula for every state.
-					 */
-					virtual std::vector<T> checkUntil(Until<T> const & obj) const = 0;
-			};
-
-			/*!
-			 * Class for an Ltl formula tree with an Until node as root.
-			 *
-			 * Has two Ltl formulas as sub formulas/trees.
-			 *
-			 * @par Semantics
-			 * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
-			 * \e left holds always.
-			 *
-			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
-			 * ownership of the subtrees they will be deleted as well.
-			 *
-			 * @see AbstractLtlFormula
-			 */
-			template <class T>
-			class Until : public AbstractLtlFormula<T> {
-
-			public:
-
-				/*!
-				 * Creates an Until node without subnodes.
-				 * The resulting object will not represent a complete formula!
-				 */
-				Until() : left(nullptr), right(nullptr) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Creates an Until node using the given parameters.
-				 *
-				 * @param left The left formula subtree.
-				 * @param right The right formula subtree.
-				 */
-				Until(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right) : left(left), right(right) {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~Until() {
-					// Intentionally left empty.
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
-				 *
-				 * @returns A new Until object that is a deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
-					auto result = std::make_shared<Until<T>>();
-					if (this->isLeftSet()) {
-					  result->setLeft(left->clone());
-					}
-					if (this->isRightSet()) {
-					  result->setRight(right->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 vector indicating the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const {
-					return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
-				}
-
-				/*!
-				 * Returns a textual representation of the formula tree with this node as root.
-				 *
-				 * @returns A string representing the formula tree.
-				 */
-				virtual std::string toString() const {
-					std::string result = "(" + left->toString();
-					result += " U ";
-					result += right->toString() + ")";
-					return result;
-				}
-
-				/*!
-				 * Gets the left child node.
-				 *
-				 * @returns The left child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
-					return left;
-				}
-
-				/*!
-				 * Gets the right child node.
-				 *
-				 * @returns The right child node.
-				 */
-				std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
-					return right;
-				}
-
-				/*!
-				 * Sets the left child node.
-				 *
-				 * @param newLeft The new left child.
-				 */
-				void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
-					left = newLeft;
-				}
-
-				/*!
-				 * Sets the right child node.
-				 *
-				 * @param newRight The new right child.
-				 */
-				void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
-					right = newRight;
-				}
-
-				/*!
-				 * Checks if the left child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the left child is set.
-				 */
-				bool isLeftSet() const {
-					return left.get() != nullptr;
-				}
-
-				/*!
-				 * Checks if the right child is set, i.e. it does not point to null.
-				 *
-				 * @return True iff the right child is set.
-				 */
-				bool isRightSet() const {
-					return right.get() != nullptr;
-				}
-
-			private:
-
-				// The left child node.
-				std::shared_ptr<AbstractLtlFormula<T>> left;
-
-				// The right child node.
-				std::shared_ptr<AbstractLtlFormula<T>> right;
-			};
-
-		} // namespace ltl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_LTL_UNTIL_H_ */

src/properties/prctl/AbstractPathFormula.h

@@ -1,62 +0,0 @@
-#ifndef STORM_PROPERTIES_PRCTL_ABSTRACTPATHFORMULA_H_
-#define STORM_PROPERTIES_PRCTL_ABSTRACTPATHFORMULA_H_
-
-#include "src/properties/prctl/AbstractPrctlFormula.h"
-#include "src/modelchecker/prctl/ForwardDeclarations.h"
-
-#include <vector>
-#include <iostream>
-#include <typeinfo>
-
-namespace storm {
-	namespace properties {
-		namespace prctl {
-
-			/*!
-			 * Abstract base class for Prctl path formulas.
-			 *
-			 * @note Differing from the formal definitions of PRCTL a path formula may be the root of a PRCTL formula.
-			 *       The result of a modelchecking process on such a formula is a vector representing the satisfaction probabilities for each state of the model.
-			 */
-			template <class T>
-			class AbstractPathFormula : public virtual storm::properties::prctl::AbstractPrctlFormula<T> {
-
-			public:
-
-				/*!
-				 * The virtual destructor.
-				 */
-				virtual ~AbstractPathFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones.
-				 *
-				 * @note This function is not implemented in this class.
-				 *
-				 * @returns A deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractPathFormula<T>> clone() const = 0;
-
-				/*!
-				 * 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 the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelChecker, bool qualitative) const = 0;
-			};
-
-		} // namespace prctl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_PRCTL_ABSTRACTPATHFORMULA_H_ */

src/properties/prctl/AbstractPrctlFormula.h

@@ -1,75 +0,0 @@
-#ifndef STORM_PROPERTIES_PRCTL_ABSTRACTPRCTLFORMULA_H_
-#define STORM_PROPERTIES_PRCTL_ABSTRACTPRCTLFORMULA_H_
-
-#include "src/properties/AbstractFormula.h"
-
-
-namespace storm {
-	namespace properties {
-		namespace prctl {
-
-			// Forward declarations.
-			template <class T> class ProbabilisticBoundOperator;
-			template <class T> class Eventually;
-			template <class T> class Until;
-
-			/*!
-			 * This is the abstract base class for all Prctl formulas.
-			 *
-			 * @note While formula classes do have copy constructors using a copy constructor
-			 *       will yield a formula objects whose formula subtree consists of the same objects
-			 *       as the original formula. The ownership of the formula tree will be shared between
-			 *       the original and the copy.
-			 */
-			template<class T>
-			class AbstractPrctlFormula : public virtual storm::properties::AbstractFormula<T> {
-			public:
-
-				/*!
-				 * The virtual destructor.
-				 */
-				virtual ~AbstractPrctlFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Checks whether the formula is a probabilistic bound reachability formula.
-				 * Returns true iff the formula conforms to the following pattern.
-				 * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP).
-				 * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional
-				 * (denoting some set of atomic propositions).
-				 *
-				 * @return True iff this is a probabilistic bound reachability formula.
-				 */
-				bool isProbEventuallyAP() const {
-
-					// Test if a probabilistic bound operator is at the root.
-					if(dynamic_cast<storm::properties::prctl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
-						return false;
-					}
-
-					auto probFormula = dynamic_cast<storm::properties::prctl::ProbabilisticBoundOperator<T> const *>(this);
-
-					// Check if the direct subformula of the probabilistic bound operator is an eventually or until formula.
-					if(std::dynamic_pointer_cast<storm::properties::prctl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
-
-						// Get the subformula and check if its subformulas are propositional.
-						auto eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<T>>(probFormula->getChild());
-						return eventuallyFormula->getChild()->isPropositional();
-
-					} else if(std::dynamic_pointer_cast<storm::properties::prctl::Until<T>>(probFormula->getChild()).get() != nullptr) {
-
-						// Get the subformula and check if its subformulas are propositional.
-						auto untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<T>>(probFormula->getChild());
-						return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
-					}
-
-					return false;
-				}
-			};
-
-		} // namespace prctl
-	} // namespace properties
-} // namespace storm
-
-#endif /* STORM_PROPERTIES_PRCTL_ABSTRACTPRCTLFORMULA_H_ */

src/properties/prctl/AbstractRewardPathFormula.h

@@ -1,63 +0,0 @@
-#ifndef STORM_PROPERTIES_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
-#define STORM_PROPERTIES_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
-
-#include "src/properties/prctl/AbstractPrctlFormula.h"
-
-namespace storm {
-	namespace properties {
-		namespace prctl {
-
-			/*!
-			 * Abstract base class for Prctl reward path formulas.
-			 *
-			 * Reward path formulas may not be subformulas of a probabilitic bound operator, as they describe rewards along paths not probabilities.
-			 *
-			 * @note Differing from the formal definitions of PRCTL a reward path formula may be the root of a PRCTL formula.
-			 *       The result of a modelchecking process on such a formula is a vector representing the rewards for each state of the model.
-			 *
-			 * @see AbstractPrctlFormula
-			 */
-			template <class T>
-			class AbstractRewardPathFormula : public virtual storm::properties::prctl::AbstractPrctlFormula<T> {
-
-			public:
-
-				/*!
-				 * Empty virtual destructor.
-				 */
-				virtual ~AbstractRewardPathFormula() {
-					// Intentionally left empty
-				}
-
-				/*!
-				 * Clones the called object.
-				 *
-				 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
-				 *
-				 * @note This function is not implemented in this class.
-				 *
-				 * @returns A deep copy of the called object.
-				 */
-				virtual std::shared_ptr<AbstractRewardPathFormula<T>> clone() const = 0;
-
-				/*!
-				 * 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 the probability that the formula holds for each state.
-				 */
-				virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
-			};
-
-		} // namespace prctl
-	} // namespace properties
-} // namespace storm
-
-
-
-#endif /* STORM_PROPERTIES_PRCTL_ABSTRACTREWARDPATHFORMULA_H_ */