From ac5f685d24ff87a476aae8583b92f5ef212debbd Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 8 Aug 2023 11:37:15 +0200 Subject: [PATCH] support smg model / testcases for optimal shields --- examples/shields/01_pre_shield.py | 3 - examples/shields/03_optimal_shield.py | 58 +++++++++++++++ examples/shields/04_optimal_shield.py | 58 +++++++++++++++ lib/stormpy/examples/files.py | 7 +- lib/stormpy/examples/files/smg/lights.prism | 73 +++++++++++++++++++ .../files/smg/robotics_planning.prism | 54 ++++++++++++++ src/mod_shields.cpp | 3 +- src/shields/shield_handling.cpp | 9 ++- src/shields/shield_handling.h | 2 +- src/storage/model.cpp | 12 +++ 10 files changed, 269 insertions(+), 10 deletions(-) create mode 100644 examples/shields/03_optimal_shield.py create mode 100644 examples/shields/04_optimal_shield.py create mode 100644 lib/stormpy/examples/files/smg/lights.prism create mode 100644 lib/stormpy/examples/files/smg/robotics_planning.prism diff --git a/examples/shields/01_pre_shield.py b/examples/shields/01_pre_shield.py index e4e157e..f90b683 100644 --- a/examples/shields/01_pre_shield.py +++ b/examples/shields/01_pre_shield.py @@ -14,8 +14,6 @@ def pre_schield_01(): path = stormpy.examples.files.prism_mdp_lava_simple formula_str = " 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__': diff --git a/examples/shields/03_optimal_shield.py b/examples/shields/03_optimal_shield.py new file mode 100644 index 0000000..d922137 --- /dev/null +++ b/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 = " <> 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() \ No newline at end of file diff --git a/examples/shields/04_optimal_shield.py b/examples/shields/04_optimal_shield.py new file mode 100644 index 0000000..75b29f3 --- /dev/null +++ b/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 = " <> 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() \ No newline at end of file diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 5fa521c..35ae415 100644 --- a/lib/stormpy/examples/files.py +++ b/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") \ No newline at end of file + +"""Optimal Shield Example 1""" +prism_smg_lights = _path("smg", "lights.prism") +"""Optimal Shield Example 2""" +prism_smg_robot = _path("smg", "robotics_planning.prism") diff --git a/lib/stormpy/examples/files/smg/lights.prism b/lib/stormpy/examples/files/smg/lights.prism new file mode 100644 index 0000000..91de934 --- /dev/null +++ b/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 diff --git a/lib/stormpy/examples/files/smg/robotics_planning.prism b/lib/stormpy/examples/files/smg/robotics_planning.prism new file mode 100644 index 0000000..fd630b5 --- /dev/null +++ b/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 (planA'=true) & (stepTaken'=false) & (waiting'=false) & (move'=1); + [] move=0 & shieldPlanA & stepA (planA'=false) & (stepTaken'=false) & (waiting'=false) & (move'=1); + + [] move=0 & !shieldPlanA & stepB (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 1 - blockedProb : (stepA'=min(stepA+1, lengthA)) & (stepTaken'=true) & (move'=0) + blockedProb : (stepA'=stepA) & (waiting'=true) & (move'=0); + + [] move=2 & !shieldPlanA & stepB (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 diff --git a/src/mod_shields.cpp b/src/mod_shields.cpp index 6d8b4a6..8b0d897 100644 --- a/src/mod_shields.cpp +++ b/src/mod_shields.cpp @@ -26,5 +26,6 @@ PYBIND11_MODULE(shields, m) { define_post_shield::index_type>(m, "Exact"); define_optimal_shield::index_type>(m, "Double"); define_optimal_shield::index_type>(m, "Exact"); - define_shield_handling::index_type>(m); + define_shield_handling::index_type>(m, "Double"); + define_shield_handling::index_type>(m, "Exact"); } diff --git a/src/shields/shield_handling.cpp b/src/shields/shield_handling.cpp index 0d4e4b1..a894fa0 100644 --- a/src/shields/shield_handling.cpp +++ b/src/shields/shield_handling.cpp @@ -4,8 +4,11 @@ #include "storm/api/export.h" template -void define_shield_handling(py::module& m) { - m.def("export_shield", &storm::api::exportShield, 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, py::arg("model"), py::arg("shield")); } -template void define_shield_handling::index_type>(py::module& m); +template void define_shield_handling::index_type>(py::module& m, std::string vt_suffix); +template void define_shield_handling::index_type>(py::module& m, std::string vt_suffix); diff --git a/src/shields/shield_handling.h b/src/shields/shield_handling.h index 07aa44c..09233b5 100644 --- a/src/shields/shield_handling.h +++ b/src/shields/shield_handling.h @@ -3,4 +3,4 @@ #include "common.h" template -void define_shield_handling(py::module& m); \ No newline at end of file +void define_shield_handling(py::module& m, std::string vt_suffix); \ No newline at end of file diff --git a/src/storage/model.cpp b/src/storage/model.cpp index cf955df..73ab53a 100644 --- a/src/storage/model.cpp +++ b/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 using ModelComponents = storm::storage::sparse::Mod template using SparseModel = storm::models::sparse::Model; template using SparseDtmc = storm::models::sparse::Dtmc; template using SparseMdp = storm::models::sparse::Mdp; +template using Smg = storm::models::sparse::Smg; template using SparsePomdp = storm::models::sparse::Pomdp; template using SparseCtmc = storm::models::sparse::Ctmc; template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; @@ -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 const& mdp, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) ; + + py::class_, std::shared_ptr>> smg(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", model); + smg + .def(py::init>(), py::arg("other_model")) + + + ; + + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Pomdp").c_str(), "POMDP in sparse representation", mdp) .def(py::init>(), py::arg("other_model")) .def(py::init const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false)