Eliminate channels

> > > >

This CIF to CIF transformation eliminates channels, introducing a regular/non-channel event per send/receive combination.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

Component definitions and component instantiations are not supported.
Specifications with SVG input mappings that may map to a channel are currently not supported.

Preprocessing

To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations if applicable:

Implementation details

Each channel is transformed into as many events as there are pairs of senders and receivers for the event. So, in case a channel has m send options and n receive options, m * n new events are created to replace it.

For instance, consider the following CIF specification:

event int chan;

automaton sender1:
  location first:
    initial;
    edge chan!1 goto second;

  location second:
    edge chan!2 goto first;
end

automaton sender2:
  location first:
    initial;
    edge chan!3 goto second;

  location second:
    edge chan!4 goto first;
end

automaton receiver1:
  location:
    initial;
    edge chan?;
end

automaton receiver2:
  location:
    initial;
    edge chan?;
end

automaton synchronizer:
  location:
    initial;
    edge chan;
end

This transformation transforms it into a new specification equivalent to the following:

event chan_1;
event chan_2;
event chan_3;
event chan_4;
event chan_5;
event chan_6;
event chan_7;
event chan_8;

automaton sender1:
  location first:
    initial;
    edge chan_1, chan_2 goto second;

  location second:
    edge chan_3, chan_4 goto first;
end

automaton sender2:
  location first:
    initial;
    edge chan_5, chan_6 goto second;

  location second:
    edge chan_7, chan_8 goto first;
end

automaton receiver1:
  location:
    initial;
    edge chan_1;
    edge chan_3;
    edge chan_5;
    edge chan_7;
end

automaton receiver2:
  location:
    initial;
    edge chan_2;
    edge chan_4;
    edge chan_6;
    edge chan_8;
end

automaton synchronizer:
  location:
    initial;
    edge chan_1, chan_2, chan_3, chan_4,
         chan_5, chan_6, chan_7, chan_8;
end

There are two send automata for channel chan, each with two send options, making for four send options. There are two receive automata, each with one receive option, making for two receive options. There are thus 4 * 2 = 8 send/receive combinations, and then 8 replacement events are created.

In the synchronizing automaton, you see the channel reference on the edge is replaced by all 8 replacement events. In the sender and receiver automata, you see the channel references are replaced only by the relevant replacement events for which the send or receive option participates.

In general, if state/event exclusion invariants, explicit alphabets of automata, monitors of automata, print declaration for declarations, and edge events on edges of automata, refer to the channel, then these references are replaced by references to the new replacement events. For a state/event exclusion invariant that applies to a channel, the invariant is cloned as many times as there are replacement events for the channel.

If a channel has no senders or no receivers, it is removed entirely, including all references to it. All state/event exclusion invariants for the channel are then removed entirely. If an explicit monitor declaration of an automaton becomes empty due to removing event references from it, the monitor declaration is removed to prevent the automaton from monitoring all events in its alphabet. If an implicit monitor declaration no longer has an effect when an automaton’s alphabet becomes empty, the monitor declaration is removed to prevent warnings about monitoring an empty alphabet. Similarly, if the for declarations of a print declaration become empty, the print declaration is removed to prevent the default for declarations from taking effect. And if all events on an edge are removed, the edge is removed to prevent it from becoming a tau edge.

For edges with a receive, all occurrences of the received value expression (?) in updates, are replaced by the send value expression of the relevant send option of the corresponding send/receive combination. Edges with multiple receives on them are first split, so that each edge has a single receive on it. For each edge with a receive, the edge is furthermore duplicated for each send/receive edge event combination that applies to it.

Renaming

This transformation creates new events to replace channels. If the name of a new event is already in use, the new event is given a different name to prevent conflicts. In case of such conflicts, a warning is printed to the console.

Size considerations

In case a channel has m send options and n receive options, m * n new events are created to replace it. This may result in a blow-up of the size of the specification, as there may be a quadratic number of events for each channel, given the number of send and receive options they have.

In places where the channel was previously referred, now multiple events may need to be referred.

In some cases, elements of the specification may be duplicated, once per replacement event. For instance, a state/event exclusion with a channel event is duplicated m * n times.

If for a channel there are no send options or no receive options, elements of the specification may get removed, reducing the size of the specification.

Optimality

If a channel is superflously referred multiple times in for instance the alphabet or monitor specification of an automaton, all references to the channel are replaced once by the replacement events, removing the redundancy.

Annotations

This transformation does not process or add any specific annotations. The annotations of channels are removed. If any other elements of the specification get removed, their annotations are also removed.