Edge order

Data-basd 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 is determined by the Edge order option (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. The following predefined orders exist:

Furthermore, a custom order can be defined. 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. An event or input variable may not be included more than once in the order. Every event and input variable needs to be included in the 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, use the default value of the option.