Automaton kinds

For supervisory controller synthesis, different kinds of automata are treated in different ways. Regular automata, as used in the language tutorial so far, are specified using only the automaton keyword. Regular automata do not specify a kind for supervisory controller synthesis, and are therefore sometimes also referred to as kindless automata. Synthesis tools typically require knowledge about the purpose of each of the automata, and therefore don’t support regular automata.

For supervisory controller synthesis, three different kinds of automata are available: plant automata, requirement automata, and supervisor automata. These automata are identical to regular automata, except for the keywords used to declare their intent. The automaton keyword is preceded or replaced by the plant, requirement, or supervisor keyword respectively.

For instance, the following are two alternative ways to model the same plant automaton:

// Plant automaton, long form.
plant automaton lamp:
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end

// Plant automaton, short form.
plant lamp:
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on goto on;

  location on:
    edge turn_off goto off;
end