Skip to content

UMB (unified Markov binary) format import + export#267

Merged
davexparker merged 9 commits into
prismmodelchecker:masterfrom
davexparker:umb2
Jan 29, 2026
Merged

UMB (unified Markov binary) format import + export#267
davexparker merged 9 commits into
prismmodelchecker:masterfrom
davexparker:umb2

Conversation

@davexparker

Copy link
Copy Markdown
Member

Use -importmodel model.umb or -exportmodel model.umb,
or the format=umb option for either switch.

For a textual view of the UMB, use -exportmodel model.umbt
or options format=umb,text.

Switch -test:umb triggers a round-trip export/import test.

Other code changes:

  • ExplicitModelImporter knows if its reading exact models

  • New ModelAccess interface to provide a unified view on all model types
    Use ModelAccess.wrap(Model) to create one

  • ModelExportOptions has showLabels and showRewards options

  • format={explicit,umb} option for -importmodel

Use -importmodel model.umb or -exportmodel model.umb,
or the format=umb option for either switch.

For a textual view of the UMB, use -exportmodel model.umbt
or options format=umb,text.

Switch -test:umb triggersa round-trip export/import test.

Other coder changes:

* ExplicitModelImporter knows if its reading exact models

* New ModelAccess interface to provide a unified view on all model types
  Use ModelAccess.wrap(Model) to create one

* ModelExportOptions has showLabels and showRewards options

* format={explicit,umb} option for -importmodel
So complain if e.g. is-state-initial.bin is not multiple of 8 bytes.
@davexparker
davexparker merged commit a124ac1 into prismmodelchecker:master Jan 29, 2026
6 checks passed
@davexparker
davexparker deleted the umb2 branch January 30, 2026 10:22
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.

1 participant