The tau event

Events allow for synchronization, allowing for interaction between automata based on events. If however an automaton has an edge that performs some internal processing, the event may not always be relevant. Consider for instance the following CIF specification:

automaton machine1:
  event process, provide;
  disc int id = 0;

  location processing:
    initial;
    edge process do id := id + 1 goto providing;

  location providing:
    edge provide goto processing;
end

automaton machine2:
  location:
    initial;
    edge machine1.provide;
end

The specification models two machines. Products enter the first machine, which processes them (event process) and assigns them an id. The machine them provides (event provide) them to the second machine. The second machine currently just accepts the products provided by the first machine, but would in reality likely perform its own processing as well. The state space of the specification is as follows:

tau event state space1

The states are labeled with the names of the current locations of automaton machine1. Since automaton machine2 has only a single location, its current location does not change, and it is therefore not included in the state names.

The provide event synchronizes over both automata, while the process event is local to the first machine. The process event is not essential, and could be left out:

automaton machine1:
  event provide;                         // No more 'process' event.
  disc int id = 0;

  location processing:
    initial;
    edge do id := id + 1 goto providing; // No more event on the edge.

  location providing:
    edge provide goto processing;
end

automaton machine2:
  location:
    initial;
    edge machine1.provide;
end

By omitting the event from an edge, the tau is used for that edge. The tau event is an event that is implicitly always present without declaring it. The state space of this modified specification is:

tau event state space2

The tau event does not synchronize. You can think of this as each automaton having its own local tau event, and since then they are different events, they do not synchronize. If multiple automata can perform a transition for an edge with the tau event, this leads to potential transitions for each of those edges. Since they are all labeled with the tau event, it is impossible to distinguish them solely based on their label. This is a form of non-determinism.

Using the tau events saves having to declare a local event, and also saves having to put that event on the edge. It thus leads to smaller specifications. However, as explained above, if tau is used on multiple edges of multiple automata, the different tau transitions can no longer be distinguished from each other in the state space. The use of the tau event is thus always a trade-off.

It is also possible to explicitly use the tau event:

edge tau goto ...;

The tau event can thus be used instead of 'regular' events, and may even be combined with 'regular' events on the same edge:

edge provide, tau goto ...;

Omitting the events from an edge defaults to a single tau event, as shown in one of the examples above.