Symbolic export (and import?) of models

[kleinj]

As suggested on the mailing list, it would be nice to have a way to export the MTBDDs of the symbolic models (DTMC/CTMC/MDP), allowing further downstream processing using other tools.

The export of the MTBDDs is algorithmically quite straight-forward, the trickier part is coming up with a good format for capturing all the meta-data in the model.

Some questions:

• Would it be sufficient to just dump the MTBDDs for the underlying annotated graph structure? I.e., states in the models are encoded via a certain number of bits, but we don't expose the internal structure/encoding of each state (modules, local variable ranges, etc)?
  I guess that plus BDDs for the labels would be sufficient as a first step.
• Are there any standard (and nice/efficient) formats for dumping (MT)BDDs as a text file?
• There are quite a bit of "mask" type BDDs (valid ranges of variables, enabled actions in each state). Do we need to export all of them as well?

Similarily, it would be nice to have a way to import a model from an existing, externally generated MTBDD-description. But that is more difficult as there are quite a few assumptions on th encoding/organization of the symbolic data.