From 972df056835164c080761d831968c74ffa255e25 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 08:17:14 +0100 Subject: [PATCH] store tuples of player name and index Store this instead of only the index. Needed for easier parsing of the rpatl formulas (prism allows player indices and names!) --- src/storm/generator/Choice.cpp | 56 +++++++++---------- src/storm/generator/Choice.h | 18 +++--- src/storm/logic/Coalition.cpp | 25 +++++++++ src/storm/logic/Coalition.h | 32 +++++++++++ ...deterministicGameInfiniteHorizonHelper.cpp | 2 +- ...ondeterministicGameInfiniteHorizonHelper.h | 4 +- 6 files changed, 97 insertions(+), 40 deletions(-) create mode 100644 src/storm/logic/Coalition.cpp create mode 100644 src/storm/logic/Coalition.h diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index a0efb04f9..27ae916d1 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -11,30 +11,30 @@ namespace storm { namespace generator { - + template Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), rewards(), labels() { // Intentionally left empty. } - + template void Choice::add(Choice const& other) { STORM_LOG_THROW(this->markovian == other.markovian, storm::exceptions::InvalidOperationException, "Type of choices do not match."); STORM_LOG_THROW(this->actionIndex == other.actionIndex, storm::exceptions::InvalidOperationException, "Action index of choices do not match."); STORM_LOG_THROW(this->rewards.size() == other.rewards.size(), storm::exceptions::InvalidOperationException, "Reward value sizes of choices do not match."); - + // Add the elements to the distribution. this->distribution.add(other.distribution); - + // Update the total mass of the choice. this->totalMass += other.totalMass; - + // Add all reward values. auto otherRewIt = other.rewards.begin(); for (auto& rewardValue : this->rewards) { rewardValue += *otherRewIt; } - + // Join label sets and origin data if given. if (other.labels) { this->addLabels(other.labels.get()); @@ -43,27 +43,27 @@ namespace storm { this->addOriginData(other.originData.get()); } } - + template typename storm::storage::Distribution::iterator Choice::begin() { return distribution.begin(); } - + template typename storm::storage::Distribution::const_iterator Choice::begin() const { return distribution.cbegin(); } - + template typename storm::storage::Distribution::iterator Choice::end() { return distribution.end(); } - + template typename storm::storage::Distribution::const_iterator Choice::end() const { return distribution.cend(); } - + template void Choice::addLabel(std::string const& newLabel) { if (!labels) { @@ -71,7 +71,7 @@ namespace storm { } labels->insert(newLabel); } - + template void Choice::addLabels(std::set const& newLabels) { if (labels) { @@ -97,8 +97,8 @@ namespace storm { } template - bool Choice::hasPlayerIndex() const { - return playerIndex.is_initialized(); + bool Choice::hasPlayer() const { + return player.is_initialized(); } template @@ -113,7 +113,7 @@ namespace storm { } else { if (!data.empty()) { // Reaching this point means that the both the existing and the given data are non-empty - + auto existingDataAsIndexSet = boost::any_cast>(&this->originData.get()); if (existingDataAsIndexSet != nullptr) { auto givenDataAsIndexSet = boost::any_cast>(&data); @@ -125,63 +125,63 @@ namespace storm { } } } - + template bool Choice::hasOriginData() const { return originData.is_initialized(); } - + template boost::any const& Choice::getOriginData() const { return originData.get(); } - + template uint_fast64_t Choice::getActionIndex() const { return actionIndex; } - + template ValueType Choice::getTotalMass() const { return totalMass; } - + template void Choice::addProbability(StateType const& state, ValueType const& value) { totalMass += value; distribution.addProbability(state, value); } - + template void Choice::addReward(ValueType const& value) { rewards.push_back(value); } - + template void Choice::addRewards(std::vector&& values) { this->rewards = std::move(values); } - + template std::vector const& Choice::getRewards() const { return rewards; } - + template bool Choice::isMarkovian() const { return markovian; } - + template std::size_t Choice::size() const { return distribution.size(); } - + template void Choice::reserve(std::size_t const& size) { distribution.reserve(size); } - + template std::ostream& operator<<(std::ostream& out, Choice const& choice) { out << "<"; @@ -191,7 +191,7 @@ namespace storm { out << ">"; return out; } - + template struct Choice; #ifdef STORM_HAVE_CARL diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 31842ddee..445560939 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -13,51 +13,51 @@ namespace storm { namespace generator { - + // A structure holding information about a particular choice. template struct Choice { public: Choice(uint_fast64_t actionIndex = 0, bool markovian = false); - + Choice(Choice const& other) = default; Choice& operator=(Choice const& other) = default; Choice(Choice&& other) = default; Choice& operator=(Choice&& other) = default; - + /*! * Adds the given choice to the current one. */ void add(Choice const& other); - + /*! * Returns an iterator to the distribution associated with this choice. * * @return An iterator to the first element of the distribution. */ typename storm::storage::Distribution::iterator begin(); - + /*! * Returns an iterator to the distribution associated with this choice. * * @return An iterator to the first element of the distribution. */ typename storm::storage::Distribution::const_iterator begin() const; - + /*! * Returns an iterator past the end of the distribution associated with this choice. * * @return An iterator past the end of the distribution. */ typename storm::storage::Distribution::iterator end(); - + /*! * Returns an iterator past the end of the distribution associated with this choice. * * @return An iterator past the end of the distribution. */ typename storm::storage::Distribution::const_iterator end() const; - + /*! * Inserts the contents of this object to the given output stream. * @@ -102,7 +102,7 @@ namespace storm { /*! * Returns whether there is an index for the player defined for this choice. */ - bool hasPlayerIndex() const; + bool hasPlayer() const; /*! * Retrieves the players index associated with this choice diff --git a/src/storm/logic/Coalition.cpp b/src/storm/logic/Coalition.cpp new file mode 100644 index 000000000..baa0736c4 --- /dev/null +++ b/src/storm/logic/Coalition.cpp @@ -0,0 +1,25 @@ +#include "storm/logic/Coalition.h" + +namespace storm { + namespace logic { + + Coalition::Coalition(std::vector> playerIds) : playerIds(playerIds) { + // Intentionally left empty. + } + + std::vector> Coalition::getPlayerIds() const { + return playerIds; + } + + std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) { + bool firstItem = true; + stream << "<<"; + for (auto const& id : coalition.playerIds) { + if(firstItem) { firstItem = false; } else { stream << ","; } + stream << id; + } + stream << ">> "; + return stream; + } + } +} diff --git a/src/storm/logic/Coalition.h b/src/storm/logic/Coalition.h new file mode 100644 index 000000000..9f3966dd1 --- /dev/null +++ b/src/storm/logic/Coalition.h @@ -0,0 +1,32 @@ +#ifndef STORM_LOGIC_COALITION_H_ +#define STORM_LOGIC_COALITION_H_ + +#include +#include + +#include +#include +#include "storm/storage/BoostTypes.h" +#include "storm/utility/OsDetection.h" + +namespace storm { + namespace logic { + + class Coalition { + public: + Coalition() = default; + Coalition(std::vector>); + Coalition(Coalition const& other) = default; + + std::vector> getPlayerIds() const; + + friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition); + + private: + std::vector> playerIds; + }; + } +} + + +#endif /* STORM_LOGIC_COALITION_H_ */ diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index baaa3782d..03538c2e9 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -22,7 +22,7 @@ namespace storm { namespace helper { template - SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices) : SparseInfiniteHorizonHelper(transitionMatrix), coalitionIndices(coalitionIndices) { + SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player) : SparseInfiniteHorizonHelper(transitionMatrix), player(player) { // Intentionally left empty. } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h index 550d12a47..fd872b807 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h @@ -27,7 +27,7 @@ namespace storm { /*! * Initializes the helper for a discrete time model with different players (i.e. SMG) */ - SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices); + SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player); /*! * TODO @@ -57,7 +57,7 @@ namespace storm { std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues); private: - std::vector coalitionIndices; + std::vector> player; };