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.

During reachability computations the edges are considered one by one to find more reachable states. Regardless of whether an edge leads to new states being found or not, the search always continues with the next edge. As long as new states are found, the edges will keep being applied one after the other. After the last edge has been considered, the first edge is considered again, then the second one, etc. Only once all edges have been applied and none of them lead to new states being found has a fixed point 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.

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.

The order in which the edges are considered for reachability computations is determined by the Edge order for backward reachability and Edge order for forward reachability options (see the options section). 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 .. 2⁶⁴ - 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.