## CIF merger

The CIF merger can be used to merge two or more CIF specifications into a single CIF specification. The result of the merger is essentially the parallel composition of the input specifications. Unlike the CIF explorer and Event-based synchronous product tools however, the parallel composition is not unfolded into a state space.

It can for instance be useful to merge a synthesized supervisor with a timed or hybrid plant, to validate the supervisor against that more detailed plant, using interactive simulation and visualization on the merged specification.

The specifications that are being merged can share events and variables, making it possible to have interaction between the merged specifications.

### Starting the transformation

The merger can be started in the following ways:

- Use the Eclipse IDE to merge multiple files:

  - Select a `.cif` or `.cifx` file in the Project Explorer tab or Package Explorer tab by left clicking on it.

  - Select additional `.cif` and/or `.cifx` files by left clicking on them while pressing the `Ctrl` or `Control` key.

  - Make sure at least two `.cif` and/or `.cifx` files are selected.

  - Right click one of the `.cif` or `.cifx` files and choose Merge CIF specifications….

- Use the Eclipse IDE to merge a single file with itself (allowed, but practically not that useful):

  - Right click a `.cif` or `.cifx` file in the Project Explorer tab or Package Explorer tab and choose CIF miscellaneous tools Merge CIF specifications….

  - Right click an open text editor for a `.cif` or `.cifx` file and choose CIF miscellaneous tools Merge CIF specifications….

- Use the `cifmerge` tool in a ToolDef script. See the scripting documentation and tools overview page for details.

- Use the `cifmerge` command line tool.

### Options

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

- Input files: The absolute or relative local file system path to the input CIF specifications. These are the files to merge.

- Output file: The absolute or relative local file system path to the merged/output CIF specification. If not specified, the output file defaults to `merged.cif`. If the merger is executed via the Eclipse GUI, the output file, if specified as a relative path (or just a file name), is resolved relative to the directory that contains the first input file.

- Merged specification is partial: Specifies whether to make the merged specification a partial specification. By default, the merged specification is a non-partial specification. The option can be enabled to make the merged specification a partial specification.

- Remove controller properties annotations: Enable this option to remove the controller properties annotations of the input specifications, so that the merged specification has no such annotations. Disable the option to keep the controller properties annotations of the input specifications and merge them into the merged specification. By default, the option is enabled, as there is no guarantee that the controller properties annotations will apply to the merged specification.

  | Disable this option with care!

  If you are sure the controller properties annotations still apply after the merge, you can disable the option to preserve the annotations. Note that if the option is disabled, and multiple input specifications have a controller properties annotation, then the merged specification will be invalid (see the merge compatibility section for more information).

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

- Eliminate component definition/instantiation

- Push SVG file declarations into other CIF/SVG declarations

- Push print file declarations into print declarations

If only one input file is provided to the CIF merger, essentially that single input file is preprocessed and written as output, without any merging taking place.

### Example

Consider the following supervisor:

    group button:
      uncontrollable u_pushed, u_released;
    end

    group lamp:
      controllable c_on, c_off;
    end

    group timer:
      controllable c_start;
      uncontrollable u_timeout;
    end

    supervisor automaton timed_lamp:
      location s0:
        initial;
        edge button.u_pushed goto s1;
        edge button.u_released;

      location s1:
        edge lamp.c_on goto s2;
        edge button.u_pushed, button.u_released;

      location s2:
        edge timer.c_start goto s3;
        edge button.u_pushed, button.u_released;

      location s3:
        edge timer.u_timeout goto s4;
        edge button.u_pushed, button.u_released;

      location s4:
        edge lamp.c_off goto s0;
        edge button.u_pushed, button.u_released;
    end

and the following timed plant:

    plant automaton button:
      uncontrollable u_pushed, u_released;

      location released:
        initial;
        edge u_pushed goto pushed;

      location pushed:
        edge u_released goto released;
    end

    plant automaton lamp:
      controllable c_on, c_off;

      location off:
        initial;
        edge c_on goto on;

      location on:
        edge c_off goto off;
    end

    plant automaton timer:
      controllable c_start;
      uncontrollable u_timeout;

      cont t der 1.0;

      location idle:
        initial;
        edge c_start do t := 0.0 goto running;

      location running:
        edge u_timeout when t >= 2.0 goto idle;
    end

