diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 06772b6ba..df79d22a5 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -57,6 +57,16 @@ namespace storm { return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } + boost::any FragmentChecker::visit(BoundedGloballyFormula const& f, boost::any const& data) const { + 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(BoundedUntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index c6e6100ee..0b0d179aa 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/src/storm/logic/FragmentChecker.h @@ -16,6 +16,7 @@ namespace storm { 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(BoundedGloballyFormula 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;