Spot October 2024

spot@lrde.epita.fr

What happened to merge_states?
by Michaël Cadilhac 07 Oct '24

07 Oct '24

Howdy spotters, *Once upon a time, *right before a rewrite of ltlsynt at: https://gitlab.lre.epita.fr/spot/spot/-/blob/7d908b93207b983a4ced81dd2240a5… … ltlsynt was still aggressively calling "merge_states", see e.g., https://gitlab.lre.epita.fr/spot/spot/-/blob/25c75c55b1e1fe7d3a502e1658839f… Being the sheep that I am, I vaguely copied at that time this behavior without really understanding it: https://github.com/gaperez64/acacia-bonsai/blob/22cff19e55b3de4bf7b348ae770… (The goal therein is simply to remove some states, then execute some simplification of the automaton.) *But then, the fire nation attacked. *For some reason, with the most recent Spot master, I get a lot of crashes in merge_states, on that line specifically: https://gitlab.lre.epita.fr/spot/spot/-/blob/master/spot/twa/twagraph.cc?re… This is probably rooted in my incorrect use of that method, its companion simplification functions, and state deletion. *So, questions:* - Why did ltlsynt stop using merge_states/merge_edges? - What is it I'm doing wrong in my use case? Thank you! Michaël

2 1