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