Metacommand:export - Walnut-Theorem-Prover/Walnut GitHub Wiki

The "export" metacommand exports intermediate automata to a specified format: BA, GV, and TXT are supported.

The export syntax for the metacommand is as follows:

[export 0 BA] ## export the 0th intermediate automaton to BA format

[export * TXT] ## export all automaton (wildcard) to TXT format

Example usage:

[export * BA]eval shortExample "T[a] < b"::

This exports the intermediate automata generated during the eval command. These are generated as: shortExample_pre_0.ba, ..., shortExample_pre_n.ba.

The "_pre" refers to these being generated before determinization happens.

The exported results are saved in the session Result/ subdirectory.