State Machine Visualizer
Java Pathfinder
***********************************************************************

*IMPORTANT*
This program requires that Graphviz's 'dot' function is accessible
from the command line.  To install Graphviz, visit this site:
http://www.graphviz.org/Download.php
(you can exclude the other libraries besides dot if you like)


***********************************************************************

The goal of this project was to create a visualization for Java 
Pathfinder's (JPF) statechart model-checking extension. 

The program (re)creates UML state machine diagrams out of JPF
state machine models, and animate traces of event sequences
produced by the model checker.  This sequence will lead to the error.


How to use
************************************************************************

-Open the Config Options and enter your desired JPF (Java Pathfinder) 
arguments. These are standard JPF arguments, but it is expected that the 
target of the JPF run is a State Machine. (-i argument not supported)

example:

	+log.info=gov.nasa.jpf.sc
	+jpf.report.console.property_violation=error
	+choice.class=.jvm.choice.sc.SCEventGenerator
	+choice.exclude=completion
	gov.nasa.jpf.sc.StateMachine
	visualize.CEV_15EOR_LOR

(See build/jpf/samplevisualizeconfigs for more sample configurations)


-Click the 'check' button to run JPF with the selected arguments. 
(Takes a few seconds to finish the run).  The output is then displayed on 
screen.  Any errors found are listed in the selection list (next to the 
'check' button), and refer to the respective error found by JPF.

-The State Machine Logging tab may be observed during animation for more
details about the machine.

-Select an error for animation using the drop down list. The default is 
Error #1.

-Navigate the diagram using the controls at the bottom of the window.
Use the 'step' button for manual animation, and play/pause for automatic.
Adjust the slider to change animation speed.

-To change the path, select an error from the the error list at any time.
To reset animation, click the reset button.


The Diagram
**********************************************************************************

-After selecting arguments, the diagram will be generated below.  Each node
of the diagram represents a state of the machine.  The edges represent
transitions caused by trigger methods.  Guards are not considered in 
diagram generation.  Initially you will be viewing the immediate 
substates of the master state.  The diagram only allows 
viewing of the states contained by a single state at one time.

-See the legend to learn about the symbols.  A composite state
is a state which contains one or more substates.  On the left there are
two state lists, which are populated according to the conditions in 
the diagram.  You can click on most states in these lists to zoom to them.

-At any point (except during automatic animation) you may zoom into 
composite states and out of the current state using the respective 
buttons.  Also, adjust the preferences for zooming with the 'Options' button.

-At the top right of the diagram, there is a button labeled "+".  This 
button adds a second diagram to the screen. After pressing this button, a 
checkbox 'parallel' and a "-" button will appear.  To have the diagrams 
animate simultaneously check parallel, otherwise animation is staggered, 
starting on the left. To remove the second diagram, click the "-" button.
