The saturation and bounded saturation algorithms fail to explore all states with specific combinations of input BDDs, which is a bug.
For example, suppose we have an old-state BDD variable x on level 0, and a corresponding new-state variable x' on level 1. (So the variable order is x > x'; terminal nodes then probably have level 2.) Let's say we want to apply saturationForward with the following input states BDD (i.e., ithVar(0)):
We use a single (trivial) relation as input, which is the true terminal:
And we use a single variable set as input, which is the singleton set {x'} (containing the BDD ithVar(1)):
We expect the saturation result to be the true terminal, since due to the variable level set, x may have any value after having applied relnext with the single relation. However, the actual saturation result turns out to be the same as the input states BDD, i.e.,
This is because saturation never applied the relation. The underlying reason is rather technical. When saturation is called, first the terminal cases are checked, which don't hold. Then after checking the cache table (assuming we have a cache miss), saturation will determine whether to recurse deeper into the structure of the states BDD, or whether to apply relations. This decision is made by the following if-statement:
if (LEVEL(states) < LEVEL(vars[current])) {
// Recursively call saturation, applied to the low and high edges of the states BDD, and then combine the saturation results.
} else {
// First advance in the transition relation list, and then apply relations on the current level.
}In our example case, LEVEL(states) is 0 and LEVEL(vars[current]) is 1, where vars[current] is our singleton variable set. Hence, saturation will decide that we need to go deeper into the structure of the states BDD to get to the right level for applying relations. So, we call saturationForward_rec(low(states), ...) and saturationForward_rec(high(states), ...). However, low(states) and high(states) are both terminal nodes. So the terminal cases of saturation will kick in. And because of that, saturation is done immediately, and relnext is never applied.
The mistake here is that, if LEVEL(states) is 0 and LEVEL(vars[current]) is 1, then we should be on the right level already to start applying relations, since levels 0 and 1 are both about the same BDD variable, namely x.
Backward saturation and the bounded variants of saturation have the same problem. Moreover, apart from this specific example, the problem occurs whenever the child edges of the input states BDD both lead to terminal nodes, and when LEVEL(states) = LEVEL(vars[current]) - 1.
Therefore, the solution is to change the if-statement condition to:
if (LEVEL(states) + 1 < LEVEL(vars[current])) {This works because LEVEL(states) always refers to the level of an old-state variable. And LEVEL(states) + 1 to the level of the corresponding new-state variable. If the top-level of the current relations to apply (i.e., LEVEL(vars[current])) is lower than this new-state variable, then we should indeed go deeper into the structure of states.
The saturation and bounded saturation algorithms fail to explore all states with specific combinations of input BDDs, which is a bug.
For example, suppose we have an old-state BDD variable
xon level 0, and a corresponding new-state variablex'on level 1. (So the variable order isx > x'; terminal nodes then probably have level 2.) Let's say we want to applysaturationForwardwith the following input states BDD (i.e.,ithVar(0)):We use a single (trivial) relation as input, which is the true terminal:
And we use a single variable set as input, which is the singleton set
{x'}(containing the BDDithVar(1)):We expect the saturation result to be the true terminal, since due to the variable level set,
xmay have any value after having appliedrelnextwith the single relation. However, the actual saturation result turns out to be the same as the input states BDD, i.e.,This is because saturation never applied the relation. The underlying reason is rather technical. When saturation is called, first the terminal cases are checked, which don't hold. Then after checking the cache table (assuming we have a cache miss), saturation will determine whether to recurse deeper into the structure of the states BDD, or whether to apply relations. This decision is made by the following if-statement:
In our example case,
LEVEL(states)is 0 andLEVEL(vars[current])is 1, wherevars[current]is our singleton variable set. Hence, saturation will decide that we need to go deeper into the structure of the states BDD to get to the right level for applying relations. So, we callsaturationForward_rec(low(states), ...)andsaturationForward_rec(high(states), ...). However,low(states)andhigh(states)are both terminal nodes. So the terminal cases of saturation will kick in. And because of that, saturation is done immediately, andrelnextis never applied.The mistake here is that, if
LEVEL(states)is 0 andLEVEL(vars[current])is 1, then we should be on the right level already to start applying relations, since levels 0 and 1 are both about the same BDD variable, namelyx.Backward saturation and the bounded variants of saturation have the same problem. Moreover, apart from this specific example, the problem occurs whenever the child edges of the input states BDD both lead to terminal nodes, and when
LEVEL(states) = LEVEL(vars[current]) - 1.Therefore, the solution is to change the if-statement condition to:
This works because
LEVEL(states)always refers to the level of an old-state variable. AndLEVEL(states) + 1to the level of the corresponding new-state variable. If the top-level of the current relations to apply (i.e.,LEVEL(vars[current])) is lower than this new-state variable, then we should indeed go deeper into the structure ofstates.