Merging these two specifications results in the following merged specification:

    plant automaton button:
      uncontrollable u_pushed;
      uncontrollable u_released;
      location released:
        initial;
        edge u_pushed goto pushed;
      location pushed:
        edge u_released goto released;
    end
    plant automaton lamp:
      controllable c_on;
      controllable c_off;
      location off:
        initial;
        edge c_on goto on;
      location on:
        edge c_off goto off;
    end
    plant automaton timer:
      controllable c_start;
      uncontrollable u_timeout;
      cont t der 1.0;
      location idle:
        initial;
        edge c_start do t := 0.0 goto running;
      location running:
        edge u_timeout when t >= 2.0 goto idle;
    end
    supervisor automaton timed_lamp:
      location s0:
        initial;
        edge button.u_pushed goto s1;
        edge button.u_released;
      location s1:
        edge lamp.c_on goto s2;
        edge button.u_pushed, button.u_released;
      location s2:
        edge timer.c_start goto s3;
        edge button.u_pushed, button.u_released;
      location s3:
        edge timer.u_timeout goto s4;
        edge button.u_pushed, button.u_released;
      location s4:
        edge lamp.c_off goto s0;
        edge button.u_pushed, button.u_released;
    end

The supervisor specification contains three skeletons: groups that only contain event declarations, and have no behavior. The skeletons represent the plants of the system, which are controlled by the supervisor. The supervisor specification also contains a supervisor automaton, which waits for the button to be pushed, then turns on the lamp and start the timer, waits for the timer to time out, turns the lamp back off, and keeps repeating this behavior. Pushing or releasing the button during the cycle has no effect.

The timed specification contains the same plants, with the same events, but here the plants are actual automata with behavior, instead of just skeleton groups. For the button and lamp, the events occur in alternating sequences. The timer has a clock that ensures that the timeout happens two time units after the timer is started.

Since both specifications contain the same events (based on their absolute names), these events are merged together. This ensures that uses of those events become linked (or coupled), and all refer to the single merged event in the merged specification. This means that the events used in the supervisor are the same events as used the timed plant. This also means that they synchronize, and the supervisor thus controls the timed plants.

### Shared events and variables

The example above shows how shared events can be used to link (or couple) multiple specifications through merging.

Similarly to the way events can be merged, it is possible to merge input variables with other variables, as long as the types are compatible. That is, an input variable can be merged with another input variable, a discrete variable, a continuous variable, an algebraic variable, a constant, or a location. The input variable is then a sort of skeleton definition that is merged with an actual definition (for instance an algebraic variable), which provides the value(s).

There are thus two ways for merged specifications to become linked (or coupled): by means of shared events and by means of shared variables (including constants).

For further details and restrictions, see the Merge compatibility section.

### Merge compatibility

In general, objects (components, declarations, etc) that only occur in one of the specifications being merged, are simply copied to the merged specification. If in two (or more) specifications objects with the same absolute name are present, they need to be merged. Not all objects can be merged with all other objects, i.e. not all objects are merge compatible. The following table gives an overview of what can be merged:

Merge with | Group | Automaton | Event | Input var | Discrete var | Continuous var | Algebraic var | Constant | Location | Type declaration | Enumeration | Enumeration literal
--- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ---
Group | yes | yes | no | no | no | no | no | no | no | no | no | no
Automaton | yes | no | no | no | no | no | no | no | no | no | no | no
Event | no | no | yes | no | no | no | no | no | no | no | no | no
Input var | no | no | no | yes | yes | yes | yes | yes | yes | no | no | no
Discrete var | no | no | no | yes | no | no | no | no | no | no | no | no
Continuous var | no | no | no | yes | no | no | no | no | no | no | no | no
Algebraic var | no | no | no | yes | no | no | no | no | no | no | no | no
Constant | no | no | no | yes | no | no | no | yes | no | no | no | no
Location | no | no | no | yes | no | no | no | no | no | no | no | no
Type declaration | no | no | no | no | no | no | no | no | no | yes | yes | no
Enumeration | no | no | no | no | no | no | no | no | no | yes | yes | no
Enumeration literal | no | no | no | no | no | no | no | no | no | no | no | yes

