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

  1. Ensure that lps2torx.exe is in your system path.

  2. Start up JTorX with the “jtorx” shell script or with “jtorx.bat”. Navigate to the “Config Items” tab (should be active by default). Set the “Model” field to the location of the helper file (see Listing 1), e.g. “D:/jtorx-helper.tx.bat”.

  3. Set the “Implementation” field to “real program, comm. labels via tcp, JTorX is server”. Set the text field below to the address of your SUT, e.g. “”.

  4. Set “Timeout” appropriately.

  5. Set “Interpretation” to “action names below”.

  6. Set “Trace kind” to “Straces”.

The picture below shows the setup screen of JTorx. .. image:: _pictures/jtorx-setup.png