added bindings for shield querying

examples/shields/01_pre_shield.py

@@ -0,0 +1,45 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+
+import stormpy.shields
+
+import stormpy.examples
+import stormpy.examples.files
+import random
+
+
+def pre_schield_01():
+    path = stormpy.examples.files.prism_mdp_lava_simple
+    formula_str = "<ShieldFileName, PreSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+
+
+    #--buildstateval --buildchoicelab
+    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_schield
+    
+    shield = result.shield
+    
+    lookup = stormpy.shields.create_shield_action_lookup(model, shield)
+    query = list(lookup.keys())[0]
+    
+    print(query)
+    print(lookup[query])
+    print(lookup)
+
+
+if __name__ == '__main__':
+    pre_schield_01()

examples/shields/02_post_shield.py

@@ -0,0 +1,43 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+
+import stormpy.shields
+
+import stormpy.examples
+import stormpy.examples.files
+import random
+
+
+def post_shield_02():
+    path = stormpy.examples.files.prism_mdp_lava_simple
+    formula_str = "<ShieldFileName, PostSafety, gamma=0.9> 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_schield
+    
+    shield = result.shield
+
+    lookup = stormpy.shields.create_shield_action_lookup(model, shield)
+    query = list(lookup.keys())[0]
+    
+    print(query)
+    print(lookup[query])
+
+
+
+if __name__ == '__main__':
+    post_shield_02()

lib/stormpy/examples/files.py

@@ -49,3 +49,8 @@ gspn_pnpro_simple = _path("gspn", "gspn_simple.pnpro")
 """GSPN example (PNPRO format)"""
 gspn_pnml_simple = _path("gspn", "gspn_simple.pnml")
 """GSPN example (PNML format)"""
+
+"""Shield Example 1"""
+prism_mdp_lava_simple = _path("mdp", "simple.prism")
+"""Shield Example 2"""
+prism_mdp_cliff_zig_zag = _path("mdp", "CliffZigZag.prism")

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

