CIF to mCRL2 transformer

The CIF to mCRL2 transformer is used to convert a CIF specification to a mCRL2 specification. 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 specification.

  • Instance tree definition: mCRL2 uses a tree of processes which you can specify manually here. If not specified, it takes the default solution, which first merges all CIF automata (one at a time), and on top of that, the variable processes of the shared variables (also one at a time). How to define your own tree is explained in the instantiation tree syntax Section.

  • Enable debug output: The transformer derives information about used and available variables in the instantiation tree, and uses that information to generate the mCRL2 action operations at every level. By enabling this option, this information is also written to an output file for further external analysis. By default, the information is written in a file with the same name as the input file, except first the .cif extension is removed (if present), and a _dbg.txt extension is appended. The name of the output file can be changed with the Debug output file path option. Setting the latter option enables this option.

  • Debug output file path: The absolute or relative file system path to use for writing derived information about used and available variables at every level in the instantiation tree. Setting this option changes the debug output file path to the given path. It also enables the Enable debug output option.

  • Output file path: The absolute or relative file system path for writing the generated mCRL2 output 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. By setting this option, the default is overridden by the given value.

  • Generate 'value' actions: To query the value of variable x, a value_x action can be used. By default, such actions are generated for every variable in the system. Using this option, you can define precisely which variables should have such an action. See the Generation of 'value' actions Section 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 translates the range of integer variables if used, but it does not enforce that the variables remain within the minimum and maximum integer values.

    • Continuous variables are not supported.

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

    • Input variables are not supported.

    • Equations are not supported.

  • Regarding events:

    • Channels are not supported.

    • The tau event is 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 trivially true or false.

    • There must be exactly one initial location in each automaton.

    • Conditional updates are not supported, only assignment updates are allowed.

    • Multi-assignments are not supported.

    • Urgency of locations and edges is ignored.

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

      • Binary operators and, or, ==, != and ⇒ on boolean-typed arguments are supported.

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

      • Location references are not 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.

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

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

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

  • Regarding other concepts:

    • Initialization predicates in components are not supported.

    • Invariants are not supported.

    • Marker predicates are ignored.

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

Generation of 'value' actions

The CIF to mCRL2 transformer generates a value action for each variable by default. 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 eliminate these unneeded value actions, the CIF to mCRL2 transformer has the Generate 'value' actions option.

The option takes a comma separated list of variable patterns. Each pattern can add or remove variables. If the pattern starts with a + character, variables are added. If the pattern starts with a - character, variables are removed. 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 to add or remove. 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 at the same time.

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

For example, assume existence of the following variables in a CIF model:

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

Below a number of example option values, and what 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 variables.

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

  • The option value +*1 selects all variables that end with a 1, which 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 variables with a 1 at any position. This matches both A.p12 and B.y1.

  • The option value +*,-B.* selects all variables, except those in automaton B. (+* adds all variables, then -B.* removes all variables that start with B., that is all variables in automaton B.)

Syntax of the instance tree

In mCRL2, a behavior process is required for every automaton in the input, and a variable process is needed for every variable used (read or written) by two or more automata. In addition, it is allowed to have a variable process for variables that are used in one automaton only (that is, a local variable of the automaton).

All these processes must be instantiated using the parallel composition operator. For larger specifications, the naive solution of instantiating all processes together in one level fails due to having too many allowed combinations of actions for the mCRL2 tool to handle.

A different solution is to instantiate smaller groups of processes at a time, and then use these groups again in other instantiations. Instantiation happens in multiple levels in this case, leading to a tree of process instantiations. At each level, the set of allowed actions is restricted by adding action operators. This results in a large reduction of the number of possible combinations of actions that need to be explored by the mCRL2 tool. Fewer combinations of actions in turn leads to enabling larger specifications to be verified.

Which processes and groups are taken together at each level in the tree has a large impact on feasibility. The CIF to mCRL2 transformer has a default scheme, where pairs of one group and one behavior process are taken together at each level (except at the bottom, where two behavior processes are merged instead). On top of that tree, pairs of a group and a variable process are taken together.

