Hi Yong, On Mon, Jun 3, 2019 at 6:32 AM Yong Li (李勇) <liyong@ios.ac.cn> wrote:
I have another question about Spot (v 2.7.4).
I am using following code to translate an LTLf formula to an NBA (full code is attached):
spot::translator trans; spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f)); cout << "done translating " << endl; print_hoa(std::cout, aut) << '\n';
When I input the following formula, the program seems to get stuck:
(G((LiVar732) & (power) & (pumppower))) -> (G(!((LiVar808) & (mechanicalpedalposL) & (mechanicalpedalposR) & (!(((mechanicalpedalposL) & ((LiVar610) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar568))) & (!(((mechanicalpedalposL) & ((LiVar608) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar567))) & (!(((mechanicalpedalposR) & ((LiVar606) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar566))) & (!(((mechanicalpedalposR) & ((LiVar604) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar565))) & (!(((mechanicalpedalposL) & ((LiVar602) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar564))) & (!(((mechanicalpedalposL) & ((LiVar600) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar563))) & (!(((mechanicalpedalposR) & ((LiVar598) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar562))) & (!(((mechanicalpedalposR) & ((LiVar596) | (LiVar809) | (!(controlsystemvalidity)))) -> (LiVar561))))))
However, Spot in command line (ltlfilt --from-ltlf -f formula | ltl2tgba) is able to translate this ltlf formula to an NBA in less than a second.
Yes, this is related to another bug I fixed two weeks ago on the development version. spot::translator has an optimization for formulas where a lot of atomic propositions are used together. When this optimization is used, a huge formulaslike yours is first rewritten as Gp0 -> Gp1, then translated to an automaton over p0, p1, and finally the occurrences of p0 and p1 in the automaton are changed back to the original Boolean formulas they represent. Doing so speeds up a lot of determinization-based algorithms that are exponential in the number of atomic propositions. The bug is that this optimization is only activated when an option_map is passed to the spot::translator object. So you should be able to fix that by just changing spot::translator trans; into spot::option_map m; spot::translator trans(&m); In the next release that will not be necessary. Of course ltl2tgba always passes an option_map to trans, because option_map is the object used to collect any option passed with the -x flag. Best regards, -- Alexandre Duret-Lutz