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