In this tutorial we give a basic introduction into the use of the mCRL2 toolset. In each of the sections we present a number of new concepts, guided by an example, and some exercises to gain hands on experience with the tools. Note that in this tutorial we mainly focus at the use of the tools, and not on the theory that is underlying the tools. For the latter, we refer to [GMRUW09] as a brief introduction of the main concepts, and to [GM14a] for an in-depth discussion.
If you are using mCRL2 on Windows, then the compiling
rewriter is unavailable, meaning that the flag
-r jittyc to
any of the tools will fail.
In this tutorial, we assume that you will be using the tools from the command line. On Windows this is the command prompt, on other platforms this is a terminal. Commands that should be entered at the prompt are displayed as:
- A Vending Machine
- Water cans
- Towers of Hanoi
- The Rope Bridge
- A Telephone Book
- Probabilistic processes
- Using mcrl2-gui
J.F. Groote and M.R. Mousavi. Modelling and Analysis of Communicating Systems. The MIT Press. 2014.
J.F. Groote, A.H.J. Mathijssen, M.A. Reniers, Y.S. Usenko and M.J. van Weerdenburg. Analysis of distributed systems with mCRL2. In Process Algebra for Parallel and Distributed Processing. M. Alexander and W. Gardner, eds. pp 99-128. Chapman & Hall, 2009.