4 Jun
2019
4 Jun
'19
11:21 a.m.
Hi Yong,
On Mon, Jun 3, 2019 at 6:32 AM Yong Li (李勇) <liyong(a)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