Resulting supervisor
If the supervisor has to restrict so much of the behavior of the uncontrolled system that no initial state remains, the controlled system becomes empty. The data-based synthesis algorithm then ends with an empty supervisor error, and no output CIF file is created.
If an initial state remains after synthesis, an output CIF file is created. The contents is the controlled system. The controlled system is obtained by taking the input specification, and modifying it. The requirement automata are changed to supervisor automata. Some or all of the requirement invariants may be removed, depending on the simplifications that are applied. The remaining requirement invariants are changed to supervisor invariants. An additional external supervisor automaton is added. Also, depending on the simplifications that are applied, the requirement automata may serve as monitors or observers for the external supervisor, or may actually impose the requirement restrictions. An external supervisor is a supervisor automaton that adds restrictions to the uncontrolled system (the plants), and potentially the requirement automata, depending on the simplifications that are applied. The supervisor uses the same events as the plants, and refers to plant and requirement locations and variables in its conditions.
By default, the resulting external supervisor automaton is put in the empty namespace, at the top level of the resulting specification. That is, the supervisor automaton is not put in any groups. See the namespace section for more information.
By default, the added supervisor automaton is named sup. Using the Supervisor name option (see the options section), it is possible to specify a different name. Custom supervisor automaton names must be valid CIF identifiers, i.e. they may consist of letters, digits, and underscores (_), but may not start with a digit. If the resulting supervisor automaton has a name that conflicts with an existing declaration, it is automatically renamed to have a non-conflicting name. In such cases, a warning is printed to the console to inform the user.
The resulting supervisor has exactly one self loop edge for each of the controllable events in the alphabet of the controlled system (which is equal to the alphabet of the uncontrolled system). These self loops represent the possible conditions under which the supervisor allows the events to occur in the controlled system. The exact predicates may vary, depending on the simplifications that are applied.
If there are controllable events that are never enabled in the controlled system, a warning is printed to the console. Enabling forward reachability ensures that warnings are also printed for events that are only enabled in the unreachable part of the statespace. Disabling forward reachability may lead to false negatives, i.e. such cases may not be reported.
The resulting supervisor may have an initialization predicate that restricts the states in which the system may be initialized (may start), on top of the initialization constraints already present in the uncontrolled system. For more information on this initialization predicate, see the section about initialization.
The added supervisor automaton and all its elements do not have any annotations. The output specification never has a controller properties annotation, even if the input specification has one.
Namespace
As indicated above, by default the resulting supervisor automaton is put in the empty namespace, at the top level of the resulting specification. That is, the supervisor automaton is not put in any groups.
It is possible to add a namespace to the entire resulting specification. That is, to put groups around the original plants and requirements, the added supervisor automaton, etc. A namespace can be added using the Supervisor namespace option (see the options section). By default, no additional namespace is added.
By adding a namespace around the entire resulting specification, the synthesis result can be easily merged with for instance a simulation model. The added namespace ensures that there are no naming conflicts between the plants of the simulation model and the similarly original plants. The events are not put in the new namespace, but are instead kept in their original place, wrapped in groups as necessary to keep their original identities (absolute names). This ensures that it remains possible to connect (merge) the events of the synthesis output with the events of the simulation model.
The namespace specified using the option, must consist of one or more valid CIF identifiers, separated by dots (.). Valid CIF identifiers consist of one or more letters, digits, and underscores (_), but may not start with a digit. As an example, consider namespace a.b. A group b is wrapped around the entire synthesis result, and a group a is wrapped around group b. Group a is then the new synthesis result.
If a part of the namespace has the same name as an event that remains in its original place, this leads to a conflict, and synthesis fails. If the namespace does not conflict, but is non-empty (it contains an event or it contains a group that contains an event), synthesis also fails.
BDD representation in CIF
Internally, predicates are represented using Binary Decision Diagrams (BDDs). The supervisor that is the output of synthesis, contains several predicates as well. For instance, it has self loops with guard predicates, and it may have an initialization predicate. The predicates represented as BDDs need to be represented as CIF predicates. There are multiple approaches to do this, and the BDD output mode option (see the options section), can be used to configure the approach to use.
The first approach, which is also the default approach (named normal), is to use either Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) predicates. Both a CNF predicate and a DNF predicate are created and the smallest one is used. If they have the same size, the CNF predicate is used. This approach has as benefit that for relatively small predicates (usually for small systems), the CIF predicates are often intuitive, and can easily understood. The downside is that for larger systems, the CIF predicates often grow exponentially in size.
The second approach (named cnf) always uses the CNF representation. The third approach (named dnf) always uses the DNF representation. Selecting one representation, when the other blows up exponentially, can prevent long running times and out-of-memory errors. But, knowing which one to select can be challenging, as this typically depends on the model being synthesized.
The fourth approached (named nodes), is to represent the internal BDD nodes directly in CIF. The BDD is then more or less coded directly in CIF, using some constants and algebraic variables, and is evaluated using a BDD evaluation function. The benefit is that for larger systems, this representation remains relatively small, and at the very least doesn’t blow up nearly as much as the CNF and DNF representations. The downside to this approach, is that it leads to a supervisor that can not be easily understood by inspecting it. For this approach, several objects are created in the top level scope of the CIF specification. The names of these declarations all share a common prefix. The default prefix is bdd, but it can be changed using the BDD output name prefix option (see the options section). No existing declarations, whose names start with that prefix, should be present in the top level scope of the specification.