From 11b16f5ddeed2e2796d797504e223a27bf2b1652 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 27 Dec 2012 17:47:25 +0100 Subject: [PATCH] Made bound/no-bound operators more consistent to reduce similar code. Changed bound operators to have a single bound and a comparison operator instead of an interval. --- CMakeLists.txt | 6 +- ...sticIntervalOperator.h => BoundOperator.h} | 104 +++++------ src/formula/Formulas.h | 8 +- ...icNoBoundsOperator.h => NoBoundOperator.h} | 46 +++-- src/formula/ProbabilisticBoundOperator.h | 96 ++++++++++ src/formula/ProbabilisticNoBoundOperator.h | 83 +++++++++ src/formula/RewardBoundOperator.h | 95 ++++++++++ src/formula/RewardIntervalOperator.h | 171 ------------------ ...undsOperator.h => RewardNoBoundOperator.h} | 55 ++---- src/modelChecker/DtmcPrctlModelChecker.h | 109 ++--------- src/storm.cpp | 18 +- 11 files changed, 398 insertions(+), 393 deletions(-) rename src/formula/{ProbabilisticIntervalOperator.h => BoundOperator.h} (60%) rename src/formula/{ProbabilisticNoBoundsOperator.h => NoBoundOperator.h} (63%) create mode 100644 src/formula/ProbabilisticBoundOperator.h create mode 100644 src/formula/ProbabilisticNoBoundOperator.h create mode 100644 src/formula/RewardBoundOperator.h delete mode 100644 src/formula/RewardIntervalOperator.h rename src/formula/{RewardNoBoundsOperator.h => RewardNoBoundOperator.h} (58%) diff --git a/CMakeLists.txt b/CMakeLists.txt index cd069197c..c4f2aec85 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -60,12 +60,13 @@ endif() if(CMAKE_COMPILER_IS_GNUCC) # Set standard flags for GCC + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic") # -Werror is atm removed as this gave some problems with existing code # May be re-set later # (Thomas Heinemann, 2012-12-21) - # Turn on popcnt instruction if possible (yes by default) + # Turn on popcnt instruction if desired (yes by default) if (USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") endif(USE_POPCNT) @@ -73,7 +74,8 @@ elseif(MSVC) # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) - # Set standard flags for GCC + # Set standard flags for clang + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/BoundOperator.h similarity index 60% rename from src/formula/ProbabilisticIntervalOperator.h rename to src/formula/BoundOperator.h index 175167292..0d0abedbd 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/BoundOperator.h @@ -1,12 +1,12 @@ /* - * ProbabilisticOperator.h + * BoundOperator.h * - * Created on: 19.10.2012 - * Author: Thomas Heinemann + * Created on: 27.12.2012 + * Author: Christian Dehnert */ -#ifndef STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ -#define STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ +#ifndef STORM_FORMULA_BOUNDOPERATOR_H_ +#define STORM_FORMULA_BOUNDOPERATOR_H_ #include "PctlStateFormula.h" #include "PctlPathFormula.h" @@ -38,17 +38,10 @@ namespace formula { * @see PctlFormula */ template -class ProbabilisticIntervalOperator : public PctlStateFormula { +class BoundOperator : public PctlStateFormula { public: - /*! - * Empty constructor - */ - ProbabilisticIntervalOperator() { - upper = storm::utility::constGetZero(); - lower = storm::utility::constGetZero(); - pathFormula = NULL; - } + enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; /*! * Constructor @@ -57,10 +50,9 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) { - this->lower = lowerBound; - this->upper = upperBound; - this->pathFormula = &pathFormula; + BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula* pathFormula) + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { + // Intentionally left empty } /*! @@ -69,8 +61,8 @@ public: * The subtree is deleted with the object * (this behavior can be prevented by setting them to NULL before deletion) */ - virtual ~ProbabilisticIntervalOperator() { - if (pathFormula != NULL) { + virtual ~BoundOperator() { + if (pathFormula != nullptr) { delete pathFormula; } } @@ -82,20 +74,6 @@ public: return *pathFormula; } - /*! - * @returns the lower bound for the probability - */ - const T& getLowerBound() const { - return lower; - } - - /*! - * @returns the upper bound for the probability - */ - const T& getUpperBound() const { - return upper; - } - /*! * Sets the child node * @@ -105,31 +83,50 @@ public: this->pathFormula = pathFormula; } + /*! + * @returns the bound for the measure + */ + const T& getBound() const { + return bound; + } + /*! * Sets the interval in which the probability that the path formula holds may lie in. * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param bound The bound for the measure */ - void setInterval(T lowerBound, T upperBound) { - this->lower = lowerBound; - this->upper = upperBound; + void setBound(T bound) { + this->bound = bound; } /*! * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "P["; - result += std::to_string(lower); - result += ";"; - result += std::to_string(upper); - result += "] ("; + 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 += std::to_string(bound); + result += " ["; result += pathFormula->toString(); - result += ")"; + result += "]"; return result; } + bool meetsBound(T value) { + 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; + } + } + /*! * Clones the called object. * @@ -137,14 +134,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { - ProbabilisticIntervalOperator* result = new ProbabilisticIntervalOperator(); - result->setInterval(lower, upper); - if (pathFormula != NULL) { - result->setPathFormula(pathFormula->clone()); - } - return result; - } + virtual PctlStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -156,12 +146,12 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkProbabilisticIntervalOperator(*this); + return modelChecker.checkBoundOperator(*this); } private: - T lower; - T upper; + ComparisonType comparisonOperator; + T bound; PctlPathFormula* pathFormula; }; @@ -169,4 +159,4 @@ private: } //namespace storm -#endif /* STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ */ +#endif /* STORM_FORMULA_BOUNDOPERATOR_H_ */ diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 2698985cd..70ed03c75 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -17,8 +17,8 @@ #include "PctlFormula.h" #include "PctlPathFormula.h" #include "PctlStateFormula.h" -#include "ProbabilisticNoBoundsOperator.h" -#include "ProbabilisticIntervalOperator.h" +#include "ProbabilisticNoBoundOperator.h" +#include "ProbabilisticBoundOperator.h" #include "Until.h" #include "Eventually.h" #include "Globally.h" @@ -27,7 +27,7 @@ #include "InstantaneousReward.h" #include "CumulativeReward.h" #include "ReachabilityReward.h" -#include "RewardIntervalOperator.h" -#include "RewardNoBoundsOperator.h" +#include "RewardBoundOperator.h" +#include "RewardNoBoundOperator.h" #endif /* STORM_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/NoBoundOperator.h similarity index 63% rename from src/formula/ProbabilisticNoBoundsOperator.h rename to src/formula/NoBoundOperator.h index 3f76cd9fd..204c102a8 100644 --- a/src/formula/ProbabilisticNoBoundsOperator.h +++ b/src/formula/NoBoundOperator.h @@ -1,17 +1,18 @@ /* - * ProbabilisticNoBoundsOperator.h + * NoBoundOperator.h * - * Created on: 12.12.2012 - * Author: thomas + * Created on: 27.12.2012 + * Author: Christian Dehnert */ -#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ -#define STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ +#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_ +#define STORM_FORMULA_NOBOUNDOPERATOR_H_ #include "PctlFormula.h" #include "PctlPathFormula.h" namespace storm { + namespace formula { /*! @@ -32,7 +33,7 @@ namespace formula { * This class does not contain a check() method like the other formula classes. * The check method should only be called by the model checker to infer the correct check function for sub * formulas. As this operator can only appear at the root, the method is not useful here. - * Use the checkProbabilisticNoBoundsOperator method from the DtmcPrctlModelChecker class instead. + * Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead. * * The subtree is seen as part of the object and deleted with it * (this behavior can be prevented by setting them to NULL before deletion) @@ -45,12 +46,12 @@ namespace formula { * @see PctlFormula */ template -class ProbabilisticNoBoundsOperator: public storm::formula::PctlFormula { +class NoBoundOperator: public storm::formula::PctlFormula { public: /*! * Empty constructor */ - ProbabilisticNoBoundsOperator() { + NoBoundOperator() { this->pathFormula = NULL; } @@ -59,14 +60,14 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundsOperator(PctlPathFormula* pathFormula) { + NoBoundOperator(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } /*! * Destructor */ - virtual ~ProbabilisticNoBoundsOperator() { + virtual ~NoBoundOperator() { if (pathFormula != NULL) { delete pathFormula; } @@ -89,20 +90,31 @@ public: } /*! - * @returns a string representation of the formula + * 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 all states that satisfy the formula represented by the called object. */ - virtual std::string toString() const { - std::string result = " P=? ("; - result += pathFormula->toString(); - result += ")"; - return result; + virtual std::vector* check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + return modelChecker.checkNoBoundOperator(*this); } + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const = 0; + private: PctlPathFormula* pathFormula; }; } /* namespace formula */ + } /* namespace storm */ -#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */ +#endif /* STORM_FORMULA_NOBOUNDOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h new file mode 100644 index 000000000..e541619c1 --- /dev/null +++ b/src/formula/ProbabilisticBoundOperator.h @@ -0,0 +1,96 @@ +/* + * ProbabilisticBoundOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ + +#include "PctlStateFormula.h" +#include "PctlPathFormula.h" +#include "BoundOperator.h" +#include "utility/ConstTemplates.h" + +namespace storm { + +namespace formula { + +/*! + * @brief + * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * Has one PCTL path formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the probability that the path formula holds is inside the bounds + * specified in this operator + * + * The subtree is seen as part of the object and deleted with it + * (this behavior can be prevented by setting them to NULL before deletion) + * + * + * @see PctlStateFormula + * @see PctlPathFormula + * @see ProbabilisticOperator + * @see ProbabilisticNoBoundsOperator + * @see PctlFormula + */ +template +class ProbabilisticBoundOperator : public BoundOperator { + +public: + /*! + * Empty constructor + */ + ProbabilisticBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + * @param pathFormula The child node + */ + ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "P ["; + result += std::to_string(this->getLowerBound()); + result += ","; + result += std::to_string(this->getUpperBound()); + result += "] ("; + result += this->getPathFormula()->toString(); + result += ")"; + return result; + } + + /*! + * 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 PctlStateFormula* clone() const { + ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); + result->setInterval(this->getLowerBound(), this->getUpperBound()); + result->setPathFormula(this->getPathFormula()->clone()); + return result; + } +}; + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h new file mode 100644 index 000000000..ad4ab4851 --- /dev/null +++ b/src/formula/ProbabilisticNoBoundOperator.h @@ -0,0 +1,83 @@ +/* + * ProbabilisticNoBoundOperator.h + * + * Created on: 12.12.2012 + * Author: thomas + */ + +#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ + +#include "PctlFormula.h" +#include "PctlPathFormula.h" +#include "NoBoundOperator.h" + +namespace storm { + +namespace formula { + +/*! + * @brief + * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities + * as root. + * + * Checking a formula with this operator as root returns the probabilities that the path formula holds + * (for each state) + * + * Has one PCTL path formula as sub formula/tree. + * + * @note + * This class is a hybrid of a state and path formula, and may only appear as the outermost operator. + * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula. + * + * @note + * This class does not contain a check() method like the other formula classes. + * The check method should only be called by the model checker to infer the correct check function for sub + * formulas. As this operator can only appear at the root, the method is not useful here. + * Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead. + * + * The subtree is seen as part of the object and deleted with it + * (this behavior can be prevented by setting them to NULL before deletion) + * + * + * @see PctlStateFormula + * @see PctlPathFormula + * @see ProbabilisticOperator + * @see ProbabilisticIntervalOperator + * @see PctlFormula + */ +template +class ProbabilisticNoBoundOperator: public NoBoundOperator { +public: + /*! + * Empty constructor + */ + ProbabilisticNoBoundOperator() : NoBoundOperator(nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(PctlPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = " P=? ["; + result += this->getPathFormula().toString(); + result += "]"; + return result; + } +}; + +} /* namespace formula */ + +} /* namespace storm */ + +#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h new file mode 100644 index 000000000..8118fdbe2 --- /dev/null +++ b/src/formula/RewardBoundOperator.h @@ -0,0 +1,95 @@ +/* + * RewardBoundOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_ +#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_ + +#include "PctlStateFormula.h" +#include "PctlPathFormula.h" +#include "BoundOperator.h" +#include "utility/ConstTemplates.h" + +namespace storm { + +namespace formula { + +/*! + * @brief + * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root. + * + * Has a reward path formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the reward of the reward path formula is inside the bounds + * specified in this operator + * + * The subtree is seen as part of the object and deleted with it + * (this behavior can be prevented by setting them to NULL before deletion) + * + * + * @see PctlStateFormula + * @see PctlPathFormula + * @see ProbabilisticOperator + * @see ProbabilisticNoBoundsOperator + * @see PctlFormula + */ +template +class RewardBoundOperator : public BoundOperator { + +public: + /*! + * Empty constructor + */ + RewardBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + * @param pathFormula The child node + */ + RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "R ["; + result += std::to_string(this->getLowerBound()); + result += ", "; + result += std::to_string(this->getUpperBound()); + result += "] ["; + result += this->getPathFormula()->toString(); + result += "]"; + return result; + } + + /*! + * 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 PctlStateFormula* clone() const { + RewardBoundOperator* result = new RewardBoundOperator(); + result->setBound(this->getLowerBound(), this->getUpperBound()); + result->setPathFormula(this->getPathFormula()->clone()); + return result; + } +}; + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */ diff --git a/src/formula/RewardIntervalOperator.h b/src/formula/RewardIntervalOperator.h deleted file mode 100644 index d18e3b7d9..000000000 --- a/src/formula/RewardIntervalOperator.h +++ /dev/null @@ -1,171 +0,0 @@ -/* - * ProbabilisticOperator.h - * - * Created on: 19.10.2012 - * Author: Thomas Heinemann - */ - -#ifndef STORM_FORMULA_REWARDINTERVALOPERATOR_H_ -#define STORM_FORMULA_REWARDINTERVALOPERATOR_H_ - -#include "PctlStateFormula.h" -#include "PctlPathFormula.h" -#include "utility/ConstTemplates.h" - -namespace storm { - -namespace formula { - -/*! - * @brief - * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root. - * - * Has a reward path formula as sub formula/tree. - * - * @par Semantics - * The formula holds iff the reward of the reward path formula is inside the bounds - * specified in this operator - * - * The subtree is seen as part of the object and deleted with it - * (this behavior can be prevented by setting them to NULL before deletion) - * - * - * @see PctlStateFormula - * @see PctlPathFormula - * @see ProbabilisticOperator - * @see ProbabilisticNoBoundsOperator - * @see PctlFormula - */ -template -class RewardIntervalOperator : public PctlStateFormula { - -public: - /*! - * Empty constructor - */ - RewardIntervalOperator() { - upper = storm::utility::constGetZero(); - lower = storm::utility::constGetZero(); - pathFormula = nullptr; - } - - /*! - * Constructor - * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability - * @param pathFormula The child node - */ - RewardIntervalOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) { - this->lower = lowerBound; - this->upper = upperBound; - this->pathFormula = &pathFormula; - } - - /*! - * Destructor - * - * The subtree is deleted with the object - * (this behavior can be prevented by setting them to NULL before deletion) - */ - virtual ~RewardIntervalOperator() { - if (pathFormula != nullptr) { - delete pathFormula; - } - } - - /*! - * @returns the child node (representation of a PCTL path formula) - */ - const PctlPathFormula& getPathFormula () const { - return *pathFormula; - } - - /*! - * @returns the lower bound for the probability - */ - const T& getLowerBound() const { - return lower; - } - - /*! - * @returns the upper bound for the probability - */ - const T& getUpperBound() const { - return upper; - } - - /*! - * Sets the child node - * - * @param pathFormula the path formula that becomes the new child node - */ - void setPathFormula(PctlPathFormula* pathFormula) { - this->pathFormula = pathFormula; - } - - /*! - * Sets the interval in which the probability that the path formula holds may lie in. - * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability - */ - void setInterval(T lowerBound, T upperBound) { - this->lower = lowerBound; - this->upper = upperBound; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "R ["; - result += std::to_string(lower); - result += ", "; - result += std::to_string(upper); - result += "] ["; - result += pathFormula->toString(); - result += "]"; - return result; - } - - /*! - * 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 PctlStateFormula* clone() const { - RewardIntervalOperator* result = new RewardIntervalOperator(); - result->setInterval(lower, upper); - if (pathFormula != nullptr) { - result->setPathFormula(pathFormula->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(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkRewardIntervalOperator(*this); - } - -private: - T lower; - T upper; - PctlPathFormula* pathFormula; -}; - -} //namespace formula - -} //namespace storm - -#endif /* STORM_FORMULA_REWARDINTERVALOPERATOR_H_ */ diff --git a/src/formula/RewardNoBoundsOperator.h b/src/formula/RewardNoBoundOperator.h similarity index 58% rename from src/formula/RewardNoBoundsOperator.h rename to src/formula/RewardNoBoundOperator.h index b1acd4acf..3362ff136 100644 --- a/src/formula/RewardNoBoundsOperator.h +++ b/src/formula/RewardNoBoundOperator.h @@ -1,15 +1,16 @@ /* - * RewardNoBoundsOperator.h + * RewardNoBoundOperator.h * - * Created on: 12.12.2012 - * Author: thomas + * Created on: 25.12.2012 + * Author: Christian Dehnert */ -#ifndef STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_ -#define STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_ +#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ #include "PctlFormula.h" #include "PctlPathFormula.h" +#include "NoBoundOperator.h" namespace storm { @@ -33,7 +34,7 @@ namespace formula { * This class does not contain a check() method like the other formula classes. * The check method should only be called by the model checker to infer the correct check function for sub * formulas. As this operator can only appear at the root, the method is not useful here. - * Use the checkRewardNoBoundsOperator method from the DtmcPrctlModelChecker class instead. + * Use the checkRewardNoBoundOperator method from the DtmcPrctlModelChecker class instead. * * The subtree is seen as part of the object and deleted with it * (this behavior can be prevented by setting them to NULL before deletion) @@ -46,13 +47,13 @@ namespace formula { * @see PctlFormula */ template -class RewardNoBoundsOperator: public storm::formula::PctlFormula { +class RewardNoBoundOperator: public NoBoundOperator { public: /*! * Empty constructor */ - RewardNoBoundsOperator() { - this->pathFormula = nullptr; + RewardNoBoundOperator() : NoBoundOperator(nullptr) { + // Intentionally left empty } /*! @@ -60,33 +61,8 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundsOperator(PctlPathFormula* pathFormula) { - this->pathFormula = pathFormula; - } - - /*! - * Destructor - */ - virtual ~RewardNoBoundsOperator() { - if (pathFormula != nullptr) { - delete pathFormula; - } - } - - /*! - * @returns the child node (representation of a PCTL path formula) - */ - const PctlPathFormula& getPathFormula () const { - return *pathFormula; - } - - /*! - * Sets the child node - * - * @param pathFormula the path formula that becomes the new child node - */ - void setPathFormula(PctlPathFormula* pathFormula) { - this->pathFormula = pathFormula; + RewardNoBoundOperator(PctlPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + // Intentionally left empty } /*! @@ -94,17 +70,14 @@ public: */ virtual std::string toString() const { std::string result = " R=? ["; - result += pathFormula->toString(); + result += this->getPathFormula().toString(); result += "]"; return result; } - -private: - PctlPathFormula* pathFormula; }; } /* namespace formula */ } /* namespace storm */ -#endif /* STORM_FORMULA_REWARDNOBOUNDSOPERATOR_H_ */ +#endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index c62cfa991..60a88adce 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -124,17 +124,17 @@ public: } /*! - * Checks the given probabilistic operator (with no bound) on the DTMC and prints the result - * (probability) for all initial states. - * @param probabilisticNoBoundsFormula The formula to be checked. + * Checks the given operator (with no bound) on the DTMC and prints the result + * (probability/rewards) for all initial states. + * @param probabilisticNoBoundFormula The formula to be checked. */ - void check(const storm::formula::ProbabilisticNoBoundsOperator& probabilisticNoBoundsFormula) const { + void check(const storm::formula::NoBoundOperator& noBoundFormula) const { std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << probabilisticNoBoundsFormula.toString()); - std::cout << "Model checking formula:\t" << probabilisticNoBoundsFormula.toString() << std::endl; + LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); + std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; std::vector* result = nullptr; try { - result = checkProbabilisticNoBoundsOperator(probabilisticNoBoundsFormula); + result = noBoundFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; for (auto initialState : *this->getModel().getLabeledStates("init")) { @@ -152,37 +152,6 @@ public: storm::utility::printSeparationLine(std::cout); } - /*! - * Checks the given reward operator (with no bound) on the DTMC and prints the result - * (reward values) for all initial states. - * @param rewardNoBoundsFormula The formula to be checked. - */ - void check(const storm::formula::RewardNoBoundsOperator& rewardNoBoundsFormula) { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << rewardNoBoundsFormula.toString()); - std::cout << "Model checking formula:\t" << rewardNoBoundsFormula.toString() << std::endl; - std::vector* result = nullptr; - try { - result = checkRewardNoBoundsOperator(rewardNoBoundsFormula); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : *this->getModel().getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); - std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - delete result; - } catch (std::exception& e) { - std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - } - /*! * The check method for a state formula; Will infer the actual type of formula and delegate it * to the specialized method @@ -255,60 +224,29 @@ public: } /*! - * The check method for a state formula with a probabilistic interval operator node as root in + * The check method for a state formula with a bound operator node as root in * its formula tree * * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - storm::storage::BitVector* checkProbabilisticIntervalOperator( - const storm::formula::ProbabilisticIntervalOperator& formula) const { + storm::storage::BitVector* checkBoundOperator(const storm::formula::BoundOperator& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. - std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); + std::vector* quantitativeResult = this->checkPathFormula(formula.getPathFormula()); // Create resulting bit vector, which will hold the yes/no-answer for every state. storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); - // Now, we can compute which states meet the bound specified in this operator, i.e. - // lie in the interval that was given along with this operator, and set the corresponding bits - // to true in the resulting vector. - Type lower = formula.getLowerBound(); - Type upper = formula.getUpperBound(); + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { - if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true); + if (formula.meetsBound((*quantitativeResult)[i])) { + result->set(i, true); + } } // Delete the probabilities computed for the states and return result. - delete probabilisticResult; - return result; - } - - /*! - * The check method for a state formula with a reward interval operator node as root in - * its formula tree - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkRewardIntervalOperator( - const storm::formula::RewardIntervalOperator& formula) const { - // First, we need to compute the probability for satisfying the path formula for each state. - std::vector* rewardResult = this->checkPathFormula(formula.getPathFormula()); - - // Create resulting bit vector, which will hold the yes/no-answer for every state. - storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); - - // Now, we can compute which states meet the bound specified in this operator, i.e. - // lie in the interval that was given along with this operator, and set the corresponding bits - // to true in the resulting vector. - Type lower = formula.getLowerBound(); - Type upper = formula.getUpperBound(); - for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { - if ((*rewardResult)[i] >= lower && (*rewardResult)[i] <= upper) result->set(i, true); - } - - // Delete the reward values computed for the states and return result. - delete rewardResult; + delete quantitativeResult; return result; } @@ -319,20 +257,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - std::vector* checkProbabilisticNoBoundsOperator( - const storm::formula::ProbabilisticNoBoundsOperator& formula) const { - return formula.getPathFormula().check(*this); - } - - /*! - * The check method for a state formula with a reward operator node without bounds as root - * in its formula tree - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - std::vector* checkRewardNoBoundsOperator( - const storm::formula::RewardNoBoundsOperator& formula) const { + std::vector* checkNoBoundOperator(const storm::formula::NoBoundOperator& formula) const { return formula.getPathFormula().check(*this); } diff --git a/src/storm.cpp b/src/storm.cpp index 5959bd537..0c5951961 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -141,11 +141,11 @@ void cleanUp() { void testCheckingDie(storm::models::Dtmc& dtmc) { storm::formula::Ap* oneFormula = new storm::formula::Ap("one"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(oneFormula); - storm::formula::ProbabilisticNoBoundsOperator* probFormula = new storm::formula::ProbabilisticNoBoundsOperator(eventuallyFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); storm::formula::Ap* done = new storm::formula::Ap("done"); storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(done); - storm::formula::RewardNoBoundsOperator* rewardFormula = new storm::formula::RewardNoBoundsOperator(reachabilityRewardFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); mc->check(*probFormula); @@ -159,7 +159,7 @@ void testCheckingDie(storm::models::Dtmc& dtmc) { void testCheckingCrowds(storm::models::Dtmc& dtmc) { storm::formula::Ap* observe0Greater1Formula = new storm::formula::Ap("observe0Greater1"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(observe0Greater1Formula); - storm::formula::ProbabilisticNoBoundsOperator* probFormula = new storm::formula::ProbabilisticNoBoundsOperator(eventuallyFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); mc->check(*probFormula); @@ -167,14 +167,14 @@ void testCheckingCrowds(storm::models::Dtmc& dtmc) { storm::formula::Ap* observeIGreater1Formula = new storm::formula::Ap("observeIGreater1"); eventuallyFormula = new storm::formula::Eventually(observeIGreater1Formula); - probFormula = new storm::formula::ProbabilisticNoBoundsOperator(eventuallyFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); mc->check(*probFormula); delete probFormula; storm::formula::Ap* observeOnlyTrueSenderFormula = new storm::formula::Ap("observeOnlyTrueSender"); eventuallyFormula = new storm::formula::Eventually(observeOnlyTrueSenderFormula); - probFormula = new storm::formula::ProbabilisticNoBoundsOperator(eventuallyFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); mc->check(*probFormula); delete probFormula; @@ -185,7 +185,7 @@ void testCheckingCrowds(storm::models::Dtmc& dtmc) { void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast64_t n) { storm::formula::Ap* electedFormula = new storm::formula::Ap("elected"); storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(electedFormula); - storm::formula::ProbabilisticNoBoundsOperator* probFormula = new storm::formula::ProbabilisticNoBoundsOperator(eventuallyFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); mc->check(*probFormula); @@ -193,7 +193,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 electedFormula = new storm::formula::Ap("elected"); storm::formula::BoundedUntil* boundedUntilFormula = new storm::formula::BoundedUntil(new storm::formula::Ap("true"), electedFormula, 1); - probFormula = new storm::formula::ProbabilisticNoBoundsOperator(boundedUntilFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedUntilFormula); for (uint_fast64_t L = 1; L < 5; ++L) { boundedUntilFormula->setBound(L*(n + 1)); @@ -203,7 +203,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 electedFormula = new storm::formula::Ap("elected"); storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(electedFormula); - storm::formula::RewardNoBoundsOperator* rewardFormula = new storm::formula::RewardNoBoundsOperator(reachabilityRewardFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); mc->check(*rewardFormula); delete rewardFormula; @@ -221,7 +221,7 @@ void testChecking() { dtmc->printModelInformationToStream(std::cout); - testCheckingDie(*dtmc); + // testCheckingDie(*dtmc); // testCheckingCrowds(*dtmc); // testCheckingSynchronousLeader(*dtmc, 4); }