diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index a5ff3e325..6bc5b1e18 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -19,6 +19,8 @@ namespace storm { const std::string memoryBoundOption = "memorybound"; const std::string fscmode = "fscmode"; std::vector fscModes = {"standard", "simple-linear", "simple-linear-inverse"}; + const std::string transformBinaryOption = "transformbinary"; + const std::string transformSimpleOption = "transformsimple"; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportAsParametricModelOption, false, "Export the parametric file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which to write the model.").build()).build()); @@ -28,6 +30,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, selfloopReductionOption, false, "Reduces the model size by removing self loop actions").build()); this->addOption(storm::settings::OptionBuilder(moduleName, memoryBoundOption, false, "Sets the maximal number of allowed memory states (1 means memoryless schedulers).").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The maximal number of memory states.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build()); } bool POMDPSettings::isExportToParametricSet() const { @@ -61,10 +65,15 @@ namespace storm { std::string POMDPSettings::getFscApplicationTypeString() const { return this->getOption(fscmode).getArgumentByName("type").getValueAsString(); } - - + bool POMDPSettings::isTransformBinarySet() const { + return this->getOption(transformBinaryOption).getHasOptionBeenSet(); + } + bool POMDPSettings::isTransformSimpleSet() const { + return this->getOption(transformSimpleOption).getHasOptionBeenSet(); + } + void POMDPSettings::finalize() { } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 6620ee3da..213d46be4 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -29,6 +29,8 @@ namespace storm { bool isAnalyzeUniqueObservationsSet() const; bool isMecReductionSet() const; bool isSelfloopReductionSet() const; + bool isTransformSimpleSet() const; + bool isTransformBinarySet() const; std::string getFscApplicationTypeString() const; uint64_t getMemoryBound() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ec30516d9..22574197f 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -24,6 +24,7 @@ #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm-pomdp-cli/settings/modules/POMDPSettings.h" @@ -37,6 +38,7 @@ #include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h" #include "storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.h" #include "storm-pomdp/transformer/PomdpMemoryUnfolder.h" +#include "storm-pomdp/transformer/BinaryPomdpTransformer.h" #include "storm-pomdp/analysis/UniqueObservationStates.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" #include "storm/api/storm.h" @@ -71,6 +73,7 @@ void initializeSettings() { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); @@ -158,7 +161,7 @@ int main(const int argc, const char** argv) { STORM_PRINT_AND_LOG(" done." << std::endl); pomdp->printModelInformationToStream(std::cout); } else { - STORM_PRINT_AND_LOG("Assumming memoryless schedulers.") + STORM_PRINT_AND_LOG("Assumming memoryless schedulers." << std::endl;) } // From now on the pomdp is considered memoryless @@ -171,8 +174,22 @@ int main(const int argc, const char** argv) { pomdp = mecChoiceEliminator.transform(*formula); STORM_PRINT_AND_LOG(" done." << std::endl); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl); + pomdp->printModelInformationToStream(std::cout); } + if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) { + if (pomdpSettings.isTransformSimpleSet()) { + STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP."); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); + } else { + STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); + } + pomdp->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG(" done." << std::endl); + } + + if (pomdpSettings.isExportToParametricSet()) { STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp new file mode 100644 index 000000000..170f6e863 --- /dev/null +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp @@ -0,0 +1,166 @@ +#include "storm-pomdp/transformer/BinaryPomdpTransformer.h" +#include + +#include "storm/storage/sparse/ModelComponents.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace transformer { + + template + BinaryPomdpTransformer::BinaryPomdpTransformer() { + // Intentionally left empty + } + + template + std::shared_ptr> BinaryPomdpTransformer::transform(storm::models::sparse::Pomdp const& pomdp, bool transformSimple) const { + auto data = transformTransitions(pomdp, transformSimple); + storm::storage::sparse::ModelComponents components; + components.stateLabeling = transformStateLabeling(pomdp, data); + for (auto const& rewModel : pomdp.getRewardModels()) { + components.rewardModels.emplace(rewModel.first, transformRewardModel(pomdp, rewModel.second, data)); + } + components.transitionMatrix = std::move(data.simpleMatrix); + components.observabilityClasses = std::move(data.simpleObservations); + + return std::make_shared>(std::move(components)); + } + + struct BinaryPomdpTransformerRowGroup { + BinaryPomdpTransformerRowGroup(uint64_t firstRow, uint64_t endRow, uint32_t origStateObservation) : firstRow(firstRow), endRow(endRow), origStateObservation(origStateObservation) { + // Intentionally left empty. + } + + uint64_t firstRow; + uint64_t endRow; + uint32_t origStateObservation; + storm::storage::BitVector auxStateId; + + uint64_t size() const { + return endRow - firstRow; + } + + std::vector split() const { + assert(size() > 1); + uint64_t midRow = firstRow + size()/2; + std::vector res; + res.emplace_back(firstRow, midRow, origStateObservation); + storm::storage::BitVector newAuxStateId = auxStateId; + newAuxStateId.resize(auxStateId.size() + 1, false); + res.back().auxStateId = newAuxStateId; + res.emplace_back(midRow, endRow, origStateObservation); + newAuxStateId.set(auxStateId.size(), true); + res.back().auxStateId = newAuxStateId; + return res; + } + }; + + struct BinaryPomdpTransformerRowGroupCompare { + bool operator () (BinaryPomdpTransformerRowGroup const& lhs, BinaryPomdpTransformerRowGroup const& rhs) const { + if (lhs.origStateObservation == rhs.origStateObservation) { + return lhs.auxStateId < rhs.auxStateId; + } else { + return lhs.origStateObservation < rhs.origStateObservation; + } + } + }; + + template + typename BinaryPomdpTransformer::TransformationData BinaryPomdpTransformer::transformTransitions(storm::models::sparse::Pomdp const& pomdp, bool transformSimple) const { + auto const& matrix = pomdp.getTransitionMatrix(); + + + // Initialize a FIFO Queue that stores the start and the end of each row group + std::queue queue; + for (uint64_t state = 0; state < matrix.getRowGroupCount(); ++state) { + queue.emplace(matrix.getRowGroupIndices()[state], matrix.getRowGroupIndices()[state+1], pomdp.getObservation(state)); + } + + std::vector newObservations; + std::map observationMap; + storm::storage::SparseMatrixBuilder builder(0,0,0,true,true); + uint64_t currRow = 0; + std::vector origRowToSimpleRowMap(pomdp.getNumberOfChoices(), std::numeric_limits::max()); + uint64 currAuxState = queue.size(); + while (!queue.empty()) { + auto group = std::move(queue.front()); + queue.pop(); + + // Get the observation + uint64_t newObservation = observationMap.insert(std::make_pair(group, observationMap.size())).first->second; + newObservations.push_back(newObservation); + + // Add matrix entries + builder.newRowGroup(currRow); + if (group.size() == 1) { + // Insert the row directly + for (auto const& entry : matrix.getRow(group.firstRow)) { + builder.addNextValue(currRow, entry.getColumn(), entry.getValue()); + } + origRowToSimpleRowMap[group.firstRow] = currRow; + ++currRow; + } else if (group.size() > 1) { + // Split the row group into two equally large parts + for (auto& splittedGroup : group.split()) { + // Check whether we can insert the row now or whether an auxiliary state is needed + if (splittedGroup.size() == 1 && (!transformSimple || matrix.getRow(splittedGroup.firstRow).getNumberOfEntries() < 2)) { + for (auto const& entry : matrix.getRow(splittedGroup.firstRow)) { + builder.addNextValue(currRow, entry.getColumn(), entry.getValue()); + } + origRowToSimpleRowMap[splittedGroup.firstRow] = currRow; + ++currRow; + } else { + queue.push(std::move(splittedGroup)); + builder.addNextValue(currRow, currAuxState, storm::utility::one()); + ++currAuxState; + ++currRow; + } + } + } + // Nothing to be done if group has size zero + } + + TransformationData result; + result.simpleMatrix = builder.build(currRow, currAuxState, currAuxState); + result.simpleObservations = std::move(newObservations); + result.originalToSimpleChoiceMap = std::move(origRowToSimpleRowMap); + return result; + } + + + template + storm::models::sparse::StateLabeling BinaryPomdpTransformer::transformStateLabeling(storm::models::sparse::Pomdp const& pomdp, TransformationData const& data) const { + storm::models::sparse::StateLabeling labeling(data.simpleMatrix.getRowGroupCount()); + for (auto const& labelName : pomdp.getStateLabeling().getLabels()) { + storm::storage::BitVector newStates = pomdp.getStateLabeling().getStates(labelName); + newStates.resize(data.simpleMatrix.getRowGroupCount(), false); + labeling.addLabel(labelName, std::move(newStates)); + } + return labeling; + } + + template + storm::models::sparse::StandardRewardModel BinaryPomdpTransformer::transformRewardModel(storm::models::sparse::Pomdp const& pomdp, storm::models::sparse::StandardRewardModel const& rewardModel, TransformationData const& data) const { + boost::optional> stateRewards, actionRewards; + if (rewardModel.hasStateRewards()) { + stateRewards = rewardModel.getStateRewardVector(); + stateRewards.get().resize(data.simpleMatrix.getRowGroupCount(), storm::utility::zero()); + } + if (rewardModel.hasStateActionRewards()) { + actionRewards = std::vector(data.simpleMatrix.getRowCount(), storm::utility::zero()); + for (uint64_t pomdpChoice = 0; pomdpChoice < pomdp.getNumberOfChoices(); ++pomdpChoice) { + STORM_LOG_ASSERT(data.originalToSimpleChoiceMap[pomdpChoice] < data.simpleMatrix.getRowCount(), "Invalid entry in map for choice " << pomdpChoice); + actionRewards.get()[data.originalToSimpleChoiceMap[pomdpChoice]] = rewardModel.getStateActionReward(pomdpChoice); + } + } + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported."); + return storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(actionRewards)); + } + + + template class BinaryPomdpTransformer; + + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.h b/src/storm-pomdp/transformer/BinaryPomdpTransformer.h new file mode 100644 index 000000000..734592ead --- /dev/null +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.h @@ -0,0 +1,32 @@ +#pragma once + +#include "storm/models/sparse/Pomdp.h" +#include "storm/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace transformer { + + template + class BinaryPomdpTransformer { + + public: + + BinaryPomdpTransformer(); + + std::shared_ptr> transform(storm::models::sparse::Pomdp const& pomdp, bool transformSimple) const; + + private: + + struct TransformationData { + storm::storage::SparseMatrix simpleMatrix; + std::vector simpleObservations; + std::vector originalToSimpleChoiceMap; + }; + + TransformationData transformTransitions(storm::models::sparse::Pomdp const& pomdp, bool transformSimple) const; + storm::models::sparse::StateLabeling transformStateLabeling(storm::models::sparse::Pomdp const& pomdp, TransformationData const& data) const; + storm::models::sparse::StandardRewardModel transformRewardModel(storm::models::sparse::Pomdp const& pomdp, storm::models::sparse::StandardRewardModel const& rewardModel, TransformationData const& data) const; + + }; + } +} \ No newline at end of file