search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

Documentation lacking #50

Open Meijuh opened 9 years ago

Meijuh commented 9 years ago

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 commented 7 years ago

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