From 016ab53f423033b10cd0391635f81add60653821 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 10 Mar 2016 16:59:38 +0100 Subject: [PATCH] making the logic formulas better Former-commit-id: bd5dd26c51966c2c10405df2fdb1b8a6ee7e2adf --- src/logic/BinaryBooleanStateFormula.cpp | 5 ++++- src/logic/BinaryBooleanStateFormula.h | 2 +- src/logic/BinaryPathFormula.cpp | 8 ++++++++ src/logic/BinaryPathFormula.h | 3 +++ src/logic/ConditionalFormula.cpp | 8 ++++++++ src/logic/ConditionalFormula.h | 3 +++ src/logic/Formula.cpp | 8 ++++++++ src/logic/Formula.h | 4 ++++ src/logic/FragmentChecker.cpp | 6 ++++++ src/logic/FragmentSpecification.cpp | 22 ++++++++++++++++++++++ src/logic/FragmentSpecification.h | 8 ++++++++ src/logic/OperatorFormula.cpp | 8 ++++++++ src/logic/OperatorFormula.h | 3 +++ src/logic/UnaryBooleanStateFormula.cpp | 5 ++++- src/logic/UnaryPathFormula.cpp | 9 +++++++++ src/logic/UnaryPathFormula.h | 3 +++ 16 files changed, 102 insertions(+), 3 deletions(-) diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp index 180ea12c1..d6757e508 100644 --- a/src/logic/BinaryBooleanStateFormula.cpp +++ b/src/logic/BinaryBooleanStateFormula.cpp @@ -2,10 +2,13 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) { - // Intentionally left empty. + STORM_LOG_THROW(this->getLeftSubformula().hasQualitativeResult() && this->getRightSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result."); } bool BinaryBooleanStateFormula::isBinaryBooleanStateFormula() const { diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h index 6956e56c6..892d28bc9 100644 --- a/src/logic/BinaryBooleanStateFormula.h +++ b/src/logic/BinaryBooleanStateFormula.h @@ -25,7 +25,7 @@ namespace storm { virtual bool isAnd() const; virtual bool isOr() const; - + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual std::shared_ptr substitute(std::map const& substitution) const override; diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index 4e028d567..40c187013 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -32,5 +32,13 @@ namespace storm { this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); } + + bool BinaryPathFormula::hasQualitativeResult() const { + return false; + } + + bool BinaryPathFormula::hasQuantitativeResult() const { + return true; + } } } \ No newline at end of file diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index fe0526bee..5550bd466 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -24,6 +24,9 @@ namespace storm { virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + private: std::shared_ptr leftSubformula; std::shared_ptr rightSubformula; diff --git a/src/logic/ConditionalFormula.cpp b/src/logic/ConditionalFormula.cpp index af3e1d95b..b12b831be 100644 --- a/src/logic/ConditionalFormula.cpp +++ b/src/logic/ConditionalFormula.cpp @@ -49,6 +49,14 @@ namespace storm { this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels); } + bool ConditionalFormula::hasQualitativeResult() const { + return false; + } + + bool ConditionalFormula::hasQuantitativeResult() const { + return true; + } + std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const { this->getSubformula().writeToStream(out); out << " || "; diff --git a/src/logic/ConditionalFormula.h b/src/logic/ConditionalFormula.h index fc6b61655..66d71ebba 100644 --- a/src/logic/ConditionalFormula.h +++ b/src/logic/ConditionalFormula.h @@ -32,6 +32,9 @@ namespace storm { virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + private: std::shared_ptr subformula; std::shared_ptr conditionFormula; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 03ee2793d..c48548f10 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -142,6 +142,14 @@ namespace storm { return false; } + bool Formula::hasQualitativeResult() const { + return true; + } + + bool Formula::hasQuantitativeResult() const { + return false; + } + bool Formula::isInFragment(FragmentSpecification const& fragment) const { FragmentChecker checker; return checker.conformsToSpecification(*this, fragment); diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 85ee131f7..b77ecfb20 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -84,6 +84,10 @@ namespace storm { virtual bool isUnaryPathFormula() const; virtual bool isUnaryStateFormula() const; + // Accessors for the return type of a formula. + virtual bool hasQualitativeResult() const; + virtual bool hasQuantitativeResult() const; + bool isInFragment(FragmentSpecification const& fragment) const; FormulaInformation info() const; diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 50c5d3115..16e1d721c 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -110,6 +110,8 @@ namespace storm { boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areTimeOperatorsAllowed(); + result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed()); + result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && f.getSubformula().isTimePathFormula(); result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { @@ -165,6 +167,8 @@ namespace storm { boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); + result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed()); + result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula()); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); @@ -177,6 +181,8 @@ namespace storm { boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areRewardOperatorsAllowed(); + result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed()); + result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index c2e396ec9..31f2eeee2 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -97,6 +97,9 @@ namespace storm { stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; varianceAsMeasureType = false; + + qualitativeOperatorResults = true; + quantitativeOperatorResults = true; } FragmentSpecification FragmentSpecification::copy() const { @@ -364,6 +367,25 @@ namespace storm { this->varianceAsMeasureType = newValue; return *this; } + + bool FragmentSpecification::areQuantitativeOperatorResultsAllowed() const { + return this->quantitativeOperatorResults; + } + + FragmentSpecification& FragmentSpecification::setQuantitativeOperatorResultsAllowed(bool newValue) { + this->quantitativeOperatorResults = newValue; + return *this; + } + + bool FragmentSpecification::areQualitativeOperatorResultsAllowed() const { + return this->qualitativeOperatorResults; + } + + FragmentSpecification& FragmentSpecification::setQualitativeOperatorResultsAllowed(bool newValue) { + this->qualitativeOperatorResults = newValue; + return *this; + } + } } \ No newline at end of file diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index d9ae9e45d..5074187b8 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -94,6 +94,12 @@ namespace storm { bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); + bool areQuantitativeOperatorResultsAllowed() const; + FragmentSpecification& setQuantitativeOperatorResultsAllowed(bool newValue); + + bool areQualitativeOperatorResultsAllowed() const; + FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue); + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -134,6 +140,8 @@ namespace storm { bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; bool varianceAsMeasureType; + bool quantitativeOperatorResults; + bool qualitativeOperatorResults; }; // Propositional. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 97690d7bf..d7f602ebe 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -69,6 +69,14 @@ namespace storm { return true; } + bool OperatorFormula::hasQualitativeResult() const { + return this->hasBound(); + } + + bool OperatorFormula::hasQuantitativeResult() const { + return !this->hasBound(); + } + std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { out << "[" << this->operatorInformation.measureType << "]"; if (hasOptimalityType()) { diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 43c97ea45..3d8de1dcd 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -46,6 +46,9 @@ namespace storm { // Measure-type-related accessors. MeasureType getMeasureType() const; + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; protected: diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp index 6d4f9ecdd..3983e5b27 100644 --- a/src/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -2,10 +2,13 @@ #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) { - // Intentionally left empty. + STORM_LOG_THROW(this->getSubformula().hasQualitativeResult(), storm::exceptions::InvalidPropertyException, "Boolean formula must have subformulas with qualitative result."); } bool UnaryBooleanStateFormula::isUnaryBooleanStateFormula() const { diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index 3e0cdaebc..415fb4d4c 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -25,5 +25,14 @@ namespace storm { void UnaryPathFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); } + + bool UnaryPathFormula::hasQualitativeResult() const { + return false; + } + + bool UnaryPathFormula::hasQuantitativeResult() const { + return true; + } + } } \ No newline at end of file diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index 3ea27d8f5..bc698338c 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -23,6 +23,9 @@ namespace storm { virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + private: std::shared_ptr subformula; };