You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Inside minimise.c's try_partition, we split an equivalence class in place, but it's arbitrarily committing to keeping whichever states lead to the same EC as the first state in the EC list. While the non-determinism doesn't affect correctness (since it will run to a fixpoint either way), using the counts to decide which to modify in place and which to separate out may improve performance.
The change would appear in update_after_parittion -- if both the src and dst ECs have more than one state and the src EC has less (or more) than the dst EC, swap them, so the larger EC always appears earlier (or later). The special case for one state is so that ECs with only 1 state end up in the "done" region at the end.
I suspect always breaking out the smaller EC should perform better, but it needs benchmarking.
The text was updated successfully, but these errors were encountered:
Inside
minimise.c
'stry_partition
, we split an equivalence class in place, but it's arbitrarily committing to keeping whichever states lead to the same EC as the first state in the EC list. While the non-determinism doesn't affect correctness (since it will run to a fixpoint either way), using the counts to decide which to modify in place and which to separate out may improve performance.The change would appear in
update_after_parittion
-- if both the src and dst ECs have more than one state and the src EC has less (or more) than the dst EC, swap them, so the larger EC always appears earlier (or later). The special case for one state is so that ECs with only 1 state end up in the "done" region at the end.I suspect always breaking out the smaller EC should perform better, but it needs benchmarking.
The text was updated successfully, but these errors were encountered: