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.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/