Combining channel communication with event synchronization

Consider again the producer/consumer example with two producers and two consumers, from a previous lesson:

event int provide;

automaton producer1:
  disc int nr = 0;

  location:
    initial;
    edge provide!nr do nr := nr + 1;
end

automaton producer2:
  disc int nr = 0;

  location:
    initial;
    edge provide!nr do nr := nr + 1;
end

automaton consumer1:
  disc list int nrs;

  location:
    initial;
    edge provide? do nrs := nrs + [?];
end

automaton consumer2:
  disc list int nrs;

  location:
    initial;
    edge provide? do nrs := nrs + [?];
end

Now assume we want to restrict communication to allow at most five products in total to be provided to the consumers. We could adapt both producers, as follows:

automaton producer1:
  disc int nr = 0;

  location:
    initial;
    edge provide!nr when nr + producer2.nr < 5 do nr := nr + 1;
end

automaton producer2:
  disc int nr = 0;

  location:
    initial;
    edge provide!nr when producer1.nr + nr < 5  do nr := nr + 1;
end

Each producer gets an additional guard condition whether it may provide a product to one of the consumers. If the total number of products provided by both providers does not exceed five, they may still provide a product. Having to adapt both producers is less than ideal.

As an alternative solution, we can add an additional automaton, instead of adapting the producers:

automaton controller:
  disc int cnt = 0;

  location:
    initial;
    edge provide when cnt < 5 do cnt := cnt + 1;
end

This controller automaton (together with the original producer automata) keeps track of the number of products provided to consumers, by counting them in variable cnt. It only allows the provide event when less than five products have been provided. If five or more products have been provided, it disables the provide event.

In the controller automaton, the provide channel is used as an event rather than a channel. When one of the producers and one of the consumers together perform a channel communication, the controller automaton that has the provide event in its alphabet, must synchronize with it. This allows the controller to impose additional restrictions on the channel communication, allowing or forbidding it in certain cases. The controller is added as a separate process, which improves scalability.

In general, every automaton may either send over a channel, receive over a channel, or synchronize with a channel. An automaton may not take on more than one of these roles, for a single event. It may however send over one channel, receive over another channel, and synchronize with yet another one.

Every event transition for a channel requires exactly one automaton that participates as sender, and exactly one automaton that participates as receiver. Furthermore, all automata that have the channel in their alphabet, must additionally participate as well, by synchronizing together with the sender and receiver. Automata that send or receive over a channel, do not have that channel in their alphabet. Only automata that synchronize with an event or channel have that event or channel in their alphabet.

Automata that synchronize over a channel can be used to further restrict the allowed channel communications, as shown in the above example. It is however also possible for the additional synchronizing automata to monitor (observe) the channel communication.