Modeling the plant

After modeling the events, the plant needs to be modeled. It represents the uncontrolled system, the system 'as is' without the controller.

Typically, for low-level controllers, start with a plant automaton per sensor and actuator. For the common case of digital sensors and actuators, model the automata with two locations, one where the sensor or actuator is off, and one where it is on. Which location should be the initial location depends on the specific sensor or actuator. Digital sensors can go on and off, and as such have two associated uncontrollable events. Similarly, digital actuators can be turned on or off, and have two associated controllable events.

Here are some examples of typical plant automata for low-level sensors and actuators:

plant Button:
  uncontrollable u_pushed, u_released;

  location Released:
    initial; marked;
    edge u_pushed goto Pushed;

  location Pushed:
    edge u_released goto Released;
end

plant Lamp:
  controllable c_on, c_off;

  location Off:
    initial; marked;
    edge c_on goto On;

  location On:
    edge c_off goto Off;
end

The events that belong to a specific sensor or actuator are typically placed within the corresponding automaton. Other events are often placed outside the automata.

See a later step for how to deal with marking. The CIF language tutorial has lessons on using variables, guards and updates.

The next step in the process to apply synthesis-based engineering in practice is to model plant relations.