Browse Source

Set up BoundedGloballyFormula to methods of Formula.*

tempestpy_adaptions
Lukas Posch 4 years ago
parent
commit
c142922182
  1. 17
      src/storm/logic/Formula.cpp
  2. 5
      src/storm/logic/Formula.h

17
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<NextFormula const&>(*this);
}
// TODO: find out why these casts are not valid
BoundedGloballyFormula& Formula::asBoundedGloballyFormula() {
return dynamic_cast<BoundedGloballyFormula&>(*this);
}
BoundedGloballyFormula const& Formula::asBoundedGloballyFormula() const {
return dynamic_cast<BoundedGloballyFormula const &>(*this);
}
LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() {
return dynamic_cast<LongRunAverageOperatorFormula&>(*this);
}

5
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;

Loading…
Cancel
Save