Hi Michaël!

Michaël Cadilhac michael@cadilhac.name writes:

… ltlsynt was still aggressively calling "merge_states"

When Maximilien and Thibaud created ltlsynt, they noticed that spot::postprocessor was spending too much time in simulation-based reductions to simplify large automata. So they disabled those, and Maximilien wrote merge_states() as a cheaper replacement, and called it from ltlsynt.

Years later, Philipp rewrote parts of merge_states() to speed it up, and also introduced a multi-threaded variant (not enabled by default: you have to compile with --enable-pthread). He also made merge_states() game-aware, so it doesn't merge states from different players.

Later, I changed spot::postprocessor so that it had two configurable thresholds: merge-states-min=128 and simul-max=4096. If the number of states of the automaton is above merge-states-min, merge_states() is called before simulation-based reductions, as merging the obvious first helps reducing the complexity of simulation-based reductions. Below that value, simulation-based reductions are usually fast enough and already do the job of merge_states(). If the number of states is above simul-max, simulation-based reduction are simply disabled.

Finally, when Philipp and Florian did a huge rewrite of ltlsynt to move several of its part to Spot (so they get exposed in Python) and include things like specification decomposition, I told them it wasn't necessary to disable simulation-based reduction or call merge_states() anymore, since spot::postprocessor had the above thresholds.

So that's when merge_states() disappeared from ltlsynt. But it should still be called by spot::postprocessor on large automata.

https://github.com/gaperez64/acacia-bonsai/blob/ 22cff19e55b3de4bf7b348ae770302663f6d24dc/src/aut_preprocessors/ surely_losing.hh#L65

Hmm... I had to rewrite defrag_states() recently, and this is called by purge_dead_states() right before your call to merge_states(). I may have broken something?

Could you test your code with the version of Spot that is just *before* commit 77a17881a3222bd8604e5e33974a542351490638?

Alexandre