[Spot] Question on LTL to buechi automata

Dear Spot team, Thanks for developing the nice tool Spot. I am a researcher at National University of Singapore using Spot in my research. I have a question about translating LTL to buechi automata using spot. My LTL properties are constraints over input/output sequences of a program, e.g., output W, output P always responds to input B (false R (! iB | (true U (oW & X (true U oP))))) where iB indicates that input B and oP indicates output P. The buechi automata of the negation of above formula given by Spot is in the following: [image: image.png] Here is a input/output trace to be evaluated: iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH *What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?* Given the input/output trace, there is no element that is iB and at the same time is oW. I assume the verification feeds element in the trace to the automata one by one. Do I miss something e.g., wrong configuration on the translation or some basic knowledge about verification? Can you give me some advice on this issue? Thank you very much. Best regards Zhen -- Zhen Dong Senior Research Fellow National University of Singapore https://www.comp.nus.edu.sg/~dongz/