Using locations as variables

> > >

Consider the following CIF specification:

automaton machine1:
  event start1, done1, reset1;
  disc bool claimed = false;

  location idle:
    initial;
    edge start1 when not machine2.claimed do claimed := true goto processing;

  location processing:
    edge done1 do claimed := false goto cool_down;

  location cool_down:
    edge reset1 goto idle;
end

automaton machine2:
  event start2, done2, reset2;
  disc bool claimed = false;

  location idle:
    initial;
    edge start1 when not machine1.claimed do claimed := true goto processing;

  location processing:
    edge done1 do claimed := false goto cool_down;

  location cool_down:
    edge reset1 goto idle;
end

This specification models two machines, which produce products. The machines share a common resource, which may only be used by at most one of them, at any time (see mutual exclusion). Initially, the machines are idle. Then, they warm themselves up. Once they start processing, they set their boolean variable claimed to true to indicate that they claimed the shared resource. After processing, the machines release the resource, by setting claimed to false. They finish their processing cycle by cooling down, before starting the cycle for the next product. To ensure that a machine can not claim the resource if the other machine has already claimed it, the edges going to the processing locations have a guard that states that it is only allowed to claim the resource and start processing, if the other machine has not already claimed the resource. The state space of this specification is:

The states are labeled with the first letters of the names of the current locations of the automata.

The specification can alternatively be modeled as follows:

automaton machine1:
  event start1, done1, reset1;

  location idle:
    initial;
    edge start1 when not machine2.processing goto processing;

  location processing:
    edge done1 cool_down;

  location cool_down:
    edge reset1 goto idle;
end

automaton machine2:
  event start2, done2, reset2;

  location idle:
    initial;
    edge start1 when not machine1.processing goto processing;

  location processing:
    edge done1 cool_down;

  location cool_down:
    edge reset1 goto idle;
end

The claimed variables and corresponding updates have been removed, and the guards no longer use those variables. Instead, the edge for the start1 event now refers to the processing location of automaton machine2. The guard states that the first machine can perform the start1 event, only if the second machine is not currently in its processing location. In other words, the guard states that the first machine can start processing as long as the second machine is not currently busy processing (and thus using the shared resource).

The processing location of automaton machine2 is used as a boolean variable. Using the location as a variable saves having to declare another variable (claimed) that essentially holds the same information, and needs to be explicitly updated (on two separate edges) to the correct value.