Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Easier access to state valuations, choice labels and choice origins #180

Merged
merged 1 commit into from
Aug 7, 2024
Merged

Easier access to state valuations, choice labels and choice origins #180

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions doc/source/doc/schedulers.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)"
]
},
{
Expand Down Expand Up @@ -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)"
]
},
{
Expand Down
12 changes: 9 additions & 3 deletions examples/schedulers/01-schedulers.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
10 changes: 7 additions & 3 deletions examples/schedulers/02-schedulers.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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__':
Expand Down
6 changes: 4 additions & 2 deletions src/storage/state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wasnt there something that this is superslow as it creates a copy?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you elaborate what exactly makes it superslow? The readonly or the general implementation of the functions getLabels?
In general, the iteration over states / actions can certainly be improved peformance-wise. One issue for instance is that we have to keep track of the model. Maybe we open a separate issue for the performance and discuss options there?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I misread it initially as if it was generating a copy of the complete state valuations everytime. That does not seem to happen. So indeed, we can merge it. We may want to discuss elsewhere whether we want to move the iteration over states with this slower high-level API to the stormvogel api.

.def_property_readonly("actions", &SparseModelState<ValueType>::getActions, "Get actions")
.def("__int__",&SparseModelState<ValueType>::getIndex)
;
Expand All @@ -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);
Expand Down
26 changes: 25 additions & 1 deletion src/storage/state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down Expand Up @@ -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;
Expand Down
16 changes: 14 additions & 2 deletions tests/storage/test_scheduler.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading