minor extensions to examples

CHANGELOG.md

@@ -8,6 +8,7 @@ Version 1.6.x
 - Documentation is largely based on Jupyter notebooks now and supports launch with Binder
 - Support for exact arithmetic in models
 - Support for timeouts/signal handlers in storm
+- Code for parametric/exact/floating-point models data structures unified. 
 - `export_parametric_to_drn` no longer exists, use `export_to_drn` instead
 
 ### Version 1.6.2 (2020/09)

examples/analysis/03-analysis.py

@@ -14,8 +14,9 @@ def example_analysis_03():
     model = stormpy.build_model(prism_program, properties)
     env = stormpy.Environment()
     env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
-    env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
-    env.solver_environment.native_solver_environment.maximum_iterations = 2
+    env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.optimistic_value_iteration
+    env.solver_environment.native_solver_environment.precision = stormpy.Rational("0.9")
+    #env.solver_environment.native_solver_environment.maximum_iterations = 2
     result = stormpy.model_checking(model, properties[0], environment=env)
     print(result.at(model.initial_states[0]))
 

examples/building_models/01-building-models.py

@@ -3,6 +3,8 @@ import stormpy.core
 
 import stormpy.examples
 import stormpy.examples.files
+import stormpy.pomdp
+
 
 
 def example_building_models_01():
@@ -23,6 +25,13 @@ def example_building_models_01():
     print(model.model_type)
     print("Number of states: {}".format(model.nr_states))
 
+    # POMDPs should be constructed with choice labels
+    path = stormpy.examples.files.drn_pomdp_maze
+    opts = stormpy.DirectEncodingParserOptions()
+    opts.build_choice_labels = True
+    pomdp = stormpy.build_model_from_drn(stormpy.examples.files.drn_pomdp_maze, opts)
+    # POMDPs need to be in a canonic representation
+    pomdp = stormpy.pomdp.make_canonic(pomdp)
 
 if __name__ == '__main__':
     example_building_models_01()

examples/pomdp/01-pomdps.py

@@ -28,55 +28,59 @@ def example_parametric_models_01():
 
     # Prevent curious side effects from earlier runs (for tests only)
     pycarl.clear_pools()
-    ###
-    # 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)
+    # ###
+    # # 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=? [!\"bad\" U \"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)
 
     ####
     # 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\"]"
+    formula_str = "P=? [!\"bad\" U \"goal\"]"
     properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
     # construct the pPOMDP
-    pomdp = stormpy.build_parametric_model(prism_program, properties)
+    options = stormpy.BuilderOptions([p.raw_formula for p in properties])
+    options.set_build_state_valuations()
+    options.set_build_choice_labels()
+    pomdp = stormpy.build_sparse_parametric_model_with_options(prism_program, options)
     # 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)
+    memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 3)
     # apply the memory onto the POMDP to get the cartesian product
-    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
+    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory, add_memory_labels=True, keep_state_valuations=True)
+    # make the POMDP simple. This step is optional but often beneficial
+    pomdp = stormpy.pomdp.make_simple(pomdp, keep_state_valuations=True)
     # 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.
+    export_pmc = True # 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)
+        stormpy.export_to_drn(pmc, "test.out", export_options)
 
 if __name__ == '__main__':
     example_parametric_models_01()