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
叶昕 yexin@hit.edu.cn writes:
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.
Hi Xin Ye,
I cannot reproduce this:
% ltlsynt -f 'G(a->Xb) & G(b->X!b)' --ins=a UNREALIZABLE
Can you show the command you used and specify the version of ltlsynt that you used? In particular verson 2.12.2 fixed a bug that cannot occur in this simple formula, but that could occur in similar formulas having a lot of terms of the form G(p1->p2).
Alexandre
-
Alexandre Duret-Lutz -
叶昕