Initial variable orders
The CIF data-based synthesis algorithm features several predefined initial BDD variable orders, and it is also possible to define a custom order.
For basic configuration, the initial order of the boolean/BDD variables can be configured using the BDD initial variable ordering option (see the options section). By default, the sorted order is used as initial variable ordering. The following predefined initial orderings can be used:
-
model ordering without interleaving (option value
model)The order of the synthesis variables is as they occur in the model. A location pointer, for an automaton with two or more locations, is put before the variables declared in that automaton.
No synthesis variables are interleaved, except for each old variable with its corresponding new variable.
-
reverse model ordering without interleaving (option value
reverse-model)The order of the synthesis variables is as they occur in the model, but reversed. A location pointer, for an automaton with two or more locations, is put after the variables declared in that automaton, in this reverse order.
No synthesis variables are interleaved, except for each old variable with its corresponding new variable. The old variables are still before the new variables; this is not reversed.
-
sorted ordering without interleaving (option value
sorted)The order of the synthesis variables is based on the names of the variables and automata. They are sorted alphabetically in ascending order, based on their absolute names.
No synthesis variables are interleaved, except for each old variable with its corresponding new variable.
-
reverse sorted ordering without interleaving (option value
reverse-sorted)The order of the synthesis variables is based on the names of the variables and automata. They are sorted alphabetically in descending order, based on their absolute names.
No synthesis variables are interleaved, except for each old variable with its corresponding new variable. The old variables are still before the new variables; this is not reversed.
-
random ordering without interleaving (option value
randomorrandom:SEED)The variables and automata 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
SEEDmust be an integer number in the range [0 .. 264 - 1]. For instance, userandom:123as option value to get a random order that can be repeated on a subsequent synthesis for the same model.No synthesis variables are interleaved, except for each old variable with its corresponding new variable.
-
custom ordering
Custom orders consist of absolute names of variables and automata. That is, for an automaton
a, with a discrete variablex, the absolute name of the variable isa.x. 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 increasingly on their absolute names, and interleaved.Multiple names can be separated with
;characters. The synthesis variables matching the name pattern before the;are ordered before the synthesis variables matching the name pattern after the;. The;separator does not introduce interleaving. The,separator can be used instead of the;separator to introduce order but also introduce interleaving.Each name pattern in the order must match at least one variable or automaton. A variable or automaton may not be included more than once in the order. Every variable and automaton (with two or more locations) needs to be included in the order. It is not possible to specify new variables, as they are always directly after their corresponding old variables, and they are always interleaved.
For instance, consider two automata:
aandb, each with three variables of typeint[0..3]:x1,x2, andx3. The automata have three locations each, so location pointers are created for them. We thus have six discrete variables:a.x1,a.x2,a.x3,b.x1,b.x2, andb.x3, and two location pointer variables:aandb. Consider the following custom order:b*;a.x3,a.x1;a.x2,a. Patternb*matches location pointer variablebas well as the three discrete variables of automatonb(b.x1,b.x2, andb.x3). They are ordered in increasing alphabetic order, and are interleaved. Variablesa.x3anda.x1are also interleaved, witha.x3beforea.x1. Finally, variablea.x2is ordered before the location pointer for automatona, and they are interleaved as well. This results in the following boolean/BDD variable ordering, with bits whose name ends with+representing bits of new variables rather than current/old variables, andx#0representing bit zero of variablex:b#0b+#0b.x1#0b.x1+#0b.x2#0b.x2+#0b.x3#0b.x3+#0b#1b+#1b.x1#1b.x1+#1b.x2#1b.x2+#1b.x3#1b.x3+#1a.x3#0a.x3+#0a.x1#0a.x1+#0a.x3#1a.x3+#1a.x1#1a.x1+#1a.x2#0a.x2+#0a#0a+#0a.x2#1a.x2+#1a#1a+#1
For advanced configuration, see the separate section on advanced variable ordering configuration.