Browse Source

added GameFormula class

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
6dd9e09ede
  1. 34
      src/storm/logic/GameFormula.cpp
  2. 35
      src/storm/logic/GameFormula.h

34
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<Formula const> 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;
}
}
}

35
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 <memory>
namespace storm {
namespace logic {
class GameFormula : public Formula {
public:
GameFormula(Coalition coalition, std::shared_ptr<Formula const> 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<Formula const> subformula;
};
}
}
#endif /* STORM_LOGIC_GAMEFORMULA_H_ */
Loading…
Cancel
Save