How to start?


1. After launching the product, the SpinRCP's splash screen appears first and then the Workspace Launcher dialog prompts you for what workspace to use for this session. A workspace is a folder where SpinRCP stores your projects. According to a platform, a default workspace is set in your home directory. The dialog will allow you to browse for or manually enter a new workspace location. After clicking the OK button, the chosen workspace with the default SpinRCP perspective opens. If there exists any previously created workspace, you may just select and reuse it. Note: Reuse of an existing workspace created with SpinRCP Version 2.x.x within SpinRCP Version 3.x.x is not possible. In this case, create a new workspace and copy the existing projects thereinto.

In the Title Bar, the SpinRCP's version and release date are shown. If the path to Spin is already set in the PATH environment variable, the Spin version and its release date are shown as well. Below the Title Bar, the Menu Bar, and the Tool Bar there are three visual components: a Model Navigator View at the left side, a Promela Editor at the upper right side, and a Console View at the bottom right side. The Model Navigator View is activated. If you move a cursor on its highlighted title bar, a tooltip Workspace appears. This means that the Model Navigator shows the contents of your workspace folder. It is empty if the workspace was newly created.


The default SpinRCP perspective
You can rearrange the layout of SpinRCP's windows by dragging and dropping views and editors to different positions within the Workbench window, resize them by dragging the sashes which separate them, or even detach any window by dragging and dropping it outside the Workbench. A detached window is very useful if you have two monitors and you maximize it to the full screen on the second monitor. Any detached window can be attached back to an arbitrary position within the SpinRCP's Workbench window by using drag and drop operation again.

2. SpinRCP needs to know the paths to three external tools: Spin, C compiler, and Graphviz dot. It is highly recommended that you update the PATH environment variable of your system with the paths to these external tools. Set these paths in SpinRCP by opening the Spin preference page Window > Preferences > Spin and enter or select individual paths using Browse... buttons. If the PATH environment variable of your computer system includes paths to Spin, C compiler, and Graphviz dot, you don't need to enter their absolute paths but just their names (e.g., spin, gcc, dot). The default path to Spin is preset to spin. If you have given the Spin executable a different file name, change the path accordingly. In addition to the latest Spin version you may have installed some of its previous versions (e.g. Spin Version 5.2.5, Spin Version 6.1.0, and Spin Version 6.4.3 under file names titled spin525, spin610, and spin643, respectively) in your Spin directory. To analyze your models with different versions of Spin, switch between versions by either entering or selecting the chosen executable file name into the Spin path text field. Paths with spaces are also allowed. SpinRCP handles them correctly.

Spin preference page




How to create or import a Promela model?

  1. Promela models can be either created or imported into the workspace. In either cases you must first create a project (or a file container), where your model(s) will be stored. You can do it by opening the File > Other wizards and when you create your very first project checking the Show All Wizards. Now a General wizard appears. Double-click it and continue by selecting Project > Next. Alternatively, you can just right-click anywhere within the Model Navigator, select New and click Project. In the New Project window, enter the project name. If you want to create the project within the default workspace, leave the checkbox Use default location checked and click Finish. If you want to put a project anywhere in the file system outside the default workspace, uncheck the checkbox and input or select an absolute path for the new project and click Finish. A newly created project appears in the Model Navigator View.

  2. You can arrange Promela models in the workspace at your will. The first choice may be to create a separate project for each model you analyze. In this case you have a flat structure of clearly separated files for each model. Alternatively, you can analyze more differently named models in the same project. In general, you may prefer several projects at the top level and a tree structure of folders and subfolders containing Promela models below them. A new folder/subfolder can be created as follows: Click the project/folder/subfolder, which will be the parent of a new folder/subfolder and then select File > Other > General > Folder > Next, enter a folder name into a Folder name text field, and click Finish. A newly generated folder/subfolder appears at the given place in the Model Navigator.

  3. A new Promela file in SpinRCP can be entered as follows: Click the project/folder/subfolder, where the file should be stored, and select File > Other > Other > Promela file > Next, enter the Promela file name into a File name text field (the file name extension must be pml), and click Finish. A newly generated Promela file appears at the given place in the Model Navigator.

  4. If you have an existing Promela model anywhere in your file system, you can simply copy-paste or drag-and-drop it to the appropriate place in the SpinRCP's Model Navigator. SpinRCP also supports the use of linked resources, i.e. files and folders that are stored in locations in the file system outside of the SpinRCP's workspace.





