changes to examples

examples/shields/02_post_shield_extraction.py

@@ -41,7 +41,7 @@ def post_shield_extraction():
   
     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} ")
+        print(F"Applied corrections in state {state_id}, are {choices.choice_map} ")
 
 
 

examples/shields/03_optimal_shield_extraction.py

@@ -29,9 +29,11 @@ def optimal_shield_extraction():
    
     shield = result.shield
 
-    for state_id in model.states:
+    state_ids = [x for x in model.states]
+
+    for state_id in state_ids[0:50]:
         choices = shield.construct().get_choice(state_id)
-        print(F"Allowed choices in state {state_id}, are {choices.choice_map} ")
+        print(F"Corrections in state {state_id}, are {choices.choice_map} ")
     
 
 

examples/shields/04_pre_shield_export.py

@@ -17,7 +17,7 @@ to a file
 
 def pre_schield():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<pre, PreSafety, gamma=0.2> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "<pre, 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/06_optimal_shield_export.py

@@ -16,7 +16,7 @@ to a file
 
 def optimal_shield_export():
     path = stormpy.examples.files.prism_smg_lights
-    formula_str = "<tlsShield, Optimal> <<shield>> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]"
+    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)

examples/shields/07_pre_shield_simulator.py

@@ -37,21 +37,23 @@ def example_pre_shield_simulator():
     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
+        state_string = model.state_valuations.get_string(current_state)
+        print(F"Simulator is in state {state_string}.")
+        choices = [x for x in pre_scheduler.get_choice(current_state).choice_map if x[0] > 0]
+        choice_labels =  [model.choice_labeling.get_labels_of_choice(model.get_choice_index(current_state, choice[1])) for choice in choices]
+        
+        if not choices:
+            break
+        
         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}")
+        choice_label = model.choice_labeling.get_labels_of_choice(model.get_choice_index(current_state, selected_action[1]))
+        print(F"Allowed Choices are {choice_labels}. Selected Action: {choice_label}")
         observation, reward = simulator.step(selected_action[1])
-        if observation not in final_outcomes:
-            final_outcomes[observation] = 1
-        else:
-            final_outcomes[observation] += 1
-        simulator.restart()
+
         
 
 

examples/shields/08_post_shield_simulator.py

@@ -0,0 +1,68 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+import stormpy.shields
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+"""
+Simulating a model with the usage of a post shield
+"""
+
+def example_post_shield_simulator():
+    path = stormpy.examples.files.prism_mdp_lava_simple
+    formula_str = "<ShieldFileName, PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"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])
+    result2 = stormpy.model_checking(model, formulas[1], extract_scheduler=True)
+
+    assert result.has_shield
+    assert result2.has_scheduler
+
+    shield = result.shield
+    scheduler = result2.scheduler
+
+    post_scheduler = shield.construct()
+
+    simulator = stormpy.simulator.create_simulator(model, seed=42)
+
+    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}.")
+
+        sched_choice = scheduler.get_choice(current_state).get_deterministic_choice()
+        # print(F"Scheduler choice {model.choice_labeling.get_labels_of_choice(model.get_choice_index(current_state, sched_choice))}")
+
+        corrections = post_scheduler.get_choice(current_state).choice_map
+        # print(corrections)
+        correction_labels =  [(model.get_label_of_choice(current_state, correction[0]),  model.get_label_of_choice(current_state, correction[1])) for correction in corrections]
+        # print(F"Correction Choices are {correction_labels}.")
+        
+        applied_correction = next((x[1] for x in corrections if x[0] == sched_choice), None)
+
+        if applied_correction != None and applied_correction != sched_choice:
+            print(F"Correction applied changed choice {sched_choice} to {applied_correction}")
+            sched_choice = applied_correction
+
+        observation, reward = simulator.step(sched_choice)
+
+
+
+
+if __name__ == '__main__':
+    example_post_shield_simulator()

examples/shields/09_optimal_shield_simulator.py

@@ -0,0 +1,53 @@
+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()

lib/stormpy/examples/files/mdp/simple.prism

@@ -32,17 +32,3 @@ module Agent
 
 endmodule
 
-// <resultingFile, PreSafety, gamma=0.9> Pmax=? [G !'AgentIsInLavaAndNotDone'];
-// Model handling soll auch das Shield zurückgeben 
-// Im SparseMdpPrctlModelChecker wird das shield mit createShield erstellt 
-// es soll irgendwie im CheckResult landen welches im model-handling.h verifyWithSparseEngine (Methode) gehandelt wird.
-
-// Result für den MDP Typen ist im SparseMdpPrctlHelper.computeUntilProbabilities
-// MDPSparseModelCheckingHelperReturnType ist der Typ von dem 
-
-// Das ergebnis vom SparseMdpPrctlModelChecker ist ein ExplicitQuantitativeCheckResult
-
-// Prinzipieller ablauf
-// PRISM -> Parser -> ModelEngine |
-//			           model_handlling.h -> AbstractMC -> SparseMDPML -> SparseMdpPrctlHelper
-// Property -> Formula Parser ->  |

lib/stormpy/examples/files/smg/robot_controller.prism

@@ -9,7 +9,7 @@ player adverseryRobot
 endplayer
 
 // (w+1)x16 - grid
-const int w;
+const int w = 2;
 const int width = w;
 const int height = 15;
 

src/storage/model.cpp

@@ -223,6 +223,8 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) {
         .def("get_choice_index", [](SparseMdp<ValueType> const& mdp, uint64_t state, uint64_t actOff) { return mdp.getNondeterministicChoiceIndices()[state]+actOff; }, py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.")
         .def("apply_scheduler", [](SparseMdp<ValueType> const& mdp, storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
         .def("__str__", &getModelInfoPrinter)
+        .def("get_label_of_choice", [](SparseMdp<ValueType> const& mdp, uint64_t state, uint64_t actOff) {return mdp.getChoiceLabeling().getLabelsOfChoice(mdp.getNondeterministicChoiceIndices()[state]+actOff);}, py::arg("state"), py::arg("action_offset"))
+        
     ;
 
     py::class_<Smg<ValueType>, std::shared_ptr<Smg<ValueType>>> smg(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", model);
@@ -231,6 +233,9 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) {
         .def(py::init<ModelComponents<ValueType> const&>(), py::arg("components"))
         .def("get_player_of_state", &Smg<ValueType>::getPlayerOfState, py::arg("state_index"))
         .def("get_player_index", &Smg<ValueType>::getPlayerIndex, py::arg("player_name"))
+        .def("get_choice_index", [](Smg<ValueType> const& smg, uint64_t state, uint64_t actOff) { return smg.getNondeterministicChoiceIndices()[state]+actOff; }, py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.")
+        .def("get_label_of_choice", [](Smg<ValueType> const& smg, uint64_t state, uint64_t actOff) {return smg.getChoiceLabeling().getLabelsOfChoice(smg.getNondeterministicChoiceIndices()[state]+actOff);}, py::arg("state"), py::arg("action_offset"))
+       
     ;
 
     py::class_<StochasticTwoPlayerGame<ValueType>, std::shared_ptr<StochasticTwoPlayerGame<ValueType>>> stg(m, ("Sparse" + vtSuffix + "Stg").c_str(), "STG in sparse representation", model);