support smg model / testcases for optimal shields

examples/shields/01_pre_shield.py

@@ -14,8 +14,6 @@ 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)
 
@@ -38,7 +36,6 @@ def pre_schield_01():
     
     print(query)
     print(lookup[query])
-    print(lookup)
 
 
 if __name__ == '__main__':

examples/shields/03_optimal_shield.py

@@ -0,0 +1,58 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+
+import stormpy.shields
+
+import stormpy.examples
+import stormpy.examples.files
+import random
+
+
+def optimal_shield_03():
+    path = stormpy.examples.files.prism_smg_lights
+    formula_str = "<tlsShield, 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
+    print(F"Check Scheduler: {result.has_scheduler}")
+    print(F"Check Shield: {result.has_schield}")
+
+    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()

examples/shields/04_optimal_shield.py

@@ -0,0 +1,58 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+
+import stormpy.shields
+
+import stormpy.examples
+import stormpy.examples.files
+import random
+
+
+def optimal_shield_03():
+    path = stormpy.examples.files.prism_smg_robot
+    formula_str = "<path_correction, Optimal> <<sh>> R{\"travel_costs\"}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
+    print(F"Check Scheduler: {result.has_scheduler}")
+    print(F"Check Shield: {result.has_schield}")
+
+    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()

lib/stormpy/examples/files.py

@@ -52,5 +52,8 @@ gspn_pnml_simple = _path("gspn", "gspn_simple.pnml")
 
 """Shield Example 1"""
 prism_mdp_lava_simple = _path("mdp", "simple.prism")
-"""Shield Example 2"""
-prism_mdp_cliff_zig_zag = _path("mdp", "CliffZigZag.prism")
+
+"""Optimal Shield Example 1"""
+prism_smg_lights = _path("smg", "lights.prism")
+"""Optimal Shield Example 2"""
+prism_smg_robot = _path("smg", "robotics_planning.prism")

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

