Added the class AbstractRewardPathFormula to the PRCTL formula tree.

- This change splits the path formulas into probabilistic path formulas like Next or Until and reward path formulas like InstantaneousReward or SteadyStateReward.
|- That way it is assured at compile time that no reward path formula can ever be subformula of any probabilistic bound operator and vise versa.

Next up: Adopt changes in the Csl formula tree to the Csl parser.


Former-commit-id: d74c88bbf8

src/formula/Prctl.h

@@ -33,6 +33,7 @@
 #include "Prctl/AbstractPrctlFormula.h"
 #include "Prctl/AbstractStateFormula.h"
 #include "Prctl/AbstractPathFormula.h"
+#include "Prctl/AbstractRewardPathFormula.h"
 
 #include "modelchecker/prctl/AbstractModelChecker.h"
 

src/formula/Prctl/AbstractPathFormula.h

@@ -25,10 +25,11 @@ namespace prctl {
  *
  * @attention This class is abstract.
  * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
- * 	   clone().
+ * 	     the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
+ * 	      clone().
  *
- * @note This class is intentionally not derived from AbstractPrctlFormula, as path formulas are not complete PRCTL 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::property::prctl::AbstractPrctlFormula<T> {

src/formula/Prctl/AbstractRewardPathFormula.h

@@ -0,0 +1,62 @@
+/*
+ * AbstractRewardPathFormula.h
+ *
+ *  Created on: May 15, 2014
+ *      Author: Manuel S. Weiand
+ */
+
+#ifndef STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
+#define STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_
+
+namespace storm {
+namespace property {
+namespace prctl {
+
+/*! Base class for reward path formulas.
+ *
+ *  Reward path formulas are subformulas of reward bound operators.
+ *  They may not be subformulas of a probabilitic bound operator.
+ *
+ */
+template <class T>
+class AbstractRewardPathFormula : public virtual storm::property::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 new AND-object that is identical the called object.
+	 */
+	virtual 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 property
+} //namespace storm
+
+
+
+#endif /* STORM_FORMULA_PRCTL_ABSTRACTREWARDPATHFORMULA_H_ */

src/formula/Prctl/CumulativeReward.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_
 #define STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "AbstractRewardPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
@@ -48,7 +47,7 @@ class ICumulativeRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class CumulativeReward : public AbstractPathFormula<T> {
+class CumulativeReward : public AbstractRewardPathFormula<T> {
 
 public:
 	/*!
@@ -81,7 +80,7 @@ public:
 	 *
 	 * @returns a new CumulativeReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const override {
+	virtual AbstractRewardPathFormula<T>* clone() const override {
 		return new CumulativeReward(this->getBound());
 	}
 

src/formula/Prctl/InstantaneousReward.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_
 #define STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "AbstractRewardPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
@@ -49,7 +48,7 @@ class IInstantaneousRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class InstantaneousReward : public AbstractPathFormula<T> {
+class InstantaneousReward : public AbstractRewardPathFormula<T> {
 
 public:
 
@@ -83,7 +82,7 @@ public:
 	 *
 	 * @returns a new InstantaneousReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const override {
+	virtual AbstractRewardPathFormula<T>* clone() const override {
 		return new InstantaneousReward(this->getBound());
 	}
 

src/formula/Prctl/PrctlFilter.h

@@ -120,6 +120,38 @@ public:
 
 			std::cout << std::endl << "-------------------------------------------" << std::endl;
 
+		}
+		else if (dynamic_cast<AbstractRewardPathFormula<T>*>(child) != nullptr) {
+
+			// Check the formula and apply the filter actions.
+			std::vector<T> result;
+
+			try {
+				result = evaluate(modelchecker, static_cast<AbstractRewardPathFormula<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.");
+				std::cout << std::endl << "-------------------------------------------" << std::endl;
+
+				return;
+			}
+
+			// Now write out the result.
+
+			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.getModel().getInitialStates()) {
+					LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
+					std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
+				}
+			}
+
+			std::cout << std::endl << "-------------------------------------------" << std::endl;
+
 		}
 		else {
 			// This branch should be unreachable. If you ended up here, something strange has happened.
@@ -207,6 +239,24 @@ private:
 		return result;
 	}
 
+	std::vector<T> evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker, AbstractRewardPathFormula<T>* formula) const {
+		// First, get the model checking result.
+		std::vector<T> result;
+
+		if(this->getActionCount() != 0 &&  dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
+			// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
+			result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
+		} else {
+			result = formula->check(modelchecker, false);
+		}
+
+		// Now apply all filter actions and return the result.
+		for(auto action : this->actions) {
+			result = action->evaluate(result);
+		}
+		return result;
+	}
+
 	AbstractPrctlFormula<T>* child;
 };
 

src/formula/Prctl/ReachabilityReward.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_
 #define STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_
 
-#include "AbstractPathFormula.h"
+#include "AbstractRewardPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
@@ -49,7 +49,7 @@ class IReachabilityRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class ReachabilityReward : public AbstractPathFormula<T> {
+class ReachabilityReward : public AbstractRewardPathFormula<T> {
 
 public:
 	/*!
@@ -87,7 +87,7 @@ public:
 	 *
 	 * @returns a new ReachabilityReward-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const override {
+	virtual AbstractRewardPathFormula<T>* clone() const override {
 		ReachabilityReward<T>* result = new ReachabilityReward<T>();
 		if (this->childIsSet()) {
 			result->setChild(this->getChild().clone());

src/formula/Prctl/RewardBoundOperator.h

@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_
 #define STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_
 
-#include "AbstractPathFormula.h"
+#include "AbstractRewardPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "utility/constants.h"
 #include "src/formula/ComparisonType.h"
@@ -69,7 +69,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+	RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractRewardPathFormula<T>* pathFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
@@ -146,7 +146,7 @@ public:
 	/*!
 	 * @returns the child node (representation of a formula)
 	 */
-	const AbstractPathFormula<T>& getPathFormula () const {
+	const AbstractRewardPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
@@ -155,7 +155,7 @@ public:
 	 *
 	 * @param pathFormula the path formula that becomes the new child node
 	 */
-	void setPathFormula(AbstractPathFormula<T>* pathFormula) {
+	void setPathFormula(AbstractRewardPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -207,7 +207,7 @@ public:
 private:
 	storm::property::ComparisonType comparisonOperator;
 	T bound;
-	AbstractPathFormula<T>* pathFormula;
+	AbstractRewardPathFormula<T>* pathFormula;
 };
 
 } //namespace prctl

src/formula/Prctl/SteadyStateReward.h

@@ -8,8 +8,7 @@
 #ifndef STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_
 #define STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "AbstractRewardPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
@@ -45,7 +44,7 @@ class ISteadyStateRewardModelChecker {
  * @see AbstractPrctlFormula
  */
 template <class T>
-class SteadyStateReward: public AbstractPathFormula<T> {
+class SteadyStateReward: public AbstractRewardPathFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -65,7 +64,7 @@ public:
 	 *
 	 * @returns a new SteadyState-object that is identical the called object.
 	 */
-	virtual AbstractPathFormula<T>* clone() const override {
+	virtual AbstractRewardPathFormula<T>* clone() const override {
 		return new SteadyStateReward<T>();
 	}
 

src/modelchecker/prctl/AbstractModelChecker.h

@@ -230,11 +230,11 @@ public:
 	}
 
 	/*!
-	 * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula.
+	 * Checks the given formula and determines whether minimum or maximum probabilities are to be computed for the formula.
 	 *
 	 * @param formula The formula to check.
-	 * @param minimumOperator True iff minimum probabilities/rewards are to be computed.
-	 * @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector.
+	 * @param minimumOperator True iff minimum probabilities are to be computed.
+	 * @returns The probabilities to satisfy the formula, represented by a vector.
 	 */
 	virtual std::vector<Type> checkMinMaxOperator(storm::property::prctl::AbstractPathFormula<Type> const & formula, bool minimumOperator) const {
 		minimumOperatorStack.push(minimumOperator);
@@ -243,6 +243,20 @@ public:
 		return result;
 	}
 
+	/*!
+	 * Checks the given formula and determines whether minimum or maximum rewards are to be computed for the formula.
+	 *
+	 * @param formula The formula to check.
+	 * @param minimumOperator True iff minimum rewards are to be computed.
+	 * @returns The the rewards accumulated by the formula, represented by a vector.
+	 */
+	virtual std::vector<Type> checkMinMaxOperator(storm::property::prctl::AbstractRewardPathFormula<Type> const & formula, bool minimumOperator) const {
+		minimumOperatorStack.push(minimumOperator);
+		std::vector<Type> result = formula.check(*this, false);
+		minimumOperatorStack.pop();
+		return result;
+	}
+
 	/*!
 	 * Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula.
 	 *

src/parser/PrctlParser.cpp

@@ -201,7 +201,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 	qi::rule<Iterator, storm::property::prctl::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::property::prctl::AbstractStateFormula<double>>>, Skipper> boundedUntil;
 	qi::rule<Iterator, storm::property::prctl::Until<double>*(), qi::locals< std::shared_ptr<storm::property::prctl::AbstractStateFormula<double>>>, Skipper> until;
 
-	qi::rule<Iterator, storm::property::prctl::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;
+	qi::rule<Iterator, storm::property::prctl::AbstractRewardPathFormula<double>*(), Skipper> rewardPathFormula;
 	qi::rule<Iterator, storm::property::prctl::CumulativeReward<double>*(), Skipper> cumulativeReward;
 	qi::rule<Iterator, storm::property::prctl::ReachabilityReward<double>*(), Skipper> reachabilityReward;
 	qi::rule<Iterator, storm::property::prctl::InstantaneousReward<double>*(), Skipper> instantaneousReward;