Version:
[release notes]

Module 4: Modeling requirements and supervisor synthesis

In Module 3, you learned that:

  • There are two kinds of events, controllable events that a supervisor may restrict, and uncontrollable events that a supervisor may not restrict.
  • How controllable and uncontrollable events can be specified in CIF.
  • In the supervisory control loop, the plant is the uncontrolled system that indicates which events are enabled in the system, and the supervisor decides when the controllable events of the system are allowed or not allowed.
  • The different forms of a supervisor can take, such as a single automaton that represents the full controlled system behavior, extra conditions for controllable events on top of the plant behavior, or something in between.
  • How automata in CIF can be specified as being part of a plant for a supervisor.
  • The four guarantees of synthesis, namely that synthesized supervisors are safe, controllable, non-blocking and maximally permissive.
  • The controllability guarantee ensures that if a synthesized supervisor controls a plant, it only disables controllable events, but never disables any uncontrollable events if they are possible in the plant.
  • The non-blockingness guarantee ensures that if a synthesized supervisor controls a plant, none of the reachable states of the controlled system are blocking.
  • Both blocking states and states where uncontrollable events are restricted by the supervisor are called bad states, and synthesis ensures that in the controlled system they can never be reached.
  • The maximal permissiveness or minimal restrictiveness guarantee ensures that if a synthesized supervisor controls a plant, only the minimal restrictions are imposed by the supervisor to ensure the other guarantees of synthesis, such that all desired behavior is preserved.
  • From a plant model and requirements, the supervisory controller synthesis algorithm step by step removes more behavior from the controlled system's state space, computing the supervisor, to ensure the controlled system adheres to the various guarantees of synthesis.
  • In CIF, groups can be used to structure a model, making it more readable.
  • In CIF, automata and groups are together called components.
  • In CIF, component definitions, with or without parameters, can be instantiated any number of times, which is useful to reduce duplication in models, allow for reuse, ensure consistency, ease evolution and improve maintainability.
  • In CIF, imports can be used to split a model over multiple files, split large models, reuse parts of a model in another model.

A plant model contains all the system's behavior, including undesired behavior. This undesired behavior can consist of blocking behavior, which is removed by synthesis, as explained in the previous module. However, a plant may also have other undesired behavior, such as unsafe behavior. For instance, it may be possible to open two opposite water lock gates simultaneously, causing a flood.

In this module, you will learn about user-specified requirements, that indicate such undesired or unsafe situations must never occur. You will learn about the different types of user-specified requirements, their pros and cons, and how to model them in CIF. You will also learn about how synthesis ensures that the controlled system adheres to the specified requirements. And, you will synthesize your first supervisory controller. You put all this in practice, by modeling the requirements for the water lock case and synthesizing a supervisor for it.

This module is divided into the following sub-modules: