Browse Source

small changes and added TODOs in class BoundedGloballyFormula

tempestpy_adaptions
Lukas Posch 4 years ago
parent
commit
9976b927f9
  1. 2
      src/storm/logic/BoundedGloballyFormula.cpp
  2. 7
      src/storm/logic/BoundedGloballyFormula.h

2
src/storm/logic/BoundedGloballyFormula.cpp

@ -3,6 +3,7 @@
namespace storm {
namespace logic {
// TODO: add 'k' as input to formula, maybe as TimeBound?
BoundedGloballyFormula::BoundedGloballyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
// Intentionally left empty.
}
@ -21,6 +22,7 @@ namespace storm {
std::ostream& BoundedGloballyFormula::writeToStream(std::ostream& out) const {
out << "G < ";
// TODO: write "{<, <=} k"
this->getSubformula().writeToStream(out);
return out;
}

7
src/storm/logic/BoundedGloballyFormula.h

@ -1,5 +1,5 @@
#ifndef STORM_BOUNDEDGLOBALLYFORMULA_H
#define STORM_BOUNDEDGLOBALLYFORMULA_H
#ifndef STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H
#define STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H
#include "storm/logic/UnaryPathFormula.h"
@ -17,9 +17,10 @@ namespace storm {
virtual bool isProbabilityPathFormula() const override;
virtual boost::any accept(FormulaVisitor const &visitor, boost::any const &data) const override;
virtual std::ostream &writeToStream(std::ostream &out) const override;
};
}
}
#endif //STORM_BOUNDEDGLOBALLYFORMULA_H
#endif /* STORM_LOGIC_BOUNDEDGLOBALLYFORMULA_H */
Loading…
Cancel
Save