From 89107ce6eed6013d87c5ad9fa3d53632ee463213 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Mon, 7 Aug 2023 16:02:28 +0200 Subject: [PATCH] added bindings for shield querying --- examples/shields/01_pre_shield.py | 45 +++++++++++++++++++ examples/shields/02_post_shield.py | 43 ++++++++++++++++++ lib/stormpy/examples/files.py | 5 +++ lib/stormpy/examples/files/mdp/simple.prism | 48 +++++++++++++++++++++ lib/stormpy/shields/__init__.py | 32 +++++++++++++- src/mod_shields.cpp | 4 -- src/shields/optimal_shield.cpp | 1 + src/shields/post_shield.cpp | 1 + src/storage/scheduler.cpp | 19 +++++++- 9 files changed, 191 insertions(+), 7 deletions(-) create mode 100644 examples/shields/01_pre_shield.py create mode 100644 examples/shields/02_post_shield.py create mode 100644 lib/stormpy/examples/files/mdp/simple.prism diff --git a/examples/shields/01_pre_shield.py b/examples/shields/01_pre_shield.py new file mode 100644 index 0000000..e4e157e --- /dev/null +++ b/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 = " 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() \ No newline at end of file diff --git a/examples/shields/02_post_shield.py b/examples/shields/02_post_shield.py new file mode 100644 index 0000000..2dc19b2 --- /dev/null +++ b/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 = " 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() \ No newline at end of file diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 427e9ad..5fa521c 100644 --- a/lib/stormpy/examples/files.py +++ b/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") \ No newline at end of file diff --git a/lib/stormpy/examples/files/mdp/simple.prism b/lib/stormpy/examples/files/mdp/simple.prism new file mode 100644 index 0000000..77e3777 --- /dev/null +++ b/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 + +// 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 -> | diff --git a/lib/stormpy/shields/__init__.py b/lib/stormpy/shields/__init__.py index 1220140..4ea31dd 100644 --- a/lib/stormpy/shields/__init__.py +++ b/lib/stormpy/shields/__init__.py @@ -1,3 +1,33 @@ import stormpy.shields from . import shields -from .shields import * \ No newline at end of file +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 diff --git a/src/mod_shields.cpp b/src/mod_shields.cpp index 7d76991..6d8b4a6 100644 --- a/src/mod_shields.cpp +++ b/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::index_type>(m, "Double"); define_abstract_shield::index_type>(m, "Exact"); define_pre_shield::index_type>(m, "Double"); diff --git a/src/shields/optimal_shield.cpp b/src/shields/optimal_shield.cpp index 46f109b..8a6e629 100644 --- a/src/shields/optimal_shield.cpp +++ b/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_>(m, shieldClassName.c_str()) + .def("construct", &OptimalShield::construct, "Construct the shield") ; } diff --git a/src/shields/post_shield.cpp b/src/shields/post_shield.cpp index a8c518a..5612b95 100644 --- a/src/shields/post_shield.cpp +++ b/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_>(m, shieldClassName.c_str()) + .def("construct", &PostShield::construct, "Construct the shield") ; } diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index ca3a0ab..211c584 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -10,8 +10,9 @@ void define_scheduler(py::module& m, std::string vt_suffix) { using Scheduler = storm::storage::Scheduler; using SchedulerChoice = storm::storage::SchedulerChoice; using PreScheduler = storm::storage::PreScheduler; + using PreSchedulerChoice = storm::storage::PreSchedulerChoice; using PostScheduler = storm::storage::PostScheduler; - + using PostSchedulerChoice = storm::storage::PostSchedulerChoice; std::string schedulerClassName = std::string("Scheduler") + vt_suffix; py::class_>> 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(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(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(m, postSchedulerChoiceClassName.c_str(), "A choice of a finite memory post scheduler"); + postSchedulerChoice + .def_property_readonly("choice_map", &PostSchedulerChoice::getChoiceMap, "Get the choice map") ; }