python bindings for our UAI18 paper on POMDP + FSC -> PMC

examples/pomdp/01-pomdps.py

@@ -0,0 +1,45 @@
+import stormpy
+import stormpy.core
+import stormpy.info
+
+import pycarl
+import pycarl.core
+
+import stormpy.examples
+import stormpy.examples.files
+
+import stormpy.pomdp
+
+import stormpy._config as config
+
+
+def example_parametric_models_02():
+    # Check support for parameters
+    if not config.storm_with_pars:
+        print("Support parameters is missing. Try building storm-pars.")
+        return
+
+    import stormpy.pars
+    from pycarl.formula import FormulaType, Relation
+    if stormpy.info.storm_ratfunc_use_cln():
+        import pycarl.cln.formula
+    else:
+        import pycarl.gmp.formula
+
+    path = stormpy.examples.files.prism_pomdp_maze
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [\"goal\"]"
+    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+    pomdp = stormpy.build_model(prism_program, properties)
+    pomdp = stormpy.pomdp.make_canonic(pomdp)
+    pomdp = stormpy.pomdp.make_simple(pomdp)
+    memory_builder = stormpy.pomdp.PomdpMemoryBuilder()
+    memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2)
+    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
+    pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear)
+
+    stormpy.export_parametric_to_drn(pmc, "test.out")
+
+if __name__ == '__main__':
+    example_parametric_models_02()

lib/stormpy/pomdp/__init__.py

@@ -2,7 +2,44 @@ from . import pomdp
 from .pomdp import *
 
 def make_canonic(model):
+    """
+    Make the POMDP canonic
+    :param model:
+    :return:
+    """
+
     if model.supports_parameters:
         return pomdp._make_canonic_Rf(model)
     else:
-        return pomdp._make_canonic_Double(model)
+        return pomdp._make_canonic_Double(model)
+
+def make_simple(model):
+    """
+    Make the POMDP simple (aka alternating), i.e., each state has at most two actions, and if there is nondeterminism, then there is no probabilistic branching,
+
+    :param model:
+    :return:
+    """
+    if model.supports_parameters:
+        return pomdp._make_simple_Rf(model)
+    else:
+        return pomdp._make_simple_Double(model)
+
+def unfold_memory(model, memory):
+    """
+    Unfold the memory for an FSC into the POMDP
+
+    :param model: A pomdp
+    :param memory: A memory structure
+    :return: A pomdp that contains states from the product of the original POMDP and the FSC Memory
+    """
+    if model.supports_parameters:
+        return pomdp._unfold_memory_Rf(model, memory)
+    else:
+        return pomdp._unfold_memory_Double(model, memory)
+
+def apply_unknown_fsc(model, mode):
+    if model.supports_parameters:
+        return pomdp._apply_unknown_fsc_Rf(model, mode)
+    else:
+        return pomdp._apply_unknown_fsc_Double(model, mode)

src/mod_pomdp.cpp

@@ -4,6 +4,7 @@
 #include "pomdp/tracker.h"
 #include "pomdp/qualitative_analysis.h"
 #include "pomdp/transformations.h"
