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.