Browse Source

fixup after merging PRs

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
8b74f49806
  1. 12
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  2. 2
      src/storm/logic/GameFormula.h
  3. 1
      src/storm/models/sparse/Smg.cpp

12
src/storm-parsers/parser/FormulaParserGrammar.cpp

@ -140,18 +140,6 @@ namespace storm {
gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
gameFormula.name("game formula"); gameFormula.name("game formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
coalitionOperator = (qi::lit("<<")
> *( (identifier[phoenix::push_back(qi::_a, qi::_1)]
| qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ','
)
> qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)];
coalitionOperator.name("coalition operator");
gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
gameFormula.name("game formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
stateFormula.name("state formula"); stateFormula.name("state formula");

2
src/storm/logic/GameFormula.h

@ -20,6 +20,8 @@ namespace storm {
virtual bool hasQualitativeResult() const override; virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override; virtual bool hasQuantitativeResult() const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
virtual std::ostream& writeToStream(std::ostream& out) const override; virtual std::ostream& writeToStream(std::ostream& out) const override;

1
src/storm/models/sparse/Smg.cpp

@ -38,6 +38,7 @@ namespace storm {
storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerOfState(uint64_t stateIndex) const { storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerOfState(uint64_t stateIndex) const {
STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << "."); STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << ".");
return statePlayerIndications[stateIndex]; return statePlayerIndications[stateIndex];
}
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerIndex(std::string const& playerName) const { storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerIndex(std::string const& playerName) const {

Loading…
Cancel
Save