Instructions for REFINER

REFINER can be run on the command line by either running the refiner script (for command-line usage), or the refiner_gui script (for GUI usage).

Regarding the possible arguments for command-line usage, when REFINER is run with the help option (refiner -h), more information on this is provided.

The GUI can be operated in an intuitive way: In the top-left corner, there are options to load and save rule systems, load a functional property, and load a model. Writing new properties and models is not the purpose of REFINER. Instead, existing explicit-state model checking toolsets such as mCRL2 and CADP can be used for this.

REFINER offers the possibility to create and edit rule systems. The lower part of the GUI is used for that. The rule selection buttons offer options to create, edit and clone new transformation and process rules. A process rule is a specific kind of transformation rule, with the purpose of introducing an entirely new process. Therefore, process rules do not consist of two, but only one pattern, describing the potential behaviour of the newly introduced process.

The rule editing buttons provide the functionality to add and delete states and processes. A glue-state is, as in graph transformation, a state that is both in the left and right pattern of a rule, and therefore process LTS states matched on by glue-states are not removed when transforming. Exclusive glue-states are glue-states with the added negative application condition that matched on states may not have transitions that are not represented in the left pattern.

For a finished rule system, REFINER can verify a number of aspects:

• Semantics preservation: Does a rule system preserve the semantics of models in general?
• Property preservation for general models: Given a specific property, does the rule system preserve it? If the fairness option is selected, this check will check for safety properties
• Property preservation for a particular model: Given a specific property and a specific model, does the rule system preserve the property when applied on the model? If the fairness option is selected, this check will check for safety properties. If the divergency option is selected, then divergency information of the model is used, i.e. the possibility for the model to diverge in particular states into infinite sequences of internal actions is taken into account during the analysis.