HI, My name is Roei Nahum. Your wonderful platform helps me to translate temporal formulas into Buchi automata. I downloaded Spot (version 2.9.4), and wrote a C++ program based on Spot API. As the following code snippet shows, I configured Spot so it will produce small state-based Buchi automata. I also skip the wdba minimalization. spot::option_map extra_options; spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::translator* trans; extra_options.set("wdba-minimize", 0); trans = new spot::translator(dict, &extra_options); trans->set_type(spot::postprocessor::BA); trans->set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans->run(pf.f); Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing: (!G(!({{a ##[1:500] b} ##[1:500] c}))) Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged? Thanks in advance, Roei