Easier access to state valuations, choice labels and choice origins (#…

…180)

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)"
    ]
   },
   {

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)

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__':

src/storage/state.cpp

@@ -13,7 +13,8 @@ void define_state(py::module& m, std::string const& vtSuffix) {
     py::class_<SparseModelState<ValueType>>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model")
         .def("__str__", &SparseModelState<ValueType>::toString)
         .def_property_readonly("id", &SparseModelState<ValueType>::getIndex, "Id")
-        .def_property_readonly("labels", &SparseModelState<ValueType>::getLabels, "Labels")
+        .def_property_readonly("labels", &SparseModelState<ValueType>::getLabels, "Get state labels")
+        .def_property_readonly("valuations", &SparseModelState<ValueType>::getValuations, "Get state valuations")
         .def_property_readonly("actions", &SparseModelState<ValueType>::getActions, "Get actions")
         .def("__int__",&SparseModelState<ValueType>::getIndex)
     ;
@@ -29,8 +30,9 @@ void define_state(py::module& m, std::string const& vtSuffix) {
         .def("__str__", &SparseModelAction<ValueType>::toString)
         .def_property_readonly("id", &SparseModelAction<ValueType>::getIndex, "Id")
         .def_property_readonly("transitions", &SparseModelAction<ValueType>::getTransitions, "Get transitions")
+        .def_property_readonly("labels", &SparseModelAction<ValueType>::getLabels, "Get choice labels")
+        .def_property_readonly("origins", &SparseModelAction<ValueType>::getOrigins, "Get choice origins")
     ;
-
 }
 
 template void define_state<double>(py::module& m, std::string const& vtSuffix);

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<ValueType> getActions() const {
             return SparseModelActions<ValueType>(this->model, stateIndex);
         }
@@ -84,15 +91,32 @@ class SparseModelAction {
         typename storm::storage::SparseMatrix<ValueType>::rows getTransitions() {
             return model.getTransitionMatrix().getRow(stateIndex, actionIndex);
         }
+
+        std::set<std::string> 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;
             stream << actionIndex;
             return stream.str();
         }
 
-
     private:
+        s_index getActionIndex() const {
+            return model.getTransitionMatrix().getRowGroupIndices()[stateIndex] + actionIndex;
+        }
+
         s_index stateIndex;
         s_index actionIndex;
         storm::models::sparse::Model<ValueType>& model;

tests/storage/test_scheduler.py

@@ -10,32 +10,44 @@ 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
             assert choice.deterministic
             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