From 957e3275b5ccb905607837e5e0cfe7267cc5acf7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 24 Jul 2024 11:57:42 +0200 Subject: [PATCH] Easier access to state valuations, choice labels and choice origins --- doc/source/doc/schedulers.ipynb | 12 +++++++++--- examples/schedulers/01-schedulers.py | 12 +++++++++--- examples/schedulers/02-schedulers.py | 10 +++++++--- src/storage/state.cpp | 6 ++++-- src/storage/state.h | 26 +++++++++++++++++++++++++- tests/storage/test_scheduler.py | 16 ++++++++++++++-- 6 files changed, 68 insertions(+), 14 deletions(-) diff --git a/doc/source/doc/schedulers.ipynb b/doc/source/doc/schedulers.ipynb index b63b42bf4..652467d38 100644 --- a/doc/source/doc/schedulers.ipynb +++ b/doc/source/doc/schedulers.ipynb @@ -39,7 +39,11 @@ ">>> formula_str = \"Pmin=? [F \\\"finished\\\" & \\\"all_coins_equal_1\\\"]\"\n", ">>> program = stormpy.parse_prism_program(path)\n", ">>> formulas = stormpy.parse_properties(formula_str, program)\n", - ">>> model = stormpy.build_model(program, formulas)" + ">>> options = stormpy.BuilderOptions(True, True)\n", + ">>> options.set_build_state_valuations()\n", + ">>> options.set_build_choice_labels()\n", + ">>> options.set_build_with_choice_origins()\n", + ">>> model = stormpy.build_sparse_model_with_options(program, options)" ] }, { @@ -99,8 +103,10 @@ "source": [ ">>> for state in model.states:\n", "... choice = scheduler.get_choice(state)\n", - "... action = choice.get_deterministic_choice()\n", - "... print(\"In state {} choose action {}\".format(state, action))" + "... action_index = choice.get_deterministic_choice()\n", + "... action = state.actions[action_index]\n", + "... print(\"In state {} ({}) choose action {} ({})\".format(state, \", \".join(state.labels), action, \", \".join(action.labels)))\n", + "... print(state.valuations)" ] }, { diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 72ece37f3..2febc68a1 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -10,7 +10,12 @@ def example_schedulers_01(): program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) - model = stormpy.build_model(program, formulas) + + options = stormpy.BuilderOptions(True, True) + options.set_build_choice_labels() + options.set_build_with_choice_origins() + 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) @@ -22,8 +27,9 @@ def example_schedulers_01(): for state in model.states: choice = scheduler.get_choice(state) - action = choice.get_deterministic_choice() - print("In state {} choose action {}".format(state, action)) + action_index = choice.get_deterministic_choice() + action = state.actions[action_index] + print("In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels))) dtmc = model.apply_scheduler(scheduler) print(dtmc) diff --git a/examples/schedulers/02-schedulers.py b/examples/schedulers/02-schedulers.py index 4d45b00ef..6c90e02fd 100644 --- a/examples/schedulers/02-schedulers.py +++ b/examples/schedulers/02-schedulers.py @@ -10,7 +10,10 @@ def example_schedulers_02(): program = stormpy.parse_prism_program(path, False, True) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) - ma = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions([f.raw_formula for f in formulas]) + options.set_build_choice_labels() + options.set_build_with_choice_origins() + ma = stormpy.build_sparse_model_with_options(program, options) assert ma.model_type == stormpy.ModelType.MA # Convert MA to MDP @@ -28,8 +31,9 @@ def example_schedulers_02(): for state in mdp.states: choice = scheduler.get_choice(state) - action = choice.get_deterministic_choice() - print("In state {} choose action {}".format(state, action)) + action_index = choice.get_deterministic_choice() + action = state.actions[action_index] + print( "In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels))) if __name__ == '__main__': diff --git a/src/storage/state.cpp b/src/storage/state.cpp index b21cae9c8..0fc402d8d 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -13,7 +13,8 @@ void define_state(py::module& m, std::string const& vtSuffix) { py::class_>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model") .def("__str__", &SparseModelState::toString) .def_property_readonly("id", &SparseModelState::getIndex, "Id") - .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("labels", &SparseModelState::getLabels, "Get state labels") + .def_property_readonly("valuations", &SparseModelState::getValuations, "Get state valuations") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") .def("__int__",&SparseModelState::getIndex) ; @@ -29,8 +30,9 @@ void define_state(py::module& m, std::string const& vtSuffix) { .def("__str__", &SparseModelAction::toString) .def_property_readonly("id", &SparseModelAction::getIndex, "Id") .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + .def_property_readonly("labels", &SparseModelAction::getLabels, "Get choice labels") + .def_property_readonly("origins", &SparseModelAction::getOrigins, "Get choice origins") ; - } template void define_state(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/state.h b/src/storage/state.h index bbe84eb00..8f33900b5 100644 --- a/src/storage/state.h +++ b/src/storage/state.h @@ -27,6 +27,13 @@ class SparseModelState { return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); } + std::string getValuations() const { + if (!this->model.hasStateValuations()) { + throw std::invalid_argument("No state valuations available"); + } + return this->model.getStateValuations().getStateInfo(this->stateIndex); + } + SparseModelActions getActions() const { return SparseModelActions(this->model, stateIndex); } @@ -84,6 +91,20 @@ class SparseModelAction { typename storm::storage::SparseMatrix::rows getTransitions() { return model.getTransitionMatrix().getRow(stateIndex, actionIndex); } + + std::set getLabels() const { + if (!this->model.hasChoiceLabeling()) { + throw std::invalid_argument("No choice labeling available"); + } + return this->model.getChoiceLabeling().getLabelsOfChoice(getActionIndex()); + } + + std::string getOrigins() const { + if (!this->model.hasChoiceOrigins()) { + throw std::invalid_argument("No choice origins available"); + } + return this->model.getChoiceOrigins()->getChoiceInfo(getActionIndex()); + } std::string toString() const { std::stringstream stream; @@ -91,8 +112,11 @@ class SparseModelAction { return stream.str(); } - private: + s_index getActionIndex() const { + return model.getTransitionMatrix().getRowGroupIndices()[stateIndex] + actionIndex; + } + s_index stateIndex; s_index actionIndex; storm::models::sparse::Model& model; diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index 2662e36a7..e5f6e9c75 100644 --- a/tests/storage/test_scheduler.py +++ b/tests/storage/test_scheduler.py @@ -10,18 +10,24 @@ class TestScheduler: def test_scheduler_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) - model = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions(True, True) + options.set_build_state_valuations() + options.set_build_choice_labels() + options.set_build_with_choice_origins() + model = stormpy.build_sparse_model_with_options(program, options) assert model.nr_states == 272 assert model.nr_transitions == 492 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler scheduler = result.scheduler assert scheduler.memoryless assert scheduler.memory_size == 1 assert scheduler.deterministic + for state in model.states: choice = scheduler.get_choice(state) assert choice.defined @@ -29,13 +35,19 @@ def test_scheduler_mdp(self): action = choice.get_deterministic_choice() assert 0 <= action assert action < len(state.actions) + action = state.actions[action] + assert action.id < 268 or "done" in action.labels distribution = choice.get_choice() assert str(distribution).startswith("{[1:") def test_scheduler_ma_via_mdp(self): program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program) - ma = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions([f.raw_formula for f in formulas]) + options.set_build_state_valuations() + options.set_build_choice_labels() + options.set_build_with_choice_origins() + ma = stormpy.build_sparse_model_with_options(program, options) assert ma.nr_states == 5 assert ma.nr_transitions == 8 assert ma.model_type == stormpy.ModelType.MA