8 Dec
2020
8 Dec
'20
1:32 a.m.
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