New header file for all PRCTL formulas

src/formula/Formulas.h

@@ -1,45 +0,0 @@
-/*
- * Formulas.h
- *
- *  Created on: 06.12.2012
- *      Author: chris
- */
-
-#ifndef STORM_FORMULA_FORMULAS_H_
-#define STORM_FORMULA_FORMULAS_H_
-
-#include "modelchecker/ForwardDeclarations.h"
-
-#include "And.h"
-#include "Ap.h"
-#include "BoundedUntil.h"
-#include "BoundedNaryUntil.h"
-#include "Next.h"
-#include "Not.h"
-#include "Or.h"
-#include "ProbabilisticNoBoundOperator.h"
-#include "ProbabilisticBoundOperator.h"
-
-#include "Until.h"
-#include "Eventually.h"
-#include "Globally.h"
-#include "BoundedEventually.h"
-
-#include "InstantaneousReward.h"
-#include "CumulativeReward.h"
-#include "ReachabilityReward.h"
-#include "RewardBoundOperator.h"
-#include "RewardNoBoundOperator.h"
-#include "SteadyStateReward.h"
-
-#include "SteadyStateNoBoundOperator.h"
-#include "SteadyStateBoundOperator.h"
-
-#include "TimeBoundedUntil.h"
-#include "TimeBoundedEventually.h"
-
-#include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-
-#endif /* STORM_FORMULA_FORMULAS_H_ */

src/formula/Prctl.h

@@ -0,0 +1,46 @@
+/*
+ * Formulas.h
+ *
+ *  Created on: 06.12.2012
+ *      Author: chris
+ */
+
+#ifndef STORM_FORMULA_FORMULAS_H_
+#define STORM_FORMULA_FORMULAS_H_
+
+#include "modelchecker/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/ProbabilisticNoBoundOperator.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/RewardNoBoundOperator.h"
+#include "Prctl/SteadyStateReward.h"
+
+/*
+#include "SteadyStateNoBoundOperator.h"
+#include "SteadyStateBoundOperator.h"
+
+#include "TimeBoundedUntil.h"
+#include "TimeBoundedEventually.h"
+
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+*/
+#endif /* STORM_FORMULA_FORMULAS_H_ */

src/formula/Prctl/Ap.h

@@ -0,0 +1,105 @@
+/*
+ * Ap.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_PRCTL_AP_H_
+#define STORM_FORMULA_PRCTL_AP_H_
+
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Ap.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+namespace prctl {
+
+template <class T> class Ap;
+
+/*!
+ *  @brief 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:
+		/*!
+         *  @brief Evaluates Ap formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with atomic proposition as root.
+ *
+ * This class represents the leaves in the formula tree.
+ *
+ * @see AbstractFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class Ap : public storm::formula::abstract::Ap<T>, public AbstractFormula<T> {
+
+public:
+	/*!
+	 * Constructor
+	 *
+	 * Creates a new atomic proposition leaf, with the label Ap
+	 *
+	 * @param ap The string representing the atomic proposition
+	 */
+	Ap(std::string ap)
+		: storm::formula::abstract::Ap<T>(ap) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor.
+	 * At this time, empty...
+	 */
+	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 AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const {
+		return new Ap(getAp());
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
+	}
+
+};
+
+} //namespace abstract
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_PRCTL_AP_H_ */