From 86a64c7f3588af01aacbd6646d85c5d2766daec3 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Wed, 9 Aug 2023 13:41:16 +0200 Subject: [PATCH] some example adaptions removed optimal simulator --- examples/shields/01_pre_shield_extraction.py | 5 +- examples/shields/07_pre_shield_simulator.py | 6 +-- .../shields/09_optimal_shield_simulator.py | 53 ------------------- examples/shields/10_optimal_controller.py | 9 ---- lib/stormpy/examples/files.py | 1 + 5 files changed, 7 insertions(+), 67 deletions(-) delete mode 100644 examples/shields/09_optimal_shield_simulator.py delete mode 100644 examples/shields/10_optimal_controller.py diff --git a/examples/shields/01_pre_shield_extraction.py b/examples/shields/01_pre_shield_extraction.py index 24f5e94..4b24a85 100644 --- a/examples/shields/01_pre_shield_extraction.py +++ b/examples/shields/01_pre_shield_extraction.py @@ -18,7 +18,7 @@ for allowed choices in a state. def pre_shield_extraction(): path = stormpy.examples.files.prism_mdp_lava_simple - formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) @@ -31,7 +31,8 @@ def pre_shield_extraction(): initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + #shield_specification = ShieldingExpression(type="PreSafety", gamma=0.8) TODO Parameter for shield expression would be nice to have + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) #, shielding_expression=shield_specification) assert result.has_scheduler assert result.has_shield diff --git a/examples/shields/07_pre_shield_simulator.py b/examples/shields/07_pre_shield_simulator.py index a5433ea..b4167a5 100644 --- a/examples/shields/07_pre_shield_simulator.py +++ b/examples/shields/07_pre_shield_simulator.py @@ -14,8 +14,8 @@ Simulating a model with the usage of a pre shield """ def example_pre_shield_simulator(): - path = stormpy.examples.files.prism_mdp_lava_simple - formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + path = stormpy.examples.files.prism_mdp_cliff_walking + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) @@ -47,7 +47,7 @@ def example_pre_shield_simulator(): if not choices: break - + index = random.randint(0, len(choices) - 1) selected_action = choices[index] choice_label = model.choice_labeling.get_labels_of_choice(model.get_choice_index(current_state, selected_action[1])) diff --git a/examples/shields/09_optimal_shield_simulator.py b/examples/shields/09_optimal_shield_simulator.py deleted file mode 100644 index 0d55c4c..0000000 --- a/examples/shields/09_optimal_shield_simulator.py +++ /dev/null @@ -1,53 +0,0 @@ -import stormpy -import stormpy.core -import stormpy.simulator - - -import stormpy.shields - -import stormpy.examples -import stormpy.examples.files - -import random - - -def optimal_shield_simulator(): - path = stormpy.examples.files.prism_smg_lights - formula_str = " <> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]" - - program = stormpy.parse_prism_program(path) - formulas = stormpy.parse_properties_for_prism_program(formula_str, program) - - options = stormpy.BuilderOptions([p.raw_formula for p in formulas]) - options.set_build_state_valuations(True) - options.set_build_choice_labels(True) - options.set_build_all_labels() - model = stormpy.build_sparse_model_with_options(program, options) - - result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) - - assert result.has_scheduler - assert result.has_shield - - shield = result.shield - - scheduler = shield.construct() - simulator = stormpy.simulator.create_simulator(model)#, seed=42) - - print(simulator) - while not simulator.is_done(): - current_state = simulator.get_current_state() - state_string = model.state_valuations.get_string(current_state) - # print(F"Simulator is in state {state_string}.") - temp = scheduler.get_choice(current_state) - # print(F"Correction map is {temp.choice_map}") - # print([model.get_label_of_choice(current_state, x) for x in simulator.available_actions()]) - print(F"Available actions {simulator.available_actions()}") - for action in simulator.available_actions(): - print(F"Action: {action} ActionLabel: {model.get_label_of_choice(current_state, action)}") - observation, reward = simulator.step() - - - -if __name__ == '__main__': - optimal_shield_simulator() \ No newline at end of file diff --git a/examples/shields/10_optimal_controller.py b/examples/shields/10_optimal_controller.py deleted file mode 100644 index 4bd9422..0000000 --- a/examples/shields/10_optimal_controller.py +++ /dev/null @@ -1,9 +0,0 @@ -import stormpy -import stormpy.core -import stormpy.simulator - - -import stormpy.shields - -import stormpy.examples -import stormpy.examples.files \ No newline at end of file diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index b2fec9a..2bda794 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -52,6 +52,7 @@ gspn_pnml_simple = _path("gspn", "gspn_simple.pnml") """Shield Example 1""" prism_mdp_lava_simple = _path("mdp", "simple.prism") +prism_mdp_cliff_walking = _path("mdp", "CliffZigZag.prism") """Optimal Shield Example 1""" prism_smg_lights = _path("smg", "lights.prism")