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()