Allow different order of fixed-point computations in CIF data-based synthesis
We have the option to enable or disable forward reachability. Enabling it may reduce the state space, which then subsequently affects also next fixed-point computations, and may improve synthesis performance (besides leading to an exact size of the controlled system behavior). As forward reachability takes time as well, it depends on the model whether it improves or degrades the performance.
We currently do the fixed-point computations always in this order:
- Backward reachability for marking (all events) -> computes the co-reachable/non-blocking states
- Backward reachability for controlled behavior (uncontrollable events) -> computes the 'controllable' states
- Forward reachability for initial states (all events, optional) -> computes the reachable states
Often backwards reachability for marking is the bottleneck. One of the reasons is that often all variable values are marked. Forward reachability is for some models much simpler. One of the reasons is that it can start in the initial state, and variables are often initialized to a single value. If forward reachability helps a lot, and is more efficient than backwards reachability of marking, doing the forward reachability first can improve synthesis performance a lot. Since the forward reachability then often leads to less states, and subsequent backward reachability computations are restricted to stay in the current controlled behavior, they may also be more efficient, etc.
Currently, there is no way to change the order of the fixed-point computations. I tested it on a model where I could only do synthesis on a cluster with 256GB memory, in 45 minutes. I quickly changed the CIF data-based synthesis tool to start with forward reachability, and then do the fixed-point computations as usual. I could then do synthesis on my own laptop with 8 GB, in 11 minutes. For a smaller version of that model, the time to synthesize on my laptop was reduced from 38 seconds to 11 seconds. So it seems that we can get a 3-4 times speedup, at least for this type of model. Likely, the result is model dependent.
I want to add a 'Fixed-point computations order' option to the CIF data-based synthesis tool to configure the order of the fixed-point computations, with the following allowed values:
nonblock-ctrl-reach
nonblock-reach-ctrl
ctrl-nonblock-reach
ctrl-reach-nonblock
reach-nonblock-ctrl
reach-ctrl-nonblock