Version:
[release notes]

Module 3: Supervisory control and plant models

In Module 2, you learned that:

  • States are reachable if there is a way to get there, from an initial state, by a sequence of zero or more transitions.
  • A deadlock state is a state where no transitions are possible, and thus no further behavior is possible.
  • A system is non-blocking if from every reachable state, it is possible to reach a marked state.
  • Any non-marked state that is reachable, that does not have a sequence of transitions to a marked state, is called a blocking state.
  • If from a non-marked state further transitions are possible, but a marked state can never be reached, the state has a livelock.
  • Non-determinism, as it is defined in this course and also generally in CIF, is the presence of multiple possible transitions for the same event from a single state.
  • Events synchronize, meaning that if multiple automata have an event in their alphabet, then a transition for that event can only occur if these automata can all participate, and they all take an edge at the same time.
  • If an automaton can take an edge for an event, it is said to enable the event.
  • If an automaton can not take any edge for an event, and this event is in its alphabet, then it is said to block or disable the event.
  • In general, it is best to place events as close as possible to where they are used (initiated, executed, and so on).
  • A discrete variable must be declared in an automaton, and only that automaton can change its value through updates on edges (local write), while any automaton can access its value (global read).
  • To refer from one automaton to a declaration from another automaton, such as an event, constant, variable or location, the name of that declaration needs to be prefixed with the name of the automaton that declares it and a period.
  • A state space consisting of all reachable states and the transitions between them, with each state consisting of a current location for each automaton and a current value for each variable, can be computed step-by-step in a systematic way.
  • A state space can be automatically computed for a CIF model using the CIF explorer.
  • A CIF model can be visualized using the CIF to yEd transformer.
  • The CIF event-based toolset can be used to analyze and manipulate CIF models, such as to perform a trim check.
  • Constants hold a fixed value, while algebraic variables hold a value that is computed from other values, such as those of constants and discrete variables.

In this module, you will dive deeper into supervisory control theory and supervisory controller synthesis. You learn among others the difference between controllable and uncontrollable events, and some of the properties that a proper supervisors adheres to, namely that it is safe, controllable, non-blocking and maximally permissive. And you find out how how synthesis prevents blocking behavior. You apply these concepts to simple problems. You expand your knowledge and experience in modeling plant models using CIF. You apply it to model the plants of the water lock case.

This module is divided into the following sub-modules: