Version:
v7.0-M1
[release notes]

# Module 4.5: Performing synthesis with CIF

CIF features multiple synthesis tools, that can automatically synthesize a proper supervisor from a CIF model with plants and requirements. In this course, we only CIF's data-based synthesis tool, which supports variables, can deal with large and complex models, and so on.

To use CIF's data-based synthesis tool within the ESCET IDE, right click any CIF model file in the Project Explorer and then select CIF synthesis tools and Apply data-based synthesis.... To accept the default settings and start synthesis, click OK.

After synthesis completes, you get a new file that has the same name as the input file, but with a name that ends in `.ctrlsys.cif`. This new file contains the controlled system, the plant together with the supervisor:

If the synthesis algorithm has to restrict so much of the behavior of the uncontrolled system that no initial state remains, the controlled system becomes empty. The synthesis tool then ends with an empty supervisor error, and no output CIF file is created:

If a supervisor can be computed, the output CIF file contains the original plant automata, the plantified requirement automata (rebranded as supervisor automata) and the requirement invariants (rebranded as supervisor invariants). It also contains an additional supervisor automaton named `sup`, with a self-loop for each controllable event in the alphabet of the controlled system. These self-loops indicate the extra conditions that must be enforced to ensure a proper controlled system. The extra supervisor automaton synchronizes with the plant and the rebranded requirements, imposing its additional restrictions.

## Example

As an example, consider the following CIF model:

                                plant p:
                                    controllable c_a, c_b, c_c;
                                    uncontrollable u_d, u_e;

                                    location v:
                                        initial;
                                        marked;
                                        edge c_a goto w;

                                    location w:
                                        edge c_b goto v;
                                        edge c_c goto x;

                                    location x:
                                        edge c_c goto y;

                                    location y:
                                        edge u_d goto z;

                                    location z:
                                        edge u_e goto v;
                                end

                                requirement not p.z;

The requirement forbids plant `p` from being in its `z` location. Since this location is reachable by uncontrollable event `u_d` from location `y`, synthesis will also mark location `y` as bad. To prevent reaching location `y`, controllable event `c_c` is disabled from location `x`. Since then location `x` is a blocking location, controllable event `c_c` is also disabled from location `w`. Controllable event `c_c` is thus disabled in all locations where it is possible in the plant. The synthesized supervisor will look something like this:

                                plant automaton p:
                                    controllable c_a;
                                    controllable c_b;
                                    controllable c_c;
                                    uncontrollable u_d;
                                    uncontrollable u_e;

                                    location v:
                                        initial;
                                        marked;
                                        edge c_a goto w;

                                    location w:
                                        edge c_b goto v;
                                        edge c_c goto x;

                                    location x:
                                        edge c_c goto y;

                                    location y:
                                        edge u_d goto z;

                                    location z:
                                        edge u_e goto v;
                                end

                                supervisor automaton sup:
                                    alphabet p.c_a, p.c_b, p.c_c;

                                    location:
                                        initial;
                                        marked;
                                        edge p.c_a when true;
                                        edge p.c_b when true;
                                        edge p.c_c when false;
                                end

                                supervisor invariant not p.z;

Controllable events `c_a` and `c_b` are not restricted by the supervisor. But, the supervisor thus completely disables event `c_c`.