A small fix: the problematic formula is:
(!(G({(a)} |=> {(b)[*32]})))
From: Roei Nahum Sent: Tuesday, December 8, 2020 2:33 AM To: spot@lrde.epita.fr Subject: Spot question
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