From 08815b8c131554c4e097fa6580e03eac44693211 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 9 Apr 2013 11:44:57 +0200 Subject: [PATCH] Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement a "StateNoBoundOperator" now... --- ...oBoundOperator.h => PathNoBoundOperator.h} | 20 +++++++++---------- src/formula/ProbabilisticNoBoundOperator.h | 12 +++++------ src/formula/RewardNoBoundOperator.h | 12 +++++------ src/modelchecker/AbstractModelChecker.h | 4 ++-- .../SparseDtmcPrctlModelChecker.h | 2 +- src/modelchecker/SparseMdpPrctlModelChecker.h | 2 +- src/parser/CslParser.cpp | 6 +++--- src/parser/PrctlFileParser.cpp | 2 +- src/parser/PrctlParser.cpp | 6 +++--- 9 files changed, 33 insertions(+), 33 deletions(-) rename src/formula/{NoBoundOperator.h => PathNoBoundOperator.h} (88%) diff --git a/src/formula/NoBoundOperator.h b/src/formula/PathNoBoundOperator.h similarity index 88% rename from src/formula/NoBoundOperator.h rename to src/formula/PathNoBoundOperator.h index cbbc9f05f..9c3668a23 100644 --- a/src/formula/NoBoundOperator.h +++ b/src/formula/PathNoBoundOperator.h @@ -1,5 +1,5 @@ /* - * NoBoundOperator.h + * PathNoBoundOperator.h * * Created on: 27.12.2012 * Author: Christian Dehnert @@ -19,7 +19,7 @@ namespace storm { namespace formula { -template class NoBoundOperator; +template class PathNoBoundOperator; /*! * @brief Interface class for model checkers that support NoBoundOperator. @@ -28,7 +28,7 @@ template class NoBoundOperator; * this pure virtual class. */ template -class INoBoundOperatorModelChecker { +class IPathNoBoundOperatorModelChecker { public: /*! * @brief Evaluates NoBoundOperator formula within a model checker. @@ -36,7 +36,7 @@ class INoBoundOperatorModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual std::vector* checkNoBoundOperator(const NoBoundOperator& obj) const = 0; + virtual std::vector* checkPathNoBoundOperator(const PathNoBoundOperator& obj) const = 0; }; /*! @@ -70,12 +70,12 @@ class INoBoundOperatorModelChecker { * @see AbstractFormula */ template -class NoBoundOperator: public storm::formula::AbstractFormula, public OptimizingOperator { +class PathNoBoundOperator: public storm::formula::AbstractFormula, public OptimizingOperator { public: /*! * Empty constructor */ - NoBoundOperator() : optimalityOperator(false), minimumOperator(false) { + PathNoBoundOperator() : optimalityOperator(false), minimumOperator(false) { this->pathFormula = nullptr; } @@ -84,7 +84,7 @@ public: * * @param pathFormula The child node. */ - NoBoundOperator(AbstractPathFormula* pathFormula) : optimalityOperator(false), minimumOperator(false) { + PathNoBoundOperator(AbstractPathFormula* pathFormula) : optimalityOperator(false), minimumOperator(false) { this->pathFormula = pathFormula; } @@ -95,7 +95,7 @@ public: * @param minimumOperator A flag indicating whether this operator is a minimizing or a * maximizing operator. */ - NoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) + PathNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) { this->pathFormula = pathFormula; } @@ -103,7 +103,7 @@ public: /*! * Destructor */ - virtual ~NoBoundOperator() { + virtual ~PathNoBoundOperator() { if (pathFormula != NULL) { delete pathFormula; } @@ -137,7 +137,7 @@ public: * @returns A vector indicating all states that satisfy the formula represented by the called object. */ virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkNoBoundOperator(*this); + return modelChecker.template as()->checkPathNoBoundOperator(*this); } /*! diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h index fcfaeebe1..66843d965 100644 --- a/src/formula/ProbabilisticNoBoundOperator.h +++ b/src/formula/ProbabilisticNoBoundOperator.h @@ -10,7 +10,7 @@ #include "AbstractFormula.h" #include "AbstractPathFormula.h" -#include "NoBoundOperator.h" +#include "PathNoBoundOperator.h" namespace storm { namespace formula { @@ -46,12 +46,12 @@ namespace formula { * @see AbstractFormula */ template -class ProbabilisticNoBoundOperator: public NoBoundOperator { +class ProbabilisticNoBoundOperator: public PathNoBoundOperator { public: /*! * Empty constructor */ - ProbabilisticNoBoundOperator() : NoBoundOperator(nullptr) { + ProbabilisticNoBoundOperator() : PathNoBoundOperator(nullptr) { // Intentionally left empty } @@ -60,7 +60,7 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : PathNoBoundOperator(pathFormula) { // Intentionally left empty } @@ -69,7 +69,7 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : NoBoundOperator(pathFormula, minimumOperator) { + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : PathNoBoundOperator(pathFormula, minimumOperator) { // Intentionally left empty } @@ -78,7 +78,7 @@ public: */ virtual std::string toString() const { std::string result = "P"; - result += NoBoundOperator::toString(); + result += PathNoBoundOperator::toString(); return result; } }; diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h index 0e935aba8..8bb0b7f66 100644 --- a/src/formula/RewardNoBoundOperator.h +++ b/src/formula/RewardNoBoundOperator.h @@ -10,7 +10,7 @@ #include "AbstractFormula.h" #include "AbstractPathFormula.h" -#include "NoBoundOperator.h" +#include "PathNoBoundOperator.h" namespace storm { namespace formula { @@ -46,12 +46,12 @@ namespace formula { * @see AbstractFormula */ template -class RewardNoBoundOperator: public NoBoundOperator { +class RewardNoBoundOperator: public PathNoBoundOperator { public: /*! * Empty constructor */ - RewardNoBoundOperator() : NoBoundOperator(nullptr) { + RewardNoBoundOperator() : PathNoBoundOperator(nullptr) { // Intentionally left empty } @@ -60,7 +60,7 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + RewardNoBoundOperator(AbstractPathFormula* pathFormula) : PathNoBoundOperator(pathFormula) { // Intentionally left empty } @@ -69,7 +69,7 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : NoBoundOperator(pathFormula, minimumOperator) { + RewardNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : PathNoBoundOperator(pathFormula, minimumOperator) { // Intentionally left empty } @@ -78,7 +78,7 @@ public: */ virtual std::string toString() const { std::string result = "R"; - result += NoBoundOperator::toString(); + result += PathNoBoundOperator::toString(); return result; } }; diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index de32619f7..1767e715b 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -52,7 +52,7 @@ class AbstractModelChecker : public virtual storm::formula::INextModelChecker, public virtual storm::formula::IBoundedUntilModelChecker, public virtual storm::formula::IBoundedEventuallyModelChecker, - public virtual storm::formula::INoBoundOperatorModelChecker, + public virtual storm::formula::IPathNoBoundOperatorModelChecker, public virtual storm::formula::IProbabilisticBoundOperatorModelChecker, public virtual storm::formula::IRewardBoundOperatorModelChecker, public virtual storm::formula::IReachabilityRewardModelChecker, @@ -154,7 +154,7 @@ public: * * @param noBoundFormula The formula to be checked. */ - void check(storm::formula::NoBoundOperator const& noBoundFormula) const { + void check(storm::formula::PathNoBoundOperator const& noBoundFormula) const { std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index 4bcf4708a..d8e8c42f9 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -64,7 +64,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - std::vector* checkNoBoundOperator(storm::formula::NoBoundOperator const& formula) const { + std::vector* checkPathNoBoundOperator(storm::formula::PathNoBoundOperator const& formula) const { // Check if the operator was an optimality operator and report a warning in that case. if (formula.isOptimalityOperator()) { LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index df9d21d8c..999020ff8 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -66,7 +66,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - std::vector* checkNoBoundOperator(const storm::formula::NoBoundOperator& formula) const { + std::vector* checkPathNoBoundOperator(const storm::formula::PathNoBoundOperator& formula) const { // Check if the operator was an non-optimality operator and report an error in that case. if (!formula.isOptimalityOperator()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 3a6c3d5d7..cd7efc53d 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -148,9 +148,9 @@ struct CslParser::CslGrammar : qi::grammar*(), Skipper> steadyStateBoundOperator; qi::rule*(), Skipper> rewardBoundOperator; - qi::rule*(), Skipper> noBoundOperator; - qi::rule*(), Skipper> probabilisticNoBoundOperator; - qi::rule*(), Skipper> rewardNoBoundOperator; + qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> rewardNoBoundOperator; qi::rule*(), Skipper> pathFormula; qi::rule*(), Skipper> boundedEventually; diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 90721ee8f..ad72486e9 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -67,7 +67,7 @@ void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractM if (stateFormula != nullptr) { modelChecker->check(*stateFormula); } - storm::formula::NoBoundOperator* noBoundFormula = dynamic_cast*>(parser.getFormula()); + storm::formula::PathNoBoundOperator* noBoundFormula = dynamic_cast*>(parser.getFormula()); if (noBoundFormula != nullptr) { modelChecker->check(*noBoundFormula); } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index e50facb0e..f64575a6a 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -140,9 +140,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> probabilisticBoundOperator; qi::rule*(), Skipper> rewardBoundOperator; - qi::rule*(), Skipper> noBoundOperator; - qi::rule*(), Skipper> probabilisticNoBoundOperator; - qi::rule*(), Skipper> rewardNoBoundOperator; + qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> rewardNoBoundOperator; qi::rule*(), Skipper> pathFormula; qi::rule*(), Skipper> boundedEventually;