From bb05b9c03ce40632690ef5517f27f2777d24a654 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 19 Aug 2020 12:04:51 +0200 Subject: [PATCH] aggregate player indices into model --- src/storm/builder/ExplicitModelBuilder.cpp | 106 ++++++++++++--------- src/storm/builder/ExplicitModelBuilder.h | 16 ++-- 2 files changed, 71 insertions(+), 51 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 2b120f8ac..10e0c8927 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -49,26 +49,26 @@ namespace storm { ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options) : generator(generator), options(options), stateStorage(generator->getStateSize()) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared>(program, generatorOptions), builderOptions) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared>(model, generatorOptions), builderOptions) { // Intentionally left empty. } - + template std::shared_ptr> ExplicitModelBuilder::build() { STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); - + switch (generator->getModelType()) { case storm::generator::ModelType::DTMC: return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Dtmc, buildModelComponents()); @@ -110,7 +110,7 @@ namespace storm { STORM_LOG_ASSERT(false, "Invalid exploration order."); } } - + return actualIndex; } @@ -120,24 +120,30 @@ namespace storm { } template - void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional& stateValuationsBuilder) { - + void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional> playerActionIndices, boost::optional& stateValuationsBuilder) { + // 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{}; + playerActionIndices.get().reserve(1000); + } + // Create a callback for the next-state generator to enable it to request the index of states. std::function stateToIdCallback = std::bind(&ExplicitModelBuilder::getOrAddStateIndex, this, std::placeholders::_1); - + // If the exploration order is something different from breadth-first, we need to keep track of the remapping // from state ids to row groups. For this, we actually store the reversed mapping of row groups to state-ids // and later reverse it. if (options.explorationOrder != ExplorationOrder::Bfs) { stateRemapping = std::vector(); } - + // Let the generator create all initial states. this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(), storm::exceptions::WrongFormatException, "The model does not have a single initial state."); @@ -150,30 +156,30 @@ namespace storm { auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); uint64_t numberOfExploredStates = 0; uint64_t numberOfExploredStatesSinceLastMessage = 0; - + // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. CompressedState currentState = statesToExplore.front().first; StateType currentIndex = statesToExplore.front().second; statesToExplore.pop_front(); - + // If the exploration order differs from breadth-first, we remember that this row group was actually // filled with the transitions of a different state. if (options.explorationOrder != ExplorationOrder::Bfs) { stateRemapping.get()[currentIndex] = currentRowGroup; } - + if (currentIndex % 100000 == 0) { STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); } - + generator->load(currentState); if (stateValuationsBuilder) { generator->addStateValuation(currentIndex, stateValuationsBuilder.get()); } storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); - + // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { @@ -181,28 +187,33 @@ namespace storm { if (behavior.wasExpanded()) { this->stateStorage.deadlockStateIndices.push_back(currentIndex); } - + if (markovianStates) { markovianStates.get().grow(currentRowGroup + 1, false); markovianStates.get().set(currentRowGroup); } - + if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } - + transitionMatrixBuilder.addNextValue(currentRow, currentIndex, storm::utility::one()); - + for (auto& rewardModelBuilder : rewardModelBuilders) { if (rewardModelBuilder.hasStateRewards()) { rewardModelBuilder.addStateReward(storm::utility::zero()); } - + if (rewardModelBuilder.hasStateActionRewards()) { rewardModelBuilder.addStateActionReward(storm::utility::zero()); } } - + + if (playerActionIndices) { + // TODO change this to storm::utility::infinity() ? + playerActionIndices.get().push_back(-1); + } + ++currentRow; ++currentRowGroup; } else { @@ -217,15 +228,15 @@ namespace storm { } ++stateRewardIt; } - + // If the model is nondeterministic, we need to open a row group. if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } - + // Now add all choices. for (auto const& choice : behavior) { - + // add the generated choice information if (choice.hasLabels()) { for (auto const& label : choice.getLabels()) { @@ -235,18 +246,18 @@ namespace storm { if (choice.hasOriginData()) { choiceInformationBuilder.addOriginData(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); } - + // Add the probabilistic behavior to the matrix. for (auto const& stateProbabilityPair : choice) { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } - + // Add the rewards to the reward models. auto choiceRewardIt = choice.getRewards().begin(); for (auto& rewardModelBuilder : rewardModelBuilders) { @@ -257,6 +268,10 @@ namespace storm { } ++currentRow; } + + if (playerActionIndices) { + playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex()); + } ++currentRowGroup; } @@ -282,24 +297,28 @@ namespace storm { break; } } - + 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) { STORM_LOG_ASSERT(stateRemapping, "Unable to fix columns without mapping."); std::vector const& remapping = stateRemapping.get(); - + // We need to fix the following entities: // (a) the transition matrix // (b) the initial states // (c) the hash map storing the mapping states -> ids // (d) fix remapping for state-generation labels - + // Fix (a). transitionMatrixBuilder.replaceColumns(remapping, 0); @@ -308,21 +327,21 @@ namespace storm { std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } ); std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end()); this->stateStorage.initialStateIndices = std::move(newInitialStateIndices); - + // Fix (c). this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } ); this->generator->remapStateIds([&remapping] (StateType const& state) { return remapping[state]; }); } } - + template storm::storage::sparse::ModelComponents ExplicitModelBuilder::buildModelComponents() { - + // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = generator->isDeterministicModel(); - + // Prepare the component builders storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); std::vector> rewardModelBuilders; @@ -331,25 +350,26 @@ namespace storm { } ChoiceInformationBuilder choiceInformationBuilder; boost::optional markovianStates; - + boost::optional> playerActionIndices; + // If we need to build state valuations, initialize them now. boost::optional stateValuationsBuilder; if (generator->getOptions().isBuildStateValuationsSet()) { stateValuationsBuilder = generator->initializeStateValuationsBuilder(); } - - buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder); - + + buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, playerActionIndices, stateValuationsBuilder); + // Initialize the model components with the obtained information. - storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); - + storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates), /* player1Matrix = */ boost::none, std::move(playerActionIndices)); + // 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())); } // Build the choice labeling modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); - + // If requested, build the state valuations and choice origins if (stateValuationsBuilder) { modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount()); @@ -374,12 +394,12 @@ namespace storm { } return modelComponents; } - + template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } - + // Explicitly instantiate the class. template class ExplicitModelBuilder, uint32_t>; template class ExplicitStateLookup; diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 132345075..af068b3fa 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -131,40 +131,40 @@ namespace storm { * @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 */ - void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional& stateValuationsBuilder); - + void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional> playerActionIndices, boost::optional& stateValuationsBuilder); + /*! * Explores the state space of the given program and returns the components of the model as a result. * * @return A structure containing the components of the resulting model. */ storm::storage::sparse::ModelComponents buildModelComponents(); - + /*! * Builds the state labeling for the given program. * * @return The state labeling of the given program. */ storm::models::sparse::StateLabeling buildStateLabeling(); - + /// The generator to use for the building process. std::shared_ptr> generator; - + /// The options to be used for the building process. Options options; /// Internal information about the states that were explored. storm::storage::sparse::StateStorage stateStorage; - + /// A set of states that still need to be explored. std::deque> statesToExplore; - + /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be /// built in case the exploration order is not BFS. boost::optional> stateRemapping; }; - + } // namespace adapters } // namespace storm