## 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` or `.cifx` 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` or `.cifx` 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 a variable or current location of an automaton, a value action can be used. By default, such actions are generated for every discrete variable, input 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.

    - The initial values of a variable, if explicitly specified, 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.

- Regarding automata:

  - There must be at least one automaton.

  - The supervisory kind of automata is ignored.

  - 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 input 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 input 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 input 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:

  - Requirement state invariants are not supported.

  - State invariants that depend on input variables are not supported.

  - 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:

- Remove I/O declarations

- Remove annotations

- Eliminate component definition/instantiation

- Simplify values

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

- Eliminate type declarations

- Eliminate constants

- Eliminate algebraic variables

- Eliminate state/event exclusion invariants

- Linearize (product with merge)

- Eliminate state invariants

- Convert `switch` expressions to `if` expressions

- Eliminate `if` updates

### 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.

#### Input variables

For each CIF input variable, an mCRL2 action is generated. Such an action is used to allow an input variable to change value. The name of the action is the mCRL2 name of the input variable, with `'input` added to it as postfix.

#### Variable 'value' actions

For each CIF discrete and input 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, each input variable, and 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 input variable, and additional alternative process expression is added. It allows the input variable to change to a different value, so to any value supported by its type, except for the value it already has.

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.

If the CIF specification has multiple initial states and/or initialization predicates in components (so outside locations), an `initialize` action is generated in the mCRL2 program. The `initialize` action is performed to determine the initial state, after which process `P` is started from that initial state. No `initialize` action is generated if the CIF specification has only one initial state and does not have any initialization predicates, including no initialization predicates generated by linearization. If the CIF specification has multiple initial states, the `initialize` action non-deterministically chooses one of them, allowing verification using mCRL2 to consider the behavior of the CIF specification from any initial state. If the CIF specification has no initial state, then the mCRL2 program always has an `initialize` action, but it is not possible to take that action, and thus the process deadlocks immediately.

#### 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 the CIF to mCRL2 transformer of the Eclipse ESCET toolkit.

    % 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/automata having certain values/locations.
    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') || (P' == P'p2')) && (Q' == Q'q1')) && ((Q'y' == 1) && ((0 <= if((P' == P'p1'), (P'x' + 1), if((P' == P'p2'), 1, P'x'))) && (if((P' == P'p1'), (P'x' + 1), if((P' == P'p2'), 1, P'x')) <= 10))))) -> a' . P(P'x' = if((P' == P'p1'), (P'x' + 1), if((P' == P'p2'), 1, P'x')), P' = if((P' == P'p1'), P'p2', if((P' == P'p2'), P'p1', P')), 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');