From b181e807b304d9190775362fab304382add40c05 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Thu, 9 Jul 2020 22:59:02 -0700
Subject: [PATCH] example for UAI18 now with comments

---
 examples/pomdp/01-pomdps.py | 41 ++++++++++++++++++++++++++++++++++---
 1 file changed, 38 insertions(+), 3 deletions(-)

diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py
index e05d4d8..2e7a3c1 100644
--- a/examples/pomdp/01-pomdps.py
+++ b/examples/pomdp/01-pomdps.py
@@ -13,7 +13,7 @@ import stormpy.pomdp
 import stormpy._config as config
 
 
-def example_parametric_models_02():
+def example_parametric_models_01():
     # Check support for parameters
     if not config.storm_with_pars:
         print("Support parameters is missing. Try building storm-pars.")
@@ -26,20 +26,55 @@ def example_parametric_models_02():
     else:
         import pycarl.gmp.formula
 
+    ###
+    # How to apply an unknown FSC to obtain a pMC from a POMDP
     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)
+    # construct the POMDP
     pomdp = stormpy.build_model(prism_program, properties)
+    # make its representation canonic.
     pomdp = stormpy.pomdp.make_canonic(pomdp)
+    # make the POMDP simple. This step is optional but often beneficial
     pomdp = stormpy.pomdp.make_simple(pomdp)
+    # construct the memory for the FSC
+    # in this case, a selective counter with two states
     memory_builder = stormpy.pomdp.PomdpMemoryBuilder()
     memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2)
+    # apply the memory onto the POMDP to get the cartesian product
     pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
+    # apply the memory onto the POMDP to get the cartesian product
     pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear)
 
-    stormpy.export_parametric_to_drn(pmc, "test.out")
+    ####
+    # How to apply an unknown FSC to obtain a pMC from a pPOMDP
+    path = stormpy.examples.files.prism_par_pomdp_maze
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [\"goal\"]"
+    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+    # construct the pPOMDP
+    pomdp = stormpy.build_parametric_model(prism_program, properties)
+    # make its representation canonic.
+    pomdp = stormpy.pomdp.make_canonic(pomdp)
+    # make the POMDP simple. This step is optional but often beneficial
+    pomdp = stormpy.pomdp.make_simple(pomdp)
+    # construct the memory for the FSC
+    # in this case, a selective counter with two states
+    memory_builder = stormpy.pomdp.PomdpMemoryBuilder()
+    memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2)
+    # apply the memory onto the POMDP to get the cartesian product
+    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
+    # apply the unknown FSC to obtain a pmc from the POMDP
+    pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear)
+
+    export_pmc = False # Set to True to export the pMC as drn.
+    if export_pmc:
+        export_options = stormpy.core.DirectEncodingOptions()
+        export_options.allow_placeholders = False
+        stormpy.export_parametric_to_drn(pmc, "test.out", export_options)
 
 if __name__ == '__main__':
-    example_parametric_models_02()
+    example_parametric_models_01()