HI,

My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I’m having an issue and I’ll appreciate if you can assist.

I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API.

The program I wrote is basically like this:

        …get the formula…

        spot::parsed_formula cex_pf = spot::parse_infix_psl(formula);

        if(cex_pf.format_errors(std::cerr)){

cout << "Invalid formula syntax: " << formula << endl;

exit(1)

        }

        spot::translator trans;

        trans.set_type(spot::postprocessor::BA);

        trans.set_pref(spot::postprocessor::Small);

        twa_graph_ptr aut = trans.run(cex_pf.f);

       …print the automata…

I tried running this code on several formulas, and it works great.

The problems started when I processed this formula:

G({(a)} |=> {(b)[*32]})

The code is running for a long time (more than a hour) without giving a result.

Did it get stuck? Is there any way I can make it work?

Thanks,

Roei Nahum