            jSpin - Java Graphical User Interface for Spin
     SpinSpider - Automatic Generation of State Transition Diagrams
              (See title bar for version number)
          Copyright 2003-10 by Mordechai (Moti) Ben-Ari.

jSpin is a graphical user interface for the Spin Model Checker
that is used for verifying concurrent and distributed programs.
The Spin website is http://spinroot.com.
The jSpin website is 
http://stwww.weizmann.ac.il/g-cs/benari/jspin/.

PLEASE READ THE MANUALS jspin-user.pdf and spider-use.pdf!!
In particular, read the sections on installation,
configuration and troubleshooting.
This Help file presents a short description of the menus.

File: 
New, Open, Save, Save As, and Exit are standard.
Switch file closes the current file and opens the previous one.

Editor: 
Undo, Redo, Copy, Cut, Paste, Find and Find again are standard.

Spin:
Run Spin in one of five modes:
Check runs a syntax check.
Random runs a random simulation.
Interactive runs an interactive simulation.
Verify runs an verification.
Guided runs a guided simulation using the trail file created
by the execution of the analyzer.

Convert:
Load loads a .prp file into the LTL formula field:
Clear clears the field.
Translate translates it into a never claim stored in a .ltl file.
LTL Name selects an internal LTL formula to use for verification.

Options - change the option strings used with Spin:
Common is used to select which data to display for Random,
Interactive and Trail: statements, local and global variables 
and messages sent and received.
The next options are for running the Spin sequence:
  Spin: Check, Random, Interactive, Verify, Trail.
  C Compiler.
  Pan.
Default restores the defaults of all options and settings.
Save saves the options, settings and the current directory for File/Open.

Settings - change settings for verification and display:
Max steps for Random, Interactive and Trail modes.
Max depth for search depth when running the pan verifier.
Seed - if non-zero its value is used for Random simulation.
Weak fairness during verification.
Safety, Acceptance, Non-progress verification modes.

Output - control display of filtered Spin output:
Maximize the right text area that displays the output.
Exclude variables - exclude (and include) these variables in the display.
Exclude statements - exclude (and include) these statements in the display.
Variable width - width of the columns used to display the variable values.
Save output - saves the filtered Spin output in a file with extension .out.
Raw output - saves the unfiltered Spin output in a file with extension .raw.
Display raw - displays this file for debugging purposes.

SpinSpider:
Display debug - display the debug file created by SpinSpider.
SpiderSpider - popup SpinSpider dialog:
   Format - graphical output format
   Dot size - size parameter for dot
   Trail style - emphasize with color or bold
   Variables - a list of the variables in the program must be given
   Processes - the number of processes
   Radio buttons:
     No trail - display state diagram without trail (if any)
     Emphasize/only trail - a trail from a verification must exist
     Automata - display the processes as automata

Help:
Help and About are standard.
