Skip to content

Conversation

@davexparker
Copy link
Member

  • Model import using .all only uses files that exist.
  • Optionally, export/import initial state info via .tra file.
  • Import of POMDPs from explicit files (.tra, .obs, etc.).
  • States/observations optional in Dot file export.

Previously, absence of e.g. model.lab would be an error.
These are included as dummy transitions, with irrelevant fields
shown as "-", i.e., each initial state s is represented by a line
"- s -" or "- - s -" for Markov chains and MDPs, respectively.

If a .lab file is read from too, the initial states info is also
extracted from there and checked for consistency.

For now, this is only actually enabled for POMDPs,
where it is required to include observations for initial states.
Use e.g. -exportmodel file.dot:states=false,obs=false
@davexparker davexparker merged commit e6752b2 into prismmodelchecker:master Dec 31, 2025
6 checks passed
@davexparker davexparker deleted the import+export branch January 1, 2026 17:43
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