Model Program to Dot

Usage Examples Options

The mp2dot tool is an alternative to mpv that does not depend on GLEE or Windows.Forms. It is a command-line program with no graphical user interface that produces an output file in the dot graph layout language.

In order to display the output generated by mp2dot, you will also need a graph layout tool such as the dot program from the Graphviz package, and a PostScript viewer such as GSView. The Graphics sample in the examples provides two command files dotps.bat and mp2ps.bat that makes it easy to use mp2dot with these programs.

The mp2dot program is included in NModel releases 1.0.21029.0 and later.

The mp2dot tool accepts all of the mpv command line options, so it can use any mpv response file.

In addition to all of the mpv options, mp2dot supports two more: /dotFileName and /machineFileName. These two options achieve the same effect as the Save as Dot... and Save as FSM... options on the mpv toolbar. If the option is absent, that file is not written.

The mp2dot tool always writes exploration statistics to the console, even when no output files are requested, as in this example:

>mp2dot @mpv_safety_liveness.txt
  121 states
  239 transitions
    2 accepting states
   61 dead states
    4 unsafe states


mp2dot [/dotFileName:<string>] [/machineFileName:<string>]
[/reference:<string>]* [/mp:<string>]* [/initialTransitions:<int>]* 
[/transitionLabels:{None|ActionSymbol|Action}]* [/nodeLabelsVisible[+|-]]* 
[/initialStateColor:<string>]* [/hoverColor:<string>]* 
[/selectionColor:<string>]* [/deadStateColor:<string>]* [/deadStatesVisible[+|-]]* 
[/unsafeStateColor:<string>]* [/maxTransitions:<int>]* [/loopsVisible[+|-]]* 
[/mergeLabels[+|-]]* [/acceptingStatesMarked[+|-]]* 
[/combineActions[+|-]]* [/livenessCheckIsOn[+|-]]* [/safetyCheckIsOn[+|-]]* 
[/testSuite:<string>]* [/fsm:<string>]* [/startTestAction:<string>]*
<model>* @<file>


mp2dot / @mpv_args.txt
mp2dot /machineFileName:M1xM2.txt /fsm:M1.txt /fsm:M2.txt
mp2dot / /r:NewsReaderUI.dll NewsReader.Factory.Create


The mp2dot tool supports all of the mpv options. It also supports these options:

File where the dot output is saved. If this option is absent, no dot output is written. (Short form: /dot)

File where the FSM is saved. If this option is absent, no FSM output is written. (Short form: /machine)

Last edited Nov 2, 2008 at 8:55 PM by jon, version 9


No comments yet.