Tutorial

From MCRL2

The mCRL2 toolset is a collection of tools to model and analyse the behaviour of communicating processes. This tutorial shows by example how to use the toolset. We use the SQuADT interface to apply the tools to files. SQuADT is also a project manager keeping track of which tools are applied where. It is not strictly necessary to use SQuADT. All tools can also be used from the command line. Use the --help flag to view the list of available options of a tool, or browse the tool manual pages.

Contents 1 Using SQuADT 2 Obtaining a linear process specification 3 Generating a labelled transition system 4 ltsgraph and ltsconvert 5 ltsview and diagraphica 6 Simulating a linear process specification 7 Setting an external editor in SQuADT 8 Concluding remarks

Using SQuADT

Start the SQuADT tool by either typing squadt on the command line, or clicking the SQuADT icon. The SQuADT window that appears starts with an empty screen. A new project can be started, or an existing one can be opened. There is an example project in the directory examples/project. After opening it, the window splits into two parts. At the left, the files in the project are shown in a tree structure. Input files are shown in white. An output file can have any of the following colours:

• green: the file is correctly generated
• red: the file is not available (e.g. due to an error)
• blue: the file is outdated
• yellow: the file is being generated.

In general, the righthand side of the SQuADT window is used by tools to ask questions and to provide feedback. This does not only allow tools to communicate with users, without implementing a user interface, it also allows SQuADT to remember the settings that are used, to automatically rebuild files.

The SQuADT interface

Ltsgraph depicts the alternating bit protocol

The ABP modulo branching bisimulation

Ltsview shows the ABP in 3D

Obtaining a linear process specification

There is only one file in the example project, namely abp.mcrl2, which contains a behavioural description of the alternating bit protocol. Right clicking on the file abp.mcrl2 shows a pop up menu with all the tools that operate on this file type. In this case it is only the tool mcrl22lps, which is used to translate a .mcrl2 file to a linear process. Linear processes have extension .lps. After selecting mcrl22lps the SQuADT window looks like the leftmost picture above. At the righthand side of the SQuADT window mcrl22lps has listed different options to linearise. After selecting ok, mcrl22lps generates an output file with the name abp0001.lps, which shows up in the SQuADT window at the left. Using the pop-up window, this file can typically be renamed, removed and detailed information about it can be obtained. Using refresh the file can be reconstructed, with the same tool options. The configure option allows to adapt the tool parameters for rebuilding, which is especially useful when long chains of tool applications are used. The clean option removes the output file from disk, but retains the information to regenerate it.

Generating a labelled transition system

From the pop-up menu it is also obvious that there are many tools that work on .lps files. In particular there is the tool lps2lts under Transformation that generates a labelled transition system from the linear process. By selecting lps2lts a menu with options pops up at the right. For the moment we ignore all options, and simply click ok. A new file called abp0002.svc is generated and shows up in the window on the left. Note that the tree structure clearly indicates that this new file is derived from abp0001.lps.

ltsgraph and ltsconvert

There are several tools that work on .svc files. In particular, they can be visualized using the tool ltsgraph. When starting ltsgraph, the states and transitions occur at random places. (Note that on some platforms the ltsgraph window may start behind the SQuADT window.) The states and labels can be moved around using the left mouse button. By pushing the neaten button, a simple positioning algorithm will start to optimize the picture. States can still be dragged around while the diagram is being optimized. Using the right mouse button (Ctrl+mouse on Mac OS X) states can be locked, which prevents them from being moved around automatically. The resulting layout can be saved and exported to scalable graphics format (SVG) or LaTeX (pstricks). It is also possible to color individual states and to change the curvature of transitions.

Another tool that works on labelled transition systems, is ltsconvert. This is a very versatile tool to translate various representations of labelled transitions systems to each other (e.g. the .aut, .svc and .fsm formats). Moreover, it can apply strong, branching, and trace equivalence reductions on the transition systems. Let's apply ltsconvert to abp0002.svc. Set the branching bisimulation reduction option, and generate the reduced transition system (abp0003.aut). Visualizing it using ltsgraph yields the third picture above: a transition system with three states. For those who know the alternating bit protocol, this exactly depicts its desired external behaviour, in case it has two data items d1 and d2.

ltsview and diagraphica

Using ltsconvert it is also possible to create an .fsm file, which is the input format for two other graphical tools, namely ltsview and diagraphica. Start ltsconvert on abp0002.svc. Select "fsm" as the output format and put abp0001.lps as the linear process specification to be used. This last step is needed because the .fsm format requires the names, sorts and values of the process variables in each state. Without it, both diagraphica and ltsview cannot show the values of the variables in each state, strongly crippling their functionality. The state space that shows up in ltsview can be navigated using the mouse. It can be coloured on the basis of the variables in each state, but also using transitions or the existence of deadlock. Note that for the alternating bit protocol it is possible to show the individual states, transitions and backpointers. For larger state spaces (with hundreds of thousands of states) showing too much detail slows the tool down dramatically.

Diagraphica visualizes process parameters

Diagraphica as a graphical simulator

Xsim simulates the alternating bit protocol

The edit window allows to use external editors

The tool diagraphica allows to visualize the process parameters that make up each state. If diagraphica is started, the process parameters are listed in the window to the left. For the alternating bit protocol these are s30, d, b, s31, etc. Using the mouse a subset of these variables can be selected, and the whole state space is projected onto the selected variables by pushing the "Cluster nodes" button. Using different options under Attributes in the main menu, it is possible to visualize properties of the selected variables.

In the view on the right, the circles represent aggregated states. The circular shapes between these nodes are aggregated transitions, and must be read clockwise. It is possible to get an impression of the distribution of all values in the state space by switching to the trace view. By selecting some variables and performing a trace view, the values of the selected variables of all states are graphically represented in the window at the bottom. The result looks as in the leftmost picture above.

Another option of diagraphica is to graphically simulate the process. A graphical view of the process can be editted in Edit mode. In the project there is a file abp.dgd that contains an initial layout, but in edit mode any layout can be made. Using the edit DOF option, that shows up when clicking an object in edit mode, a pop up window shows up using which the colours, shape, position and even transparency of objects can be made dependent on the state of the process. Back in analysis mode, with the simulation view, it is possible to observe how the layout changes while doing simulation steps.

Simulating a linear process specification

The tool xsim operates on .lps files and can be used to simulate a process. The third picture above shows its interface. A very useful feature of xsim is its capability to load traces. Traces generated with other tools (such as lps2lts) can be easily investigated in this way. For this purpose there are a trace view possibility and capabilities to walk back and forth through the trace. The tool xsim can be interfaced to external viewers to build realistic prototype simulation of the modelled artefacts.

Setting an external editor in SQuADT

SQuADT does not provide editors for its input files. In order to edit within the context of SQuADT external editors must be installed. This can be done on the "Editing" tab on the "Preferences" window (Edit -> Preferences). For each file type an associated editor can be used. Use the $ symbol to indicate the current file on which the editor must work. The edit option can also be used to inspect generated files. For instance, a .lps file can be printed in human readable format using the tool lpspp. By sending its output to an external editor the result can be inspected. Note that an editor must be started in its own window. Therefore, indicating vi $ as an editor does not work. Using xterm -e vi $ does work, as it will start vi in a separate xterm window.

Concluding remarks

With these tools many basic analyses on behavioural descriptions can be performed. All available tools are described in the tool manual pages, although generally in terms of command line invocation. Note that SQuADT is a tool interface that is independent from mCRL2. Using the SQuADT interface library everybody can write tools that can be accessed via SQuADT.