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