diff --git a/src/formula/Prctl.h b/src/formula/Prctl.h
index 5f12911ea..e174d445e 100644
--- a/src/formula/Prctl.h
+++ b/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"
diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h
index 1c0be2dd6..62bb1f7f4 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/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> {
diff --git a/src/formula/Prctl/AbstractRewardPathFormula.h b/src/formula/Prctl/AbstractRewardPathFormula.h
new file mode 100644
index 000000000..844adb25b
--- /dev/null
+++ b/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_ */
diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h
index a31f75a5d..baffaecd1 100644
--- a/src/formula/Prctl/CumulativeReward.h
+++ b/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());
}
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h
index 774d07e5e..cec958780 100644
--- a/src/formula/Prctl/InstantaneousReward.h
+++ b/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());
}
diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h
index f766a5942..d5559246b 100644
--- a/src/formula/Prctl/PrctlFilter.h
+++ b/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;
};
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h
index 0368b4ba9..5f88343da 100644
--- a/src/formula/Prctl/ReachabilityReward.h
+++ b/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());
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h
index 73dea7ab3..bf12d471d 100644
--- a/src/formula/Prctl/RewardBoundOperator.h
+++ b/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
diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h
index f850988fa..86624d876 100644
--- a/src/formula/Prctl/SteadyStateReward.h
+++ b/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>();
}
diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
index ed79fdace..fcaf0c2a9 100644
--- a/src/modelchecker/prctl/AbstractModelChecker.h
+++ b/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.
*
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 4be6ad1a3..82d0a3550 100644
--- a/src/parser/PrctlParser.cpp
+++ b/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;