Relabel supervisors as plants

This CIF to CIF transformation relabels supervisors as plants.

Supported specifications

This transformation supports all CIF specifications.

Preprocessing

n/a

Implementation details

This CIF to CIF transformation relabels:

  • Supervisor automaton definitions as plant automaton definitions.

  • Supervisor automata as plant automata.

  • Supervisor invariants as plant invariants.

For instance, consider the following partial CIF specification:

supervisor button:
  location off:
    initial;
    marked;
    edge u_on goto on;
  location on:
    edge u_off goto off;
end

supervisor invariant actuator.c_on needs button.pushed;

It gets transformed to:

plant button:
  location off:
    initial;
    marked;
    edge u_on goto on;
  location on:
    edge u_off goto off;
end

plant invariant actuator.c_on needs button.pushed;

Renaming

n/a

Size considerations

Automata and invariants may get a different supervisory kind. This does not change the size of the specification.

Optimality

n/a

Annotations

This transformation does not process, add, or remove any annotations.