Viewing and editing a Promela model


Promela Editor is a special case of a text editor, which helps a user to specify models in Promela. It is the largest part of the default SpinRCP perspective. Many instances of the Promela Editor containing Promela (or other) files can be opened simultaneously, but only one editor can be active at any one time. The active editor is the one, the title of which is highlighted. By right-clicking anywhere within the Promela Editor, a drop-down menu opens, which offers a subset of the Eclipse editor functions. For ease of viewing and editing models the following features are available: syntax highlighting, code folding, content assist, and marking a place of a syntax error.

Syntax highlighting is a feature of Promela Editor that displays the text of the source file in different colors according to the category of terms. Highlighting does not affect the meaning of the text itself; it is only intended for human readers. The colors for different groups of reserved words, comments, and default text can be selected on the Promela Editor preference page. The default colors for text and comments are black and blue, respectively. Promela reserved words can be grouped into seven sections. All the reserved words in a section will be displayed in the same color. In each section a different color can be set. By default, reserved words from all seven sections are displayed in the same (violet) color.

Promela Editor preference page

Code folding allows the user to selectively hide or display sections of a currently edited file. This allows the user to manage large amounts of text whilst viewing only those subsections of the text that are specifically relevant at any given time. Code folding is possible between an opening curly bracket "{" and closing curly bracket "}". This feature is commonly used to hide/display the bodies of large proctype declarations and is essential for studying the specifications in real-size systems.

Matching bracket highlighting is a feature of Promela Editor that facilitates the work with brackets. Positioning the cursor immediately after a bracket will highlight the corresponding closing or opening bracket by drawing a small standing rectangle around it. Matching bracket highlighting is supported for the round, curly, and square brackets.

Content assist or autocomplete is a functionality provided by SpinRCP which helps you to write the code faster. You can just type in the first letter(s) of the reserved word and then press Ctrl+Space to be offered all the choices that match the entered letters that are valid for the current context. You simply select the wanted word. This help is especially useful for a beginner who is not yet well acquainted with Promela syntax.




First examination of a model


After you create or import a Promela model, you have to check if it is syntactically correct. Select a model and click Syntax Check in the Tool bar. If the Spin syntax checker detects a syntax error within Promela source code, SpinRCP parses its error message and finds out the line number where the error occurred. The Promela Editor marks this line with an error icon. A detail reason for the displayed syntax error is shown in the Console and in the Problems View. The No Syntax Error. output is written to the Console if no errors are found.

In addition, it is wise to perform the following examinations in order to become more acquainted with the model: Redundancy Check, Symbol Table, Automata View, and State Tables. They can be started by clicking the corresponding buttons in the Tool bar. The corresponding outputs produced by Spin are shown in the Console View.

Problem markers

Redundancy Check applies a property-based slicing algorithm for the selected model, which can detect eventual redundancies in the model and generate suggestions on how the model could be revised in order to use less memory.

Symbol Table prints out a detailed information about all objects in the selected Promela model. The information for each Promela object in the produced symbol table depends on its type.

Automata View generates state transition tables for each proctype and each never claim in the model in the format accepted by the dot tool from Graphviz, which transforms them to the corresponding state transition diagrams. On the Automata View preference page you can select in which graphical format the automata should be displayed, whether the Automata View dialog will be shown after graph creation (default) and whether statement merging for automata creation should be turned off (default) or on, regardless of whether it is enabled or disabled on the Verification preference page. Nine different graphic formats are currently supported. In the Select the automaton to view dialog a proctype or the never claim to be displayed can be selected. Finally, a system program, assigned to a given file format is opened and the selected automaton is displayed.


Automata View preference page


Select the automaton to view dialog


The automaton for nnode


