Skip to content

Umb bindings#400

Merged
sjunges merged 9 commits into
stormchecker:masterfrom
sjunges:umb-bindings
May 22, 2026
Merged

Umb bindings#400
sjunges merged 9 commits into
stormchecker:masterfrom
sjunges:umb-bindings

Conversation

@sjunges
Copy link
Copy Markdown
Contributor

@sjunges sjunges commented May 21, 2026

Provide bindings for importing and exporting umb in stormpy.

Copy link
Copy Markdown
Contributor

@volkm volkm left a comment

Choose a reason for hiding this comment

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

LGTM, thanks for adding the support.

Just a few minor comments for potential improvements.

Comment thread lib/stormpy/__init__.py
return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT)
if intermediate.supports_uncertainty:
return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL)
return _convert_sparse_model(intermediate, value_type=_ValueType.DOUBLE)
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I guess we do not need a check for parametric?

Comment thread tests/storage/test_umb.py
Comment thread tests/storage/test_umb.py
assert model.nr_transitions == model2.nr_transitions
assert model.nr_choices == model2.nr_choices

def test_dtmc_short_round_trip(self, dtmc):
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Is this not the same as test_export_and_build_dtmc? Maybe we only keep this function?
Similar for the MDP.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Yes, we can remove them. We only added the highlevel convenience methods later...

Comment thread tests/storage/test_umb.py Outdated
Comment thread tests/storage/test_umb.py
import_opts.build_state_valuations = False
umb2 = stormpy.import_umb(tmp_umb, import_opts)
model2 = stormpy.sparse_model_from_umb(umb2, import_opts)
self._assert_same_structure(dtmc, model2)
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Maybe explicitly check here for the missing state valuations?

sjunges and others added 4 commits May 21, 2026 15:54
Co-authored-by: Matthias Volk <volkm@users.noreply.github.com>
Co-authored-by: Matthias Volk <volkm@users.noreply.github.com>
@sjunges sjunges merged commit 9d75fbd into stormchecker:master May 22, 2026
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants