One can skip an entire relnext*() operation in the Chain algorithm by abusing the following insights:
Consider the initial state the first pivot
Here, the already computed set reachable is the entire forward set.
Hence, the only thing still missing is the backwards set (relprev*()).
So, one can essentially do a loop-unrolling with the initial state as the pivot. This can potentially (in the best case) result in halving the number of symbolic steps.
One can skip an entire
relnext*()operation in the Chain algorithm by abusing the following insights:reachableis the entire forward set.relprev*()).So, one can essentially do a loop-unrolling with the initial state as the pivot. This can potentially (in the best case) result in halving the number of symbolic steps.