Model Program Viewer

Usage Examples Options FileMenu Toolbar Selections ContextMenu

Use mpv to visualize and analyze the behavior of one or more model programs. For example, visualize the model program from this page by mpv /r:PowerSwitch.dll PowerSwitch.Contract.Create.



The mpv tool performs exploration, which generates a finite state machine (FSM) from a (possibly "infinite'') model program. The tool displays the graph of the generated FSM. The tool explores and displays the composition of all the model programs named on its command line, which can be C# model programs or FSMs. The tool provides many options (on the command line and in its GUI) for adjusting the appearance of the displayed graph, and for saving and restoring the results of exploration. It also provides facilities for inspecting the states (program variables and their values), and for exploring programs interactively (incrementally, working forward from some state of interest).

By searching the FSM, mpv can perform safety analysis that checks whether the system can reach forbidden (unsafe) states, and liveness analysis that identifies dead states from which goals cannot be reached. The mpv tool can also check temporal properties expressed as FSMs by using composition.

In order to run mpv, you must also install the graph layout engine GLEE. Notice that GLEE uses a less permissive license than NModel. Alternatively to mpv (or in addition to it), you may use mp2dot (Model Program to Dot). The mp2dot program does not require GLEE, and is covered by the more permissive NModel license.

Usage

mpv [/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[+|-]]* 
[/stateShape:{Box|Circle|Diamond|Ellipse|Octagon|Plaintext}]* 
[/direction:{TopToBottom|LeftToRight|RightToLeft|BottomToTop}]* 
[/combineActions[+|-]]* [/livenessCheckIsOn[+|-]]* [/safetyCheckIsOn[+|-]]* 
[/testSuite:<string>]* [/fsm:<string>]* [/startTestAction:<string>]*
[/group:<string>]*
<model>* @<file>

Examples

mpv @mpv_args.txt
mpv /fsm:M1.txt /fsm:M2.txt
mpv /testSuite:ContractTest.txt
mpv /r:NewsReaderUI.dll NewsReader.Factory.Create
mpv /r:NewsReaderUI.dll /mp:NewsReader
mpv /r:Controller.dll Reactive.Factory.Create /safetyCheckIsOn+
mpv /r:Controller.dll /mp:Reactive /safetyCheckIsOn+

Options

/?, /help
Displays usage information and exits.

[/reference:<string>]*
Referenced assemblies. (Short form: /r)

[/mp:<string>]*
Model programs given in the form M or M[F1,...,Fn] where M is a model program name (namespace) and each Fi is a feature in M. Multiple model programs are composed into a product. No factory method is needed if this option is used.

[/initialTransitions:<int>]*
Number of transitions that are explored initially up to maxTransitions. Negative value implies no bound. Default value: '-1'

[/transitionLabels:{None|ActionSymbol|Action}]*
Determines what is shown as a transition label. Default value: 'Action'

[/nodeLabelsVisible[+|-]]*
Visibility of node labels. Default value: '+'

[/initialStateColor:<string>]*
Background color of the initial state. Default value: 'LightGray'

[/hoverColor:<string>]*
Line and action label color to use when edges or nodes are hovered over. Default value: 'Lime'

[/selectionColor:<string>]*
Background color to use when a node is selected. Default value: 'Blue'

[/deadStateColor:<string>]*
Background color of dead states. Dead states are states from which no accepting state is reachable. Default value: 'Yellow'

[/deadStatesVisible[+|-]]*
Visibility of dead states. Default value: '+'

[/unsafeStateColor:<string>]*
Background color of states that violate a safety condition (state invariant). Default value: 'Red'

[/maxTransitions:<int>]*
Maximum number of transitions to draw in the graph. Default value: '100'

[/loopsVisible[+|-]]*
Visibility of transitions whose start and end states are the same. Default value: '+'

[/mergeLabels[+|-]]*
Multiple transitions between same start and end states are shown as one transition with a merged label. Default value: '+'

[/acceptingStatesMarked[+|-]]*
Mark accepting states with a bold outline. Default value: '+'

[/stateShape:{Box|Circle|Diamond|Ellipse|Octagon|Plaintext}]*
State shape. Default value: 'Ellipse'

[/direction:{TopToBottom|LeftToRight|RightToLeft|BottomToTop}]*
Direction of graph layout. Default value: 'TopToBottom'

[/combineActions[+|-]]*
Whether to view matching start and finish actions by a single label. Default value: '-'

[/livenessCheckIsOn[+|-]]*
Mark states from which no accepting state is reachable in the current view. Default value: '-'

[/safetyCheckIsOn[+|-]]*
Mark states that violate a safety condition (state invariant). Default value: '-'

/testSuite:<string>]*
File name of a file containing a sequence of actions sequences (test cases) to be viewed.

