some example adaptions removed optimal simulator

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 = "<ShieldFileName, PreSafety, gamma=0.9> 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
     

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 = "<ShieldFileName, PreSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    path = stormpy.examples.files.prism_mdp_cliff_walking
+    formula_str = "<ShieldFileName, PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)

examples/shields/09_optimal_shield_simulator.py

@@ -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 = "<optimal, Optimal> <<shield>> 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()

examples/shields/10_optimal_controller.py

@@ -1,9 +0,0 @@
-import stormpy
-import stormpy.core
-import stormpy.simulator
-
-
-import stormpy.shields
-
-import stormpy.examples
-import stormpy.examples.files

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