From 75a2c70af637e92b65b28d743f08301122dbfa41 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 20 Oct 2020 14:41:01 -0700 Subject: [PATCH] minor extensions to examples --- CHANGELOG.md | 1 + examples/analysis/03-analysis.py | 5 +- .../building_models/01-building-models.py | 9 +++ examples/pomdp/01-pomdps.py | 62 ++++++++++--------- 4 files changed, 46 insertions(+), 31 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a4ed052..d1d6ec9 100644 --- a/CHANGELOG.md +++ b/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) diff --git a/examples/analysis/03-analysis.py b/examples/analysis/03-analysis.py index a43638e..d6936ea 100644 --- a/examples/analysis/03-analysis.py +++ b/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])) diff --git a/examples/building_models/01-building-models.py b/examples/building_models/01-building-models.py index 2ecccbf..1061254 100644 --- a/examples/building_models/01-building-models.py +++ b/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() \ No newline at end of file diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py index e6671d4..322773c 100644 --- a/examples/pomdp/01-pomdps.py +++ b/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()