Using an mcrl2 model as Model or Implementation

There are two ways in which you can use an mcrl2 model as Model or Implementation.
Both these ways start with the same step:
  • linearize the .mcrl2 file to obtain a .lps file

After this first step, the model must be made available to JTorX.
This can be done in two ways, discussed below.
If your model has a finite state space, best is to use the second method (generate a .aut file), because accessing the model via .aut is faster than via .tx.

  1. by using lps2torx to access the model on-the-fly during the test run (lps2torx.exe on Windows)
    this works for all models (including those with an infinite state space, as long as they are finitely branching and don't contain infinite sequences of internal transitions (tau steps))
    this involves writing a shell script on Unix, or batch file windows, to allow JTorX to access the model in the .lps file, and configuring JTorX to use the script or batch file:
    • to allow JTorX to access the model in the .lps file
      • on Unix (linux, mac os x) create a .tx file
      • on Windows create a .tx.bat file
    • configure JTorX to use the .tx(.bat) file as Model or Implementation
       
  2. by using lps2lts to generate a .aut file, and configuring JTorX to use the .aut file
    this only works on finite models (otherwise, generation of the .aut file never finishes)
The remaining steps are the same for both ways:
  • configure Interpretation as "action names below" and list all action names of the model as Input (stimulus) or Output (response)
  • disable visualization before you start a test run (or else JTorX may hang)
  • click the "Abort" button ("Start" button with new name) to abort a test run, when it hangs while it starts

Details follow below.

Linearizing .mcrl2 to obtain .lps

  1. linearize the mcrl2 model (e.g. spec.mcrl2) to obtain an .lps file (e.g. spec.lps)
    by doing: mcrl22lps spec.mcrl2 spec.lps

Note: of course, also the mCRL2 graphical user interface can be used to obtain a .lps file.
Note: you may want to use the -D command line option of mcrl22lps (see the mcrl22lps manual page)

Creation of .tx(.bat) file

For now such a file has to be created by hand as described below1.

Unix: Creation of .tx file

Note: the following assumes a non-windows platform.

  1. write a shell script (text file) of which the name ends in .tx (e.g. spec.tx) in which the tool lps2torx is invoked on the .lps file you obtained in the previous step:
    #!/bin/sh
    d=`dirname $0`
    exec lps2torx $d/spec.lps
    Alternative that hides possible diagnostic/debugging output from lps2torx:
    (Note: this alternative also hides diagnostics and error messages -- if things don't work, use the version above to be able to see what goes wrong!)
    #!/bin/sh
    d=`dirname $0`
    exec lps2torx $d/spec.lps 2>/dev/null
  2. make the shell script executable:
    chmod 755 spec.tx
Note: for Unix there are two lps2torx programs that both can be used:
  1. one that comes with the mcrl2 toolkit
  2. one that comes with the LTSmin toolkit (and that under-the-hood uses mcrl2 libraries)

Unix: getting best performance with lps2torx

Independent of which lps2torx you use, while it works (while it computes the possible stimuli and expected responses from the model in the .lps file), it does something that is called rewriting.
It can do this rewriting in two ways:
  1. using an interpreter, and
  2. using just-in-time-compiled code (code that is generated and compiled when lps2torx is started).

Using just-in-time-compiled code will typically be (much!) faster.
For the LTSmin version of lps2torx, this is the default.
However, for the mcrl2 version of lps2torx, the default is to use the interpreter; to make it use the just-in-time-compiled code, invoke that lps2torx with option: -rjittyc
Then your shell script becomes:

#!/bin/sh
d=`dirname $0`
exec lps2torx -rjittyc $d/spec.lps

For more information about additional options to lps2torx consult the documentation of mcrl2 toolkit or the LTSmin toolkit.

Windows: Creation of .tx.bat file

  1. write a batch script (text file) of which the name ends in .tx.bat (e.g. spec.tx.bat) in which the tool lps2torx.exe is invoked on the .lps file you obtained in the previous step:
    @echo off
    "c:\Program Files\mCRL2\bin\lps2torx.exe" "%~dp0\spec.lps" 
    

Note: in above example you have to adjust the path to lps2torx.exe according to the installation location on your system.

Creation of .aut file

  1. create an .aut file by doing: lps2lts spec.lps spec.aut

Configure Model or Implementation in JTorX

  1. if you want to use the mcrl2 model as Model
    1. Enter the path to the spec.tx or spec.tx.bat or spec.aut file in "Config Items" text fiĀeld "Model"
      (or use the Browse button; make sure it shows "TorX_Explorer programs (.tx[.bat,.exe])" respectively "Aldebaran files (.aut)")
  2. if you want to use the mcrl2 model as Implementation
    1. Make sure that the Implementation type is set to "simulation of given model - directly connected"
    2. Enter the path to the spec.tx or spec.tx.bat or spec.aut file in "Config Items" text field "Implementation"
      (or use the Browse button; make sure it shows "TorX_Explorer programs (.tx[.bat,.exe])" respectively "Aldebaran files (.aut)")

Configuring Interpretation

Typically, labels in an mcrl2 model have the form: sendMessage(1, 2), recvMessage(3, 4).

When using such model as Model for testing with JTorX you have to specify the Interpretation in JTorX as "action names below", and use the action name (first 'word') of the label.
For the example above, you could specify:

Input actions: sendMessage
Output actions: recvMessage

Then, actions with action name sendMessage will be used as stimuli, and actions with action name recvMessage will be interpreted as observations (responses).

Multiple action names can be given with whitespace or comma as separator.
It is not possible to use the same action name both for input and for output.

Note: for historical reasons, when you use lps2torx to access the .lps that is generated from your .mcrl2 (this is discussed below), the labels may look different:
Labels that look like sendMessage(1, 2), recvMessage(3, 4) in e.g. the mcrl2 simulator look like sendMessage!1!2), recvMessage!3!4) via lps2torx.
When you write an adapter, the 'glue code' that allows JTorX to interact with your system-under-test, your adapter has to work with these same labels as representation of stimuli that are to be applied and responses that have been obtained and must be checked.

Disabling visualization before start of test run

If you use a mcrl2 model as Model or as Implementation, before you start a test run you want to make sure that visualization is turned off, otherwise JTorX may hang.
To do this:
  • uncheck "Show model" (if you use an mcrl2 model as Model)
  • uncheck "Show impl" (if you use an mcrl2 model as Implementation)

If you forgot this, and pressed the "Start" button, you may notice that the text in the button now reads "Abort".
Clicking "Abort" will break off the attempt to start the test run.
You can then uncheck the visualization buttons, and try clicking "Start" again.

1 We intend to make it possible to use .lps files as Model and Implementation files in the Configuration pane of JTorX, i.e. in the future it should not be needed to create .tx files, at least for mclr2 models, see Issue #208.