For components (i.e. groups and automata) that are present in more than one specification, the contents are recursively merged into a single component. The contents of components consists not only of their declarations (such as events) and their sub-components (for groups), but also of their invariants, initialization predicates, marker predicates, equations, locations (for automata), etc.

As the button/lamp example above shows, automata can be merged with groups (often acting as skeletons), resulting in an automaton with the contents of the group merged into it. Since automata can’t contain sub-components and user-defined functions, groups with sub-components and/or user-defined functions can not be merged with automata.

Groups can also be merged with other groups. Automata however can not be merged with other automata, as that may lead to the merge of conflicting behavioral specifications.

Events can be merged with other events. Each event must then either be a channel in all of the specifications in which it occurs, or in none of them. If it is a channel, the data type must be exactly the same in all specifications in which it is declared. Events that have different controllability in different specifications, can also not be merged.

Constants can be merged with other constants. However, the constants must then have the exact same type and value in all the specifications in which they occur. This restriction prevents the merge of conflicting values. Due to this restriction, constants that have a type of which the values can not be compared for equality (e.g. function types), are not supported (can not be merged).

As mentioned in the Shared events and variables section, an input variable can be merged with another input variable, discrete variable, continuous variable, algebraic variable, constant, or location. Input variables can only be merged with other objects that have the exact same type.

A location can be merged with an input variable that has a boolean type. The input variable is then a placeholder for the location, indicating whether the location is the current location of its automaton.

It is not allowed to merge two algebraic variables, two discrete variables, or two continuous variables, as that may lead to the merge of conflicting values.

In general, only one of the specifications defines the variable as a concrete variable that defines a value (e.g. as a discrete, continuous, or algebraic variable). All the other specifications that have that same variable must declare it as an input variable (essentially a placeholder). It is however allowed to merge two or more constants with the same type and the same value.

Type declarations can be merged with other type declarations, as long as they have the exact same type.

Enumerations can be merged with other enumerations, as long as they are compatible. Two enumerations are compatible if they have the same number of literals, with the exact same names, in the same order.

Enumeration literals can only be merged as the result of the enumerations of which they are a part being merged. Merging two literals from different enumerations (which then have different names) is not supported.

Type declarations and enumerations can be merged, as long as the type of the type declaration is compatible with the enumeration.

Invariants can never be merged with other objects of the same name.

User-defined functions can never be merged with other objects of the same name.

Specifications are treated as groups.

By default, the merged specification never has a controller properties annotation, even if an input specification has one. If the Remove controller properties annotations option is disabled, the controller properties annotations of the input specifications are preserved and merged into the merged specification. Make sure to only use this option if you are sure that the information captured in such annotations is preserved in the merged specification! If the option is disabled, and multiple input specifications have a controller properties annotation, then the merged specification will have multiple such annotations. This is not allowed and thus the merge will fail. If you disable the option, make sure only one of the input specifications has a controller properties annotation.

By default, the merged specification is a non-partial specification. The Merged specification is partial option can be enabled to make the merged specification a partial specification.

### Merge problems

Even when two or more CIF specifications are merge compatible, as described above, the resulting merged CIF specification can still be invalid. In such cases, merging fails. For instance, consider the following two CIF specifications:

    input int x;
    alg int y = x;

    alg int x = y;
    input int y;

Merging them would result in:

    alg int x = y;
    alg int y = x;

But this merged specification is invalid, as `x` is defined in terms of `y`, which is defined in terms of `x`, leading to a loop (definition/use cycle).

A second example of merge problems is two CIF specifications that have SVG output mappings for the same SVG element id and attribute, for the same SVG image file. In the individual CIF specifications there are no duplicate output mappings, but in the merged specification there are.

A third example of merge problems is a specification that has an SVG input mapping for an input variable that is merged with a non-input variable. In the merged specification, the SVG input mapping updates a non-input variable, which is not allowed.

The merged specification is also checked for any problems with annotations, as annotations may be on different objects after merging, and not all annotations are supported for all objects. An example of this is merging multiple specifications with a controller properties annotation, provided the option to remove such annotations is disabled; see for more information the section on merge compatibility.