Dear LTLSYNT Team,

I'm an associate researcher from Harbin Institute of Technology. When I was using LTLSYNT for experiments, I may find a bug. Consider a LTL formula G(a-> X b) and G(b-> X not b) where a is the input and b is the output. Obviously, it is unrealizable. As whenever the input event ’a’ holds in two consecutive steps, the system can not produce a value for the output event ’b’. However, when I try it in LTLSYNT, I got 'realizable'. I'm assuming it is a bug and report it to you. 

Best regards,

Xin Ye