Proof solver taking far longer after fixing issue with saturation

[thecathe]

Overview

After fixing an issue with the saturation (src/saturate_model) in this commit the pre-existing test proofs appear to work, but take far more iterations.

The old saturation algorithm did not add additional weak transitions. The algorithm collects reflexive-transitive closure weak transitions from each given state. A crucial part of the algorithm is that it keeps track of whether it has traversed a "named action" during its exploration, and uses this to determine whether it should stop exploring a given trace (i.e., when it finds it's second "named action").

Example

Given the saturated action annotation:
(0) --{None}-> (1); (1) --{None}-> (2); (2) --{Some _}-> (3); (3) --{None}-> (4);
the previous algorithm would have failed to identify the following additional saturated action:
(0) --{None}-> (1); (1) --{None}-> (2); (2) --{Some _}-> (3);

Suspected Cause

I believe the issue is caused by Mebi_proof.get_action_to in src/mebi_proof which naively takes the first action that leads to the desired destination state, and that this is causing us to explore the "back-alleys" of the state-space.

Additionally, it is also a chance that in some cases where the old algorithm would have picked some weak-transition, the new one is taking some sub-transition of the old one, resulting in instances where the same overall transition would eat up far more iterations and computing power.

Proposed Actions

• Revisit how the proof solving algorithm decides which transition to take, and make sure it doesn't choose one that is inefficient/suboptimal and result in wasted computational effort.

[thecathe]

Also worth noting that at this point the plugin can solve the first half of the CADP example. (This is a first!)

[thecathe]

So far the examples it takes too long are the Proc.Test2 and the second half of the CADP example. In the latter case my laptop ran out of memory. I will need to optimize this before proceeding with anything else