Automata are represented by directed graphs containing states and edges between states. Colored states and edge types have the following meanings:
  • Blue rectangle represents a Promela end state. It can be either the state where the Promela proctype terminates its execution (after the closing curly bracket) or the state labeled with the "end" prefix (e.g. end1 endstate) within the Promela model.
  • Red ellipse represents a Promela accept state. Accept states are mainly used within automatic generated never claims.
  • Green ellipse represents a Promela progress state.
  • Non-bold edge represents a Promela statement that contains only local variables, otherwise it is bold.
  • Dotted edge represents the statement(s) within an atomic or d_step block.
A click on the Quit button closes the dialog window and completes Automata View command execution.

State Tables produces state tables for each proctype and each never claim in the model. On the State Tables preference page a user can select, which version of the verifier state tables should be displayed: the original one, two intermediate ones, or the final, optimal one (default). Regardless of whether the statement merging is enabled or disabled on the Verification preference page, statement merging for state table creation may be turned off (default) or on. Spin output is postprocessed and the most useful information is pretty-printed on the Console. The following information is contained in each state table: the source and target state of the transition (From State and To State), the transition ID, the transition type (A=atomic, D=d_step, L=local, G=global), source-state labels (p=progress, e=end, a=accept), the line number and the statement in the Promela model source file causing the transition.

In order to get more insight into the dynamic behavior of the model, you can run either a random or an interactive simulation. They are described in the Simulation section.




Verification


The most powerful functionality in Spin that actually performs model checking is the verification. It is selected by clicking the Verification tab in the SpinRCP’s Tool bar. Now the quite complex Verification preference page is shown. In the upper part, you can export current verification parameters (verification profile) to an xml file and import or reload a previously saved verification profile. The current verification profile filename including date and time of its creation are shown. Verification options are accessible below in three tabs: Basic Options, Advanced Options, and Iterative/Swarm Run.

