lps2torx is intended to do model based testing using the JTorx environment. It can be invoked (on a Windows environment) by:
"lps2torx.exe" "your-mcrl2-model.lps"
You should note the following
The picture below shows the setup screen of JTorx. .. image:: _pictures/jtorx-setup.png
lps2torx [OPTION]... INFILE
Provide a TorX explorer interface to the LPS in INFILE.
The LPS can be explored using TorX as described in torx_explorer(5).
-y
, --dummy
replace free variables in the LPS with dummy values
-QNUM
, --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
-rNAME
, --rewriter=NAME
use rewrite strategy NAME:
jitty
jitty rewriting
jittyc
compiled jitty rewriting
jittyp
jitty rewriting with prover
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-q
, --quiet
do not display warning messages
-v
, --verbose
display short intermediate messages
-d
, --debug
display detailed intermediate messages
--log-level=LEVEL
display intermediate messages up to and including level
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options
Muck van Weerdenburg, Frank Stappers