Skip to content

CIF data-based synthesis documentation: mention fixed point computation order on the forward reachability page

We have a documentation page that explains what forward reachability is and that it can be enabled and why that can help with readability of the result as well as with performance. What isn't clear from this page, is that forward reachability is by default done last. So, enabling it to solve issues with slow backward reachability for marking in the first iteration, won't have any effect, as forward reachability is by default done last. We should document when it is applied, referring to the page that explains the fixed-point computations order option, which allows one to change the order. Adding a bit of extra documentation and linking will prevent confusion and surprises for users.

Thanks to @alihaghassan for pointing out this issue.