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: