From 790fbffd6df386ffdbb995449dea664e6c47b8fd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 22 Aug 2017 19:22:44 +0200 Subject: [PATCH] pomdps in an own cli, support for application of stochastic schedulers, etc --- src/CMakeLists.txt | 2 + src/storm-pomdp-cli/CMakeLists.txt | 11 ++ .../settings/modules/POMDPSettings.cpp | 44 ++++++ .../settings/modules/POMDPSettings.h | 41 ++++++ src/storm-pomdp-cli/storm-pomdp.cpp | 126 ++++++++++++++++++ src/storm-pomdp/CMakeLists.txt | 40 ++++++ .../ApplyFiniteSchedulerToPomdp.cpp | 74 ++++++++++ .../transformer/ApplyFiniteSchedulerToPomdp.h | 23 ++++ .../GlobalPOMDPSelfLoopEliminator.cpp | 64 +++++++++ .../GlobalPOMDPSelfLoopEliminator.h | 20 +++ 10 files changed, 445 insertions(+) create mode 100644 src/storm-pomdp-cli/CMakeLists.txt create mode 100644 src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp create mode 100644 src/storm-pomdp-cli/settings/modules/POMDPSettings.h create mode 100644 src/storm-pomdp-cli/storm-pomdp.cpp create mode 100644 src/storm-pomdp/CMakeLists.txt create mode 100644 src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp create mode 100644 src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h create mode 100644 src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp create mode 100644 src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index acf819119..ef985f4e3 100644 --- a/src/CMakeLists.txt +++ b/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) diff --git a/src/storm-pomdp-cli/CMakeLists.txt b/src/storm-pomdp-cli/CMakeLists.txt new file mode 100644 index 000000000..b9a207371 --- /dev/null +++ b/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) diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp new file mode 100644 index 000000000..249ef585a --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h new file mode 100644 index 000000000..bbf5fa19f --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp new file mode 100644 index 000000000..3989b75f4 --- /dev/null +++ b/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::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(false); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + + storm::settings::addModule(); +} + +/*! + * 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(); + auto const& pomdpSettings = storm::settings::getModule(); + + // 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(symbolicInput, engine); + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP."); + storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*(model->template as>())); + + if (pomdpSettings.isExportToParametricSet()) { + auto const &pmc = toPMCTransformer.transform(); + storm::analysis::ConstraintCollector constraints(*pmc); + pmc->printModelInformationToStream(std::cout); + auto const& parameterSet = constraints.getVariables(); + std::vector parameters(parameterSet.begin(), parameterSet.end()); + std::vector 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; + } +} \ No newline at end of file diff --git a/src/storm-pomdp/CMakeLists.txt b/src/storm-pomdp/CMakeLists.txt new file mode 100644 index 000000000..53643b738 --- /dev/null +++ b/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) + diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp new file mode 100644 index 000000000..1c9cd87d2 --- /dev/null +++ b/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()) { + + } + + storm::RationalFunction translate(storm::RationalFunctionVariable const& var) { + storm::Polynomial pol(storm::RawPolynomial(var), cache); + return storm::RationalFunction(pol); + } + + std::shared_ptr cache; + }; + + template + std::shared_ptr> ApplyFiniteSchedulerToPomdp::transform() const { + uint64_t nrStates = pomdp.getNumberOfStates(); + std::unordered_map> parameters; + bool nondeterminism = false; + storm::storage::SparseMatrixBuilder 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 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 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(entry.getValue()) * localWeights[action]; //carl::rationalize(entry.getValue()) * localWeights[action]; + } else { + it->second += storm::utility::convertNumber(entry.getValue()) * localWeights[action]; + } + } + } + + for (auto const& entry : weightedTransitions) { + smb.addNextValue(state, entry.first, entry.second); + } + } + + // TODO rewards. + + storm::storage::sparse::ModelComponents modelComponents(smb.build(),pomdp.getStateLabeling()); + return std::make_shared>(modelComponents); + + } + + template class ApplyFiniteSchedulerToPomdp; + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h new file mode 100644 index 000000000..42fd45d94 --- /dev/null +++ b/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 +#include + +namespace storm { + namespace transformer { + + template + class ApplyFiniteSchedulerToPomdp { + + public: + ApplyFiniteSchedulerToPomdp(storm::models::sparse::Pomdp const& pomdp) : pomdp(pomdp) { + + } + + std::shared_ptr> transform() const; + storm::models::sparse::Pomdp const& pomdp; + }; + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp new file mode 100644 index 000000000..823e9f382 --- /dev/null +++ b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp @@ -0,0 +1,64 @@ +#include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h" +#include "storm/storage/BitVector.h" +#include + +namespace storm { + namespace transformer { + + + template + std::shared_ptr> GlobalPOMDPSelfLoopEliminator::transform() const + { + uint64_t nrStates = pomdp.getNumberOfStates(); + bool nondeterminism = false; + + std::vector 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 modelComponents(smb.build(),pomdp.getStateLabeling()); + //return std::make_shared>(modelComponents); + + } + + template class GlobalPOMDPSelfLoopEliminator; + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h new file mode 100644 index 000000000..6dec59124 --- /dev/null +++ b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h @@ -0,0 +1,20 @@ +#pragma once + +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace transformer { + + template + class GlobalPOMDPSelfLoopEliminator { + + public: + GlobalPOMDPSelfLoopEliminator(storm::models::sparse::Pomdp const& pomdp) : pomdp(pomdp) { + + } + + std::shared_ptr> transform() const; + storm::models::sparse::Pomdp const& pomdp; + }; + } +} \ No newline at end of file