diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 6270d5664..d682d02aa 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -1,6 +1,9 @@ #include "src/logic/Formulas.h" #include +#include "src/logic/FragmentChecker.h" +#include "src/logic/FormulaInformationVisitor.h" + namespace storm { namespace logic { bool Formula::isPathFormula() const { @@ -111,6 +114,10 @@ namespace storm { return false; } + bool Formula::isReachabilityRewardFormula() const { + return false; + } + bool Formula::isLongRunAverageRewardFormula() const { return false; } @@ -131,6 +138,16 @@ namespace storm { return false; } + bool Formula::isInFragment(FragmentSpecification const& fragment) const { + FragmentChecker checker; + return checker.conformsToSpecification(*this, fragment); + } + + FormulaInformation Formula::info() const { + FormulaInformationVisitor visitor; + return visitor.getInformation(*this); + } + std::shared_ptr Formula::getTrueFormula() { return std::shared_ptr(new BooleanLiteralFormula(true)); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index ae879fce6..f2e06bc0b 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -19,8 +19,11 @@ namespace storm { // Forward-declare visitor for accept() method. class FormulaVisitor; - // Also foward-declare base model checker class. - class ModelChecker; + // Forward-declare fragment specification for isInFragment() method. + class FragmentSpecification; + + // Forward-declare formula information class for info() method. + class FormulaInformation; class Formula : public std::enable_shared_from_this { public: @@ -80,7 +83,10 @@ namespace storm { virtual bool isUnaryPathFormula() const; virtual bool isUnaryStateFormula() const; - virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const = 0; + bool isInFragment(FragmentSpecification const& fragment) const; + FormulaInformation info() const; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0; static std::shared_ptr getTrueFormula(); diff --git a/src/logic/FormulaInformation.cpp b/src/logic/FormulaInformation.cpp new file mode 100644 index 000000000..b49f4a23b --- /dev/null +++ b/src/logic/FormulaInformation.cpp @@ -0,0 +1,46 @@ +#include "src/logic/FormulaInformation.h" + +namespace storm { + namespace logic { + FormulaInformation::FormulaInformation() { + this->mContainsRewardOperator = false; + this->mContainsNextFormula = false; + this->mContainsBoundedUntilFormula = false; + } + + bool FormulaInformation::containsRewardOperator() const { + return this->mContainsRewardOperator; + } + + bool FormulaInformation::containsNextFormula() const { + return this->mContainsNextFormula; + } + + bool FormulaInformation::containsBoundedUntilFormula() const { + return this-mContainsBoundedUntilFormula; + } + + FormulaInformation FormulaInformation::join(FormulaInformation const& other) { + FormulaInformation result; + result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator(); + result.mContainsNextFormula = this->containsNextFormula() || other.containsNextFormula(); + result.mContainsBoundedUntilFormula = this->containsBoundedUntilFormula() || other.containsBoundedUntilFormula(); + return result; + } + + FormulaInformation& FormulaInformation::setContainsRewardOperator(bool newValue) { + this->mContainsRewardOperator = newValue; + return *this; + } + + FormulaInformation& FormulaInformation::setContainsNextFormula(bool newValue) { + this->mContainsNextFormula = newValue; + return *this; + } + + FormulaInformation& FormulaInformation::setContainsBoundedUntilFormula(bool newValue) { + this->mContainsBoundedUntilFormula = newValue; + return *this; + } + } +} \ No newline at end of file diff --git a/src/logic/FormulaInformation.h b/src/logic/FormulaInformation.h new file mode 100644 index 000000000..53269696c --- /dev/null +++ b/src/logic/FormulaInformation.h @@ -0,0 +1,29 @@ +#ifndef STORM_LOGIC_FORMULAINFORMATION_H_ +#define STORM_LOGIC_FORMULAINFORMATION_H_ + +namespace storm { + namespace logic { + + class FormulaInformation { + public: + FormulaInformation(); + bool containsRewardOperator() const; + bool containsNextFormula() const; + bool containsBoundedUntilFormula() const; + + FormulaInformation join(FormulaInformation const& other); + + FormulaInformation& setContainsRewardOperator(bool newValue = true); + FormulaInformation& setContainsNextFormula(bool newValue = true); + FormulaInformation& setContainsBoundedUntilFormula(bool newValue = true); + + private: + bool mContainsRewardOperator; + bool mContainsNextFormula; + bool mContainsBoundedUntilFormula; + }; + + } +} + +#endif /* STORM_LOGIC_FORMULAINFORMATION_H_ */ \ No newline at end of file diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp new file mode 100644 index 000000000..f8ef57f92 --- /dev/null +++ b/src/logic/FormulaInformationVisitor.cpp @@ -0,0 +1,85 @@ +#include "src/logic/FormulaInformationVisitor.h" + +#include "src/logic/Formulas.h" + +namespace storm { + namespace logic { + FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast(result); + } + + boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getLeftSubformula().accept(*this)).join(boost::any_cast(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula(); + } + + boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getSubformula().accept(*this)).join(boost::any_cast(f.getConditionFormula().accept(*this))); + } + + boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + + boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getSubformula().accept(*this)).setContainsNextFormula(); + } + + boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getSubformula().accept(*this)).setContainsRewardOperator(); + } + + boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this); + } + + boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const { + return boost::any_cast(f.getLeftSubformula().accept(*this)).join(boost::any_cast(f.getRightSubformula().accept(*this))); + } + + } +} \ No newline at end of file diff --git a/src/logic/FormulaInformationVisitor.h b/src/logic/FormulaInformationVisitor.h new file mode 100644 index 000000000..2e2cc0d6d --- /dev/null +++ b/src/logic/FormulaInformationVisitor.h @@ -0,0 +1,38 @@ +#ifndef STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ +#define STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ + +#include "src/logic/FormulaVisitor.h" +#include "src/logic/FormulaInformation.h" + +namespace storm { + namespace logic { + + class FormulaInformationVisitor : public FormulaVisitor { + public: + FormulaInformation getInformation(Formula const& f) 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_FORMULAINFORMATIONVISITOR_H_ */ \ No newline at end of file diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index d94056f58..405b75a27 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -4,49 +4,75 @@ namespace storm { namespace logic { + class InheritedInformation { + public: + InheritedInformation(FragmentSpecification const& fragmentSpecification) : fragmentSpecification(fragmentSpecification) { + // Intentionally left empty. + } + + FragmentSpecification const& getSpecification() const { + return fragmentSpecification; + } + + private: + FragmentSpecification const& fragmentSpecification; + }; + bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const { - boost::any result = f.accept(*this, specification); + boost::any result = f.accept(*this, InheritedInformation(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(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areAtomicExpressionFormulasAllowed(); } boost::any FragmentChecker::visit(AtomicLabelFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areAtomicLabelFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().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)); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areBinaryBooleanStateFormulasAllowed(); + 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(BooleanLiteralFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areBooleanLiteralFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - bool result = specification.areBoundedUntilFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getLeftSubformula().isPathFormula(); + result = result && !f.getRightSubformula().isPathFormula(); + } + if (f.hasDiscreteTimeBound()) { + result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed(); + } else { + result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed(); + } 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); + InheritedInformation const& inherited = boost::any_cast(data); bool result = true; if (f.isConditionalProbabilityFormula()) { - result &= specification.areConditionalProbabilityFormulasAllowed(); + result = result && inherited.getSpecification().areConditionalProbabilityFormulasAllowed(); } else if (f.Formula::isConditionalRewardFormula()) { - result &= specification.areConditionalRewardFormulasFormulasAllowed(); + result = result && inherited.getSpecification().areConditionalRewardFormulasFormulasAllowed(); + } + if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) { + result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula(); } result = result && boost::any_cast(f.getSubformula().accept(*this, data)); result = result && boost::any_cast(f.getConditionFormula().accept(*this, data)); @@ -54,65 +80,124 @@ namespace storm { } boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areCumulativeRewardFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areCumulativeRewardFormulasAllowed(); } boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - bool result = specification.areEventuallyFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = true; + if (f.isEventuallyFormula()) { + result = inherited.getSpecification().areEventuallyFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getSubformula().isPathFormula(); + } + } else if (f.isReachabilityRewardFormula()) { + result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed(); + result = result && f.getSubformula().isStateFormula(); + } else if (f.isReachbilityExpectedTimeFormula()) { + result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed(); + result = result && f.getSubformula().isStateFormula(); + } 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(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed(); + result = result && f.getSubformula().isExpectedTimePathFormula(); + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { + result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; } boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areGloballyFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areGloballyFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getSubformula().isPathFormula(); + } + result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; } boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areInstantaneousRewardFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areInstantaneousRewardFormulasAllowed(); } boost::any FragmentChecker::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areLongRunAverageOperatorsAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed(); + result = result && f.getSubformula().isStateFormula(); + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { + result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; } boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areLongRunAverageRewardFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); } boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areNextFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areNextFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getSubformula().isPathFormula(); + } + result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; } boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areProbabilityOperatorsAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); + result = result && f.getSubformula().isProbabilityPathFormula(); + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { + result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; } boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areRewardOperatorsAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areRewardOperatorsAllowed(); + result = result && f.getSubformula().isRewardPathFormula(); + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { + result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + } else { + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + return result; } boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areUnaryBooleanStateFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed(); + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); + return result; } boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const { - FragmentSpecification const& specification = boost::any_cast(data); - return specification.areUntilFormulasAllowed(); + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areUntilFormulasAllowed(); + if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { + result = result && !f.getLeftSubformula().isPathFormula(); + result = result && !f.getRightSubformula().isPathFormula(); + } + result = result && boost::any_cast(f.getLeftSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); + return result; } } } \ No newline at end of file diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index eeb697582..d8c02a18e 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -3,6 +3,99 @@ namespace storm { namespace logic { + FragmentSpecification propositional() { + FragmentSpecification propositional; + + propositional.setBooleanLiteralFormulasAllowed(true); + propositional.setBinaryBooleanStateFormulasAllowed(true); + propositional.setUnaryBooleanStateFormulasAllowed(true); + propositional.setAtomicExpressionFormulasAllowed(true); + propositional.setAtomicLabelFormulasAllowed(true); + + return propositional; + } + + FragmentSpecification pctl() { + FragmentSpecification pctl = propositional(); + + pctl.setProbabilityOperatorsAllowed(true); + pctl.setGloballyFormulasAllowed(true); + pctl.setEventuallyFormulasAllowed(true); + pctl.setNextFormulasAllowed(true); + pctl.setUntilFormulasAllowed(true); + pctl.setBoundedUntilFormulasAllowed(true); + pctl.setStepBoundedUntilFormulasAllowed(true); + + return pctl; + } + + FragmentSpecification prctl() { + FragmentSpecification prctl = pctl(); + + prctl.setRewardOperatorsAllowed(true); + prctl.setCumulativeRewardFormulasAllowed(true); + prctl.setInstantaneousFormulasAllowed(true); + prctl.setReachabilityRewardFormulasAllowed(true); + prctl.setLongRunAverageOperatorsAllowed(true); + + return prctl; + } + + FragmentSpecification csl() { + FragmentSpecification csl = pctl(); + + csl.setTimeBoundedUntilFormulasAllowed(true); + + return csl; + } + + FragmentSpecification csrl() { + FragmentSpecification csrl; + + csrl.setRewardOperatorsAllowed(true); + csrl.setCumulativeRewardFormulasAllowed(true); + csrl.setInstantaneousFormulasAllowed(true); + csrl.setReachabilityRewardFormulasAllowed(true); + csrl.setLongRunAverageOperatorsAllowed(true); + + return csrl; + } + + FragmentSpecification::FragmentSpecification() { + probabilityOperator = false; + rewardOperator = false; + expectedTimeOperator = false; + longRunAverageOperator = false; + + globallyFormula = false; + eventuallyFormula = false; + nextFormula = false; + untilFormula = false; + boundedUntilFormula = false; + + atomicExpressionFormula = false; + atomicLabelFormula = false; + booleanLiteralFormula = false; + unaryBooleanStateFormula = false; + binaryBooleanStateFormula = false; + + cumulativeRewardFormula = false; + instantaneousRewardFormula = false; + reachabilityRewardFormula = false; + longRunAverageRewardFormula = false; + + conditionalProbabilityFormula = false; + conditionalRewardFormula = false; + + reachabilityExpectedTimeFormula = false; + + nestedOperators = true; + nestedPathFormulas = false; + onlyEventuallyFormuluasInConditionalFormulas = true; + stepBoundedUntilFormulas = false; + timeBoundedUntilFormulas = false; + } + FragmentSpecification FragmentSpecification::copy() const { return FragmentSpecification(*this); } @@ -205,5 +298,60 @@ namespace storm { return *this; } + bool FragmentSpecification::areNestedPathFormulasAllowed() const { + return this->nestedPathFormulas; + } + + FragmentSpecification& FragmentSpecification::setNestedPathFormulasAllowed(bool newValue) { + this->nestedPathFormulas = newValue; + return *this; + } + + bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const { + return this->onlyEventuallyFormuluasInConditionalFormulas; + } + + FragmentSpecification& FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue) { + this->onlyEventuallyFormuluasInConditionalFormulas = newValue; + return *this; + } + + bool FragmentSpecification::areStepBoundedUntilFormulasAllowed() const { + return this->stepBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setStepBoundedUntilFormulasAllowed(bool newValue) { + this->stepBoundedUntilFormulas = newValue; + return *this; + } + + bool FragmentSpecification::areTimeBoundedUntilFormulasAllowed() const { + return this->timeBoundedUntilFormulas; + } + + FragmentSpecification& FragmentSpecification::setTimeBoundedUntilFormulasAllowed(bool newValue) { + this->timeBoundedUntilFormulas = newValue; + return *this; + } + + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { + this->setProbabilityOperatorsAllowed(newValue); + this->setRewardOperatorsAllowed(newValue); + this->setLongRunAverageOperatorsAllowed(newValue); + this->setExpectedTimeOperatorsAllowed(newValue); + return *this; + } + + FragmentSpecification& FragmentSpecification::setExpectedTimeAllowed(bool newValue) { + this->setExpectedTimeOperatorsAllowed(newValue); + this->setReachbilityExpectedTimeFormulasAllowed(newValue); + return *this; + } + + FragmentSpecification& FragmentSpecification::setLongRunAverageProbabilitiesAllowed(bool newValue) { + this->setLongRunAverageOperatorsAllowed(newValue); + return *this; + } + } } \ No newline at end of file diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index 91099703f..1bd46f4f7 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -5,6 +5,12 @@ namespace storm { namespace logic { class FragmentSpecification { public: + FragmentSpecification(); + FragmentSpecification(FragmentSpecification const& other) = default; + FragmentSpecification(FragmentSpecification&& other) = default; + FragmentSpecification& operator=(FragmentSpecification const& other) = default; + FragmentSpecification& operator=(FragmentSpecification&& other) = default; + FragmentSpecification copy() const; bool areProbabilityOperatorsAllowed() const; @@ -73,6 +79,22 @@ namespace storm { bool areNestedOperatorsAllowed() const; FragmentSpecification& setNestedOperatorsAllowed(bool newValue); + bool areNestedPathFormulasAllowed() const; + FragmentSpecification& setNestedPathFormulasAllowed(bool newValue); + + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; + FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); + + bool areStepBoundedUntilFormulasAllowed() const; + FragmentSpecification& setStepBoundedUntilFormulasAllowed(bool newValue); + + bool areTimeBoundedUntilFormulasAllowed() const; + FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); + + FragmentSpecification& setOperatorsAllowed(bool newValue); + FragmentSpecification& setExpectedTimeAllowed(bool newValue); + FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); + private: // Flags that indicate whether it is legal to see such a formula. bool probabilityOperator; @@ -104,8 +126,27 @@ namespace storm { // Members that indicate certain restrictions. bool nestedOperators; - + bool nestedPathFormulas; + bool onlyEventuallyFormuluasInConditionalFormulas; + bool stepBoundedUntilFormulas; + bool timeBoundedUntilFormulas; }; + + // Propositional. + FragmentSpecification propositional(); + + // Regular PCTL. + FragmentSpecification pctl(); + + // PCTL + cumulative, instantaneous, reachability and long-run rewards. + FragmentSpecification prctl(); + + // Regular CSL. + FragmentSpecification csl(); + + // CSL + cumulative, instantaneous, reachability and long-run rewards. + FragmentSpecification csrl(); + } } diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 0e025c208..711f78789 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -32,6 +32,10 @@ namespace storm { return this->rewardModelName.get(); } + bool RewardOperatorFormula::hasRewardModelName() const { + return static_cast(rewardModelName); + } + boost::optional const& RewardOperatorFormula::getOptionalRewardModelName() const { return this->rewardModelName; } diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index e99c77057..3ff75a0e1 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -12,10 +12,6 @@ namespace storm { return true; } - boost::any UnaryStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { - return visitor.visit(*this, data); - } - Formula const& UnaryStateFormula::getSubformula() const { return *subformula; } diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index 1dcf00023..29149ebc8 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -14,8 +14,6 @@ namespace storm { } virtual bool isUnaryStateFormula() const override; - - virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; Formula const& getSubformula() const; diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index c6b7c9d1e..a08d7a6b1 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -10,6 +10,8 @@ #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" +#include "src/logic/FragmentSpecification.h" + namespace storm { namespace modelchecker { template @@ -25,7 +27,7 @@ namespace storm { template bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslFormula() || formula.isRewardFormula(); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } template diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e91547e81..ee545cb27 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -13,6 +13,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" @@ -32,7 +34,7 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula(); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } template diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index b5966bf4c..9892eb530 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -12,6 +12,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" @@ -30,7 +32,9 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isCslStateFormula() || formula.isCslPathFormula(); + storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true); + fragment.setExpectedTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true); + return formula.isInFragment(fragment); } template diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index b9b0bec0a..31628f4ed 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -17,6 +17,8 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidArgumentException.h" @@ -36,7 +38,7 @@ namespace storm { template bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isPctlStateFormula() || formula.isPctlPathFormula(); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true)); } template diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index cd39e8c62..f79bbb933 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -8,6 +8,8 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" @@ -30,16 +32,7 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { - return true; - } - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } - if (formula.isGloballyFormula()) { - return true; - } - return false; + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index dce8a8138..df7f1ee9a 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -11,6 +11,8 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" +#include "src/logic/FragmentSpecification.h" + #include "src/models/sparse/StandardRewardModel.h" #include "src/settings/modules/GeneralSettings.h" @@ -34,22 +36,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { - return true; - } - if (formula.isGloballyFormula()) { - return true; - } - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } - if (formula.isConditionalPathFormula()) { - storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); - if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { - return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); - } - } - return false; + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); } template @@ -129,13 +116,13 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { - storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); - STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); + STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index acc7d9283..264f1725d 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -24,7 +24,7 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index a7a56a890..614522e01 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -8,6 +8,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -39,22 +41,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { - return true; - } - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } - if (formula.isGloballyFormula()) { - return true; - } - if (formula.isConditionalPathFormula()) { - storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); - if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { - return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); - } - } - return false; + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); } template @@ -106,15 +93,15 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { - storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); - STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); - STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 37cd6ef5b..b08c9abc5 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -22,7 +22,7 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 2394a3176..311ef7590 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -10,6 +10,9 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" + +#include "src/logic/FragmentSpecification.h" + #include "src/solver/SymbolicLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" @@ -32,16 +35,7 @@ namespace storm { template bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { - return true; - } - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } - if (formula.isGloballyFormula()) { - return true; - } - return false; + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 9b74594dc..d6a3554e3 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -5,6 +5,8 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/models/symbolic/StandardRewardModel.h" #include "src/utility/macros.h" @@ -32,16 +34,7 @@ namespace storm { template bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) { - return true; - } - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } - if (formula.isGloballyFormula()) { - return true; - } - return false; + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); } template diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index f56843aef..aa947c8cb 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -10,6 +10,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidPropertyException.h" @@ -23,7 +25,7 @@ namespace storm { template bool SparsePropositionalModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isPropositionalFormula(); + return formula.isInFragment(storm::logic::propositional()); } template diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 943ecf7db..eee71e3c8 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -10,6 +10,8 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidPropertyException.h" @@ -23,7 +25,7 @@ namespace storm { template bool SymbolicPropositionalModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isPropositionalFormula(); + return formula.isInFragment(storm::logic::propositional()); } template diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 98afe49a1..7022b92c8 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -16,6 +16,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/logic/FragmentSpecification.h" + #include "src/utility/graph.h" #include "src/utility/vector.h" #include "src/utility/macros.h" @@ -82,45 +84,9 @@ namespace storm { template bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula())); - } else if (formula.isRewardOperatorFormula()) { - return this->canHandle(checkTask.substituteFormula(formula.asRewardOperatorFormula().getSubformula())); - } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { - if (formula.isUntilFormula()) { - storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); - if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isEventuallyFormula()) { - storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); - if (eventuallyFormula.getSubformula().isPropositionalFormula()) { - return true; - } - } - } else if (formula.isBoundedUntilFormula()) { - storm::logic::BoundedUntilFormula const& boundedUntilFormula = formula.asBoundedUntilFormula(); - if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isConditionalPathFormula()) { - storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); - if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { - return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); - } - } else if (formula.isLongRunAverageOperatorFormula()) { - storm::logic::LongRunAverageOperatorFormula const& longRunAverageOperatorFormula = formula.asLongRunAverageOperatorFormula(); - if (longRunAverageOperatorFormula.getSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isLongRunAverageRewardFormula()) { - return true; - } - - else if (formula.isPropositionalFormula()) { - return true; - } - return false; + storm::logic::FragmentSpecification fragment = storm::logic::prctl().setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false); + fragment.setNestedOperatorsAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true); + return formula.isInFragment(fragment); } template @@ -646,15 +612,15 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { - storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. - STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); - STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); + STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); @@ -680,7 +646,7 @@ namespace storm { if (this->getModel().getInitialStates().isSubsetOf(statesWithProbability1)) { STORM_LOG_INFO("The condition holds with probability 1, so the regular reachability probability is computed."); std::shared_ptr trueFormula = std::make_shared(true); - std::shared_ptr untilFormula = std::make_shared(trueFormula, pathFormula.getLeftSubformula().asSharedPointer()); + std::shared_ptr untilFormula = std::make_shared(trueFormula, conditionalFormula.getSubformula().asSharedPointer()); return this->computeUntilProbabilities(*untilFormula); } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index af5b464be..8b86e1dd9 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -28,7 +28,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 1298b3fa2..983f64cae 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -120,8 +120,8 @@ namespace storm { qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - qi::rule(bool), Skipper> conditionalFormula; - qi::rule(bool), Skipper> eventuallyFormula; + qi::rule(storm::logic::ConditionalFormula::Context), Skipper> conditionalFormula; + qi::rule(storm::logic::EventuallyFormula::Context), Skipper> eventuallyFormula; qi::rule(), Skipper> nextFormula; qi::rule(), Skipper> globallyFormula; qi::rule(), Skipper> untilFormula; @@ -142,11 +142,11 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, bool reward) const; + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::ConditionalFormula::Context context) const; std::pair, boost::optional>> createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; @@ -253,7 +253,7 @@ namespace storm { cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - rewardPathFormula = eventuallyFormula(true) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(true); + rewardPathFormula = eventuallyFormula(storm::logic::EventuallyFormula::Context::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(storm::logic::ConditionalFormula::Context::Reward); rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -286,7 +286,7 @@ namespace storm { nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - pathFormulaWithoutUntil = eventuallyFormula(false) | globallyFormula | nextFormula | stateFormula; + pathFormulaWithoutUntil = eventuallyFormula(storm::logic::EventuallyFormula::Context::Probability) | globallyFormula | nextFormula | stateFormula; pathFormulaWithoutUntil.name("path formula"); untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; @@ -298,7 +298,7 @@ namespace storm { timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; timeBound.name("time bound"); - pathFormula = conditionalFormula(false); + pathFormula = conditionalFormula(storm::logic::ConditionalFormula::Context::Probability); pathFormula.name("path formula"); operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; @@ -313,7 +313,7 @@ namespace storm { rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; rewardOperator.name("reward operator"); - expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(true) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::EventuallyFormula::Context::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; expectedTimeOperator.name("expected time operator"); probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -422,7 +422,7 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); @@ -431,7 +431,7 @@ namespace storm { return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); } } else { - return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, reward)); + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } } @@ -456,8 +456,8 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, bool reward) const { - return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula, reward)); + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::ConditionalFormula::Context context) const { + return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); } std::pair, boost::optional>> FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 902a69288..aedd4a998 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -15,6 +15,9 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/logic/FormulaInformation.h" +#include "src/logic/FragmentSpecification.h" + #include "src/utility/macros.h" #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidOptionException.h" @@ -55,11 +58,14 @@ namespace storm { phiStates = boost::none; psiStates = boost::none; + // Retrieve information about formula. + storm::logic::FormulaInformation info = formula.info(); + // Preserve rewards if necessary. - keepRewards = keepRewards || formula.containsRewardOperator(); + keepRewards = keepRewards || info.containsRewardOperator(); // Preserve bounded properties if necessary. - bounded = bounded || (formula.containsBoundedUntilFormula() || formula.containsNextFormula()); + bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula()); // Compute the relevant labels and expressions. this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas()); @@ -67,10 +73,13 @@ namespace storm { template void BisimulationDecomposition::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) { - keepRewards = formula.containsRewardOperator(); + // Retrieve information about formula. + storm::logic::FormulaInformation info = formula.info(); + + keepRewards = info.containsRewardOperator(); // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula. - bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula(); + bounded = info.containsBoundedUntilFormula() || info.containsNextFormula(); // Compute the relevant labels and expressions. this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas()); @@ -114,12 +123,12 @@ namespace storm { if (newFormula->isUntilFormula()) { leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer(); rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer(); - if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) { + if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) { measureDrivenInitialPartition = true; } } else if (newFormula->isEventuallyFormula()) { rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); - if (rightSubformula->isPropositionalFormula()) { + if (rightSubformula->isInFragment(storm::logic::propositional())) { measureDrivenInitialPartition = true; } } diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp new file mode 100644 index 000000000..6f21467af --- /dev/null +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -0,0 +1,14 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/FragmentSpecification.h" +#include "src/exceptions/WrongFormatException.h" + +TEST(FragmentCheckerTest, PctlTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "\"label\""; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + +} diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index 15f116125..a3d78632b 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/FormulaParser.h" +#include "src/logic/FragmentSpecification.h" #include "src/exceptions/WrongFormatException.h" TEST(FormulaParserTest, LabelTest) { @@ -20,7 +21,7 @@ TEST(FormulaParserTest, ComplexLabelTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); } @@ -35,7 +36,7 @@ TEST(FormulaParserTest, ExpressionTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); } @@ -50,11 +51,11 @@ TEST(FormulaParserTest, LabelAndExpressionTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); input = "x | y > 3 | !\"a\""; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isPropositionalFormula()); + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); } TEST(FormulaParserTest, ProbabilityOperatorTest) { @@ -98,7 +99,7 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) { EXPECT_TRUE(formula->isProbabilityOperatorFormula()); storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula(); - EXPECT_TRUE(probFormula.getSubformula().isConditionalPathFormula()); + EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); } TEST(FormulaParserTest, NestedPathFormulaTest) {