diff --git a/src/storm/builder/ChoiceInformationBuilder.cpp b/src/storm/builder/ChoiceInformationBuilder.cpp
deleted file mode 100644
index 6578fe590..000000000
--- a/src/storm/builder/ChoiceInformationBuilder.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-#include "storm/builder/ChoiceInformationBuilder.h"
-
-namespace storm {
- namespace builder {
-
- void ChoiceInformationBuilder::addLabel(std::string const& label, uint_fast64_t choiceIndex) {
- storm::storage::BitVector& labeledChoices = labels[label];
- labeledChoices.grow(choiceIndex + 1);
- labeledChoices.set(choiceIndex, true);
- }
-
- void ChoiceInformationBuilder::addOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
- if (dataOfOrigins.size() != choiceIndex) {
- dataOfOrigins.resize(choiceIndex);
- }
- dataOfOrigins.push_back(originData);
- }
-
- boost::optional<storm::models::sparse::ChoiceLabeling> ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
- if (labels.empty()) {
- return boost::none;
- } else {
- storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
- for (auto& label : labels) {
- label.second.resize(totalNumberOfChoices, false);
- result.addLabel(label.first, std::move(label.second));
- }
- return result;
- }
- }
-
- std::vector<boost::any> ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
- dataOfOrigins.resize(totalNumberOfChoices);
- return std::move(dataOfOrigins);
- }
-
- }
-}
diff --git a/src/storm/builder/ChoiceInformationBuilder.h b/src/storm/builder/ChoiceInformationBuilder.h
deleted file mode 100644
index 8dbe8721a..000000000
--- a/src/storm/builder/ChoiceInformationBuilder.h
+++ /dev/null
@@ -1,40 +0,0 @@
-#pragma once
-
-#include <memory>
-#include <string>
-#include <unordered_map>
-#include <vector>
-#include <boost/any.hpp>
-
-#include "storm/models/sparse/ChoiceLabeling.h"
-#include "storm/storage/BitVector.h"
-#include "storm/storage/sparse/PrismChoiceOrigins.h"
-#include "storm/storage/prism/Program.h"
-
-
-namespace storm {
- namespace builder {
-
- /*!
- * This class collects information regarding the choices
- */
- class ChoiceInformationBuilder {
- public:
-
- ChoiceInformationBuilder() = default;
-
- void addLabel(std::string const& label, uint_fast64_t choiceIndex);
-
- void addOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
-
- boost::optional<storm::models::sparse::ChoiceLabeling> buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
-
- std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
-
- private:
- std::unordered_map<std::string, storm::storage::BitVector> labels;
- std::vector<boost::any> dataOfOrigins;
- };
- }
-}
-
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 10e0c8927..b80825d1d 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -4,7 +4,7 @@
#include "storm/builder/RewardModelBuilder.h"
-#include "storm/builder/ChoiceInformationBuilder.h"
+#include "storm/builder/StateAndChoiceInformationBuilder.h"
#include "storm/exceptions/AbortException.h"
#include "storm/exceptions/WrongFormatException.h"
@@ -120,18 +120,11 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename StateType>
- void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
+ void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder) {
- // Create markovian states bit vector, if required.
- if (generator->getModelType() == storm::generator::ModelType::MA) {
- // The bit vector will be resized when the correct size is known.
- markovianStates = storm::storage::BitVector(1000);
- }
-
- // Create the player indices vector, if required.
- if (generator->getModelType() == storm::generator::ModelType::SMG) {
- playerActionIndices = std::vector<uint_fast32_t>{};
- playerActionIndices.get().reserve(1000);
+ // Initialize building state valuations (if necessary)
+ if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+ stateAndChoiceInformationBuilder.stateValuationsBuilder() = generator->initializeStateValuationsBuilder();
}
// Create a callback for the next-state generator to enable it to request the index of states.
@@ -175,8 +168,8 @@ namespace storm {
}
generator->load(currentState);
- if (stateValuationsBuilder) {
- generator->addStateValuation(currentIndex, stateValuationsBuilder.get());
+ if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+ generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder());
}
storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
@@ -188,11 +181,6 @@ namespace storm {
this->stateStorage.deadlockStateIndices.push_back(currentIndex);
}
- if (markovianStates) {
- markovianStates.get().grow(currentRowGroup + 1, false);
- markovianStates.get().set(currentRowGroup);
- }
-
if (!generator->isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
@@ -208,11 +196,14 @@ namespace storm {
rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>());
}
}
-
- if (playerActionIndices) {
- // TODO change this to storm::utility::infinity<ValueType>() ?
- playerActionIndices.get().push_back(-1);
+
+ // This state shall be Markovian (to not introduce Zeno behavior)
+ if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) {
+ stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup);
}
+ // Other state-based information does not need to be treated, in particular:
+ // * StateValuations have already been set above
+ // * The associated player shall be the "default" player, i.e. INVALID_PLAYER_INDEX
++currentRow;
++currentRowGroup;
@@ -235,22 +226,26 @@ namespace storm {
}
// Now add all choices.
+ bool firstChoiceOfState = true;
for (auto const& choice : behavior) {
// add the generated choice information
- if (choice.hasLabels()) {
+ if (stateAndChoiceInformationBuilder.isBuildChoiceLabels() && choice.hasLabels()) {
for (auto const& label : choice.getLabels()) {
- choiceInformationBuilder.addLabel(label, currentRow);
+ stateAndChoiceInformationBuilder.addChoiceLabel(label, currentRow);
}
}
- if (choice.hasOriginData()) {
- choiceInformationBuilder.addOriginData(choice.getOriginData(), currentRow);
+ if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins() && choice.hasOriginData()) {
+ stateAndChoiceInformationBuilder.addChoiceOriginData(choice.getOriginData(), currentRow);
}
-
- // If we keep track of the Markovian choices, store whether the current one is Markovian.
- if (markovianStates && choice.isMarkovian()) {
- markovianStates.get().grow(currentRowGroup + 1, false);
- markovianStates.get().set(currentRowGroup);
+ if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications() && choice.hasPlayerIndex()) {
+ STORM_LOG_ASSERT(firstChoiceOfState || stateAndChoiceInformationBuilder.hasStatePlayerIndicationBeenSet(choice.getPlayerIndex(), currentRowGroup), "There is a state where different players have an enabled choice."); // Should have been detected in generator, already
+ if (firstChoiceOfState) {
+ stateAndChoiceInformationBuilder.addStatePlayerIndication(choice.getPlayerIndex(), currentRowGroup);
+ }
+ }
+ if (stateAndChoiceInformationBuilder.isBuildMarkovianStates() && choice.isMarkovian()) {
+ stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup);
}
// Add the probabilistic behavior to the matrix.
@@ -267,11 +262,9 @@ namespace storm {
++choiceRewardIt;
}
++currentRow;
+ firstChoiceOfState = false;
}
- if (playerActionIndices) {
- playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex());
- }
++currentRowGroup;
}
@@ -298,15 +291,6 @@ namespace storm {
}
}
- if (markovianStates) {
- // Since we now know the correct size, cut the bit vector to the correct length.
- markovianStates->resize(currentRowGroup, false);
- }
-
- if (playerActionIndices) {
- playerActionIndices.get().shrink_to_fit();
- }
-
// If the exploration order was not breadth-first, we need to fix the entries in the matrix according to
// (reversed) mapping of row groups to indices.
if (options.explorationOrder != ExplorationOrder::Bfs) {
@@ -348,39 +332,48 @@ namespace storm {
for (uint64_t i = 0; i < generator->getNumberOfRewardModels(); ++i) {
rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i));
}
- ChoiceInformationBuilder choiceInformationBuilder;
- boost::optional<storm::storage::BitVector> markovianStates;
- boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
-
- // If we need to build state valuations, initialize them now.
- boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;
- if (generator->getOptions().isBuildStateValuationsSet()) {
- stateValuationsBuilder = generator->initializeStateValuationsBuilder();
- }
-
- buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, playerActionIndices, stateValuationsBuilder);
-
+ StateAndChoiceInformationBuilder stateAndChoiceInformationBuilder;
+ stateAndChoiceInformationBuilder.setBuildChoiceLabels(generator->getOptions().isBuildChoiceLabelsSet());
+ stateAndChoiceInformationBuilder.setBuildChoiceOrigins(generator->getOptions().isBuildChoiceOriginsSet());
+ stateAndChoiceInformationBuilder.setBuildStatePlayerIndications(generator->getModelType() == storm::generator::ModelType::SMG);
+ stateAndChoiceInformationBuilder.setBuildMarkovianStates(generator->getModelType() == storm::generator::ModelType::MA);
+ stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet());
+
+ buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder);
+
// Initialize the model components with the obtained information.
- storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates), /* player1Matrix = */ boost::none, std::move(playerActionIndices));
+ storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel());
+
+ uint_fast64_t numStates = modelComponents.transitionMatrix.getColumnCount();
+ uint_fast64_t numChoices = modelComponents.transitionMatrix.getRowCount();
// Now finalize all reward models.
for (auto& rewardModelBuilder : rewardModelBuilders) {
- modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
+ modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(numChoices, modelComponents.transitionMatrix.getColumnCount(), numStates));
+ }
+ // Build the player assignment
+ if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications()) {
+ modelComponents.statePlayerIndications = stateAndChoiceInformationBuilder.buildStatePlayerIndications(numStates);
+ modelComponents.playerNameToIndexMap = generator->getPlayerNameToIndexMap();
+ }
+ // Build Markovian states
+ if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) {
+ modelComponents.markovianStates = stateAndChoiceInformationBuilder.buildMarkovianStates(numStates);
}
// Build the choice labeling
- modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
-
+ if (stateAndChoiceInformationBuilder.isBuildChoiceLabels()) {
+ modelComponents.choiceLabeling = stateAndChoiceInformationBuilder.buildChoiceLabeling(numChoices);
+ }
// If requested, build the state valuations and choice origins
- if (stateValuationsBuilder) {
- modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount());
+ if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
+ modelComponents.stateValuations = stateAndChoiceInformationBuilder.stateValuationsBuilder().build(numStates);
}
- if (generator->getOptions().isBuildChoiceOriginsSet()) {
- auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
+ if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins()) {
+ auto originData = stateAndChoiceInformationBuilder.buildDataOfChoiceOrigins(numChoices);
modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData);
}
if (generator->isPartiallyObservable()) {
- std::vector<uint32_t> classes;
- classes.resize(stateStorage.getNumberOfStates());
+ std::vector<uint32_t> classes(stateStorage.getNumberOfStates());
std::unordered_map<uint32_t, std::vector<std::pair<std::vector<std::string>, uint32_t>>> observationActions;
for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
uint32_t varObservation = generator->observabilityClass(bitVectorIndexPair.first);
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index af068b3fa..f33b37ba3 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -43,7 +43,7 @@ namespace storm {
// Forward-declare classes.
template <typename ValueType> class RewardModelBuilder;
- class ChoiceInformationBuilder;
+ class StateAndChoiceInformationBuilder;
template<typename StateType>
class ExplicitStateLookup {
@@ -127,11 +127,9 @@ namespace storm {
*
* @param transitionMatrixBuilder The builder of the transition matrix.
* @param rewardModelBuilders The builders for the selected reward models.
- * @param choiceInformationBuilder The builder for the requested information of the choices
- * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
- * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
+ * @param stateAndChoiceInformationBuilder The builder for the requested information of the individual states and choices
*/
- void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
+ void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder);
/*!
* Explores the state space of the given program and returns the components of the model as a result.
diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.cpp b/src/storm/builder/StateAndChoiceInformationBuilder.cpp
new file mode 100644
index 000000000..13d21624a
--- /dev/null
+++ b/src/storm/builder/StateAndChoiceInformationBuilder.cpp
@@ -0,0 +1,121 @@
+#include "storm/builder/StateAndChoiceInformationBuilder.h"
+
+namespace storm {
+ namespace builder {
+
+ StateAndChoiceInformationBuilder::StateAndChoiceInformationBuilder() : _buildChoiceLabels(false), _buildChoiceOrigins(false), _buildStatePlayerIndications(false), _buildMarkovianStates(false), _buildStateValuations(false) {
+ // Intentionally left empty
+ }
+
+ void StateAndChoiceInformationBuilder::setBuildChoiceLabels(bool value) {
+ _buildChoiceLabels = value;
+ }
+
+ bool StateAndChoiceInformationBuilder::isBuildChoiceLabels() const {
+ return _buildChoiceLabels;
+ }
+
+ void StateAndChoiceInformationBuilder::addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex) {
+ STORM_LOG_ASSERT(_buildChoiceLabels, "Building ChoiceLabels was not enabled.");
+ storm::storage::BitVector& labeledChoices = _choiceLabels[label];
+ labeledChoices.grow(choiceIndex + 1, false);
+ labeledChoices.set(choiceIndex, true);
+ }
+
+ storm::models::sparse::ChoiceLabeling StateAndChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
+ storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
+ for (auto& label : _choiceLabels) {
+ label.second.resize(totalNumberOfChoices, false);
+ result.addLabel(label.first, std::move(label.second));
+ }
+ return result;
+ }
+
+ void StateAndChoiceInformationBuilder::setBuildChoiceOrigins(bool value) {
+ _buildChoiceOrigins = value;
+ }
+
+ bool StateAndChoiceInformationBuilder::isBuildChoiceOrigins() const {
+ return _buildChoiceOrigins;
+ }
+
+ void StateAndChoiceInformationBuilder::addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
+ STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled.");
+ STORM_LOG_ASSERT(_dataOfChoiceOrigins.size() <= choiceIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
+ if (_dataOfChoiceOrigins.size() != choiceIndex) {
+ _dataOfChoiceOrigins.resize(choiceIndex);
+ }
+ _dataOfChoiceOrigins.push_back(originData);
+ }
+
+ std::vector<boost::any> StateAndChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
+ STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled.");
+ _dataOfChoiceOrigins.resize(totalNumberOfChoices);
+ _dataOfChoiceOrigins.shrink_to_fit();
+ return std::move(_dataOfChoiceOrigins);
+ }
+
+ void StateAndChoiceInformationBuilder::setBuildStatePlayerIndications(bool value) {
+ _buildStatePlayerIndications = value;
+ }
+
+ bool StateAndChoiceInformationBuilder::isBuildStatePlayerIndications() const {
+ return _buildStatePlayerIndications;
+ }
+
+ void StateAndChoiceInformationBuilder::addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex) {
+ STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+ STORM_LOG_ASSERT(_statePlayerIndications.size() <= stateIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
+ if (_statePlayerIndications.size() != stateIndex) {
+ _statePlayerIndications.resize(stateIndex, storm::storage::INVALID_PLAYER_INDEX);
+ }
+ _statePlayerIndications.push_back(player);
+ }
+
+ bool StateAndChoiceInformationBuilder::hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const {
+ STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+ return (stateIndex < _statePlayerIndications.size()) && (_statePlayerIndications[stateIndex] == expectedPlayer);
+ }
+
+ std::vector<storm::storage::PlayerIndex> StateAndChoiceInformationBuilder::buildStatePlayerIndications(uint_fast64_t totalNumberOfStates) {
+ STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled.");
+ _statePlayerIndications.resize(totalNumberOfStates, storm::storage::INVALID_PLAYER_INDEX);
+ _statePlayerIndications.shrink_to_fit();
+ return std::move(_statePlayerIndications);
+ }
+
+ void StateAndChoiceInformationBuilder::setBuildMarkovianStates(bool value) {
+ _buildMarkovianStates = value;
+ }
+
+ bool StateAndChoiceInformationBuilder::isBuildMarkovianStates() const {
+ return _buildMarkovianStates;
+ }
+
+ void StateAndChoiceInformationBuilder::addMarkovianState(uint_fast64_t markovianStateIndex) {
+ STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled.");
+ _markovianStates.grow(markovianStateIndex + 1, false);
+ _markovianStates.set(markovianStateIndex, true);
+ }
+
+ storm::storage::BitVector StateAndChoiceInformationBuilder::buildMarkovianStates(uint_fast64_t totalNumberOfStates) {
+ STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled.");
+ _markovianStates.resize(totalNumberOfStates, false);
+ return _markovianStates;
+ }
+
+ void StateAndChoiceInformationBuilder::setBuildStateValuations(bool value) {
+ _buildStateValuations = value;
+ }
+
+ bool StateAndChoiceInformationBuilder::isBuildStateValuations() const {
+ return _buildStateValuations;
+ }
+
+ storm::storage::sparse::StateValuationsBuilder& StateAndChoiceInformationBuilder::stateValuationsBuilder() {
+ STORM_LOG_ASSERT(_buildStateValuations, "Building StateValuations was not enabled.");
+ return _stateValuationsBuilder;
+ }
+
+ }
+}
diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.h b/src/storm/builder/StateAndChoiceInformationBuilder.h
new file mode 100644
index 000000000..413dcd50f
--- /dev/null
+++ b/src/storm/builder/StateAndChoiceInformationBuilder.h
@@ -0,0 +1,75 @@
+#pragma once
+
+#include <memory>
+#include <string>
+#include <unordered_map>
+#include <vector>
+#include <boost/any.hpp>
+
+#include "storm/models/sparse/ChoiceLabeling.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/PlayerIndex.h"
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
+#include "storm/storage/prism/Program.h"
+#include "storm/storage/sparse/StateValuations.h"
+
+
+namespace storm {
+ namespace builder {
+
+ /*!
+ * This class collects information regarding the states and choices during model building.
+ * It is expected that the provided indices are in ascending order
+ */
+ class StateAndChoiceInformationBuilder {
+ public:
+
+ StateAndChoiceInformationBuilder();
+
+ void setBuildChoiceLabels(bool value);
+ bool isBuildChoiceLabels() const;
+ void addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex);
+ storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
+
+ void setBuildChoiceOrigins(bool value);
+ bool isBuildChoiceOrigins() const;
+ void addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
+ std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
+
+ void setBuildStatePlayerIndications(bool value);
+ bool isBuildStatePlayerIndications() const;
+ /*!
+ * @note: skipped choiceIndices get assigned the invalid player index.
+ */
+ void addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex);
+ bool hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const;
+ std::vector<storm::storage::PlayerIndex> buildStatePlayerIndications(uint_fast64_t totalNumberOfStates);
+
+ void setBuildMarkovianStates(bool value);
+ bool isBuildMarkovianStates() const;
+ void addMarkovianState(uint_fast64_t markovianStateIndex);
+ storm::storage::BitVector buildMarkovianStates(uint_fast64_t totalNumberOfStates);
+
+ void setBuildStateValuations(bool value);
+ bool isBuildStateValuations() const;
+ storm::storage::sparse::StateValuationsBuilder& stateValuationsBuilder();
+
+ private:
+ bool _buildChoiceLabels;
+ std::unordered_map<std::string, storm::storage::BitVector> _choiceLabels;
+
+ bool _buildChoiceOrigins;
+ std::vector<boost::any> _dataOfChoiceOrigins;
+
+ bool _buildStatePlayerIndications;
+ std::vector<storm::storage::PlayerIndex> _statePlayerIndications;
+
+ bool _buildMarkovianStates;
+ storm::storage::BitVector _markovianStates;
+
+ bool _buildStateValuations;
+ storm::storage::sparse::StateValuationsBuilder _stateValuationsBuilder;
+ };
+ }
+}
+
diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp
index fc1d41999..a0efb04f9 100644
--- a/src/storm/generator/Choice.cpp
+++ b/src/storm/generator/Choice.cpp
@@ -3,7 +3,6 @@
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/utility/constants.h"
-#include "storm/builder/ChoiceInformationBuilder.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"
diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
index b68380935..4112920e4 100644
--- a/src/storm/generator/NextStateGenerator.cpp
+++ b/src/storm/generator/NextStateGenerator.cpp
@@ -278,6 +278,11 @@ namespace storm {
return classId;
}
+ template<typename ValueType, typename StateType>
+ std::map<std::string, storm::storage::PlayerIndex> NextStateGenerator<ValueType, StateType>::getPlayerNameToIndexMap() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Generating player mappings is not supported for this model input format");
+ }
+
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::remapStateIds(std::function<StateType(StateType const&)> const& remapping) {
if (overlappingGuardStates != boost::none) {
diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
index 671158870..eee62412d 100644
--- a/src/storm/generator/NextStateGenerator.h
+++ b/src/storm/generator/NextStateGenerator.h
@@ -11,6 +11,7 @@
#include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm/storage/sparse/ChoiceOrigins.h"
#include "storm/storage/sparse/StateValuations.h"
+#include "storm/storage/PlayerIndex.h"
#include "storm/builder/BuilderOptions.h"
#include "storm/builder/RewardModelInformation.h"
@@ -74,6 +75,8 @@ namespace storm {
std::string stateToString(CompressedState const& state) const;
uint32_t observabilityClass(CompressedState const& state) const;
+
+ virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const;
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index ecf7e792d..ead36e763 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -734,6 +734,11 @@ namespace storm {
}
}
+ template<typename ValueType, typename StateType>
+ std::map<std::string, storm::storage::PlayerIndex> PrismNextStateGenerator<ValueType, StateType>::getPlayerNameToIndexMap() const {
+ return program.getPlayerNameToIndexMapping();
+ }
+
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
// Gather a vector of labels and their expressions.
diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h
index 4e1901134..e8a7a81ff 100644
--- a/src/storm/generator/PrismNextStateGenerator.h
+++ b/src/storm/generator/PrismNextStateGenerator.h
@@ -4,7 +4,6 @@
#include "storm/generator/NextStateGenerator.h"
#include "storm/storage/prism/Program.h"
-#include "storm/storage/PlayerIndex.h"
#include "storm/storage/BoostTypes.h"
namespace storm {
@@ -43,7 +42,8 @@ namespace storm {
virtual std::size_t getNumberOfRewardModels() const override;
virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
-
+ virtual std::map<std::string, storm::storage::PlayerIndex> getPlayerNameToIndexMap() const override;
+
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h
index 29ae3d14b..1011efbd7 100644
--- a/src/storm/storage/sparse/ModelComponents.h
+++ b/src/storm/storage/sparse/ModelComponents.h
@@ -13,6 +13,7 @@
#include "storm/storage/sparse/ChoiceOrigins.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/BitVector.h"
+#include "storm/storage/PlayerIndex.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
@@ -30,9 +31,8 @@ namespace storm {
std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(),
bool rateTransitions = false,
boost::optional<storm::storage::BitVector> const& markovianStates = boost::none,
- boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none,
- boost::optional<std::vector<uint_fast32_t>> const& playerActionIndices = boost::none)
- : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) {
+ boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none)
+ : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) {
// Intentionally left empty
}
@@ -41,15 +41,12 @@ namespace storm {
std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(),
bool rateTransitions = false,
boost::optional<storm::storage::BitVector>&& markovianStates = boost::none,
- boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none,
- boost::optional<std::vector<uint_fast32_t>>&& playerActionIndices = boost::none)
- : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)), playerActionIndices(std::move(playerActionIndices)) {
+ boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none)
+ : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) {
// Intentionally left empty
}
-
-
// General components (applicable for all model types):
// The transition matrix.
@@ -68,7 +65,6 @@ namespace storm {
// POMDP specific components
// The POMDP observations
boost::optional<std::vector<uint32_t>> observabilityClasses;
-
boost::optional<storm::storage::sparse::StateValuations> observationValuations;
// Continuous time specific components (CTMCs, Markov Automata):
@@ -84,8 +80,10 @@ namespace storm {
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> player1Matrix;
// Stochastic multiplayer game specific components:
- // The vector mapping state choices to players
- boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
+ // The vector mapping states to player indices.
+ boost::optional<std::vector<storm::storage::PlayerIndex>> statePlayerIndications;
+ // A mapping of player names to player indices.
+ boost::optional<std::map<std::string, storm::storage::PlayerIndex>> playerNameToIndexMap;
};
}
}