In the Basic Options tab, you can select first a correctness property to be proved (either safety (default) or liveness) and several additional options (assertion violations and invalid end states for safety properties, non-progress or acceptance cycles with/without weak fairness for liveness properties, and whether to report unreachable code and check xr/xs assertions or not for both correctness properties types. Then, the storage mode (exhaustive, bitstate hashing or hash-compact) can be selected. Two lossless compression methods (minimized automata and collapse compression) are available for the exhaustive storage mode.

If any never claim exists, it may be considered in the model verification process by clicking the Apply never claim button. A never claim can be specified in four different ways.
  • In the first one, which is a default, a never claim or an LTL formula is specified in the model itself. In the text field right to the label a name of the never claim/LTL formula to be checked against the model has to be written. Such an in-model never claim specification is possible since Spin Version 6.
  • The second way is to enter an LTL formula in the text field.
  • The third one is to enter or select the file name, in which the single-line LTL formula is written.
  • The last way to specify a never claim is to enter or select a file name with a contained never claim.

Basic verification options

By checking the Use these parameters checkbox, the Compile-time and Run-time text fields become enabled and a user can explicitly enter the compile-time and run-time parameters that supersede the clicked options and parameters entered elsewhere. All other buttons, checkboxes, labels, and text boxes become disabled.


Advanced verification options
In the Advanced Options tab it is possible to enter several advanced verification parameters (the amount of the available physical memory in megabytes, the estimated state space size, the maximum search depth, number of hash-functions in bitstate mode, the size for minimized automaton, extra verifier generation options, extra compile-time directives, and extra run-time options).

Next, some error-trapping options can be selected. A user can enter an error number at which verification will stop or require that verification does not stop at errors. Additional options in error trapping is to save all error trails, add complexity profiling and compute variable ranges.

Similar as in simulation, the behavior of a full queue in the verification process can be selected. It may either block (default) or lose new messages.

In the last group of options on this tag, two different search modes can be selected (depth-first search (default) or breadth-first search). In both options, partial ordered reduction may be applied for reducing the number of reachable states. In the depth-first search mode, two additional options are available: iterative search for short trail and bounded context switching using a given bound (default 0).

The Iterative/Swarm Run tag can be used to apply iterative sequential or swarm parallel runs of a pan verifier if the bitstate hashing storage mode is selected. If the verification process uses other storage modes, exhaustive or hash-compact, all buttons, labels, and text fields on this tag are disabled.

Two bitstate search refinements are available: iterative sequential runs (default) of pan verifier with the hashtable size increasing step by step from -w18 up to -w35 until an error is found and so-called swarm parallel runs, where N instances of pan verifiers are executed in parallel (on N cores) and -w is incremented every M runs. For each run, several other parameters are also randomized for spreading search in different directions and thus increasing the covered fraction of state space. Values for parameters N and M have to be set. The default values of N and M are 10 and 1, respectively.

A printout of a verification run is shown in the Console View. If the verification finds an error, a counterexample is generated and saved in a so-called trail file with the file extension trail appended to the original Promela model file name. If selected, multiple error-trail files may be produced. The trail file(s) can be used in a guided simulation that replays the execution that violated the property.

Iterative/Swarm Run options




Simulation


A click on the Simulation button in the Tool bar opens the Simulation preference page. It offers the user the possibility to select the Spin simulation mode (random, guided, or interactive), the number of initial steps skipped (default 0), the maximum number of simulation steps (default 10000), how a full queue is simulated (either blocks (default) or loses new messages), select simulation output filters (tracking global and/or local variables, very verbose tracking of variables, suppress details at the end of simulation, suppress print statements in simulation) and select or enter extra Spin options.

Random simulation is a good approach for first examination of a Promela model behavior by observing its execution run. At each point of the execution path where more nondeterministic choices can be taken, a choice for the continuation of the execution run is selected at random. A seed value can be set for random simulation. It ensures repeatability. The same seed produces the same execution run. If no seed is set, it will be randomly generated for each run. If checked, the seed value will be printed at the end of simulation.

Simulation preference page


Interactive simulation dialog
Interactive simulation allows you to select one out of all executable Promela statements in order to resolve the nondeterministic continuation of the execution run. The selection can be done in the interactive simulation dialog. A click on the Quit button closes the dialog and terminates the interactive simulation.

Guided simulation uses an error-trail file produced in a verification run. Therefore, if the verification discloses an error, the guided simulation will be used for displaying the execution run that violates the checked property of a model. Either the default Spin trail file with the extension .trail added to the original Promela source file or any other Spin trail file can be selected for guided simulation. The latter option should be used in cases where the verification run produced more trail files, one for each disclosed error. For example, the Promela model specified in protocol.pml file could produce the following error-trail files: protocol.pml1.trail, protocol.pml2.trail, and protocol.pml3.trail. In guided simulation mode, a user can select the option to use pan instead of Spin to simulate the model containing embedded C-code. If this option is selected, pan will read and execute the trail, found previously during the verification run. The default pan execute trail option is -r, but several other options may be selected. Displaying of MSCs is possible only by using -g option.

After the Simulation button in the Tool Bar has been pressed and the Simulation preference page confirmed the Simulation View is shown. At the top of the view there is a label showing the selected simulation type (Random Simulation, Guided Simulation, or Interactive Simulation) including the Promela model filename and four Simulation/Replay buttons: Run, Stop, Message Step, and Single Step. The simulation type can be changed by clicking the View Menu (a small downward pointing arrow in the top right corner of the Simulation View) and selecting the new simulation type from the drop-down menu that appears.

During the simulation/replay, two Java threads run in parallel: a Spin simulation/replay thread and an MSC refreshing thread. The simulation/replay thread executes the Spin simulation (random, guided, or interactive) and displays Spin textual simulation outputs on the Console. The variable values and queue contents values are updated in two separate tables at the bottom of the Simulation View. The current simulation step number is shown at the top of the tables. In parallel, the MSC refreshing thread is displaying the MSC in MSC Viewer window »on the fly«.

Simulation/Replay view


By clicking the Run button, the simulation starts and continues without stopping till the end or till the click on the Stop button. MSCs are being refreshed periodically each time the MSC refresh interval expires as given on the MSC Viewer preference page. The default and minimal value of the MSC refresh interval are 5 and 1 millisecond, respectively. During the simulation run the replay buttons Message Step and Single Step are being disabled. They become enabled again when the simulation ends or is stopped. By clicking the Single Step button, a user can replay the simulation run step by step through Promela model statements. On the other side, by clicking the Message Step button, MSC is being drawn message by message (if any message is sent and received in the model at all) and process by process (each time a new process has been created). Message by message and step by step simulation replay can be combined. For example, by successive clicking the Message Step button a user could come to the interesting part of the simulation trace, then replay it in detail by clicking the Single Step button and finally use the Message Step button again. Not only the simulation run, but also the replay run can be stopped with a click on the Stop button.


Spin textual simulation
outputs on the Console

A random simulation MSC for leader.pml


MSC Viewer preference page

Several Simulation View options to adapt the display of MSCs are available below the simulation buttons. The user can do the following:
  • select a subset of messages that will be ignored and not displayed in the MSC diagram,
  • select a subset of messages that will be displayed in the MSC diagram,
  • rename selected messages,
  • join two or more processes into a new virtual process, and
  • select whether to show or hide message parameters.
For the first four options, a hint about the input command syntax which has to be typed into the corresponding text field together with an example of use is displayed if you place the cursor above that text field. In order to illustrate some of these options, the display of an MSC with a virtual process called joined23 that joins original processes with IDs 2 and 3 and with the renamed messages, where each message ID was prefixed by letter 'm' is requested. In the MSC Viewer you can see how the corresponding MSC is being changed accordingly.



Simulation view with parameters

An MSC View with the renamed
messages and a virtual process
Each Spin simulation output is written to a file. Its name is obtained by concatenating the name of a Promela model, simulation mode (rnd_sim, gui_sim or int_sim), and file extension out. For example, the Spin random simulation output of leader.pml Promela model is stored to file name leader.pml.rnd_sim.out. An already generated simulation trail from a file of type out can be graphically displayed in the MSC Viewer in two different ways, either by a double-click on an out file in the Model Navigator View or by a click on the Import Trail button in the Tool Bar when the Simulation View is active and selecting an out file from the Import Trail dialog. An out file can be read into the SpinRCP's text editor as text if you right-click it in the Model Navigator View and select Open With > Text Editor.



Conversion of Spin simulation trace to MSC


SpinRCP includes another view called Spin Trail To MSC that is not shown by default. You can disclose it by clicking Window > Show View > Other… SpinRCP > Spin Trail To MSC. It is intended for converting a Spin simulation output trail (produced either by random, interactive, or guided simulation) to the standard MSC text file formatted according to ITU-T Z.120, which can be displayed in graphical form using external design tools that support that standard (e.g. ObjectGEODE). First, you have to select the Spin simulation trail file (extension out) that has to be converted and then enter or select the name of an MSC file (extension msc) to be generated. If you want to display the list of all processes and the list of all transmitted messages among them during the simulation run, just click the Read button. Both lists will appear in the tables at the bottom of the view. The displayed lists are helpful, especially if you decide to enter any of the available options before the conversion. Three options are the same as in the Simulation View. The last one gives a user the possibility to enter a comment to be added in the msc file. Finally, make a conversion by clicking the Convert button.

Spin Trail to MSC View



A hierarchical display of leader.pml.rnd_sim.msc file in ObjectGEODE

The conversion can be done even more easily. If an MSC in the MSC Viewer is selected, the Export to MSC button in the Tool bar is enabled. You just click it and enter or select the msc file name and the conversion begins.

Here you can see, how the ObjectGEODE tool hierarchicaly displays the generated leader.pml.rnd_sim.msc file. The MSC at the left side shows the top level view, where the original processes 2 and 3 are joined and thus the communication between them is hidden. The MSC at the right side shows the internal messages within the joined23 process. Such abstraction is very useful if you want to analyze huge MSCs in a top-down manner in order to hide details that are not interesting at a given abstraction level and would otherwise represent an unnecessary complexity. Using the option for creation of joined (virtual) processes you can display MSCs at more than two hierarchical levels.


X