pomdps in an own cli, support for application of stochastic schedulers, etc

src/CMakeLists.txt

@@ -14,6 +14,8 @@ add_subdirectory(storm-dft)
 add_subdirectory(storm-dft-cli)
 add_subdirectory(storm-pars)
 add_subdirectory(storm-pars-cli)
+add_subdirectory(storm-pomdp)
+add_subdirectory(storm-pomdp-cli)
 
 
 

src/storm-pomdp-cli/CMakeLists.txt

@@ -0,0 +1,11 @@
+# Create storm-pomdp.
+
+file(GLOB_RECURSE STORM_POMDP_CLI_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pomdp-cli/*/*.cpp)
+add_executable(storm-pomdp-cli ${PROJECT_SOURCE_DIR}/src/storm-pomdp-cli/storm-pomdp.cpp ${STORM_POMDP_CLI_SOURCES})
+target_link_libraries(storm-pomdp-cli storm-pomdp storm-cli-utilities) # Adding headers for xcode
+set_target_properties(storm-pomdp-cli PROPERTIES OUTPUT_NAME "storm-pomdp")
+
+add_dependencies(binaries storm-pomdp-cli)
+
+# installation
+install(TARGETS storm-pomdp-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)

src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp

@@ -0,0 +1,44 @@
+#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include "storm/exceptions/InvalidSettingsException.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string POMDPSettings::moduleName = "pomdp";
+            const std::string exportAsParametricModelOption = "parametric-drn";
+
+
+            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());
+
+            }
+
+            bool POMDPSettings::isExportToParametricSet() const {
+                return this->getOption(exportAsParametricModelOption).getHasOptionBeenSet();
+            }
+
+            std::string POMDPSettings::getExportToParametricFilename() const {
+                return this->getOption(exportAsParametricModelOption).getArgumentByName("filename").getValueAsString();
+            }
+
+            void POMDPSettings::finalize() {
+            }
+
+            bool POMDPSettings::check() const {
+                // Ensure that at most one of min or max is set
+                return true;
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -0,0 +1,41 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for DFT model checking.
+             */
+            class POMDPSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of DFT settings.
+                 */
+                POMDPSettings();
+
+                virtual ~POMDPSettings() = default;
+                
+                bool isExportToParametricSet() const;
+                std::string getExportToParametricFilename() const;
+                
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+
+                
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -0,0 +1,126 @@
+
+
+#include "storm/utility/initialize.h"
+
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
+#include "storm/settings/modules/CuddSettings.h"
+#include "storm/settings/modules/SylvanSettings.h"
+#include "storm/settings/modules/EigenEquationSolverSettings.h"
+#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/settings/modules/EliminationSettings.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/settings/modules/GameSolverSettings.h"
+#include "storm/settings/modules/BisimulationSettings.h"
+#include "storm/settings/modules/GlpkSettings.h"
+#include "storm/settings/modules/GurobiSettings.h"
+#include "storm/settings/modules/Smt2SmtSolverSettings.h"
+#include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+#include "storm/settings/modules/ExplorationSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/AbstractionSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
+#include "storm/settings/modules/JitBuilderSettings.h"
+#include "storm/settings/modules/MultiObjectiveSettings.h"
+#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
+
+#include "storm/analysis/GraphConditions.h"
+
+#include "storm-cli-utilities/cli.h"
+#include "storm-cli-utilities/model-handling.h"
+
+#include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h"
+
+/*!
+ * Initialize the settings manager.
+ */
+void initializeSettings() {
+    storm::settings::mutableManager().setName("Storm-POMDP", "storm-pomdp");
+
+    storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+    storm::settings::addModule<storm::settings::modules::IOSettings>();
+    storm::settings::addModule<storm::settings::modules::CoreSettings>();
+    storm::settings::addModule<storm::settings::modules::DebugSettings>();
+    storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(false);
+    storm::settings::addModule<storm::settings::modules::CuddSettings>();
+    storm::settings::addModule<storm::settings::modules::SylvanSettings>();
+    storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::EliminationSettings>();
+    storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+    storm::settings::addModule<storm::settings::modules::GlpkSettings>();
+    storm::settings::addModule<storm::settings::modules::GurobiSettings>();
+    storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::Smt2SmtSolverSettings>();
+    storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
+    storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+    storm::settings::addModule<storm::settings::modules::AbstractionSettings>();
+    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::POMDPSettings>();
+}
+
+/*!
+ * Entry point for the pomdp backend.
+ *
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return Return code, 0 if successfull, not 0 otherwise.
+ */
+int main(const int argc, const char** argv) {
+    try {
+        storm::utility::setUp();
+        storm::cli::printHeader("Storm-pomdp", argc, argv);
+        initializeSettings();
+
+        bool optionsCorrect = storm::cli::parseOptions(argc, argv);
+        if (!optionsCorrect) {
+            return -1;
+        }
+
+
+        auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+        auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
+
+        // For several engines, no model building step is performed, but the verification is started right away.
+        storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
+
+        storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput();
+        auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, engine);
+        STORM_LOG_THROW(model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
+        storm::transformer::ApplyFiniteSchedulerToPomdp<storm::RationalNumber> toPMCTransformer(*(model->template as<storm::models::sparse::Pomdp<storm::RationalNumber>>()));
+
+        if (pomdpSettings.isExportToParametricSet()) {
+            auto const &pmc = toPMCTransformer.transform();
+            storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
+            pmc->printModelInformationToStream(std::cout);
+            auto const& parameterSet = constraints.getVariables();
+            std::vector<storm::RationalFunctionVariable> parameters(parameterSet.begin(), parameterSet.end());
+            std::vector<std::string> parameterNames;
+            for (auto const& parameter : parameters) {
+                parameterNames.push_back(parameter.getName());
+            }
+            storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames);
+        }
+
+        // All operations have now been performed, so we clean up everything and terminate.
+        storm::utility::cleanUp();
+        return 0;
+    } catch (storm::exceptions::BaseException const &exception) {
+        STORM_LOG_ERROR("An exception caused Storm-pomdp to terminate. The message of the exception is: " << exception.what());
+        return 1;
+    } catch (std::exception const &exception) {
+        STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pomdp to terminate. The message of this exception is: " << exception.what());
+        return 2;
+    }
+}

