Monitoring

> > >

This lesson explains the concept of monitoring. It is explained using the following CIF specification:

automaton producer:
  event produce, provide_a, provide_b;

  location producing:
    initial;
    edge produce goto idle;

  location idle:
    edge provide_a goto producing;
    edge provide_b goto producing;
end

automaton detect_changeover:
  disc int count = 0;

  location start:
    initial;
    edge producer.provide_a goto a;
    edge producer.provide_b goto b;

  location a:
    edge producer.provide_b do count := count + 1 goto b;

  location b:
    edge producer.provide_a do count := count + 1 goto a;
end

The producer automaton represents a producer that can repeatedly produce a product, and provide it to either consumer 'a' (event provide_a) or consumer 'b' (event provide_b). The consumers are not modeled.

The detect_changeover automaton detects consumer changes. That is, it detects and counts how often the producer switching from providing consumer 'a' with products to providing consumer 'b' with products, and vice versa. Initially, the automaton waits for the first product to be provided. It goes to either location a or location b, depending on which consumer is provided that first product. Whenever a product is then provided to the other consumer, the count is incremented by one to account for the changeover taking place. This also switches the location to the location for the other consumer, where once again the automaton waits for a changeover.

The monitoring problem

There is a problem with the detect_changeover automaton. In its a location, it disables the provide_a event, as there is no edge for that event, and the automaton has that event in its (implicit) alphabet. This means that after a product is provided to consumer 'a', no more products can be provided to that same consumer, until the producer provides a product to the consumer 'b', and the automaton switches to the corresponding b location. However, the idea is that the producer can provide products to either consumer, at all times, as that is the way it is intended. The detect_changeover automaton currently prevents behavior that is present in the producer, while it is only meant to observe or monitor products being provided. The state space of the specification is:

The states are labeled with the first letters of the names of the current locations of the automata. Note how the i/a and i/b locations only have outgoing transitions for either the provide_a transition or the provide_b transition.

Monitoring with self loops

A simple solution is to allow the disabled events:

automaton detect_changeover:
  disc int count = 0;

  location start:
    initial;
    edge producer.provide_a goto a;
    edge producer.provide_b goto b;

  location a:
    edge producer.provide_a; // Added self loop.
    edge producer.provide_b do count := count + 1 goto b;

  location b:
    edge producer.provide_a do count := count + 1 goto a;
    edge producer.provide_b; // Added self loop.
end

The provide_a event has been added to an edge in the a location. The edge is a self loop, meaning the current location of automaton detect_changeover does not change as a result of taking the edge. This means that essentially the event is ignored by the detect_changeover automaton, as the edge also has no updates. The state space of the modified specification is:

Now, whenever the provide_a event is possible, the provide_b event is also possible, and vice versa, just as in the producer automaton. The detect_changeover automaton no longer restricts the occurrence of the events; it only monitors them.

Monitoring with monitor automata

An alternative to adding self loops, is to use a monitor automaton. A monitor automaton is an automaton that monitors or observes one or more events. The events that it monitors, are never blocked (disabled) by that automaton. For our producer/changeover example, we can turn the detect_changeover automaton into a monitor automaton for the provide_a and provide_b events:

automaton detect_changeover:
  monitor producer.provide_a, producer.provide_b; // Monitor instead of the self loops.

  disc int count = 0;

  location start:
    initial;
    edge producer.provide_a goto a;
    edge producer.provide_b goto b;

  location a:
    edge producer.provide_b do count := count + 1 goto b;

  location b:
    edge producer.provide_a do count := count + 1 goto a;
end

By default, automata don’t monitor any events. Using a monitor declaration with one or more events, turns the automaton into a monitor automaton for those events. For the producer/changeover example, the behavior with the monitor automaton is exactly identical to the behavior of the specification with the self loops.

By omitting the events from the monitor declaration, an automaton monitors all events of its alphabet:

monitor; // Monitor all events in the alphabet of the automaton.

For the producer/changeover, which has only the provide_a and provide_b events in its alphabet, this would result in the same behavior as for the automaton that monitors the two events explicitly.

Using a monitor automaton instead of self loops has several advantages. A monitor declaration has to be provided only once, while self loops often have to be added to several locations. Furthermore, if the automaton is changed, it may be necessary to add or remove self loops, while the monitor declaration can most often be kept as is.