diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp new file mode 100644 index 000000000..8e42f7e65 --- /dev/null +++ b/src/storm/logic/GameFormula.cpp @@ -0,0 +1,34 @@ +#include "storm/logic/GameFormula.h" + +#include "storm/logic/FormulaVisitor.h" + +namespace storm { + namespace logic { + GameFormula::GameFormula(Coalition coalition, std::shared_ptr subFormula) : coalition(coalition), subformula(subformula) { + STORM_PRINT_AND_LOG("CTOR subf usecount:" << subformula.use_count() << std::endl); + // Intentionally left empty. + } + + bool GameFormula::isGameFormula() const { + return true; + } + + Formula const& GameFormula::getSubformula() const { + return *subformula; + } + + Coalition GameFormula::getCoalition() const { + return coalition; + } + + boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + std::ostream& GameFormula::writeToStream(std::ostream& out) const { + out << coalition; + this->getSubformula().writeToStream(out); + return out; + } + } +} diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h new file mode 100644 index 000000000..81384ddcf --- /dev/null +++ b/src/storm/logic/GameFormula.h @@ -0,0 +1,35 @@ +#ifndef STORM_LOGIC_GAMEFORMULA_H_ +#define STORM_LOGIC_GAMEFORMULA_H_ + +#include "storm/logic/Formula.h" +#include "storm/logic/Coalition.h" +#include + +namespace storm { + namespace logic { + class GameFormula : public Formula { + public: + GameFormula(Coalition coalition, std::shared_ptr subFormula); + + ~GameFormula() { + // Intentionally left empty. + } + + bool isGameFormula() const; + + Formula const& getSubformula() const; + Coalition getCoalition() const; + + boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const; + + std::ostream& writeToStream(std::ostream& out) const; + + private: + Coalition coalition; + std::shared_ptr subformula; + + }; + } +} + +#endif /* STORM_LOGIC_GAMEFORMULA_H_ */