Documentation lacking

[Meijuh]

it is not so easy for mcrl2 users to find their way in the documentation.
one must click on "sequential", "symbolic" or "distributed" to get at

the page "lpo2lts-grey" etc, to find out that one needs lps2lts-grey.

Just an index (sorted list) of all tools could help to navigate, or even better
extra page with "example dialogue for mcrl2 users". (probably similar

for Promela)

example:

Linearization
mcrl22lps -D onebit.mcrl2 onebit.lps
Symbolic generator:
lps-reach onebit.lps
Explicit generator/compressed file, with and without caching:
lps2lts-grey -out onebit1.gcf onebit.lps
lps2lts-grey -cache -out onebit1.gcf onebit.lps
Distributed generator, (2 processors), this time in (compressed) dir-format:
mkdir onebit2.dir
mpirun -np 2 -mca btl tcp,self lps2lts-mpi -out onebit2.dir/%s onebit.lps
Reduction (and conversion to aut):
mpirun -mca btl tcp,self ltsmin-mpi -b onebit1.gcf onebit-min1.gcf
mpirun -np 2 -mca btl tcp,self ltsmin-mpi -b onebit2.dir/%s onebit-min2.gcf
Conversion to aut or bcg:
ltsmin-convert onebit-min1.gcf onebit-min1.aut

ltsmin-convert onebit-min2.gcf onebit-min2.bcg

[Meijuh]

New releases of the website will have a list of manpages.