From 56e70c3417e93e54c08a7901e7e707bdd5b5596a Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 4 Mar 2021 13:57:18 +0100 Subject: [PATCH] setBoundedGloballyFormulasAllowed in FragmentSpecification.* --- src/storm/logic/FragmentSpecification.cpp | 10 ++++++++++ src/storm/logic/FragmentSpecification.h | 4 ++++ 2 files changed, 14 insertions(+) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 1e7e1f357..dc93f7f9c 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -68,6 +68,7 @@ namespace storm { rpatl.setUntilFormulasAllowed(true); rpatl.setGloballyFormulasAllowed(true); rpatl.setNextFormulasAllowed(true); + rpatl.setBoundedGloballyFormulasAllowed(true); return rpatl; } @@ -316,6 +317,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areBoundedGloballyFormulasAllowed() const { + return boundedGloballyFormula; + } + + FragmentSpecification& FragmentSpecification::setBoundedGloballyFormulasAllowed(bool newValue) { + this->boundedGloballyFormula = newValue; + return *this; + } + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { return atomicExpressionFormula; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 8ac56b885..f097e940f 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -52,6 +52,9 @@ namespace storm { bool areBoundedUntilFormulasAllowed() const; FragmentSpecification& setBoundedUntilFormulasAllowed(bool newValue); + bool areBoundedGloballyFormulasAllowed() const; + FragmentSpecification& setBoundedGloballyFormulasAllowed(bool newValue); + bool areAtomicExpressionFormulasAllowed() const; FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue); @@ -176,6 +179,7 @@ namespace storm { bool nextFormula; bool untilFormula; bool boundedUntilFormula; + bool boundedGloballyFormula; bool atomicExpressionFormula; bool atomicLabelFormula;