[/fsm:<string>]*
File name of a file containing the term representation fsm.ToTerm() of an fsm (object of type FSM). Multiple FSMs are composed into a product.

[/group:<string>]*
Name of a state property to use as the abstraction function for grouping.

[/startTestAction:<string>]*
Name of start action of a test case. This value is used only if a testSuite is provided. Default value: 'Test'

<model>*
Fully qualified names of factory methods returning an object that is an instance of ModelProgram. Multiple model programs are composed into a product. No factory method arguments are needed if the /mp: option is used instead.

@<file>
Read response file for more options.

File Menu

Save Settings...
Saves the values of all the options (above) in a response file so they can be restored into another mpv session with the @<file> command line option.

Toolbar

The mpv tool provides several operations on a toolbar, a row of icons across the top of its window. Some icons include a down arrow you can click to display a drop-down menu. Hovering the mouse pointer over a toolbar icon displays a tooltip, text that identifies its function. Here are descriptions of the toolbar operations, each labeled by its tooltip.

(Model program name)
The name of the model program whose FSM is currently displayed. M[F1,F2] indicates model program M with features F1 and F2 included. M1 x M2 indicates the product of M1 and M2 formed by composition. Selecting M1 or M2 from the drop down menu displays the FSM of that program projected onto the product.

Zoom In
Enlarge the displayed FSM within the window. Use the scroll bars at bottom and right to pan the enlarged graph, or use Pan (below). You can also enlarge the entire window by dragging on its sides or corners; the graph will enlarge to fit.

Save as image...
Save the displayed FSM in a file. From the drop-down menu, Save as Image... saves an image in JPG format, Save as Dot... saves a text file in the dot language used by Graphviz, and Save as FSM... saves a text file in the term representation used by NModel, that can be restored into another mpv session with the /fsm:<file> command line option.

Zoom Out
Reduce the displayed FSM within the window.

Pan
Drag enlarged FSM in window, by holding down left mouse button while moving mouse. Alternative to scroll bars.

Print
Print the FSM, opens Print dialog.

Merge Labels
Toggles the mergeLabels option. When the option is '+', True, the graph appears less cluttered.

Show Self-Loops
Toggles the loopsVisible option. When the option is '-', False, the graph appears less cluttered.

Transition Labels
Cycles through the transitionLabels options: Action (most verbose), ActionSymbol (less verbose), None. The Action can always be displayed by hovering the mouse over a transition arc in the graph.

Combine Start and Finish Actions
Toggles the combineActions option. When the option is '+', True, the graph appears less cluttered.

Layout Direction
The drop-down menu offers the direction options: TopToBottom, LeftToRight, RightToLeft, BottomToTop.

State Viewer
Displays (or hides) the state viewer in a panel on the right side of the window. The state viewer shows the state variables and their values in the state that is selected by left-clicking in the displayed graph. The state can always be displayed by hovering the mouse over a state bubble in the graph.

Advanced Properties
Displays (or hides) the display of all the option values in a panel on the right side of the window. You can toggle/cycle/edit the option values in the panel. This panel also shows Exploration statistics: the number of States, Transitions, Accepting States, Unsafe States, and Dead States, so you do not need to search the graph by eye.

Selections and highlighting

Hovering the mouse over a state bubble highlights that state and shows the state variables and their values. Hovering the mouse over a transition arc highlights the arc displays its action (the action method invocation, and its return value if there is one).

Left clicking on a state bubble selects that state. The selected state is indicated by the SelectionColor. The state variables and their values in the selected state appear in the State Viewer panel, if it has been toggled on. Context menu items and keyboard shortcuts apply to the selected state.

Context menu and keyboard shortcuts

Right-clicking on a state bubble selects that state and displays a context menu with these entries:

Show Outgoing (Enter)
Hide Outgoing (Backspace)
Show Reachable (Insert)
Hide Reachable (Delete)
Select Next (n)
Select Previous (p)

To explore interactively, select the initial state, press the Delete key to hide all the transitions and other states, press the Enter key to show the transitions enabled in the initial state, press the n or p keys to select another state, and so on.