diff --git a/examples/shields/01_pre_shield_extraction.py b/examples/shields/01_pre_shield_extraction.py new file mode 100644 index 0000000..24f5e94 --- /dev/null +++ b/examples/shields/01_pre_shield_extraction.py @@ -0,0 +1,46 @@ +import stormpy +import stormpy.core +import stormpy.simulator + + +import stormpy.shields + +import stormpy.examples +import stormpy.examples.files + +""" + +Example for the extraction of a Pre Safety Shield +from a model checking result and querying the shield +for allowed choices in a state. + +""" + +def pre_shield_extraction(): + path = stormpy.examples.files.prism_mdp_lava_simple + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + + 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) + + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + assert result.has_scheduler + assert result.has_shield + + shield = result.shield + + for state_id in model.states: + choices = shield.construct().get_choice(state_id) + print(F"Allowed choices in state {state_id}, are {choices.choice_map} ") + + +if __name__ == '__main__': + pre_shield_extraction() \ No newline at end of file diff --git a/examples/shields/02_post_shield_extraction.py b/examples/shields/02_post_shield_extraction.py new file mode 100644 index 0000000..4e7199a --- /dev/null +++ b/examples/shields/02_post_shield_extraction.py @@ -0,0 +1,49 @@ +import stormpy +import stormpy.core +import stormpy.simulator + + +import stormpy.shields + +import stormpy.examples +import stormpy.examples.files + + +""" + +Example for the extraction of a Post Safety Shield +from a model checking result and querying the shield +for allowed actions. + +""" + + +def post_shield_extraction(): + path = stormpy.examples.files.prism_mdp_lava_simple + formula_str = " Pmax=? [G !\"AgentIsInLavaAndNotDone\"]" + + 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) + + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + assert result.has_scheduler + assert result.has_shield + + shield = result.shield + + for state_id in model.states: + choices = shield.construct().get_choice(state_id) + print(F"Allowed choices in state {state_id}, are {choices.choice_map} ") + + + +if __name__ == '__main__': + post_shield_extraction() \ No newline at end of file diff --git a/examples/shields/04_optimal_shield.py b/examples/shields/03_optimal_shield_extraction.py similarity index 54% rename from examples/shields/04_optimal_shield.py rename to examples/shields/03_optimal_shield_extraction.py index 75b29f3..6b03f14 100644 --- a/examples/shields/04_optimal_shield.py +++ b/examples/shields/03_optimal_shield_extraction.py @@ -7,10 +7,9 @@ import stormpy.shields import stormpy.examples import stormpy.examples.files -import random -def optimal_shield_03(): +def optimal_shield_extraction(): path = stormpy.examples.files.prism_smg_robot formula_str = " <> R{\"travel_costs\"}min=? [ LRA ]" @@ -24,35 +23,17 @@ def optimal_shield_03(): model = stormpy.build_sparse_model_with_options(program, options) result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) - assert result.has_scheduler - print(F"Check Scheduler: {result.has_scheduler}") - print(F"Check Shield: {result.has_schield}") - print(type(result)) + assert result.has_scheduler + assert result.has_shield shield = result.shield - scheduler = result.scheduler - - print(type(shield)) - - assert scheduler.memoryless - assert scheduler.deterministic - constructed_shield = shield.construct() - - print(type(constructed_shield)) - - stormpy.shields.export_shieldDouble(model, shield) + for state_id in model.states: + choices = shield.construct().get_choice(state_id) + print(F"Allowed choices in state {state_id}, are {choices.choice_map} ") - # for state in model.states: - # choice = scheduler.get_choice(state) - # action = choice.get_deterministic_choice() - # print("In state {} choose action {}".format(state, action)) - - # dtmc = model.apply_scheduler(scheduler) - # print(dtmc) - if __name__ == '__main__': - optimal_shield_03() \ No newline at end of file + optimal_shield_extraction() \ No newline at end of file diff --git a/examples/shields/02_post_shield.py b/examples/shields/04_pre_shield_export.py similarity index 71% rename from examples/shields/02_post_shield.py rename to examples/shields/04_pre_shield_export.py index 2dc19b2..3b4daef 100644 --- a/examples/shields/02_post_shield.py +++ b/examples/shields/04_pre_shield_export.py @@ -7,12 +7,17 @@ import stormpy.shields import stormpy.examples import stormpy.examples.files -import random +""" -def post_shield_02(): +Example of exporting a Pre Safety Shield +to a file + +""" + +def pre_schield(): 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) @@ -27,17 +32,13 @@ def post_shield_02(): assert initial_state == 0 result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler - assert result.has_schield + assert result.has_shield shield = result.shield - lookup = stormpy.shields.create_shield_action_lookup(model, shield) - query = list(lookup.keys())[0] + stormpy.shields.export_shieldDouble(model, shield) - print(query) - print(lookup[query]) - if __name__ == '__main__': - post_shield_02() \ No newline at end of file + pre_schield() \ No newline at end of file diff --git a/examples/shields/01_pre_shield.py b/examples/shields/05_post_shield_export.py similarity index 71% rename from examples/shields/01_pre_shield.py rename to examples/shields/05_post_shield_export.py index f90b683..b6265b0 100644 --- a/examples/shields/01_pre_shield.py +++ b/examples/shields/05_post_shield_export.py @@ -7,12 +7,17 @@ import stormpy.shields import stormpy.examples import stormpy.examples.files -import random +""" -def pre_schield_01(): +Example of exporting a Pre Safety Shield +to a file + +""" + +def pre_schield(): 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) @@ -27,16 +32,13 @@ def pre_schield_01(): assert initial_state == 0 result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler - assert result.has_schield + assert result.has_shield shield = result.shield + + stormpy.shields.export_shieldDouble(model, shield) - lookup = stormpy.shields.create_shield_action_lookup(model, shield) - query = list(lookup.keys())[0] - - print(query) - print(lookup[query]) if __name__ == '__main__': - pre_schield_01() \ No newline at end of file + pre_schield() \ No newline at end of file diff --git a/examples/shields/03_optimal_shield.py b/examples/shields/06_optimal_shield_export.py similarity index 57% rename from examples/shields/03_optimal_shield.py rename to examples/shields/06_optimal_shield_export.py index d922137..f8087f5 100644 --- a/examples/shields/03_optimal_shield.py +++ b/examples/shields/06_optimal_shield_export.py @@ -7,10 +7,14 @@ import stormpy.shields import stormpy.examples import stormpy.examples.files -import random -def optimal_shield_03(): +""" +Example of exporting a Optimal Shield +to a file +""" + +def optimal_shield_export(): path = stormpy.examples.files.prism_smg_lights formula_str = " <> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]" @@ -25,34 +29,12 @@ def optimal_shield_03(): result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler - print(F"Check Scheduler: {result.has_scheduler}") - print(F"Check Shield: {result.has_schield}") + assert result.has_shield - print(type(result)) - shield = result.shield - scheduler = result.scheduler - - print(type(shield)) - - assert scheduler.memoryless - assert scheduler.deterministic - - constructed_shield = shield.construct() - - print(type(constructed_shield)) stormpy.shields.export_shieldDouble(model, shield) - - # for state in model.states: - # choice = scheduler.get_choice(state) - # action = choice.get_deterministic_choice() - # print("In state {} choose action {}".format(state, action)) - - # dtmc = model.apply_scheduler(scheduler) - # print(dtmc) - if __name__ == '__main__': - optimal_shield_03() \ No newline at end of file + optimal_shield_export() \ No newline at end of file diff --git a/examples/shields/07_pre_shield_simulator.py b/examples/shields/07_pre_shield_simulator.py new file mode 100644 index 0000000..f08d7ff --- /dev/null +++ b/examples/shields/07_pre_shield_simulator.py @@ -0,0 +1,59 @@ +import stormpy +import stormpy.core +import stormpy.simulator + +import stormpy.shields + +import stormpy.examples +import stormpy.examples.files + +import random + +""" +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\"]" + + 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) + + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) + assert result.has_scheduler + assert result.has_shield + + shield = result.shield + + pre_scheduler = shield.construct() + + simulator = stormpy.simulator.create_simulator(model, seed=42) + final_outcomes = dict() + for n in range(1000): + while not simulator.is_done(): + current_state = simulator.get_current_state() + choices = pre_scheduler.get_choice(current_state).choice_map + index = random.randint(0, len(choices) - 1) + selected_action = choices[index] + state_string = model.state_valuations.get_string(current_state) + print(F"Simulator is in state {state_string}. Allowed Choices are {choices}. Selected Action: {selected_action}") + observation, reward = simulator.step(selected_action[1]) + if observation not in final_outcomes: + final_outcomes[observation] = 1 + else: + final_outcomes[observation] += 1 + simulator.restart() + + + +if __name__ == '__main__': + example_pre_shield_simulator() diff --git a/examples/shields/08_post_shield_simulator.py b/examples/shields/08_post_shield_simulator.py new file mode 100644 index 0000000..e69de29 diff --git a/examples/shields/09_optimal_shield_simulator.py b/examples/shields/09_optimal_shield_simulator.py new file mode 100644 index 0000000..e69de29 diff --git a/examples/shields/10_optimal_controller.py b/examples/shields/10_optimal_controller.py new file mode 100644 index 0000000..4bd9422 --- /dev/null +++ b/examples/shields/10_optimal_controller.py @@ -0,0 +1,9 @@ +import stormpy +import stormpy.core +import stormpy.simulator + + +import stormpy.shields + +import stormpy.examples +import stormpy.examples.files \ No newline at end of file