Dear Spot Team,
Thanks for providing a wonderful tool.
During constructing Buchi automata for LTL, Spot always shows non-determinism automata
although I select the "deterministic" item. Would you mind telling me how to
construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13
& (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U
ousr2_ai3_ce8)))))). The following is its automata but non-determinism.
[cid:83ad2cd0-bc60-443c-b387-4bc7953c05d2]
Looking forward to your response.
Kind Regards,
Ruijie