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 file in the Project Explorer tab or Package Explorer tab by left clicking on it.

    • Select additional .cif files by left clicking on them while pressing the Ctrl or Control key.

    • Make sure at least two .cif files are selected.

    • Right click one of the .cif 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 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 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.

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:

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. The merged specification never has a controller properties annotation, even if any of the input specifications has one.

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.