@@ -0,0 +1,48 @@
+mdp
+
+formula AgentCannotMoveNorth = (xAgent=2&yAgent=1) | (xAgent=3&yAgent=1) | (xAgent=4&yAgent=1) | (xAgent=5&yAgent=1) | (xAgent=6&yAgent=1) | (xAgent=1&yAgent=1);
+formula AgentCannotMoveEast  = (xAgent=6&yAgent=1) | (xAgent=6&yAgent=2) | (xAgent=6&yAgent=3) | (xAgent=6&yAgent=4) | (xAgent=6&yAgent=5);
+formula AgentCannotMoveSouth = (xAgent=1&yAgent=5) | (xAgent=2&yAgent=5) | (xAgent=3&yAgent=5) | (xAgent=4&yAgent=5) | (xAgent=5&yAgent=5) | (xAgent=6&yAgent=5);
+formula AgentCannotMoveWest  = (xAgent=1&yAgent=2) | (xAgent=1&yAgent=3) | (xAgent=1&yAgent=4) | (xAgent=1&yAgent=5) | (xAgent=1&yAgent=1);
+formula AgentIsOnSlippery = false;
+formula AgentIsInLava = (xAgent=2&yAgent=2) | (xAgent=3&yAgent=2) | (xAgent=2&yAgent=3) | (xAgent=3&yAgent=3) | (xAgent=2&yAgent=4) | (xAgent=3&yAgent=4);
+formula AgentIsInLavaAndNotDone = AgentIsInLava & !AgentDone;
+label "AgentIsInLavaAndNotDone" = AgentIsInLava & !AgentDone;
+
+formula AgentIsInGoal = (xAgent=6&yAgent=5);
+formula AgentIsInGoalAndNotDone = AgentIsInGoal & !AgentDone;
+label "AgentIsInGoalAndNotDone" = AgentIsInGoal & !AgentDone;
+module Agent
+	xAgent : [1..6] init 1;
+	yAgent : [1..7] init 1;
+
+	AgentDone : bool init false;
+	viewAgent : [0..3] init 0;
+
+	[Agent_turn_right]   !AgentIsInGoal & !AgentIsInLava & !AgentIsOnSlippery -> (viewAgent'=mod(viewAgent + 1, 4)) ;
+	[Agent_turn_left]    !AgentIsInGoal & !AgentIsInLava & !AgentIsOnSlippery & viewAgent>0 -> (viewAgent'=viewAgent - 1) ;
+	[Agent_turn_left]    !AgentIsInGoal & !AgentIsInLava & !AgentIsOnSlippery & viewAgent=0 -> (viewAgent'=3) ;
+
+
+	[Agent_move_north]  viewAgent=3 &  !AgentIsOnSlippery & !AgentIsInLava &!AgentIsInGoal &  !AgentCannotMoveNorth -> (yAgent'=yAgent-1);
+	[Agent_move_east]   viewAgent=0 &  !AgentIsOnSlippery & !AgentIsInLava &!AgentIsInGoal &  !AgentCannotMoveEast  -> (xAgent'=xAgent+1);
+	[Agent_move_south]  viewAgent=1 &  !AgentIsOnSlippery & !AgentIsInLava &!AgentIsInGoal &  !AgentCannotMoveSouth -> (yAgent'=yAgent+1);
+	[Agent_move_west]   viewAgent=2 &  !AgentIsOnSlippery & !AgentIsInLava &!AgentIsInGoal &  !AgentCannotMoveWest  -> (xAgent'=xAgent-1);
+	[Agent_done] AgentIsInGoal | AgentIsInLava -> (AgentDone'=true);
+
+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/shields/__init__.py

@@ -1,3 +1,33 @@
 import stormpy.shields
 from . import shields
 from .shields import *
+
+def create_action_lookup(model, scheduler):
+    ret = {}
+
+    for state_id in model.states:
+        choice = scheduler.get_choice(state_id)
+        action = choice.get_deterministic_choice()
+        state_valuation = model.state_valuations.get_string(state_id)
+
+        action_to_be_executed = model.choice_labeling.get_labels_of_choice(model.get_choice_index(state_id, action))
+        ret[state_valuation] = action_to_be_executed
+
+    return ret
+
+def create_shield_action_lookup(model, shield):
+    ret = {}
+
+    for state_id in model.states:
+        choices = shield.construct().get_choice(state_id)
+        state_valuation = model.state_valuations.get_string(state_id)
+
+        l = []
+        for choice in choices.choice_map:
+            action = choice[1]
+            action_to_be_executed = model.choice_labeling.get_labels_of_choice(model.get_choice_index(state_id, action))
+            l.append(action_to_be_executed)
+        
+        ret[state_valuation] = l
+
+    return ret

src/mod_shields.cpp

@@ -4,7 +4,6 @@
 #include "shields/post_shield.h"
 #include "shields/pre_shield.h"
 #include "shields/shield_handling.h"
-#include "shields/debug.h"
 
 
 #include "storm/storage/Scheduler.h"
@@ -19,9 +18,6 @@ PYBIND11_MODULE(shields, m) {
     py::options options;
     options.disable_function_signatures();
 #endif
-
-    define_pet(m);
-    define_add(m);
     define_abstract_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m, "Double");
     define_abstract_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m, "Exact");
     define_pre_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m, "Double");

src/shields/optimal_shield.cpp

@@ -11,6 +11,7 @@ void define_optimal_shield(py::module& m, std::string vt_suffix) {
     std::string shieldClassName = std::string("OptimalShield") + vt_suffix;
 
     py::class_<OptimalShield, AbstractShield, std::shared_ptr<OptimalShield>>(m, shieldClassName.c_str())
+        .def("construct", &OptimalShield::construct, "Construct the shield")
     ;
 }
 

src/shields/post_shield.cpp

@@ -11,6 +11,7 @@ void define_post_shield(py::module& m, std::string vt_suffix) {
     std::string shieldClassName = std::string("PostShield") + vt_suffix;
     
     py::class_<PostShield, AbstractShield, std::shared_ptr<PostShield>>(m, shieldClassName.c_str())
+        .def("construct", &PostShield::construct, "Construct the shield")
     ;
 }
 

src/storage/scheduler.cpp

@@ -10,8 +10,9 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
     using Scheduler = storm::storage::Scheduler<ValueType>;
     using SchedulerChoice = storm::storage::SchedulerChoice<ValueType>;
     using PreScheduler = storm::storage::PreScheduler<ValueType>;
+    using PreSchedulerChoice = storm::storage::PreSchedulerChoice<ValueType>;
     using PostScheduler = storm::storage::PostScheduler<ValueType>;
-
+    using PostSchedulerChoice = storm::storage::PostSchedulerChoice<ValueType>;
 
     std::string schedulerClassName = std::string("Scheduler") + vt_suffix;
     py::class_<Scheduler, std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler(m, schedulerClassName.c_str(), "A Finite Memory Scheduler");
@@ -43,14 +44,28 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
         preScheduler
             .def_property_readonly("memoryless", &PreScheduler::isMemorylessScheduler, "is the pre scheduler memoryless?")
             .def_property_readonly("memory_size", &PreScheduler::getNumberOfMemoryStates, "How much memory does the scheduler take?")
+            .def("get_choice", &PreScheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0)       
+    ;
 
+    std::string  preSchedulerChoiceClassName = std::string("PreSchedulerChoice") + vt_suffix;
+    py::class_<PreSchedulerChoice> preSchedulerChoice(m, preSchedulerChoiceClassName.c_str(), "A choice of a finite memory pre scheduler");
+    preSchedulerChoice
+        .def_property_readonly("choice_map", &PreSchedulerChoice::getChoiceMap, "Get the choice map")
     ;
 
     std::string postSchedulerClassName = std::string("PostScheduler") + vt_suffix;
     py::class_<PostScheduler> postScheduler(m, postSchedulerClassName.c_str(), "A post scheduler");
         postScheduler
             .def_property_readonly("memoryless", &PostScheduler::isMemorylessScheduler, "is the pre scheduler memoryless?")
+            .def_property_readonly("deterministic", &PostScheduler::isDeterministicScheduler, "Is the scheduler deterministic?")
+            .def("get_choice", &PostScheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0)
+            
+    ;
 
+    std::string postSchedulerChoiceClassName = std::string("PostSchedulerChoice") + vt_suffix;
+    py::class_<PostSchedulerChoice> postSchedulerChoice(m, postSchedulerChoiceClassName.c_str(), "A choice of a finite memory post scheduler");
+    postSchedulerChoice
+                .def_property_readonly("choice_map", &PostSchedulerChoice::getChoiceMap, "Get the choice map")
     ;
 
 }