CIF 3

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.

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 or Package Explorer 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 3 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 or Package Explorer and choose CIF miscellaneous tools ‣ Merge CIF 3 specifications....
    • Right click an open text editor for a .cif file and choose CIF miscellaneous tools ‣ Merge CIF 3 specifications....
  • Use the cif3merge tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3merge 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 3 specifications. These are the files to merge.
  • Output file: The absolute or relative local file system path to the merged/output CIF 3 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 3 specifications that can be transformed:

If only one input file is provided to the CIF 3 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 defines the value.

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.

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

Invariants

Merging a group with an automaton, may change the supervisory kinds of the invariants of the group. For instance, consider the following CIF specifications:

group x:
  input int y;
  invariant y = 1;
end
plant automaton x:
  disc int y;
end

When merged, this leads to the following CIF specification:

plant automaton x:
  disc int y;
  invariant y = 1;
end

In the original group x, the invariant did not have a supervisory kind. After merging, the invariant still does not specify a supervisory kind. However, since it is now specified in an automaton x of kind plant, the invariant implicitly becomes a plant invariant as well.

When an invariant gets an implicit supervisory kind as a result of merging, the merge tool prints a warning to the console.

To get rid of the warning, the invariant in group x can be declared explicitly as being a plant invariant. The supervisory kind then matches the supervisory kind of automaton x. When the group and automaton are merged, the invariant keeps its explicit supervisory plant kind. The merge result is thus the same as the earlier merge result, as in both cases the invariant in the merged specification is interpreted as a print invariant. However, in this last case, no warning is printed to the console.

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

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