added transformation to binary pomdp

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<std::string> 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 {
@@ -62,8 +66,13 @@ namespace storm {
                 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() {
             }

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;
                 

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::modules::JaniExportSettings>();
     storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
     storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
+    storm::settings::addModule<storm::settings::modules::BuildSettings>();
 
 
     storm::settings::addModule<storm::settings::modules::POMDPSettings>();
@@ -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<storm::RationalNumber>().transform(*pomdp, true);
+                } else {
+                    STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP.");
+                    pomdp = storm::transformer::BinaryPomdpTransformer<storm::RationalNumber>().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<storm::RationalNumber> toPMCTransformer(*pomdp);

src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp

@@ -0,0 +1,166 @@
+#include "storm-pomdp/transformer/BinaryPomdpTransformer.h"
+#include <queue>
+
+#include "storm/storage/sparse/ModelComponents.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<typename  ValueType>
+        BinaryPomdpTransformer<ValueType>::BinaryPomdpTransformer() {
+            // Intentionally left empty
+        }
+        
+        template<typename  ValueType>
+        std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> BinaryPomdpTransformer<ValueType>::transform(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool transformSimple) const {
+            auto data = transformTransitions(pomdp, transformSimple);
+            storm::storage::sparse::ModelComponents<ValueType> 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<storm::models::sparse::Pomdp<ValueType>>(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<BinaryPomdpTransformerRowGroup> split() const {
+                assert(size() > 1);
+                uint64_t midRow = firstRow + size()/2;
+                std::vector<BinaryPomdpTransformerRowGroup> 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  ValueType>
+        typename BinaryPomdpTransformer<ValueType>::TransformationData BinaryPomdpTransformer<ValueType>::transformTransitions(storm::models::sparse::Pomdp<ValueType> 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<BinaryPomdpTransformerRowGroup> queue;
+            for (uint64_t state = 0; state < matrix.getRowGroupCount(); ++state) {
+                queue.emplace(matrix.getRowGroupIndices()[state], matrix.getRowGroupIndices()[state+1], pomdp.getObservation(state));
+            }
+            
+            std::vector<uint32_t> newObservations;
+            std::map<BinaryPomdpTransformerRowGroup, uint32_t, BinaryPomdpTransformerRowGroupCompare> observationMap;
+            storm::storage::SparseMatrixBuilder<ValueType> builder(0,0,0,true,true);
+            uint64_t currRow = 0;
+            std::vector<uint64_t> origRowToSimpleRowMap(pomdp.getNumberOfChoices(), std::numeric_limits<uint64_t>::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<ValueType>());
+                            ++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<typename  ValueType>
+        storm::models::sparse::StateLabeling BinaryPomdpTransformer<ValueType>::transformStateLabeling(storm::models::sparse::Pomdp<ValueType> 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<typename  ValueType>
+        storm::models::sparse::StandardRewardModel<ValueType> BinaryPomdpTransformer<ValueType>::transformRewardModel(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, TransformationData const& data) const {
+            boost::optional<std::vector<ValueType>> stateRewards, actionRewards;
+            if (rewardModel.hasStateRewards()) {
+                stateRewards = rewardModel.getStateRewardVector();
+                stateRewards.get().resize(data.simpleMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+            }
+            if (rewardModel.hasStateActionRewards()) {
+                actionRewards = std::vector<ValueType>(data.simpleMatrix.getRowCount(), storm::utility::zero<ValueType>());
+                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<ValueType>(std::move(stateRewards), std::move(actionRewards));
+        }
+        
+        
+        template class BinaryPomdpTransformer<storm::RationalNumber>;
+
+    }
+}

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<typename ValueType>
+        class BinaryPomdpTransformer {
+
+        public:
+            
+            BinaryPomdpTransformer();
+            
+            std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> transform(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool transformSimple) const;
+
+        private:
+    
+            struct TransformationData {
+                storm::storage::SparseMatrix<ValueType> simpleMatrix;
+                std::vector<uint32_t> simpleObservations;
+                std::vector<uint64_t> originalToSimpleChoiceMap;
+            };
+            
+            TransformationData transformTransitions(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool transformSimple) const;
+            storm::models::sparse::StateLabeling transformStateLabeling(storm::models::sparse::Pomdp<ValueType> const& pomdp, TransformationData const& data) const;
+            storm::models::sparse::StandardRewardModel<ValueType> transformRewardModel(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, TransformationData const& data) const;
+            
+        };
+    }
+}