@@ -0,0 +1,73 @@
+smg
+
+player controller
+  cont
+endplayer
+
+player shield
+  [reduceNS_Shield], [reduceEW_Shield], [reduceNS_ShieldDev], [reduceEW_ShieldDev]
+endplayer
+
+player environment
+  env
+endplayer
+
+global move : [0..2];
+
+const int lmax = 1;
+
+global N : [0..lmax];
+global E : [0..lmax];
+global S : [0..lmax];
+global W : [0..lmax];
+
+module env
+  [] move=0 -> 1/8 : (N'=min(lmax,N+1)) & (move'=1) +
+               1/8 : (S'=min(lmax,S+1)) & (move'=1) +
+               1/8 : (E'=min(lmax,E+1)) & (move'=1) +
+               1/8 : (W'=min(lmax,W+1)) & (move'=1) +
+
+               7/120 : (N'=min(lmax,N+1)) & (S'=min(lmax,S+1)) & (move'=1) +
+               7/120 : (S'=min(lmax,S+1)) & (W'=min(lmax,W+1)) & (move'=1) +
+               7/120 : (E'=min(lmax,E+1)) & (N'=min(lmax,N+1)) & (move'=1) +
+               7/120 : (W'=min(lmax,W+1)) & (N'=min(lmax,N+1)) & (move'=1) +
+               7/120 : (E'=min(lmax,E+1)) & (S'=min(lmax,S+1)) & (move'=1) +
+               7/120 : (W'=min(lmax,W+1)) & (S'=min(lmax,S+1)) & (move'=1) +
+
+               3/120 : (E'=min(lmax,E+1)) & (N'=min(lmax,N+1)) & (W'=min(lmax,W+1)) & (move'=1) +
+               3/120 : (W'=min(lmax,W+1)) & (N'=min(lmax,N+1)) & (E'=min(lmax,E+1)) & (move'=1) +
+               3/120 : (E'=min(lmax,E+1)) & (S'=min(lmax,S+1)) & (W'=min(lmax,W+1)) & (move'=1) +
+               3/120 : (W'=min(lmax,W+1)) & (S'=min(lmax,S+1)) & (N'=min(lmax,N+1)) & (move'=1) +
+
+               6/120 : (W'=min(lmax,W+1)) & (S'=min(lmax,S+1)) & (E'=min(lmax,E+1)) & (N'=min(lmax,N+1)) & (move'=1);
+endmodule
+
+module cont
+  action : [0..1];
+
+  [] move=1 -> (action'=0) & (move'=2);
+  [] move=1 -> (action'=1) & (move'=2);
+endmodule
+
+module sh
+  [reduceNS_Shield] move=2 & action=0    -> (N'=max(0,N-1)) & (S'=max(0,S-1)) & (move'=0);
+  [reduceEW_Shield] move=2 & action=1    -> (W'=max(0,W-1)) & (E'=max(0,E-1)) & (move'=0);
+
+  [reduceNS_ShieldDev] move=2 & action=1 -> (N'=max(0,N-1)) & (S'=max(0,S-1)) & (move'=0);
+  [reduceEW_ShieldDev] move=2 & action=0 -> (W'=max(0,W-1)) & (E'=max(0,E-1)) & (move'=0);
+endmodule
+
+formula diff = pow(pow((N+S)-(E+W),2),0.5);
+rewards "difference"
+  true : diff;
+endrewards
+
+const double lambda = 0.8;
+const double interference = 2 * lmax;
+
+rewards "differenceWithInterferenceCost"
+  [reduceNS_Shield] true : lambda * diff;
+  [reduceEW_Shield] true : lambda * diff;
+  [reduceNS_ShieldDev] true : lambda * diff + (1 - lambda) * interference;
+  [reduceEW_ShieldDev] true : lambda * diff + (1 - lambda) * interference;
+endrewards

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

@@ -0,0 +1,54 @@
+smg
+
+player sh
+  [planA], [planA_Dev], [planB], [planB_Dev]
+endplayer
+
+player learned_controller
+  controller, env
+endplayer
+
+global move : [0..2] init 0;
+
+const int lengthA = 10;
+const int lengthB = lengthA + 5;
+
+global stepA : [0..lengthA] init 0;
+global stepB : [0..lengthB] init 0;
+
+global planA : bool init true;
+global shieldPlanA : bool init true;
+
+global stepTaken : bool init false;
+global waiting : bool init false;
+
+const int waiting_cost = 2;
+
+const double blockedProb = 0.5;
+module controller
+  [] move=0 & shieldPlanA & stepA<lengthA -> (planA'=true)  & (stepTaken'=false) & (waiting'=false) & (move'=1);
+  [] move=0 & shieldPlanA & stepA<lengthA -> (planA'=false) & (stepTaken'=false) & (waiting'=false) & (move'=1);
+
+  [] move=0 & !shieldPlanA & stepB<lengthB -> (planA'=false) & (stepTaken'=false) & (waiting'=false) & (move'=1);
+endmodule
+
+module shield
+  [planA] move=1 & planA ->  (shieldPlanA'=true)  & (move'=2);
+  [planB_Dev] move=1 & planA ->  (shieldPlanA'=false) & (move'=2);
+
+  [planB] move=1 & !planA -> (shieldPlanA'=false) & (move'=2);
+  [planA_Dev] move=1 & !planA -> (shieldPlanA'=true)  & (move'=2);
+endmodule
+
+module env
+  [] move=2 & shieldPlanA& stepA<lengthA -> 1 - blockedProb : (stepA'=min(stepA+1, lengthA)) & (stepTaken'=true) & (move'=0) + blockedProb : (stepA'=stepA) & (waiting'=true) & (move'=0);
+
+  [] move=2 & !shieldPlanA & stepB<lengthB -> (stepB'=min(stepB+1, lengthB)) & (stepTaken'=true) & (move'=0);
+
+  [] move=2 & (lengthB=stepB | lengthA=stepA) -> (stepTaken'=false) & (waiting'=false);
+endmodule
+
+rewards "travel_costs"
+  stepTaken : 1;
+  waiting : waiting_cost;
+endrewards

src/mod_shields.cpp

@@ -26,5 +26,6 @@ PYBIND11_MODULE(shields, m) {
     define_post_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m, "Exact");
     define_optimal_shield<double, typename storm::storage::SparseMatrix<double>::index_type>(m, "Double");
     define_optimal_shield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m, "Exact");
-    define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(m);
+    define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(m, "Double");
+    define_shield_handling<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(m, "Exact");
 }

src/shields/shield_handling.cpp

@@ -4,8 +4,11 @@
 #include "storm/api/export.h"
 
 template <typename ValueType, typename IndexType>
-void define_shield_handling(py::module& m) {
-    m.def("export_shield", &storm::api::exportShield<ValueType, IndexType>, py::arg("model"), py::arg("shield"));
+void define_shield_handling(py::module& m, std::string vt_suffix) {
+    std::string shieldHandlingname = std::string("export_shield") + vt_suffix;
+
+    m.def(shieldHandlingname.c_str(), &storm::api::exportShield<ValueType, IndexType>, py::arg("model"), py::arg("shield"));
 }
 
-template void define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m);
+template void define_shield_handling<double, typename storm::storage::SparseMatrix<double>::index_type>(py::module& m, std::string vt_suffix);
+template void define_shield_handling<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>(py::module& m, std::string vt_suffix);

src/shields/shield_handling.h

@@ -3,4 +3,4 @@
 #include "common.h"
 
 template <typename ValueType, typename IndexType>
-void define_shield_handling(py::module& m);
+void define_shield_handling(py::module& m, std::string vt_suffix);

src/storage/model.cpp

@@ -5,6 +5,7 @@
 #include "storm/models/sparse/Model.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Smg.h"
 #include "storm/models/sparse/Pomdp.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
@@ -33,6 +34,7 @@ template<typename ValueType> using ModelComponents = storm::storage::sparse::Mod
 template<typename ValueType> using SparseModel = storm::models::sparse::Model<ValueType>;
 template<typename ValueType> using SparseDtmc = storm::models::sparse::Dtmc<ValueType>;
 template<typename ValueType> using SparseMdp = storm::models::sparse::Mdp<ValueType>;
+template<typename ValueType> using Smg = storm::models::sparse::Smg<ValueType>;
 template<typename ValueType> using SparsePomdp = storm::models::sparse::Pomdp<ValueType>;
 template<typename ValueType> using SparseCtmc = storm::models::sparse::Ctmc<ValueType>;
 template<typename ValueType> using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
@@ -97,6 +99,7 @@ void define_model(py::module& m) {
         .value("POMDP", storm::models::ModelType::Pomdp)
         .value("CTMC", storm::models::ModelType::Ctmc)
         .value("MA", storm::models::ModelType::MarkovAutomaton)
+        .value("SMG", storm::models::ModelType::Smg)
     ;
 
     // ModelBase
@@ -219,6 +222,15 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) {
         .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)
     ;
+
+    py::class_<Smg<ValueType>, std::shared_ptr<Smg<ValueType>>> smg(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", model);
+    smg
+        .def(py::init<Smg<ValueType>>(), py::arg("other_model"))
+        
+
+    ;
+        
+
     py::class_<SparsePomdp<ValueType>, std::shared_ptr<SparsePomdp<ValueType>>>(m, ("Sparse" + vtSuffix + "Pomdp").c_str(), "POMDP in sparse representation", mdp)
         .def(py::init<SparsePomdp<ValueType>>(), py::arg("other_model"))
         .def(py::init<ModelComponents<ValueType> const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false)