[Spot] Re: What happened to merge_states?

Hi Michaël! Michaël Cadilhac <michael(a)cadilhac.name> writes: 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. 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