CIF to mCRL2 transformer

The CIF to mCRL2 transformer is used to convert a CIF specification to an mCRL2 model. mCRL2 is a tool for verifying properties of the model.

Starting the transformation

The transformation can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF simulation, validation and verification tools  Convert CIF to mCRL2…​.

  • In Eclipse, right click an open text editor for a .cif file and choose CIF simulation, validation and verification tools  Convert CIF to mCRL2…​.

  • Use the cif2mcrl2 tool in a ToolDef script. See the scripting documentation and tools overview page for details.

  • Use the cif2mcrl2 command line tool.

Options

Besides the general application options, this application has the following options:

  • Input file path: The absolute or relative file system path to the input CIF file.

  • Output file path: The absolute or relative file system path to the output mCRL2 file. By default, the output file path is the same as the input file path, but with the .cif extension removed (if it exists), and the .mcrl2 extension added. This option can be used to override the default.

  • Generate 'value' actions: To query the value of variable or current location of an automaton, a value action can be used. By default, such actions are generated for every variable and automaton with at least two locations of the CIF specification. Using this option, you can define a reduced set of variables and automata that should get such an action. See the section on value actions for more details.

  • Generate 'marked' action: Whether to generate a 'marked' action in the generated mCRL2 model. By default, a 'marked' action is generated. Using this option, generation of this action can be disabled. See the section on the marked action for more details.

Supported specifications

The CIF to mCRL2 transformer supports a subset of CIF specifications.

  • Regarding variables:

    • Discrete variables are supported. The following restrictions apply:

      • They must have a bool, enum, or int type. The latter may have a range.

      • Variables with multiple potential initial values are not supported.

      • The initial value of a variable must be a statically evaluable.

      • The transformation ensures that integer variables remain within their range, thus preventing runtime errors.

    • Continuous variables are not supported.

    • Algebraic variables are supported, if their types and values are supported.

    • Input variables are not supported.

  • Regarding automata:

    • There must be at least one automaton.

    • The supervisory kind of automata is ignored.

    • The initialization predicates in locations must be statically evaluable to true or false.

    • There must be exactly one initial location in each automaton, and it must be possible to determine this statically.

    • Multi-assignments are not supported. Multiple assignments on an edge is supported.

    • Urgent locations and edges are not supported.

  • Regarding expressions:

    • All expressions and sub-expressions must be of type bool, enum, or int. The latter may have a range.

    • Regarding boolean-typed expressions (resulting in a boolean as value):

      • Boolean literals (false and true) are supported.

      • Boolean-typed constants are supported.

      • Boolean-typed discrete variables are supported.

      • Boolean-typed algebraic variables are supported.

      • Boolean-typed received values.

      • Binary operators and, or, => and <=> on boolean-typed arguments are supported.

      • Binary operators = and != on boolean, enum and integer-typed arguments are supported.

      • Binary operators <, <=, > and >= on integer-typed arguments are supported.

      • Unary operator not on boolean-typed arguments is supported.

      • Location references are supported.

      • if expressions with a boolean-typed result are supported.

      • switch expressions with a boolean-typed result, and supported switch and key values, are supported.

      • Cast expressions on boolean-typed arguments that don’t change the type are supported.

    • Regarding enumeration-typed expressions (resulting in an enumeration literal as value):

      • Enumeration literals are supported.

      • Enumeration-typed constants are supported.

      • Enumeration-typed discrete variables are supported.

      • Enumeration-typed algebraic variables are supported.

      • Enumeration-typed received values.

      • if expressions with an enumeration-typed result are supported.

      • switch expressions with an enumeration-typed result, and supported switch and key values, are supported.

      • Cast expressions on enumeration-typed arguments that don’t change the type are supported.

    • Regarding integer-typed expressions (resulting in an integer as value):

      • Integer literals are supported.

      • Integer-typed constants are supported.

      • Integer-typed discrete variables are supported.

      • Integer-typed algebraic variables are supported.

      • Integer-typed received values.

      • Binary operators +, * and - on integer-typed arguments are supported.

      • Binary operators div and mod on positive divisors are supported.

      • Unary operators - and + on integer-typed arguments are supported.

      • if expressions with an integer-typed result are supported.

      • switch expressions with an integer-typed result, and supported switch and key values, are supported.

      • Cast expressions on integer-typed arguments that don’t change the type are supported.

  • Regarding other concepts:

    • Initialization predicates in components are not supported, unless they are statically evaluable to true.

    • Invariants are not supported, unless they do not pose any restriction.

    • I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.

    • Annotations are ignored.

