State requirement invariants
Before synthesis, the entire CIF specification is converted to Binary Decision Diagrams (BDDs), a representation of predicates that allows for efficient synthesis. The state requirement invariants of the specification thus also need to be part of the BDD representation of the specification. These requirements can be enforced by applying them to the BDDs in multiple ways:
-
Controlled behavior:
All state requirement invariants are enforced via the 'controlled behavior' BDD. This BDD represents all states of the controlled system. Since the controlled system has to adhere to the state requirement invariants, these invariants can be put directly into the controlled behavior BDD.
-
Edge guard or controlled behavior:
The decision how to enforce state requirement invariants is made per per edge. For each edge with a controllable events, the invariants are enforced via the guards of the edge, by strengthened the existing guards with sufficient extra conditions that ensure that after taking the edge the state requirement invariants hold. The initialization predicate of the controlled system is restricted as well, to ensure the state requirement invariants also hold in initial states. As synthesis may not restrict the guards of edges with uncontrollable events, for those edges the extra restrictions are put into the controlled behavior BDD instead.
By default, all state requirement invariants are enforced via the controlled behavior. This can be changed by using the State requirement invariant enforcement option (see the options section).
The effect of the different approaches on the computational effort of synthesis can be quite complex:
-
Upfront effort: Using approach 2, the edge guard restrictions need to be computed for each edge and each state requirement invariant, which potentially requires significant computational effort. Using approach 1, each state requirement invariant is considered only once, when putting it into the controlled behavior, which may require less computational effort.
-
Size of controlled behavior: Reachability computations rely heavily on the controlled behavior predicate. Using approach 1, putting state requirement invariants into the controlled behavior, may restrict the controlled behavior, potentially leading to a smaller predicate and reduced computational effort. However, putting state requirement invariants into the controlled behavior may also lead to a controlled behavior predicate with more BDD nodes to express the additional restrictions, potentially increasing the computational effort.
-
Reachability fixed point: Using approach 1, with a more restricted controlled behavior predicate, may lead to more quickly reaching a fixed point in reachability computations, potentially reducing computational effort.
-
Post-synthesis effort: Using approach 1, the state requirement invariants are put into the controlled behavior, but they still need to be put into the edge guards after synthesis, which requires computational effort. Using approach 2, putting the state requirement invariants into the edge guards at the start of synthesis, means that the restrictions do not need to be applied at the end of synthesis, potentially reducing computational effort.
Both approaches have potential benefits and drawbacks, making for a trade-off between their various effects. Which approach is most efficient depends on the model.
For more information, see the scientific publication by [Thuijsman et al. (2021)], where the two approaches are compared.