The CIF to mCRL2 transformer does not perform analysis to decide how processes and variables should combined. In many cases this provides a working solution. For some specifications however, you may want to have more influence in the order of grouping. For this reason, the Instance tree definition option exists. It allows you to define which processes should be taken together at each level in the instantiation tree.

The current implementation has limits with respect to ordering. Automata processes must be merged first (but the number of levels and the order of combining is free), and then variables must be added one at a time (but which variable to use at each level is free).

The option expects absolute names of all automata in the specification and absolute names of all discrete variables used in two more automata, separated by white space or commas. In addition you may add the absolute names of variables used in only one automaton. For each element mentioned, a process is created in mCRL2. Variables used in one automaton that are not mentioned, become local variables of the behavior process of the automaton that uses the variable.

Processes for the mentioned CIF elements are instantiated. Sub-groups of processes are written by surrounding them with parentheses. For example:

( ( A B C ) A.x ) B.y

takes automata A, B, C together. One level higher, variable A.x is added, and finally variable B.y is added at the highest level. Another order is:

( ( ( A B ) C ) B.y ) A.x

First processes A and B are combined, then process C is added, and finally variables B.y and A.x at the top-most two levels.

Debug output

The transformer analyzes use of the variables by each automaton, and computes variable usage and availability of the variables at each level in the instantiation tree. This information is written to a file with debug output by enabling the Enable debug output option. As an example, consider the following artificial CIF specification:

event a, b, c;

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

  location p1:
    initial;
    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:
    edge b when y = 1 and P.x < 8 and P.zero = 0 goto q1;
end

This specification has two automata P and Q, and two shared variables P.x and Q.y. The ranges of the variables are important, mCRL2 considers the integer type unbounded, depending on your CIF file, without giving upper and lower bounds for the variables, you may end up in the situation that mCRL2 tries every single value of its infinite integer type, which takes a very long time!

Variable zero is not shared, only automaton Q uses it. The transformer moves it to the Q process. Normally however, you would use a constant instead of a variable.

The instance tree used in the transformation is ( ( P Q ) P.x ) Q.y. The debug output for P is:

===============================================================
Node 1.1.1.1

Variable use by behavior processes ordered by event:
    a:
        P.x  read:SOMETIMES  write:ALWAYS
    c:
        Q.y  read:ALWAYS  write:NEVER

Automaton P has one c edge, which checks the value of Q.y but it does not change its value. It has two a edges, only the a edge in location p1 reads P.x (to compute x + 1). Both edges assign a new value to P.x.

In a similar way, the node information for automaton Q is computed. The result is:

===============================================================
Node 1.1.1.2

Variable use by behavior processes ordered by event:
    a:
        Q.y  read:ALWAYS  write:NEVER
    b:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:ALWAYS  write:NEVER

The automaton only checks values rather than writing them. As you can see, variable P.x is not mentioned with event a, since there is no edge in the automaton with event a that accesses variable P.x.

The node that merges both automata, i.e. ( P Q ), has the following formation:

===============================================================
Node 1.1.1

Variable use by behavior processes ordered by event:
    a:
        P.x  read:SOMETIMES  write:ALWAYS
        Q.y  read:ALWAYS     write:NEVER
    c:
        Q.y  read:ALWAYS  write:NEVER
    b:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:ALWAYS  write:NEVER

Children:
    node 1.1.1.1
    node 1.1.1.2

Variable use by each event is simply merged. In this example there is no overlap, but that works as you would expect, SOMETIMES overrides NEVER, and ALWAYS overrides SOMETIMES.

The node for variable process for P.x only provides a variable:

===============================================================
Node 1.1.2

Available variable processes:
    P.x

The output states that variable P.x is available here.

At ( P Q ) P.x node, the merge of the variable P.x with the two automata, this results in:

===============================================================
Node 1.1

Available variable processes:
    P.x

Variable use by behavior processes ordered by event:
    a:
        P.x  read:SOMETIMES  write:ALWAYS
        Q.y  read:ALWAYS     write:NEVER
    c:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:NEVER   write:NEVER
    b:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:ALWAYS  write:NEVER

