diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 18a156e08..e265f70c5 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -227,10 +227,8 @@ namespace storm { // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { - if (formula.containsRewardOperator()) { - std::set referencedRewardModels = formula.getReferencedRewardModels(); - rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); - } + std::set referencedRewardModels = formula.getReferencedRewardModels(); + rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); } // Extract all the labels used in the formula. diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index d345d9f05..d7c2f6293 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -185,10 +185,8 @@ namespace storm { // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { - if (formula.containsRewardOperator()) { - std::set referencedRewardModels = formula.getReferencedRewardModels(); - rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); - } + std::set referencedRewardModels = formula.getReferencedRewardModels(); + rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); } // Extract all the labels used in the formula. diff --git a/src/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp index 35c7149b0..5f8f0f509 100644 --- a/src/logic/AtomicExpressionFormula.cpp +++ b/src/logic/AtomicExpressionFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/AtomicExpressionFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { AtomicExpressionFormula::AtomicExpressionFormula(storm::expressions::Expression const& expression) : expression(expression) { @@ -10,22 +12,10 @@ namespace storm { return true; } - bool AtomicExpressionFormula::isPctlStateFormula() const { - return true; + boost::any AtomicExpressionFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } - bool AtomicExpressionFormula::isPctlWithConditionalStateFormula() const { - return true; - } - - bool AtomicExpressionFormula::isLtlFormula() const { - return true; - } - - bool AtomicExpressionFormula::isPropositionalFormula() const { - return true; - } - storm::expressions::Expression const& AtomicExpressionFormula::getExpression() const { return expression; } diff --git a/src/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h index 2b2e36dd5..12636475d 100644 --- a/src/logic/AtomicExpressionFormula.h +++ b/src/logic/AtomicExpressionFormula.h @@ -15,10 +15,7 @@ namespace storm { virtual bool isAtomicExpressionFormula() const override; - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool isPropositionalFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; storm::expressions::Expression const& getExpression() const; diff --git a/src/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp index 36c00eb23..19a5f673f 100644 --- a/src/logic/AtomicLabelFormula.cpp +++ b/src/logic/AtomicLabelFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/AtomicLabelFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { AtomicLabelFormula::AtomicLabelFormula(std::string const& label) : label(label) { @@ -10,20 +12,8 @@ namespace storm { return true; } - bool AtomicLabelFormula::isPctlStateFormula() const { - return true; - } - - bool AtomicLabelFormula::isPctlWithConditionalStateFormula() const { - return true; - } - - bool AtomicLabelFormula::isLtlFormula() const { - return true; - } - - bool AtomicLabelFormula::isPropositionalFormula() const { - return true; + boost::any AtomicLabelFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::string const& AtomicLabelFormula::getLabel() const { diff --git a/src/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h index 3d326c211..795704305 100644 --- a/src/logic/AtomicLabelFormula.h +++ b/src/logic/AtomicLabelFormula.h @@ -17,10 +17,7 @@ namespace storm { virtual bool isAtomicLabelFormula() const override; - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool isPropositionalFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; std::string const& getLabel() const; diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp index 521869129..180ea12c1 100644 --- a/src/logic/BinaryBooleanStateFormula.cpp +++ b/src/logic/BinaryBooleanStateFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/BinaryBooleanStateFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) { @@ -10,8 +12,8 @@ namespace storm { return true; } - bool BinaryBooleanStateFormula::isPropositionalFormula() const { - return this->getLeftSubformula().isPropositionalFormula() && this->getRightSubformula().isPropositionalFormula(); + boost::any BinaryBooleanStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } BinaryBooleanStateFormula::OperatorType BinaryBooleanStateFormula::getOperator() const { diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h index 23a330ae0..6956e56c6 100644 --- a/src/logic/BinaryBooleanStateFormula.h +++ b/src/logic/BinaryBooleanStateFormula.h @@ -19,7 +19,7 @@ namespace storm { virtual bool isBinaryBooleanStateFormula() const override; - virtual bool isPropositionalFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; OperatorType getOperator() const; diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index 5075894c4..4e028d567 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -9,47 +9,7 @@ namespace storm { bool BinaryPathFormula::isBinaryPathFormula() const { return true; } - - bool BinaryPathFormula::isPctlPathFormula() const { - return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); - } - - bool BinaryPathFormula::isPctlWithConditionalPathFormula() const { - return this->getLeftSubformula().isPctlWithConditionalPathFormula() && this->getRightSubformula().isPctlWithConditionalPathFormula(); - } - - bool BinaryPathFormula::isCslPathFormula() const { - return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); - } - - bool BinaryPathFormula::isLtlFormula() const { - return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula(); - } - - bool BinaryPathFormula::containsBoundedUntilFormula() const { - return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula(); - } - - bool BinaryPathFormula::containsNextFormula() const { - return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula(); - } - - bool BinaryPathFormula::containsProbabilityOperator() const { - return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator(); - } - - bool BinaryPathFormula::containsNestedProbabilityOperators() const { - return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators(); - } - - bool BinaryPathFormula::containsRewardOperator() const { - return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator(); - } - - bool BinaryPathFormula::containsNestedRewardOperators() const { - return this->getLeftSubformula().containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators(); - } - + Formula const& BinaryPathFormula::getLeftSubformula() const { return *leftSubformula; } diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index 14d162926..fe0526bee 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -17,17 +17,6 @@ namespace storm { virtual bool isBinaryPathFormula() const override; - virtual bool isPctlPathFormula() const override; - virtual bool isPctlWithConditionalPathFormula() const override; - virtual bool isCslPathFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool containsBoundedUntilFormula() const override; - virtual bool containsNextFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; - virtual bool containsRewardOperator() const override; - virtual bool containsNestedRewardOperators() const override; - Formula const& getLeftSubformula() const; Formula const& getRightSubformula() const; diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index bcaa2d39b..9fcdad992 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -9,47 +9,7 @@ namespace storm { bool BinaryStateFormula::isBinaryStateFormula() const { return true; } - - bool BinaryStateFormula::isPctlStateFormula() const { - return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); - } - - bool BinaryStateFormula::isPctlWithConditionalStateFormula() const { - return this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula(); - } - - bool BinaryStateFormula::isCslStateFormula() const { - return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); - } - - bool BinaryStateFormula::isLtlFormula() const { - return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula(); - } - - bool BinaryStateFormula::containsBoundedUntilFormula() const { - return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula(); - } - - bool BinaryStateFormula::containsNextFormula() const { - return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula(); - } - - bool BinaryStateFormula::containsProbabilityOperator() const { - return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator(); - } - - bool BinaryStateFormula::containsNestedProbabilityOperators() const { - return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators(); - } - - bool BinaryStateFormula::containsRewardOperator() const { - return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator(); - } - - bool BinaryStateFormula::containsNestedRewardOperators() const { - return this->containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators(); - } - + Formula const& BinaryStateFormula::getLeftSubformula() const { return *leftSubformula; } diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index c259aa759..3820097ca 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -15,17 +15,6 @@ namespace storm { virtual bool isBinaryStateFormula() const override; - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isCslStateFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool containsBoundedUntilFormula() const override; - virtual bool containsNextFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; - virtual bool containsRewardOperator() const override; - virtual bool containsNestedRewardOperators() const override; - Formula const& getLeftSubformula() const; Formula const& getRightSubformula() const; diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp index d021bbc64..897fbf377 100644 --- a/src/logic/BooleanLiteralFormula.cpp +++ b/src/logic/BooleanLiteralFormula.cpp @@ -1,11 +1,17 @@ #include "src/logic/BooleanLiteralFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { BooleanLiteralFormula::BooleanLiteralFormula(bool value) : value(value) { // Intenionally left empty. } + bool BooleanLiteralFormula::isBooleanLiteralFormula() const { + return true; + } + bool BooleanLiteralFormula::isTrueFormula() const { return value; } @@ -14,24 +20,8 @@ namespace storm { return !value; } - bool BooleanLiteralFormula::isPctlStateFormula() const { - return true; - } - - bool BooleanLiteralFormula::isPctlWithConditionalStateFormula() const { - return true; - } - - bool BooleanLiteralFormula::isLtlFormula() const { - return true; - } - - bool BooleanLiteralFormula::isPropositionalFormula() const { - return true; - } - - bool BooleanLiteralFormula::isBooleanLiteralFormula() const { - return true; + boost::any BooleanLiteralFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::shared_ptr BooleanLiteralFormula::substitute(std::map const& substitution) const { diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h index 1283fde71..405044600 100644 --- a/src/logic/BooleanLiteralFormula.h +++ b/src/logic/BooleanLiteralFormula.h @@ -16,11 +16,8 @@ namespace storm { virtual bool isBooleanLiteralFormula() const override; virtual bool isTrueFormula() const override; virtual bool isFalseFormula() const override; - - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool isPropositionalFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp index 9a1f867e1..8f3e73286 100644 --- a/src/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -3,6 +3,8 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) { @@ -22,30 +24,18 @@ namespace storm { return true; } - bool BoundedUntilFormula::containsBoundedUntilFormula() const { + bool BoundedUntilFormula::isProbabilityPathFormula() const { return true; } + boost::any BoundedUntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + bool BoundedUntilFormula::hasDiscreteTimeBound() const { return bounds.which() == 0; } - - bool BoundedUntilFormula::isValidProbabilityPathFormula() const { - return true; - } - - bool BoundedUntilFormula::isPctlPathFormula() const { - return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula(); - } - - bool BoundedUntilFormula::isPctlWithConditionalPathFormula() const { - return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula(); - } - - bool BoundedUntilFormula::isCslPathFormula() const { - return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula(); - } - + std::pair const& BoundedUntilFormula::getIntervalBounds() const { return boost::get>(bounds); } diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h index bc14d8def..222bab142 100644 --- a/src/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -15,17 +15,14 @@ namespace storm { virtual bool isBoundedUntilFormula() const override; - virtual bool containsBoundedUntilFormula() const override; + virtual bool isProbabilityPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; bool hasDiscreteTimeBound() const; std::pair const& getIntervalBounds() const; uint_fast64_t getDiscreteTimeBound() const; - - virtual bool isValidProbabilityPathFormula() const override; - virtual bool isPctlWithConditionalPathFormula() const override; - virtual bool isPctlPathFormula() const override; - virtual bool isCslPathFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/ConditionalFormula.cpp b/src/logic/ConditionalFormula.cpp new file mode 100644 index 000000000..2b63fd941 --- /dev/null +++ b/src/logic/ConditionalFormula.cpp @@ -0,0 +1,42 @@ +#include "src/logic/ConditionalFormula.h" + +#include "src/logic/FormulaVisitor.h" + +namespace storm { + namespace logic { + ConditionalFormula::ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, Context context) : subformula(subformula), conditionFormula(conditionFormula), context(context) { + // Intentionally left empty. + } + + Formula const& ConditionalFormula::getSubformula() const { + return *subformula; + } + + Formula const& ConditionalFormula::getConditionFormula() const { + return *conditionFormula; + } + + bool ConditionalFormula::isConditionalProbabilityFormula() const { + return context == Context::Probability; + } + + bool ConditionalFormula::isConditionalRewardFormula() const { + return context == Context::Reward; + } + + boost::any ConditionalFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + std::shared_ptr ConditionalFormula::substitute(std::map const& substitution) const { + return std::make_shared(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution)); + } + + std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const { + this->getSubformula().writeToStream(out); + out << " || "; + this->getConditionFormula().writeToStream(out); + return out; + } + } +} \ No newline at end of file diff --git a/src/logic/ConditionalFormula.h b/src/logic/ConditionalFormula.h new file mode 100644 index 000000000..d7b4dc7cd --- /dev/null +++ b/src/logic/ConditionalFormula.h @@ -0,0 +1,38 @@ +#ifndef STORM_LOGIC_CONDITIONALFORMULA_H_ +#define STORM_LOGIC_CONDITIONALFORMULA_H_ + +#include "src/logic/BinaryPathFormula.h" + +namespace storm { + namespace logic { + class ConditionalFormula : public Formula { + public: + enum class Context { Probability, Reward }; + + ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, Context context = Context::Probability); + + virtual ~ConditionalFormula() { + // Intentionally left empty. + } + + Formula const& getSubformula() const; + Formula const& getConditionFormula() const; + + virtual bool isConditionalProbabilityFormula() const override; + virtual bool isConditionalRewardFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + virtual std::shared_ptr substitute(std::map const& substitution) const override; + + private: + std::shared_ptr subformula; + std::shared_ptr conditionFormula; + Context context; + }; + } +} + +#endif /* STORM_LOGIC_CONDITIONALFORMULA_H_ */ \ No newline at end of file diff --git a/src/logic/ConditionalPathFormula.cpp b/src/logic/ConditionalPathFormula.cpp deleted file mode 100644 index 676a83185..000000000 --- a/src/logic/ConditionalPathFormula.cpp +++ /dev/null @@ -1,40 +0,0 @@ -#include "src/logic/ConditionalPathFormula.h" - -namespace storm { - namespace logic { - ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, bool isRewardFormula) : BinaryPathFormula(leftSubformula, rightSubformula), isRewardFormula(isRewardFormula) { - // Intentionally left empty. - } - - bool ConditionalPathFormula::isConditionalPathFormula() const { - return true; - } - - bool ConditionalPathFormula::isValidProbabilityPathFormula() const { - return true; - } - - bool ConditionalPathFormula::isPctlWithConditionalPathFormula() const { - return this->getLeftSubformula().isPctlPathFormula() && this->getRightSubformula().isPctlPathFormula(); - } - - bool ConditionalPathFormula::isRewardPathFormula() const { - return this->isRewardFormula && this->isValidRewardPathFormula(); - } - - bool ConditionalPathFormula::isValidRewardPathFormula() const { - return this->getLeftSubformula().isRewardPathFormula() && !this->getLeftSubformula().isConditionalPathFormula() && this->getRightSubformula().isPctlPathFormula(); - } - - std::shared_ptr ConditionalPathFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution)); - } - - std::ostream& ConditionalPathFormula::writeToStream(std::ostream& out) const { - this->getLeftSubformula().writeToStream(out); - out << " || "; - this->getRightSubformula().writeToStream(out); - return out; - } - } -} \ No newline at end of file diff --git a/src/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h deleted file mode 100644 index 94053606b..000000000 --- a/src/logic/ConditionalPathFormula.h +++ /dev/null @@ -1,32 +0,0 @@ -#ifndef STORM_LOGIC_CONDITIONALPATHFORMULA_H_ -#define STORM_LOGIC_CONDITIONALPATHFORMULA_H_ - -#include "src/logic/BinaryPathFormula.h" - -namespace storm { - namespace logic { - class ConditionalPathFormula : public BinaryPathFormula { - public: - ConditionalPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, bool isRewardFormula = false); - - virtual ~ConditionalPathFormula() { - // Intentionally left empty. - } - - virtual bool isPctlWithConditionalPathFormula() const override; - virtual bool isRewardPathFormula() const override; - virtual bool isConditionalPathFormula() const override; - virtual bool isValidProbabilityPathFormula() const override; - virtual bool isValidRewardPathFormula() const override; - - virtual std::ostream& writeToStream(std::ostream& out) const override; - - virtual std::shared_ptr substitute(std::map const& substitution) const override; - - private: - bool isRewardFormula; - }; - } -} - -#endif /* STORM_LOGIC_CONDITIONALPATHFORMULA_H_ */ \ No newline at end of file diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp index 2a00c04f3..d8318164d 100644 --- a/src/logic/CumulativeRewardFormula.cpp +++ b/src/logic/CumulativeRewardFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/CumulativeRewardFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) { @@ -10,16 +12,16 @@ namespace storm { // Intentionally left empty. } - bool CumulativeRewardFormula::isRewardPathFormula() const { + bool CumulativeRewardFormula::isCumulativeRewardFormula() const { return true; } - bool CumulativeRewardFormula::isCumulativeRewardFormula() const { + bool CumulativeRewardFormula::isRewardPathFormula() const { return true; } - bool CumulativeRewardFormula::isValidRewardPathFormula() const { - return true; + boost::any CumulativeRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } bool CumulativeRewardFormula::hasDiscreteTimeBound() const { diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h index 0192a8a49..6a5e8c035 100644 --- a/src/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -16,10 +16,11 @@ namespace storm { virtual ~CumulativeRewardFormula() { // Intentionally left empty. } - - virtual bool isRewardPathFormula() const override; + virtual bool isCumulativeRewardFormula() const override; - virtual bool isValidRewardPathFormula() const override; + virtual bool isRewardPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index 8b09281cd..3d2e6fb57 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -1,25 +1,39 @@ #include "src/logic/EventuallyFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, bool isRewardFormula) : UnaryPathFormula(subformula), isRewardFormula(isRewardFormula) { + EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, Context context) : UnaryPathFormula(subformula), context(context) { // Intentionally left empty. } bool EventuallyFormula::isEventuallyFormula() const { - return true; + return context == Context::Probability; + } + + bool EventuallyFormula::isReachabilityRewardFormula() const { + return context == Context::Reward; + } + + bool EventuallyFormula::isReachbilityExpectedTimeFormula() const { + return context == Context::ExpectedTime; + } + + bool EventuallyFormula::isProbabilityPathFormula() const { + return this->isEventuallyFormula(); } bool EventuallyFormula::isRewardPathFormula() const { - return isRewardFormula; + return this->isReachabilityRewardFormula(); } - bool EventuallyFormula::isValidProbabilityPathFormula() const { - return !isRewardFormula; + bool EventuallyFormula::isExpectedTimePathFormula() const { + return this->isReachbilityExpectedTimeFormula(); } - bool EventuallyFormula::isValidRewardPathFormula() const { - return isRewardFormula; + boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::shared_ptr EventuallyFormula::substitute(std::map const& substitution) const { diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index 3b121d320..d7a81fa83 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -7,23 +7,29 @@ namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { public: - EventuallyFormula(std::shared_ptr const& subformula, bool isRewardFormula = false); + enum class Context { Probability, Reward, ExpectedTime }; + + EventuallyFormula(std::shared_ptr const& subformula, Context context = Context::Probability); virtual ~EventuallyFormula() { // Intentionally left empty. } virtual bool isEventuallyFormula() const override; + virtual bool isReachabilityRewardFormula() const override; + virtual bool isReachbilityExpectedTimeFormula() const override; + virtual bool isProbabilityPathFormula() const override; virtual bool isRewardPathFormula() const override; - virtual bool isValidProbabilityPathFormula() const override; - virtual bool isValidRewardPathFormula() const override; + virtual bool isExpectedTimePathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; private: - bool isRewardFormula; + Context context; }; } } diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index 8165710a1..5dc8161ae 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/ExpectedTimeOperatorFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) { @@ -22,20 +24,8 @@ namespace storm { return true; } - bool ExpectedTimeOperatorFormula::isPctlStateFormula() const { - return this->getSubformula().isPctlStateFormula(); - } - - bool ExpectedTimeOperatorFormula::isPctlWithConditionalStateFormula() const { - return this->getSubformula().isPctlWithConditionalStateFormula(); - } - - bool ExpectedTimeOperatorFormula::containsProbabilityOperator() const { - return this->getSubformula().containsProbabilityOperator(); - } - - bool ExpectedTimeOperatorFormula::containsNestedProbabilityOperators() const { - return this->getSubformula().containsNestedProbabilityOperators(); + boost::any ExpectedTimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index 162fb39f8..5e1925b44 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -3,6 +3,8 @@ #include "src/logic/OperatorFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { class ExpectedTimeOperatorFormula : public OperatorFormula { @@ -18,11 +20,8 @@ namespace storm { } virtual bool isExpectedTimeOperatorFormula() const override; - - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 9f9151b84..6270d5664 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -71,135 +71,63 @@ namespace storm { return false; } - bool Formula::isConditionalPathFormula() const { + bool Formula::isConditionalProbabilityFormula() const { return false; } - bool Formula::isNextFormula() const { - return false; - } - - bool Formula::isLongRunAverageOperatorFormula() const { - return false; - } - - bool Formula::isExpectedTimeOperatorFormula() const { - return false; - } - - bool Formula::isCumulativeRewardFormula() const { - return false; - } - - bool Formula::isInstantaneousRewardFormula() const { - return false; - } - - bool Formula::isLongRunAverageRewardFormula() const { - return false; - } - - bool Formula::isProbabilityOperatorFormula() const { - return false; - } - - bool Formula::isRewardOperatorFormula() const { - return false; - } - - bool Formula::isOperatorFormula() const { + bool Formula::isConditionalRewardFormula() const { return false; } - bool Formula::isPctlFormula() const { - return this->isPctlStateFormula() || this->isPctlPathFormula(); - } - - bool Formula::isPctlWithConditionalFormula() const { - return this->isPctlWithConditionalStateFormula() || this->isPctlWithConditionalPathFormula(); - } - - bool Formula::isRewardFormula() const { - return this->isRewardStateFormula() || this->isRewardPathFormula(); - } - - bool Formula::isCslFormula() const { - return this->isCslStateFormula() || this->isCslPathFormula(); - } - - bool Formula::isPctlPathFormula() const { - return false; - } - - bool Formula::isPctlStateFormula() const { - return false; - } - - bool Formula::isPctlWithConditionalPathFormula() const { - return false; - } - - bool Formula::isPctlWithConditionalStateFormula() const { + bool Formula::isProbabilityPathFormula() const { return false; } - bool Formula::isCslPathFormula() const { - return this->isPctlPathFormula(); - } - - bool Formula::isCslStateFormula() const { - return this->isPctlStateFormula(); - } - bool Formula::isRewardPathFormula() const { return false; } - bool Formula::isRewardStateFormula() const { + bool Formula::isExpectedTimePathFormula() const { return false; } - bool Formula::isPltlFormula() const { - return false; - } - - bool Formula::isLtlFormula() const { + bool Formula::isNextFormula() const { return false; } - bool Formula::isPropositionalFormula() const { + bool Formula::isLongRunAverageOperatorFormula() const { return false; } - bool Formula::isValidProbabilityPathFormula() const { + bool Formula::isExpectedTimeOperatorFormula() const { return false; } - bool Formula::isValidRewardPathFormula() const { + bool Formula::isCumulativeRewardFormula() const { return false; } - bool Formula::containsBoundedUntilFormula() const { + bool Formula::isInstantaneousRewardFormula() const { return false; } - bool Formula::containsNextFormula() const { + bool Formula::isLongRunAverageRewardFormula() const { return false; } - bool Formula::containsProbabilityOperator() const { + bool Formula::isReachbilityExpectedTimeFormula() const { return false; } - bool Formula::containsNestedProbabilityOperators() const { + bool Formula::isProbabilityOperatorFormula() const { return false; } - bool Formula::containsRewardOperator() const { + bool Formula::isRewardOperatorFormula() const { return false; } - bool Formula::containsNestedRewardOperators() const { + bool Formula::isOperatorFormula() const { return false; } @@ -239,12 +167,12 @@ namespace storm { return dynamic_cast(*this); } - ConditionalPathFormula& Formula::asConditionalPathFormula() { - return dynamic_cast(*this); + ConditionalFormula& Formula::asConditionalFormula() { + return dynamic_cast(*this); } - ConditionalPathFormula const& Formula::asConditionalPathFormula() const { - return dynamic_cast(*this); + ConditionalFormula const& Formula::asConditionalFormula() const { + return dynamic_cast(*this); } BinaryBooleanStateFormula& Formula::asBinaryBooleanStateFormula() { diff --git a/src/logic/Formula.h b/src/logic/Formula.h index cf4333eb4..ae879fce6 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -6,37 +6,18 @@ #include #include +#include + #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" +#include "src/logic/FormulasForwardDeclarations.h" + namespace storm { namespace logic { - // Forward-declare all formula classes. - class PathFormula; - class StateFormula; - class BinaryStateFormula; - class UnaryStateFormula; - class BinaryBooleanStateFormula; - class UnaryBooleanStateFormula; - class BooleanLiteralFormula; - class AtomicExpressionFormula; - class AtomicLabelFormula; - class UntilFormula; - class BoundedUntilFormula; - class EventuallyFormula; - class GloballyFormula; - class BinaryPathFormula; - class UnaryPathFormula; - class ConditionalPathFormula; - class NextFormula; - class LongRunAverageOperatorFormula; - class ExpectedTimeOperatorFormula; - class CumulativeRewardFormula; - class InstantaneousRewardFormula; - class LongRunAverageRewardFormula; - class ProbabilityOperatorFormula; - class RewardOperatorFormula; - class OperatorFormula; + + // Forward-declare visitor for accept() method. + class FormulaVisitor; // Also foward-declare base model checker class. class ModelChecker; @@ -49,59 +30,57 @@ namespace storm { }; friend std::ostream& operator<<(std::ostream& out, Formula const& formula); - - // Methods for querying the exact formula type. + + // Basic formula types. virtual bool isPathFormula() const; virtual bool isStateFormula() const; - virtual bool isBinaryStateFormula() const; - virtual bool isUnaryStateFormula() const; + virtual bool isConditionalProbabilityFormula() const; + virtual bool isConditionalRewardFormula() const; + + virtual bool isProbabilityPathFormula() const; + virtual bool isRewardPathFormula() const; + virtual bool isExpectedTimePathFormula() const; + virtual bool isBinaryBooleanStateFormula() const; virtual bool isUnaryBooleanStateFormula() const; + + // Operator formulas. + virtual bool isOperatorFormula() const; + virtual bool isLongRunAverageOperatorFormula() const; + virtual bool isExpectedTimeOperatorFormula() const; + virtual bool isProbabilityOperatorFormula() const; + virtual bool isRewardOperatorFormula() const; + + // Atomic state formulas. virtual bool isBooleanLiteralFormula() const; virtual bool isTrueFormula() const; virtual bool isFalseFormula() const; virtual bool isAtomicExpressionFormula() const; virtual bool isAtomicLabelFormula() const; + + // Probability path formulas. + virtual bool isNextFormula() const; virtual bool isUntilFormula() const; virtual bool isBoundedUntilFormula() const; virtual bool isEventuallyFormula() const; virtual bool isGloballyFormula() const; - virtual bool isBinaryPathFormula() const; - virtual bool isUnaryPathFormula() const; - virtual bool isConditionalPathFormula() const; - virtual bool isNextFormula() const; - virtual bool isLongRunAverageOperatorFormula() const; - virtual bool isExpectedTimeOperatorFormula() const; + + // Reward formulas. virtual bool isCumulativeRewardFormula() const; virtual bool isInstantaneousRewardFormula() const; + virtual bool isReachabilityRewardFormula() const; virtual bool isLongRunAverageRewardFormula() const; - virtual bool isProbabilityOperatorFormula() const; - virtual bool isRewardOperatorFormula() const; - virtual bool isOperatorFormula() const; + + // Expected time formulas. + virtual bool isReachbilityExpectedTimeFormula() const; + + // Type checks for abstract intermediate classes. + virtual bool isBinaryPathFormula() const; + virtual bool isBinaryStateFormula() const; + virtual bool isUnaryPathFormula() const; + virtual bool isUnaryStateFormula() const; - bool isPctlFormula() const; - bool isPctlWithConditionalFormula() const; - bool isRewardFormula() const; - bool isCslFormula() const; - virtual bool isPctlPathFormula() const; - virtual bool isPctlStateFormula() const; - virtual bool isPctlWithConditionalPathFormula() const; - virtual bool isPctlWithConditionalStateFormula() const; - virtual bool isCslPathFormula() const; - virtual bool isCslStateFormula() const; - virtual bool isRewardPathFormula() const; - virtual bool isRewardStateFormula() const; - virtual bool isPltlFormula() const; - virtual bool isLtlFormula() const; - virtual bool isPropositionalFormula() const; - virtual bool isValidProbabilityPathFormula() const; - virtual bool isValidRewardPathFormula() const; - virtual bool containsBoundedUntilFormula() const; - virtual bool containsNextFormula() const; - virtual bool containsProbabilityOperator() const; - virtual bool containsNestedProbabilityOperators() const; - virtual bool containsRewardOperator() const; - virtual bool containsNestedRewardOperators() const; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const = 0; static std::shared_ptr getTrueFormula(); @@ -150,8 +129,8 @@ namespace storm { UnaryPathFormula& asUnaryPathFormula(); UnaryPathFormula const& asUnaryPathFormula() const; - ConditionalPathFormula& asConditionalPathFormula(); - ConditionalPathFormula const& asConditionalPathFormula() const; + ConditionalFormula& asConditionalFormula(); + ConditionalFormula const& asConditionalFormula() const; NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; diff --git a/src/logic/FormulaVisitor.h b/src/logic/FormulaVisitor.h new file mode 100644 index 000000000..a2e5b1a4f --- /dev/null +++ b/src/logic/FormulaVisitor.h @@ -0,0 +1,36 @@ +#ifndef STORM_LOGIC_FORMULAVISITOR_H_ +#define STORM_LOGIC_FORMULAVISITOR_H_ + +#include + +#include "src/logic/FormulasForwardDeclarations.h" + +namespace storm { + namespace logic { + + class FormulaVisitor { + public: + virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0; + }; + + } +} + +#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */ \ No newline at end of file diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 7da9321c6..a5218eeb8 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -23,7 +23,7 @@ #include "src/logic/UnaryPathFormula.h" #include "src/logic/UnaryStateFormula.h" #include "src/logic/UntilFormula.h" -#include "src/logic/ConditionalPathFormula.h" +#include "src/logic/ConditionalFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/RewardOperatorFormula.h" #include "src/logic/ComparisonType.h" \ No newline at end of file diff --git a/src/logic/FormulasForwardDeclarations.h b/src/logic/FormulasForwardDeclarations.h new file mode 100644 index 000000000..13b4c326c --- /dev/null +++ b/src/logic/FormulasForwardDeclarations.h @@ -0,0 +1,36 @@ +#ifndef STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ +#define STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ + +namespace storm { + namespace logic { + // Forward-declare all formula classes. + class Formula; + class AtomicExpressionFormula; + class AtomicLabelFormula; + class BinaryBooleanStateFormula; + class BinaryPathFormula; + class BinaryStateFormula; + class BooleanLiteralFormula; + class BoundedUntilFormula; + class ConditionalFormula; + class CumulativeRewardFormula; + class EventuallyFormula; + class ExpectedTimeOperatorFormula; + class GloballyFormula; + class InstantaneousRewardFormula; + class LongRunAverageOperatorFormula; + class LongRunAverageRewardFormula; + class NextFormula; + class OperatorFormula; + class PathFormula; + class ProbabilityOperatorFormula; + class RewardOperatorFormula; + class StateFormula; + class UnaryBooleanStateFormula; + class UnaryPathFormula; + class UnaryStateFormula; + class UntilFormula; + } +} + +#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */ \ No newline at end of file diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp new file mode 100644 index 000000000..d94056f58 --- /dev/null +++ b/src/logic/FragmentChecker.cpp @@ -0,0 +1,118 @@ +#include "src/logic/FragmentChecker.h" + +#include "src/logic/Formulas.h" + +namespace storm { + namespace logic { + bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const { + boost::any result = f.accept(*this, specification); + return boost::any_cast(result); + } + + boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areAtomicExpressionFormulasAllowed(); + } + + boost::any FragmentChecker::visit(AtomicLabelFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areAtomicLabelFormulasAllowed(); + } + + boost::any FragmentChecker::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + bool result = specification.areBinaryBooleanStateFormulasAllowed(); + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, specification)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, specification)); + return result; + } + + boost::any FragmentChecker::visit(BooleanLiteralFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areBooleanLiteralFormulasAllowed(); + } + + boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + bool result = specification.areBoundedUntilFormulasAllowed(); + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); + return result; + } + + boost::any FragmentChecker::visit(ConditionalFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + bool result = true; + if (f.isConditionalProbabilityFormula()) { + result &= specification.areConditionalProbabilityFormulasAllowed(); + } else if (f.Formula::isConditionalRewardFormula()) { + result &= specification.areConditionalRewardFormulasFormulasAllowed(); + } + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getConditionFormula().accept(*this, data)); + return result; + } + + boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areCumulativeRewardFormulasAllowed(); + } + + boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + bool result = specification.areEventuallyFormulasAllowed(); + result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; + } + + boost::any FragmentChecker::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areExpectedTimeOperatorsAllowed(); + } + + boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areGloballyFormulasAllowed(); + } + + boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areInstantaneousRewardFormulasAllowed(); + } + + boost::any FragmentChecker::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areLongRunAverageOperatorsAllowed(); + } + + boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areLongRunAverageRewardFormulasAllowed(); + } + + boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areNextFormulasAllowed(); + } + + boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areProbabilityOperatorsAllowed(); + } + + boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areRewardOperatorsAllowed(); + } + + boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areUnaryBooleanStateFormulasAllowed(); + } + + boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const { + FragmentSpecification const& specification = boost::any_cast(data); + return specification.areUntilFormulasAllowed(); + } + } +} \ No newline at end of file diff --git a/src/logic/FragmentChecker.h b/src/logic/FragmentChecker.h new file mode 100644 index 000000000..3d22390e6 --- /dev/null +++ b/src/logic/FragmentChecker.h @@ -0,0 +1,39 @@ +#ifndef STORM_LOGIC_FRAGMENTCHECKER_H_ +#define STORM_LOGIC_FRAGMENTCHECKER_H_ + +#include "src/logic/FormulaVisitor.h" + +#include "src/logic/FragmentSpecification.h" + +namespace storm { + namespace logic { + + class FragmentChecker : public FormulaVisitor { + public: + bool conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const; + + virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; + virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; + virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; + virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; + virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; + virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; + }; + + } +} + + +#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */ \ No newline at end of file diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp new file mode 100644 index 000000000..eeb697582 --- /dev/null +++ b/src/logic/FragmentSpecification.cpp @@ -0,0 +1,209 @@ +#include "src/logic/FragmentSpecification.h" + +namespace storm { + namespace logic { + + FragmentSpecification FragmentSpecification::copy() const { + return FragmentSpecification(*this); + } + + bool FragmentSpecification::areProbabilityOperatorsAllowed() const { + return probabilityOperator; + } + + FragmentSpecification& FragmentSpecification::setProbabilityOperatorsAllowed(bool newValue) { + this->probabilityOperator = newValue; + return *this; + } + + bool FragmentSpecification::areRewardOperatorsAllowed() const { + return rewardOperator; + } + + FragmentSpecification& FragmentSpecification::setRewardOperatorsAllowed(bool newValue) { + this->rewardOperator = newValue; + return *this; + } + + bool FragmentSpecification::areExpectedTimeOperatorsAllowed() const { + return expectedTimeOperator; + } + + FragmentSpecification& FragmentSpecification::setExpectedTimeOperatorsAllowed(bool newValue) { + this->expectedTimeOperator = newValue; + return *this; + } + + bool FragmentSpecification::areLongRunAverageOperatorsAllowed() const { + return longRunAverageOperator; + } + + FragmentSpecification& FragmentSpecification::setLongRunAverageOperatorsAllowed(bool newValue) { + this->longRunAverageOperator = newValue; + return *this; + } + + bool FragmentSpecification::areGloballyFormulasAllowed() const { + return globallyFormula; + } + + FragmentSpecification& FragmentSpecification::setGloballyFormulasAllowed(bool newValue) { + this->globallyFormula = newValue; + return *this; + } + + bool FragmentSpecification::areEventuallyFormulasAllowed() const { + return eventuallyFormula; + } + + FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) { + this->eventuallyFormula = newValue; + return *this; + } + + bool FragmentSpecification::areNextFormulasAllowed() const { + return nextFormula; + } + + FragmentSpecification& FragmentSpecification::setNextFormulasAllowed(bool newValue) { + this->nextFormula = newValue; + return *this; + } + + bool FragmentSpecification::areUntilFormulasAllowed() const { + return untilFormula; + } + + FragmentSpecification& FragmentSpecification::setUntilFormulasAllowed(bool newValue) { + this->untilFormula = newValue; + return *this; + } + + bool FragmentSpecification::areBoundedUntilFormulasAllowed() const { + return boundedUntilFormula; + } + + FragmentSpecification& FragmentSpecification::setBoundedUntilFormulasAllowed(bool newValue) { + this->boundedUntilFormula = newValue; + return *this; + } + + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { + return atomicExpressionFormula; + } + + FragmentSpecification& FragmentSpecification::setAtomicExpressionFormulasAllowed(bool newValue) { + this->atomicExpressionFormula = newValue; + return *this; + } + + bool FragmentSpecification::areAtomicLabelFormulasAllowed() const { + return atomicLabelFormula; + } + + FragmentSpecification& FragmentSpecification::setAtomicLabelFormulasAllowed(bool newValue) { + this->atomicLabelFormula = newValue; + return *this; + } + + bool FragmentSpecification::areBooleanLiteralFormulasAllowed() const { + return booleanLiteralFormula; + } + + FragmentSpecification& FragmentSpecification::setBooleanLiteralFormulasAllowed(bool newValue) { + this->booleanLiteralFormula = newValue; + return *this; + } + + bool FragmentSpecification::areUnaryBooleanStateFormulasAllowed() const { + return unaryBooleanStateFormula; + } + + FragmentSpecification& FragmentSpecification::setUnaryBooleanStateFormulasAllowed(bool newValue) { + this->unaryBooleanStateFormula = newValue; + return *this; + } + + bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const { + return binaryBooleanStateFormula; + } + + FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) { + this->binaryBooleanStateFormula = newValue; + return *this; + } + + bool FragmentSpecification::areCumulativeRewardFormulasAllowed() const { + return cumulativeRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setCumulativeRewardFormulasAllowed(bool newValue) { + this->cumulativeRewardFormula = newValue; + return *this; + } + + bool FragmentSpecification::areInstantaneousRewardFormulasAllowed() const { + return instantaneousRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setInstantaneousFormulasAllowed(bool newValue) { + this->instantaneousRewardFormula = newValue; + return *this; + } + + bool FragmentSpecification::areReachabilityRewardFormulasAllowed() const { + return reachabilityRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setReachabilityRewardFormulasAllowed(bool newValue) { + this->reachabilityRewardFormula = newValue; + return *this; + } + + bool FragmentSpecification::areLongRunAverageRewardFormulasAllowed() const { + return longRunAverageRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setLongRunAverageRewardFormulasAllowed(bool newValue) { + this->longRunAverageRewardFormula = newValue; + return *this; + } + + bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const { + return conditionalProbabilityFormula; + } + + FragmentSpecification& FragmentSpecification::setConditionalProbabilityFormulasAllowed(bool newValue) { + this->conditionalProbabilityFormula = newValue; + return *this; + } + + bool FragmentSpecification::areConditionalRewardFormulasFormulasAllowed() const { + return conditionalRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setConditionalRewardFormulasAllowed(bool newValue) { + this->conditionalRewardFormula = newValue; + return *this; + } + + bool FragmentSpecification::areReachbilityExpectedTimeFormulasAllowed() const { + return reachabilityExpectedTimeFormula; + } + + FragmentSpecification& FragmentSpecification::setReachbilityExpectedTimeFormulasAllowed(bool newValue) { + this->reachabilityExpectedTimeFormula = newValue; + return *this; + } + + bool FragmentSpecification::areNestedOperatorsAllowed() const { + return this->nestedOperators; + } + + FragmentSpecification& FragmentSpecification::setNestedOperatorsAllowed(bool newValue) { + this->nestedOperators = newValue; + return *this; + } + + } +} \ No newline at end of file diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h new file mode 100644 index 000000000..91099703f --- /dev/null +++ b/src/logic/FragmentSpecification.h @@ -0,0 +1,112 @@ +#ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_ +#define STORM_LOGIC_FRAGMENTSPECIFICATION_H_ + +namespace storm { + namespace logic { + class FragmentSpecification { + public: + FragmentSpecification copy() const; + + bool areProbabilityOperatorsAllowed() const; + FragmentSpecification& setProbabilityOperatorsAllowed(bool newValue); + + bool areRewardOperatorsAllowed() const; + FragmentSpecification& setRewardOperatorsAllowed(bool newValue); + + bool areExpectedTimeOperatorsAllowed() const; + FragmentSpecification& setExpectedTimeOperatorsAllowed(bool newValue); + + bool areLongRunAverageOperatorsAllowed() const; + FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue); + + bool areGloballyFormulasAllowed() const; + FragmentSpecification& setGloballyFormulasAllowed(bool newValue); + + bool areEventuallyFormulasAllowed() const; + FragmentSpecification& setEventuallyFormulasAllowed(bool newValue); + + bool areNextFormulasAllowed() const; + FragmentSpecification& setNextFormulasAllowed(bool newValue); + + bool areUntilFormulasAllowed() const; + FragmentSpecification& setUntilFormulasAllowed(bool newValue); + + bool areBoundedUntilFormulasAllowed() const; + FragmentSpecification& setBoundedUntilFormulasAllowed(bool newValue); + + bool areAtomicExpressionFormulasAllowed() const; + FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue); + + bool areAtomicLabelFormulasAllowed() const; + FragmentSpecification& setAtomicLabelFormulasAllowed(bool newValue); + + bool areBooleanLiteralFormulasAllowed() const; + FragmentSpecification& setBooleanLiteralFormulasAllowed(bool newValue); + + bool areUnaryBooleanStateFormulasAllowed() const; + FragmentSpecification& setUnaryBooleanStateFormulasAllowed(bool newValue); + + bool areBinaryBooleanStateFormulasAllowed() const; + FragmentSpecification& setBinaryBooleanStateFormulasAllowed(bool newValue); + + bool areCumulativeRewardFormulasAllowed() const; + FragmentSpecification& setCumulativeRewardFormulasAllowed(bool newValue); + + bool areInstantaneousRewardFormulasAllowed() const; + FragmentSpecification& setInstantaneousFormulasAllowed(bool newValue); + + bool areReachabilityRewardFormulasAllowed() const; + FragmentSpecification& setReachabilityRewardFormulasAllowed(bool newValue); + + bool areLongRunAverageRewardFormulasAllowed() const; + FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue); + + bool areConditionalProbabilityFormulasAllowed() const; + FragmentSpecification& setConditionalProbabilityFormulasAllowed(bool newValue); + + bool areConditionalRewardFormulasFormulasAllowed() const; + FragmentSpecification& setConditionalRewardFormulasAllowed(bool newValue); + + bool areReachbilityExpectedTimeFormulasAllowed() const; + FragmentSpecification& setReachbilityExpectedTimeFormulasAllowed(bool newValue); + + bool areNestedOperatorsAllowed() const; + FragmentSpecification& setNestedOperatorsAllowed(bool newValue); + + private: + // Flags that indicate whether it is legal to see such a formula. + bool probabilityOperator; + bool rewardOperator; + bool expectedTimeOperator; + bool longRunAverageOperator; + + bool globallyFormula; + bool eventuallyFormula; + bool nextFormula; + bool untilFormula; + bool boundedUntilFormula; + + bool atomicExpressionFormula; + bool atomicLabelFormula; + bool booleanLiteralFormula; + bool unaryBooleanStateFormula; + bool binaryBooleanStateFormula; + + bool cumulativeRewardFormula; + bool instantaneousRewardFormula; + bool reachabilityRewardFormula; + bool longRunAverageRewardFormula; + + bool conditionalProbabilityFormula; + bool conditionalRewardFormula; + + bool reachabilityExpectedTimeFormula; + + // Members that indicate certain restrictions. + bool nestedOperators; + + }; + } +} + +#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */ \ No newline at end of file diff --git a/src/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp index 5ddfd8feb..df33f0b52 100644 --- a/src/logic/GloballyFormula.cpp +++ b/src/logic/GloballyFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/GloballyFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { GloballyFormula::GloballyFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { @@ -10,9 +12,13 @@ namespace storm { return true; } - bool GloballyFormula::isValidProbabilityPathFormula() const { + bool GloballyFormula::isProbabilityPathFormula() const { return true; } + + boost::any GloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } std::shared_ptr GloballyFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getSubformula().substitute(substitution)); diff --git a/src/logic/GloballyFormula.h b/src/logic/GloballyFormula.h index e3fc82f2d..011c61de9 100644 --- a/src/logic/GloballyFormula.h +++ b/src/logic/GloballyFormula.h @@ -14,7 +14,9 @@ namespace storm { } virtual bool isGloballyFormula() const override; - virtual bool isValidProbabilityPathFormula() const override; + virtual bool isProbabilityPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp index 7289f18e9..4f1f65429 100644 --- a/src/logic/InstantaneousRewardFormula.cpp +++ b/src/logic/InstantaneousRewardFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/InstantaneousRewardFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) { @@ -14,12 +16,12 @@ namespace storm { return true; } - bool InstantaneousRewardFormula::isValidRewardPathFormula() const { + bool InstantaneousRewardFormula::isRewardPathFormula() const { return true; } - bool InstantaneousRewardFormula::isRewardPathFormula() const { - return true; + boost::any InstantaneousRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } bool InstantaneousRewardFormula::hasDiscreteTimeBound() const { diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h index 967f03a2b..069bf21bd 100644 --- a/src/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -17,10 +17,12 @@ namespace storm { // Intentionally left empty. } - virtual bool isRewardPathFormula() const override; virtual bool isInstantaneousRewardFormula() const override; - virtual bool isValidRewardPathFormula() const override; + virtual bool isRewardPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; bool hasDiscreteTimeBound() const; diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index 1563dc67e..c9d781905 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/LongRunAverageOperatorFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) { @@ -22,20 +24,8 @@ namespace storm { return true; } - bool LongRunAverageOperatorFormula::isPctlStateFormula() const { - return this->getSubformula().isPctlStateFormula(); - } - - bool LongRunAverageOperatorFormula::isPctlWithConditionalStateFormula() const { - return this->getSubformula().isPctlWithConditionalStateFormula(); - } - - bool LongRunAverageOperatorFormula::containsProbabilityOperator() const { - return this->getSubformula().containsProbabilityOperator(); - } - - bool LongRunAverageOperatorFormula::containsNestedProbabilityOperators() const { - return this->getSubformula().containsNestedProbabilityOperators(); + boost::any LongRunAverageOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 85eb9f969..d4a785b80 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -19,10 +19,7 @@ namespace storm { virtual bool isLongRunAverageOperatorFormula() const override; - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/LongRunAverageRewardFormula.cpp b/src/logic/LongRunAverageRewardFormula.cpp index 9d9dc898d..30bfd7ba9 100644 --- a/src/logic/LongRunAverageRewardFormula.cpp +++ b/src/logic/LongRunAverageRewardFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/LongRunAverageRewardFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { LongRunAverageRewardFormula::LongRunAverageRewardFormula() { @@ -10,12 +12,12 @@ namespace storm { return true; } - bool LongRunAverageRewardFormula::isValidRewardPathFormula() const { + bool LongRunAverageRewardFormula::isRewardPathFormula() const { return true; } - bool LongRunAverageRewardFormula::isRewardPathFormula() const { - return true; + boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::shared_ptr LongRunAverageRewardFormula::substitute(std::map const& substitution) const { diff --git a/src/logic/LongRunAverageRewardFormula.h b/src/logic/LongRunAverageRewardFormula.h index 929a6f3c8..3dfea465e 100644 --- a/src/logic/LongRunAverageRewardFormula.h +++ b/src/logic/LongRunAverageRewardFormula.h @@ -13,9 +13,10 @@ namespace storm { // Intentionally left empty. } - virtual bool isRewardPathFormula() const override; virtual bool isLongRunAverageRewardFormula() const override; - virtual bool isValidRewardPathFormula() const override; + virtual bool isRewardPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp index b7400eb7d..e73171a95 100644 --- a/src/logic/NextFormula.cpp +++ b/src/logic/NextFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/NextFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { NextFormula::NextFormula(std::shared_ptr const& subformula) : UnaryPathFormula(subformula) { @@ -10,12 +12,12 @@ namespace storm { return true; } - bool NextFormula::isValidProbabilityPathFormula() const { + bool NextFormula::isProbabilityPathFormula() const { return true; } - bool NextFormula::containsNextFormula() const { - return true; + boost::any NextFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::shared_ptr NextFormula::substitute(std::map const& substitution) const { diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h index f0de43cc6..bade60456 100644 --- a/src/logic/NextFormula.h +++ b/src/logic/NextFormula.h @@ -14,9 +14,9 @@ namespace storm { } virtual bool isNextFormula() const override; - virtual bool isValidProbabilityPathFormula() const override; + virtual bool isProbabilityPathFormula() const override; - virtual bool containsNextFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index cb584b034..09680cbc5 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/ProbabilityOperatorFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) { @@ -22,30 +24,10 @@ namespace storm { return true; } - bool ProbabilityOperatorFormula::isPctlStateFormula() const { - return this->getSubformula().isPctlPathFormula(); - } - - bool ProbabilityOperatorFormula::isPctlWithConditionalStateFormula() const { - return this->getSubformula().isPctlWithConditionalPathFormula(); - } - - bool ProbabilityOperatorFormula::isCslStateFormula() const { - return this->getSubformula().isCslPathFormula(); - } - - bool ProbabilityOperatorFormula::isPltlFormula() const { - return this->getSubformula().isLtlFormula(); + boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } - - bool ProbabilityOperatorFormula::containsProbabilityOperator() const { - return true; - } - - bool ProbabilityOperatorFormula::containsNestedProbabilityOperators() const { - return this->getSubformula().containsProbabilityOperator(); - } - + ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 163e05f58..1172247d0 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -17,14 +17,9 @@ namespace storm { // Intentionally left empty. } - virtual bool isPctlStateFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isCslStateFormula() const override; - virtual bool isPltlFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; - virtual bool isProbabilityOperatorFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 0eea0eedc..0e025c208 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/RewardOperatorFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) { @@ -22,20 +24,8 @@ namespace storm { return true; } - bool RewardOperatorFormula::isRewardStateFormula() const { - return this->getSubformula().isRewardPathFormula(); - } - - bool RewardOperatorFormula::containsRewardOperator() const { - return true; - } - - bool RewardOperatorFormula::containsNestedRewardOperators() const { - return this->getSubformula().containsRewardOperator(); - } - - bool RewardOperatorFormula::hasRewardModelName() const { - return static_cast(this->rewardModelName); + boost::any RewardOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::string const& RewardOperatorFormula::getRewardModelName() const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 0cbfe955e..6bcf015d8 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -19,11 +19,9 @@ namespace storm { } virtual bool isRewardOperatorFormula() const override; - virtual bool isRewardStateFormula() const override; - virtual bool containsRewardOperator() const override; - virtual bool containsNestedRewardOperators() const override; - + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp index ec9a4ff0a..6d4f9ecdd 100644 --- a/src/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/UnaryBooleanStateFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) { @@ -9,6 +11,10 @@ namespace storm { bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const { return true; } + + boost::any UnaryBooleanStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } UnaryBooleanStateFormula::OperatorType UnaryBooleanStateFormula::getOperator() const { return operatorType; diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h index fa0a83023..93d45f862 100644 --- a/src/logic/UnaryBooleanStateFormula.h +++ b/src/logic/UnaryBooleanStateFormula.h @@ -17,6 +17,8 @@ namespace storm { virtual bool isUnaryBooleanStateFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + OperatorType getOperator() const; virtual bool isNot() const; diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index 01ccadde8..3e0cdaebc 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -9,43 +9,7 @@ namespace storm { bool UnaryPathFormula::isUnaryPathFormula() const { return true; } - - bool UnaryPathFormula::isPctlPathFormula() const { - return this->getSubformula().isPctlStateFormula(); - } - - bool UnaryPathFormula::isPctlWithConditionalPathFormula() const { - return this->getSubformula().isPctlWithConditionalStateFormula(); - } - - bool UnaryPathFormula::isLtlFormula() const { - return this->getSubformula().isLtlFormula(); - } - - bool UnaryPathFormula::containsBoundedUntilFormula() const { - return this->getSubformula().containsBoundedUntilFormula(); - } - - bool UnaryPathFormula::containsNextFormula() const { - return this->getSubformula().containsNextFormula(); - } - - bool UnaryPathFormula::containsProbabilityOperator() const { - return this->getSubformula().containsProbabilityOperator(); - } - - bool UnaryPathFormula::containsNestedProbabilityOperators() const { - return this->getSubformula().containsNestedProbabilityOperators(); - } - - bool UnaryPathFormula::containsRewardOperator() const { - return this->getSubformula().containsRewardOperator(); - } - - bool UnaryPathFormula::containsNestedRewardOperators() const { - return this->getSubformula().containsNestedRewardOperators(); - } - + Formula const& UnaryPathFormula::getSubformula() const { return *subformula; } diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index be60edbd9..3ea27d8f5 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -17,16 +17,6 @@ namespace storm { virtual bool isUnaryPathFormula() const override; - virtual bool isPctlPathFormula() const override; - virtual bool isPctlWithConditionalPathFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool containsBoundedUntilFormula() const override; - virtual bool containsNextFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; - virtual bool containsRewardOperator() const override; - virtual bool containsNestedRewardOperators() const override; - Formula const& getSubformula() const; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index a57b86b1e..e99c77057 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/UnaryStateFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { UnaryStateFormula::UnaryStateFormula(std::shared_ptr subformula) : subformula(subformula) { @@ -10,44 +12,8 @@ namespace storm { return true; } - bool UnaryStateFormula::isPropositionalFormula() const { - return this->getSubformula().isPropositionalFormula(); - } - - bool UnaryStateFormula::isPctlStateFormula() const { - return this->getSubformula().isPctlStateFormula(); - } - - bool UnaryStateFormula::isPctlWithConditionalStateFormula() const { - return this->getSubformula().isPctlWithConditionalStateFormula(); - } - - bool UnaryStateFormula::isLtlFormula() const { - return this->getSubformula().isLtlFormula(); - } - - bool UnaryStateFormula::containsBoundedUntilFormula() const { - return this->getSubformula().containsBoundedUntilFormula(); - } - - bool UnaryStateFormula::containsNextFormula() const { - return this->getSubformula().containsNextFormula(); - } - - bool UnaryStateFormula::containsProbabilityOperator() const { - return getSubformula().containsProbabilityOperator(); - } - - bool UnaryStateFormula::containsNestedProbabilityOperators() const { - return getSubformula().containsNestedProbabilityOperators(); - } - - bool UnaryStateFormula::containsRewardOperator() const { - return this->getSubformula().containsRewardOperator(); - } - - bool UnaryStateFormula::containsNestedRewardOperators() const { - return this->getSubformula().containsNestedRewardOperators(); + boost::any UnaryStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } Formula const& UnaryStateFormula::getSubformula() const { diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 8b5539a88..1dcf00023 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -15,16 +15,7 @@ namespace storm { virtual bool isUnaryStateFormula() const override; - virtual bool isPropositionalFormula() const override; - virtual bool isPctlWithConditionalStateFormula() const override; - virtual bool isPctlStateFormula() const override; - virtual bool isLtlFormula() const override; - virtual bool containsBoundedUntilFormula() const override; - virtual bool containsNextFormula() const override; - virtual bool containsProbabilityOperator() const override; - virtual bool containsNestedProbabilityOperators() const override; - virtual bool containsRewardOperator() const override; - virtual bool containsNestedRewardOperators() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; Formula const& getSubformula() const; diff --git a/src/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp index b15f3743f..a00eae77d 100644 --- a/src/logic/UntilFormula.cpp +++ b/src/logic/UntilFormula.cpp @@ -1,5 +1,7 @@ #include "src/logic/UntilFormula.h" +#include "src/logic/FormulaVisitor.h" + namespace storm { namespace logic { UntilFormula::UntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) { @@ -10,10 +12,14 @@ namespace storm { return true; } - bool UntilFormula::isValidProbabilityPathFormula() const { + bool UntilFormula::isProbabilityPathFormula() const { return true; } + boost::any UntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + std::shared_ptr UntilFormula::substitute(std::map const& substitution) const { return std::make_shared(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution)); } diff --git a/src/logic/UntilFormula.h b/src/logic/UntilFormula.h index 87ceef806..887d39b45 100644 --- a/src/logic/UntilFormula.h +++ b/src/logic/UntilFormula.h @@ -14,8 +14,10 @@ namespace storm { } virtual bool isUntilFormula() const override; - virtual bool isValidProbabilityPathFormula() const override; + virtual bool isProbabilityPathFormula() const override; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + virtual std::shared_ptr substitute(std::map const& substitution) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 56a65b39e..e7fabdec1 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -17,11 +17,15 @@ namespace storm { if (formula.isStateFormula()) { return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); } else if (formula.isPathFormula()) { - if (checkTask.computeProbabilities()) { + if (formula.isProbabilityPathFormula()) { return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula())); - } else if (checkTask.computeRewards()) { + } else if (formula.isRewardPathFormula()) { return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula())); } + } else if (formula.isConditionalProbabilityFormula()) { + return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula())); + } else if (formula.isConditionalRewardFormula()) { + return this->computeConditionalRewards(checkTask.substituteFormula(formula.asConditionalFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -30,8 +34,6 @@ namespace storm { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); if (pathFormula.isBoundedUntilFormula()) { return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(pathFormula.asBoundedUntilFormula())); - } else if (pathFormula.isConditionalPathFormula()) { - return this->computeConditionalProbabilities(checkTask.substituteFormula(pathFormula.asConditionalPathFormula())); } else if (pathFormula.isEventuallyFormula()) { return this->computeEventuallyProbabilities(checkTask.substituteFormula(pathFormula.asEventuallyFormula())); } else if (pathFormula.isGloballyFormula()) { @@ -48,7 +50,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + std::unique_ptr AbstractModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } @@ -84,6 +86,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } + std::unique_ptr AbstractModelChecker::computeConditionalRewards(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + } + std::unique_ptr AbstractModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } @@ -171,8 +177,6 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); - STORM_LOG_THROW(stateFormula.getSubformula().isValidProbabilityPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); if (stateFormula.hasBound()) { @@ -185,8 +189,6 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula(); - STORM_LOG_THROW(stateFormula.getSubformula().isValidRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); - std::unique_ptr result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); if (checkTask.isBoundSet()) { diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index f827c99ff..c79302808 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -36,8 +36,8 @@ namespace storm { // The methods to compute probabilities for path formulas. virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeEventuallyProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask); @@ -45,6 +45,7 @@ namespace storm { // The methods to compute the rewards for path formulas. virtual std::unique_ptr computeRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeConditionalRewards(CheckTask const& checkTask); virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask); virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask); virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask); diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index a780ef168..8693f09f2 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -63,8 +63,6 @@ namespace storm { } } } else if (formula.isRewardOperatorFormula()) { - this->checkType = CheckType::Rewards; - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); @@ -82,7 +80,7 @@ namespace storm { */ template CheckTask substituteFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->checkType, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); } /*! @@ -91,27 +89,6 @@ namespace storm { FormulaType const& getFormula() const { return formula.get(); } - - /*! - * Retrieves whether probabilities are to be computed. - */ - bool computeProbabilities() const { - return checkType == CheckType::Probabilities; - } - - /*! - * Retrieves whether rewards are to be computed. - */ - bool computeRewards() const { - return checkType == CheckType::Rewards; - } - - /*! - * Retrieves the type of this task. - */ - CheckType getCheckType() const { - return checkType; - } /*! * Retrieves whether an optimization direction was set. @@ -211,7 +188,6 @@ namespace storm { * Creates a task object with the given options. * * @param formula The formula to attach to the task. - * @param checkType The type of task: whether to compute probabilities or rewards. * @param optimizationDirection If set, the probabilities will be minimized/maximized. * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values @@ -222,16 +198,13 @@ namespace storm { * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, CheckType checkType, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), checkType(checkType), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } // The formula that is to be checked. std::reference_wrapper formula; - // A type indicating whether probabilities or rewards are to be computed. - CheckType checkType; - // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection;