diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index d5359875a..70379b8ba 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -79,10 +79,6 @@ namespace storm { return false; } - bool Formula::isBoundedGloballyFormula() const { - return false; - } - bool Formula::isGloballyFormula() const { return false; } @@ -119,6 +115,10 @@ namespace storm { return false; } + bool Formula::isBoundedGloballyFormula() const { + return false; + } + bool Formula::isLongRunAverageOperatorFormula() const { return false; } @@ -377,6 +377,15 @@ namespace storm { return dynamic_cast(*this); } + // TODO: find out why these casts are not valid + BoundedGloballyFormula& Formula::asBoundedGloballyFormula() { + return dynamic_cast(*this); + } + + BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const { + return dynamic_cast(*this); + } + LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() { return dynamic_cast(*this); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index 24c288619..62aab0dde 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -173,7 +173,10 @@ namespace storm { NextFormula& asNextFormula(); NextFormula const& asNextFormula() const; - + + BoundedGloballyFormula& asBoundedGloballyFormula(); + BoundedGloballyFormula const& asBoundedGloballyFormula() const; + LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula(); LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;