CIF 3

Location/variable duality (2/2)ΒΆ

The lesson that introduces automata, used an example of a lamp:

automaton lamp:
  event turn_on, turn_off;

  location on:
    initial;
    edge turn_off goto off;

  location off:
    edge turn_on goto on;
end

The automaton uses two locations to keep track of the current state of the lamp. Instead of two locations, it is also possible to use a variable:

automaton lamp:
  event turn_on, turn_off;

  disc bool on = true;

  location:
    initial;
    edge turn_on  when not on do on := true;
    edge turn_off when     on do on := false;
end

This alternate automaton uses a single variable named on. The data type of the variable is bool, which means that the variable can only have one of two possible values: true or false. If variable on has value true, the lamp is on, and if it has value false it is off. Initially, the lamp is on, as the initial value of the variable is true. The automaton has only one location, with two edges. The first edge indicates that the lamp can be turned on (event turn_on), only when it is not currently on (guard not on), and then afterwards is on (variable on becomes true). Similarly, the second edge indicates that the lamp can be turned off, only when it is currently on, and then afterwards is on.

Both models represent a lamp that is initially on, and can be turned off, on, off again, on again, etc, repeating the behavior forever. Which approach is best depends on your preference, and on the rest of the model. It is however also possible to use both locations and a variable:

automaton lamp:
  event turn_on, turn_off;

  disc bool on2 = true;

  location on:
    initial;
    edge turn_off do on2 := false goto off;

  location off:
    edge turn_on  do on2 := true  goto on;
end

This automaton has the same behavior as the previous two automata. Variable on is renamed to on2, as a variable can not have the same name as a location of that same automaton.

While it is possible to model a lamp like this, this automaton duplicates the information about whether the lamp is on or off. This makes the automaton larger and more complex than it needs to be. In general, it is usually better to choose either a variable, or multiple locations, to express something, and not both. In several future lessons, we’ll see that combining multiple locations with variables is useful, but not to express the same thing. Furthermore, an other future lesson explains how to use a location as a variable.