Please ensure that both REFINER and the mCRL2 toolset are correctly installed.
The experimental data archive contains a number of folders, each containing a model, at least one rule system to refine the model,
and some properties to check on the model and the rule system.
There is a file called README.txt present in each folder, offering information on the specific file names.
Its format is as follows:
MODEL DESCRIPTION
Network base name: (NETWORK)
Rulesystem base name: (RSYSTEM) ...
Properties: (PROP1) ...
Required options for preservation checking: (OPTS)
This information can be used to transform the network, and check for property preservation of the rule system(s).
To give an impression of the possibilities when running from the command-line, we list the standard operations with REFINER using the IDs of the README example given above.
Check that a rule system is semantics preserving. If not, produce a counter-example:
refiner -c RSYSTEM
Check that a property is preserved by a rule system for network in general. If not, produce a counter-example:
refiner -p PROP1 -c RSYSTEM
Check that a property is preserved by a rule system when applied on a given network. If not, produce a counter-example:
refiner -p PROP1 -c RSYSTEM -n NETWORK
To use multiple cores to perform checking in parallel, use the -t option, with nc the number of cores:
refiner -p PROP1 -c RSYSTEM -t nc -n NETWORK
If the property is either a safety or a fairness property, the following can also be invoked:
refiner -p PROP1 -c RSYSTEM -f -t nc -n NETWORK
Finally, if a liveness property must be checked, divergency information about the network can be incorporated in the check:
refiner -p PROP1 -c RSYSTEM -d -t nc -n NETWORK
Transform the network according to a rule system:
refiner -r RSYSTEM -n NETWORK
A possible option is to propagate divergency information along transforming, to avoid having to compute this for transformed models:
refiner -r RSYSTEM -d -n NETWORK
When running REFINER with the GUI, by default, 8 threads are run when verification is performed. Other numbers can be set at the command line, when launching refiner-gui:
refiner-gui -t nc
Besides creating and editing rule systems, the GUI offers the same options as the ones listed above for the command-line version.