Preprocessing

The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:

The following transformations are additionally applied as preprocesing (in the given order), after checking preconditions, to simplify the transformation:

Output of the transformation

Names

The mCRL2 names of CIF objects, such as automata, variables and events, are based on the absolute names of the CIF objects. Each . is replaced by an apostrophe ('), to form a valid mCRL2 name. A single apostrophe is added at the end of each name, to ensure that the names don’t conflict with mCRL2 keywords. For an automaton a with a location x, its absolute name is a.x. Its mCRL2 name is thus a'x'.

Enumerations

The generated mCRL2 model starts with an mCRL2 sort for each CIF enumeration. For compatible enumerations, a single representative is used. Due to linearization, locations of automata with at least two locations are represented as location pointer variables, and their values come from enumerations as well.

Events

For each CIF event, an mCRL2 action is generated.

Variable 'value' actions

For each CIF discrete variable, a 'value' action may be generated. Due to linearization, locations of automata with at least two locations are represented as location pointer variables, and thus an action may be generated for them as well. The name of the action is the mCRL2 name of the variable, with 'varvalue added to it as postfix. These mCRL2 actions have as type the type of the corresponding CIF variable.

By default, a 'value' action is generated for each discrete variable and for each automaton with at least two locations. In some cases, this may not be wanted. Variables that never have to be queried for their value do not need such an action. Having such an action available anyway increases the amount of work that has to be done by the mCRL2 tool. To restrict the generation of 'value' actions, the Generate 'value' actions option can be used (--value-actions=…​ or -v …​).

The option takes a comma separated list of variable/automata name patterns, that are considered in the order they are given. Each pattern can add or remove variables and automata. If the pattern starts with a + character, variables are added and thus get a 'value' action. If the pattern starts with a - character, variables are removed and thus don’t get a 'value' action. If the pattern start neither with a + nor with a - character, variables are added.

The main part of each pattern is the name of the variable or automaton to add or remove. The absolute names of variables and automata should be used. Only automata with at least two locations can be used. In addition, you can use the * character as a shorthand for 'zero or more arbitrary characters', allowing you to write abbreviations, and match several variables and/or automata at the same time.

The list of patterns is interpreted relative to selecting no variables. That is, if an empty list of patterns is specified, no variables and automata are added. By default, the +* pattern is used, which adds all variables.

For example, assume existence of the following automata and variables in a CIF specification:

A.p12 A.q2 A.z B B.x B.y1 B.y2 B.z C.q

Below a number of example option values are given, together with what automata and variables they select from the above list.

  • The option value B.x,+A.z selects variables B.x and A.z.

  • The option value +* selects all automata and variables.

  • The 'empty' option value selects no automata and variables. On the command line or in ToolDef scripts, when using the -v short option, use '' for the 'empty' option value.

  • The option value +*1 selects all automata and variables that end with a 1, which in this case is variable B.y1 only. Variable A.p12 does have a 1 in it, but not at the end.

  • The option value +*1* selects all automata and variables with a 1 at any position. This matches both A.p12 and B.y1.

  • The option value +*,-B,-B.* selects all automata and variables, except automaton B and the variables defined in it. First, +* adds all automata and variables. Then, -B removes automaton B. Finally, -B* removes all variables that start with B., so all variables in automaton B.

'marked' action

By default, a marked action is generated. The action is enabled when the CIF specification’s marker predicate holds, and is disabled otherwise. The action allows to verify properties in mCRL2 that relate to marked states of the CIF specification. To disable the generated of this action, use the Generate 'marked' action option can be used (--marked-action=off or -a0).

Behavior

A single mCRL2 process named P is generated that represents the behavior of the CIF specification. The process has a parameter for each variable of the CIF specification. Due to linearization, this includes the location pointer variables for automata with at least two locations.

The process consists of alternative process expressions. For each linearized CIF edge, there is one alternative. Each of these alternatives consists of a guard, an action and a recursive invocation of process P with the updates to the variables. The mCRL2 guard expressions are constructed from the guards of the linearized CIF edges. Additional guards are added to ensure that integer variables remain within their ranges, thus preventing runtime errors.

For each CIF variable and automaton with a variable 'value' action, an additional alternative process expression is added. It allows the variable 'value' action to occur for the current value of the variable.

Initialization

At the end of the generated mCRL2 program, an initial mCRL2 process is given. It matches the initial state of the CIF specification.

Example

Consider the following CIF specification:

event a, b, c;

automaton P:
  disc int[0..10] x = 0;
  disc int[-5..5] zero = 0;

  location p1:
    initial;
    marked;
    edge a do x := x + 1 goto p2;

  location p2:
    edge c when Q.y != 0 goto p1;
    edge a do x := 1 goto p1;
end

automaton Q:
  disc int[0..1] y = 1;

  location q1:
    initial;
    edge a when y = 1 goto q2;

  location q2:
    marked;
    edge b when y = 1 and P.x < 8 and P.zero = 0 goto q1;
    edge b when y = 0 => P.x >= 8 goto q1;
end

By default, the following mCRL2 model is generated for it:

% Generated by CIF to mCRL2.

% Sorts for CIF enumerations.
sort P'LPE' = struct P'p1' | P'p2';
sort Q'LPE' = struct Q'q1' | Q'q2';

% Actions for CIF events.
act a';
act b';
act c';

% Actions for CIF variables having certain values.
act P''varvalue: P'LPE';
act P'x''varvalue: Int;
act P'zero''varvalue: Int;
act Q''varvalue: Q'LPE';
act Q'y''varvalue: Int;

% Action for CIF marker predicate.
act marked;

% Process for behavior of the CIF specification.
proc P(
    P'x': Int,
    P'zero': Int,
    P': P'LPE',
    Q'y': Int,
    Q': Q'LPE'
) =
    % CIF linearized edges.
    ((((P' == P'p1') && (Q' == Q'q1')) && ((Q'y' == 1) && ((0 <= (P'x' + 1)) && ((P'x' + 1) <= 10))))) -> a' . P(P'x' = (P'x' + 1), P' = P'p2', Q' = Q'q2')
    +
    ((((P' == P'p2') && (Q' == Q'q1')) && (Q'y' == 1))) -> a' . P(P'x' = 1, P' = P'p1', Q' = Q'q2')
    +
    ((((Q' == Q'q2') && (Q'y' == 1)) && ((P'x' < 8) && (P'zero' == 0)))) -> b' . P(Q' = Q'q1')
    +
    (((Q' == Q'q2') && ((Q'y' == 0) => (P'x' >= 8)))) -> b' . P(Q' = Q'q1')
    +
    (((P' == P'p2') && (Q'y' != 0))) -> c' . P(P' = P'p1')
    +
    % CIF variable value actions.
    P''varvalue(P') . P()
    +
    P'x''varvalue(P'x') . P()
    +
    P'zero''varvalue(P'zero') . P()
    +
    Q''varvalue(Q') . P()
    +
    Q'y''varvalue(Q'y') . P()
    +
    % CIF 'marked' action.
    (((P' == P'p1') && (Q' == Q'q2'))) -> marked . P()
;

% Initialization.
init P(0, 0, P'p1', 1, Q'q1');