//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[lang-tut-synthesis-intro]]
== Supervisory controller synthesis

indexterm:[supervisory controller synthesis]
Supervisory controller synthesis (or supervisor synthesis, or just synthesis) is a generative technique, where one derives a supervisory controller from a collection of plants and requirements.
Synthesis is the main ingredient of the <<sbe-chapter-index,synthesis-based engineering>> approach to develop supervisory controllers.
Synthesis allows to focus on the _what_, i.e. which requirements should hold, rather than on the _how_, i.e. how to implement this in a controller.

indexterm:[plant]
indexterm:[requirement]
indexterm:[supervisor]

[[lang-tut-synthesis-plant-req-sup]]
The _plants_ describe capabilities or behavior of a physical system 'as is', without any integrated control.
They represent the available behavior of the uncontrolled system.
_Requirements_ model (a part of) the functions a system is supposed to perform.
They represents behavior that is allowed in the controlled system, or more precisely, they specify the behavior that is not allowed in the controlled system.
In other words, requirements restrict the behavior of the plants, to ensure that only the desired behavior remains.
The goal of supervisory controller synthesis is to compute a supervisory controller (or _supervisor_) that enforces the requirements, assuming the behavior of the plants, additionally preventing deadlock and livelock, and without restricting the system any further than is required.

CIF has several features that are used solely of modeling systems for the purpose of supervisory controller synthesis.
These concepts are explained in upcoming lessons:

* <<lang-tut-synthesis-autkind>>
* <<lang-tut-synthesis-invkind>>
* <<lang-tut-synthesis-evtctrl>>
* <<lang-tut-synthesis-marked>>
* <<lang-tut-annotations-reachability-requirement>> (as part of the 'annotations' lessons category)

When a model is not used for supervisory controller synthesis, e.g. for simulation, these concepts are usually ignored.

For an example of how these concepts can be used for modeling of a concrete example, see the <<sbe-in-practice-example,synthesis-based engineering in practice example>> section.