Children:
    node 1.1.1
    node 1.1.2

In this node, variable P.x is also available. The variable process does not perform events, so the event variable table of node 1.1.1 is copied. The only exception is the additional line P.x for event c. The reason for this line is that while ( P Q ) may not use P.x in combination with event c, other automata higher up in the tree may still need that variable. (In a future version of the transformer tool, it may be detected that such use never happens, and there is no need to add the line here.)

Node 1.2 is the variable process of Q.y. It looks the same as node 1.1.2, except for the name of the variable.

Finally the top-node that merges ( P Q ) P.x with Q.y, bringing everything together, looks like:

===============================================================
Node 1

Available variable processes:
    P.x
    Q.y

Variable use by behavior processes ordered by event:
    a:
        P.x  read:SOMETIMES  write:ALWAYS
        Q.y  read:ALWAYS     write:NEVER
    c:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:NEVER   write:NEVER
    b:
        Q.y  read:ALWAYS  write:NEVER
        P.x  read:ALWAYS  write:NEVER

Children:
    node 1.1
    node 1.2

The Q.y variable is now also available. The event variable table is again copied. Since all events already used variable Q.y no additional lines were added.

Output of the transformation

A variable process in mCRL2 handles shared access to a variable. For variable P.x in the above example it looks like:

act value_x, vread_x, vwrite_x, sync_x, aread_x, awrite_x : Int;

proc VarProc_x(v:Int) =
  value_x(v) . VarProc_x(v) +
  vread_x(v) . VarProc_x(v) +
  sum m:Int . ((m >= 0) && (m <= 10)) -> vwrite_x(m) . VarProc_x(m) +
  sum m:Int . ((m >= 0) && (m <= 10)) -> vread_x(v) | vwrite_x(m) . VarProc_x(m);

The name of the actions all end with the name of the variable. If the CIF specification has two or more variables with the same name, a number gets appended to make each variable unique in mCRL2.

A behavior process is generated for each automaton instance. Like the variables, the name of the automaton is used in the output. If there are name conflicts, a number is appended to make it unique. The process is the same list of edges of the original CIF automaton, with added read and write actions for synchronizing with the variable processes:

sort LocSort_P = struct loc_P_p1 | loc_P_p2;

proc BehProc_P(Locvar_P : LocSort_P) =
  sum x : Int . ((x >= 0) && (x <= 10) && (Locvar_P == loc_P_p1)) -> a | aread_x(x) | awrite_x((x + 1)) . BehProc_P(loc_P_p2) +
  sum y : Int . ((y >= 0) && (y <= 1) && (Locvar_P == loc_P_p2) && (y != 0)) -> c | aread_y(y) . BehProc_P(loc_P_p1) +
  (Locvar_P == loc_P_p2) -> a | awrite_x(1) . BehProc_P(loc_P_p1);

Locations are encoded in a struct and variable read and write actions are added as needed.

The instantiation tree is dominated by the action operators needed for synchronizing and restricting actions. The value_... actions are allowed up the to top level node, to give access to variable values in the verification. This leads to:

act a, renamed_a, c, renamed_c, b, renamed_b;

init block({aread_y, awrite_y, vread_y, vwrite_y},
     hide({sync_y},
     comm({aread_y | vread_y -> sync_y,
           awrite_y | vwrite_y -> sync_y},
     (
       block({aread_x, awrite_x, vread_x, vwrite_x},
       hide({sync_x},
       comm({aread_x | vread_x -> sync_x,
             awrite_x | vwrite_x -> sync_x},
       (
         allow({value_zero,
            a | awrite_x | aread_y,
                a | awrite_x | aread_x | aread_y,
                c | aread_y,
                b | aread_y | aread_x},
         rename({renamed_a -> a},
         block({a},
         comm({a | a -> renamed_a},
         (
           BehProc_P(loc_P_p1)
         ||
           BehProc_Q(loc_Q_q1, 0)
         )))))
       ||
         VarProc_x(0)
       ))))
     ||
       VarProc_y(1)
     ))));