Edge order

Data-based supervisor synthesis involves many reachability computations to determine which states can be reached from which other states (forward reachability), or which states can reach which other states (backward reachability). This involves repeatedly following edges to find those states, using a fixed point computation.

Synthesis does not directly use the edges from the model. It applies linearization and then uses the edges from the linearized model. Edges are internally also added to support input variables during synthesis. Furthermore, edges may be combined to form less granular edges, before they are used for reachability computations.

During reachability computations the edges are then considered one by one to find more reachable states. As long as new states are found, the edges will keep being followed. Once it is clear that considering edges no longer leads to finding new states, a fixed point has been reached and the computation stops.

The order in which the edges are considered for such computations has no effect on the final fixed point result. The order can however significantly influence the performance of supervisor synthesis. For instance, consider that there are dozens of edges and from the already discovered states there is only one edge that leads to more states being found. Then considering that one particular edge first will immediately lead to more states being found. Considering other edges first will lead to wasted computations, as they won’t find any new states.

Besides finding or not finding new states, which new states are found first and in what order may also influence performance. It may lead to smaller or larger intermediate BDD representations of predicates. See the section about BDD variable order for more information.

Three approaches

There are three approaches that determine the order in which edges are considered:

  • Fixed order:

    A fixed order is determined upfront, before any reachability computations. Each of the edges is considered in that fixed order, one after the other. Regardless of whether an edge leads to new states being found or not, the search always continues with the next edge from the fixed order. Each edge is applied to all reached states, including those of the previously applied edges. After the last edge has been considered, the first edge is considered again, then the second one, etc. This way of applying edges is known as the chaining strategy for reachability computation. A fixed point is reached once:

    • All edges have been considered at least once.

    • Since all edges have last been considered, no new states were found.

  • Workset algorithm:

    The order in which the edges are considered is dynamic, rather than fixed. The algorithm also follows the chaining exploration strategy, and works as follows:

    • Initially, all edges are in a workset.

    • While the workset is not empty:

      • Select an edge from the workset. In principle any edge may be selected, but using a smart heuristic improves performance.

      • Use the selected edge to find new states, repeatedly, until it no longer has an effect (no longer finds new states).

      • If any new states were found using the selected edge (it had an effect), add the dependencies of that edge to the workset. The dependencies of an edge are those other edges that may be enabled after using it.

      • Remove the selected edge from the workset.

    The workset algorithm can only be used in combination with a 'per event' edge granularity. The workset algorithm can not be used when duplicate events are allowed in a custom edge order.

  • Saturation:

    Saturation is a strategy for BDD-based symbolic reachability computations that exploits locality of the edges that are considered. The edges to consider are sorted on the top-most BDD variable of their BDD representations. The order of edges with the same such top-most BDD variable is determined based on the configured order. The saturation algorithm then uses this order to saturate the BDD representation of the set of reachable states from the bottom up. This is done by first applying edges over the lowest part of the BDD until they no longer lead to new states, and then gradually go upward in the sorted edge order until saturation is reached for all edges. Saturation thereby tries to reduce blow-ups of BDDs at intermediate points during reachability computations, which can sometimes be observed with other exploration strategies, like chaining.

    The saturation strategy can not be used when duplicate events are allowed in a custom edge order.

Which approach to use during synthesis, can be configured using the Exploration strategy option (see the options section). Saturation is used by default.

Which approach works best depends on the model, and this may involve a trade-off. The workset algorithm may reduce the maximum amount of memory used during synthesis, compared to using a fixed order. However, this often comes at the cost of extra computations that require more time, especially if edges have many other edges as their dependencies. Saturation generally works best.

Configuring the order

The order in which the edges are considered when a fixed order is used, is determined by the Edge order for backward reachability and Edge order for forward reachability options (see the options section). If the workset algorithm is used, the edges in the workset are ordered according to the configured order. The configured order may therefore also influence the order in which edges are selected by the workset algorithm’s edge selection heuristics. And if saturation is used, the configured edge order determines the order of the edges with the same top-most BDD variable.

Several predefined orders exist, and it is also possible to define a custom order. By default, the model ordering is used for both backward and forward reachability computations. The following orders can be used:

  • model ordering (option value model)

    The order of the edges is as they occur in the linearized model. Edges for input variables are always put after the other edges, sorted based on the variable order. Edges are considered exactly once per reachability iteration.

  • reverse model ordering (option value reverse-model)

    The order of the edges is as they occur in the linearized model, but reversed. Edges for input variable are thus always put before the other edges, sorted based on the reversed variable order. Edges are considered exactly once per reachability iteration.

  • sorted ordering (option value sorted)

    The order of the edges is based on the names of their corresponding events and input variables. They are sorted alphabetically in ascending order, based on their absolute names. In case edges are labeled with the same event, the edges are ordered based on the linearized model order. Edges are considered exactly once per reachability iteration.

  • reverse sorted ordering (option value reverse-sorted)

    The order of the edges is based on the names of their corresponding events and input variables. They are sorted alphabetically in descending order, based on their absolute names. In case edges are labeled with the same event, the edges are ordered based on the reversed linearized model order. Edges are considered exactly once per reachability iteration.

  • random ordering (option value random or random:SEED)

    The edges are ordered randomly. If no seed is specified, a random seed is used, resulting in a random random order. If a seed is specified, a fixed random order is used. That is, using the same seed again, results in the same random order. The SEED must be an integer number in the range [0 .. 264 - 1]. For instance, use random:123 as option value to get a random order that can be repeated on a subsequent synthesis for the same model.

  • custom ordering

    Custom orders consist of absolute names of events and input variables. That is, for an automaton a, with an event x, the absolute name of the event is a.x. In case edges are labeled with the same event, the edges are ordered based on the linearized model order. The * character can be used as wildcard in those names, and indicates zero or more characters. In case of multiple matches, the matches are sorted alphabetically in ascending order, based on their absolute names.

    Multiple names can be separated with , characters. The edges and input variables matching the name pattern before the , are ordered before the edges and input variables matching the name pattern after the ,.

    Each name pattern in the order must match at least one event or input variable. Every event and input variable needs to be included in the order.

    By default, an event or input variable may not be included more than once in the order. This allows detecting accidental duplicate inclusion of events in the order. It can however be useful to include events multiple times in the order, for instance if for some model considering the event twice leads to immediately finding a new state during the reachability operation, while this would otherwise only be found in the next iteration. To allow events to be included multiple times in the custom order, use the Edge order duplicate events option (see the options section). This option applies to both the backward and forward edge order.

Determining the best edge order is difficult as it can be tricky to predict which edges will lead to finding new states and quickly reaching the fixed point result. When in doubt, keep the default values of the options. If you specify a custom edge order for backward reachability, typically the reverse order is a decent order for forward reachability, and vice versa.