+#include "pomdp/memory.h"
 #include <storm/adapters/RationalFunctionAdapter.h>
 
 PYBIND11_MODULE(pomdp, m) {
@@ -16,6 +17,8 @@ PYBIND11_MODULE(pomdp, m) {
     define_tracker(m);
     define_qualitative_policy_search<double>(m, "Double");
     define_qualitative_policy_search_nt(m);
+    define_memory(m);
+    define_transformations_nt(m);
     define_transformations<double>(m, "Double");
     define_transformations<storm::RationalFunction>(m, "Rf");
 }

src/pomdp/memory.cpp

@@ -0,0 +1,27 @@
+#include "memory.h"
+#include "src/helpers.h"
+#include <storm-pomdp/storage/PomdpMemory.h>
+
+
+void define_memory(py::module& m) {
+    py::class_<storm::storage::PomdpMemory> memory(m, "PomdpMemory", "Memory for POMDP policies");
+    memory.def_property_readonly("nr_states",&storm::storage::PomdpMemory::getNumberOfStates, "How many states does the memory structure have");
+
+    // Trivial, FixedCounter, SelectiveCounter, FixedRing, SelectiveRing, SettableBits, Full
+    py::enum_<storm::storage::PomdpMemoryPattern>(m, "PomdpMemoryPattern", "Memory pattern for POMDP memory")
+            .value("trivial", storm::storage::PomdpMemoryPattern::Trivial)
+            .value("fixed_counter", storm::storage::PomdpMemoryPattern::FixedCounter)
+            .value("selective_counter", storm::storage::PomdpMemoryPattern::SelectiveCounter)
+            .value("fixed_ring", storm::storage::PomdpMemoryPattern::FixedRing)
+            .value("selective_ring", storm::storage::PomdpMemoryPattern::SelectiveRing)
+            .value("settable_bits", storm::storage::PomdpMemoryPattern::SettableBits)
+            .value("full", storm::storage::PomdpMemoryPattern::Full)
+            ;
+
+
+    py::class_<storm::storage::PomdpMemoryBuilder> memorybuilder(m, "PomdpMemoryBuilder", "MemoryBuilder for POMDP policies");
+    memorybuilder.def(py::init<>());
+    memorybuilder.def("build", &storm::storage::PomdpMemoryBuilder::build, py::arg("pattern"), py::arg("nr_states"));
+
+
+}

src/pomdp/memory.h

@@ -0,0 +1,4 @@
+#pragma once
+#include "common.h"
+
+void define_memory(py::module& m);

src/pomdp/transformations.cpp

@@ -1,5 +1,8 @@
 #include "transformations.h"
 #include <storm-pomdp/transformer/MakePOMDPCanonic.h>
+#include <storm-pomdp/transformer/PomdpMemoryUnfolder.h>
+#include <storm-pomdp/transformer/BinaryPomdpTransformer.h>
+#include <storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h>
 
 template<typename ValueType>
 std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::models::sparse::Pomdp<ValueType> const& pomdp) {
@@ -7,9 +10,41 @@ std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::mod
     return makeCanonic.transform();
 }
 
+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::PomdpMemory const& memory) {
+    storm::transformer::PomdpMemoryUnfolder<ValueType> unfolder(pomdp, memory);
+    return unfolder.transform();
+}
+
+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const& pomdp) {
+    storm::transformer::BinaryPomdpTransformer<ValueType> transformer;
+    return transformer.transform(pomdp,true);
+}
+
+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> apply_unknown_fsc(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::transformer::PomdpFscApplicationMode const& applicationMode) {
+    storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> transformer(pomdp);
+    return transformer.transform(applicationMode);
+}
+// STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL
+void define_transformations_nt(py::module &m) {
+    py::enum_<storm::transformer::PomdpFscApplicationMode>(m, "PomdpFscApplicationMode")
+            .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD)
+            .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR)
+            .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE)
+            .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG)
+            .value("full", storm::transformer::PomdpFscApplicationMode::FULL)
+            ;
+
+}
+
 template<typename ValueType>
 void define_transformations(py::module& m, std::string const& vtSuffix) {
     m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic<ValueType>, "Return a canonicly-ordered POMDP", py::arg("pomdp"));
+    m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory<ValueType>, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"));
+    m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple<ValueType>, "Make POMDP simple", py::arg("pomdp"));
+    m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
 }
 
 template void define_transformations<double>(py::module& m, std::string const& vtSuffix);

src/pomdp/transformations.h

@@ -2,5 +2,6 @@
 
 #include "common.h"
 
+void define_transformations_nt(py::module& m);
 template<typename VT>
 void define_transformations(py::module& m, std::string const& vtSuffix);

src/storage/expressions.cpp

@@ -14,8 +14,6 @@ void define_expressions(py::module& m) {
     using Variable = storm::expressions::Variable;
     using Valuation = storm::expressions::Valuation;
 
-
-
     // ExpressionManager
     py::class_<storm::expressions::ExpressionManager, std::shared_ptr<storm::expressions::ExpressionManager>>(m, "ExpressionManager", "Manages variables for expressions")
         .def(py::init(), "Constructor")