src/storm-pomdp/CMakeLists.txt

@@ -0,0 +1,40 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.h ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-pomdp)
+
+
+
+file(GLOB_RECURSE STORM_POMDP_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.cpp)
+file(GLOB_RECURSE STORM_POMDP_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.h)
+
+
+# Create storm-pomdp.
+add_library(storm-pomdp SHARED ${STORM_POMDP_SOURCES} ${STORM_POMDP_HEADERS})
+
+# Remove define symbol for shared libstorm.
+set_target_properties(storm-pomdp PROPERTIES DEFINE_SYMBOL "")
+#add_dependencies(storm resources)
+list(APPEND STORM_TARGETS storm-pomdp)
+set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
+
+target_link_libraries(storm-pomdp PUBLIC storm ${STORM_POMDP_LINK_LIBRARIES})
+
+# Install storm headers to include directory.
+foreach(HEADER ${STORM_POMDP_HEADERS})
+    string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
+    string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
+    string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
+    add_custom_command(
+            OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+            COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
+            COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
+            DEPENDS ${HEADER}
+    )
+    list(APPEND STORM_POMDP_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
+endforeach()
+add_custom_target(copy_storm_pomdp_headers DEPENDS ${STORM_POMDP_OUTPUT_HEADERS} ${STORM_POMDP_HEADERS})
+add_dependencies(storm-pomdp copy_storm_pomdp_headers)
+
+# installation
+install(TARGETS storm-pomdp RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+

src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp

@@ -0,0 +1,74 @@
+#include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h"
+
+namespace storm {
+    namespace transformer {
+
+        struct RationalFunctionConstructor {
+            RationalFunctionConstructor() : cache(std::make_shared<RawPolynomialCache>()) {
+
+            }
+
+            storm::RationalFunction translate(storm::RationalFunctionVariable const& var) {
+                storm::Polynomial pol(storm::RawPolynomial(var), cache);
+                return storm::RationalFunction(pol);
+            }
+
+            std::shared_ptr<RawPolynomialCache> cache;
+        };
+
+        template<typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::transform() const {
+            uint64_t nrStates = pomdp.getNumberOfStates();
+            std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> parameters;
+            bool nondeterminism = false;
+            storm::storage::SparseMatrixBuilder<storm::RationalFunction> smb(nrStates, nrStates, 0, !nondeterminism, false, nrStates);
+
+            RationalFunctionConstructor ratFuncConstructor;
+
+            for (uint64_t state = 0; state < nrStates; ++state) {
+                if (nondeterminism) {
+                    smb.newRowGroup(state);
+                }
+                auto observation = pomdp.getObservation(state);
+                auto it = parameters.find(observation);
+                std::vector<storm::RationalFunction> localWeights;
+                if (it == parameters.end()) {
+                    storm::RationalFunction lastWeight(1);
+                    for (uint64_t a = 0; a < pomdp.getNumberOfChoices(state) - 1; ++a) {
+                        std::string varName = "p" + std::to_string(observation) + "_" + std::to_string(a);
+                        localWeights.push_back(ratFuncConstructor.translate(carl::freshRealVariable(varName)));
+                        lastWeight -= localWeights.back();
+                    }
+                    localWeights.push_back(lastWeight);
+                    parameters.emplace(observation, localWeights);
+                } else {
+                    STORM_LOG_ASSERT(it->second.size() == pomdp.getNumberOfChoices(state), "Number of choices must be equal for every state with same number of actions");
+                    localWeights = it->second;
+                }
+                std::map<uint64_t, storm::RationalFunction> weightedTransitions;
+                for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
+                    for (auto const& entry: pomdp.getTransitionMatrix().getRow(state, action)) {
+                        auto it = weightedTransitions.find(entry.getColumn());
+                        if (it == weightedTransitions.end()) {
+                            weightedTransitions[entry.getColumn()] = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(entry.getValue()) * localWeights[action]; //carl::rationalize<storm::RationalFunctionCoefficient>(entry.getValue()) * localWeights[action];
+                        } else {
+                            it->second += storm::utility::convertNumber<storm::RationalFunctionCoefficient>(entry.getValue()) * localWeights[action];
+                        }
+                    }
+                }
+
+                for (auto const& entry : weightedTransitions) {
+                    smb.addNextValue(state, entry.first, entry.second);
+                }
+            }
+
+            // TODO rewards.
+
+            storm::storage::sparse::ModelComponents<storm::RationalFunction> modelComponents(smb.build(),pomdp.getStateLabeling());
+            return std::make_shared<storm::models::sparse::Dtmc<storm::RationalFunction>>(modelComponents);
+
+        }
+
+        template class ApplyFiniteSchedulerToPomdp<storm::RationalNumber>;
+    }
+}

src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h

@@ -0,0 +1,23 @@
+#pragma once
+
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Pomdp.h"
+#include <map>
+#include <string>
+
+namespace storm {
+    namespace transformer {
+
+        template<typename ValueType>
+        class ApplyFiniteSchedulerToPomdp {
+
+        public:
+            ApplyFiniteSchedulerToPomdp(storm::models::sparse::Pomdp<ValueType> const& pomdp) : pomdp(pomdp) {
+
+            }
+
+            std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transform() const;
+            storm::models::sparse::Pomdp<ValueType> const& pomdp;
+        };
+    }
+}

src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp

@@ -0,0 +1,64 @@
+#include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h"
+#include "storm/storage/BitVector.h"
+#include <vector>
+
+namespace storm {
+    namespace transformer {
+
+
+        template<typename ValueType>
+        std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> GlobalPOMDPSelfLoopEliminator<ValueType>::transform() const
+        {
+            uint64_t nrStates = pomdp.getNumberOfStates();
+            bool nondeterminism = false;
+
+            std::vector<storm::storage::BitVector> observationSelfLoopMasks;
+            for (uint64_t obs = 0; obs < pomdp.getNrObservations(); ++obs) {
+                observationSelfLoopMasks.push_back(storm::storage::BitVector());
+            }
+
+
+            for (uint64_t state = 0; state < nrStates; ++state) {
+                uint32_t observation = pomdp.getObservation(state);
+                storm::storage::BitVector actionVector(pomdp.getNumberOfChoices(state), false);
+                for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
+                    // We just look at the first entry.
+                    for (auto const& entry: pomdp.getTransitionMatrix().getRow(state, action)) {
+                        if (storm::utility::isOne(entry.getValue()) && entry.getColumn() == state) {
+                            actionVector.set(action);
+                        }
+                        break;
+                    }
+                }
+                if (observationSelfLoopMasks[observation].size() == 0) {
+                    observationSelfLoopMasks[observation] = actionVector;
+                } else {
+                    observationSelfLoopMasks[observation] &= actionVector;
+                }
+            }
+
+            storm::storage::BitVector filter(pomdp.getNumberOfChoices(), true);
+            uint64_t offset = 0;
+            for (uint64_t state = 0; state < nrStates; ++state) {
+                uint32_t observation = pomdp.getObservation(state);
+                storm::storage::BitVector& vec = observationSelfLoopMasks[observation];
+                if (vec.full()) {
+                    vec.set(0, false);
+                }
+                for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
+                    if (vec.get(action)) {
+                        filter.set(offset + action);
+                    }
+                }
+                offset += pomdp.getNumberOfChoices(state);
+            }
+            // TODO rewards.
+
+            //storm::storage::sparse::ModelComponents<storm::RationalFunction> modelComponents(smb.build(),pomdp.getStateLabeling());
+            //return std::make_shared<storm::models::sparse::Dtmc<storm::RationalFunction>>(modelComponents);
+
+        }
+
+        template class GlobalPOMDPSelfLoopEliminator<storm::RationalNumber>;
+    }
+}

src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h

@@ -0,0 +1,20 @@
+#pragma once
+
+#include "storm/models/sparse/Pomdp.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<typename ValueType>
+        class GlobalPOMDPSelfLoopEliminator {
+
+        public:
+            GlobalPOMDPSelfLoopEliminator(storm::models::sparse::Pomdp<ValueType> const& pomdp) : pomdp(pomdp) {
+
+            }
+
+            std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> transform() const;
+            storm::models::sparse::Pomdp<ValueType> const& pomdp;
+        };
+    }
+}