µCRL toolset with POR for Branching Security Protocols
The µCRL toolset version 2.18.5 for Linux extended with POR for branching security protocols can be downloaded here.
The µCRL specifications and .tbf files of the optimistic fair exchange protocol case study can be downloaded here.
For instructions how to use the µCRL modelling language see the official website.
How to compile the µCRL toolset
Unpack the tool archive and cd to the main folder. We recommend compiling the µCRL toolset
by typing the following at the command line (as root):
1. ./configure --enable-development
3. ./make install
How to obtain the .tbf files from the specifications
Although the .tbf files (which are linearised versions of the µCRL specifications)
are provided in the case study package above, they can be generated
from the µCRL specifications with some additional optimisations, by typing the following
at the command line (for a given specification a.mcrl):
mcrl -stdout -regular -nocluster a.mcrl | constelm | parelm | sumelm | constelm | stategraph | constelm > a.tbf
How to use the generation algorithms in the µCRL toolset
Given a .tbf file a.tbf, type the following at the command line to run
the three different generation algorithms:
Exhaustive breadth-first generation (Gen(F))
instantiators -local a.tbf
Pruning algorithm (Gen(P))
instantiators -local -select com_recv a.tbf
Reduction algorithm (Gen(R))
instantiators -local -select1 com_recv a.tbf