30 Jan
2025
30 Jan
'25
10:18 a.m.
叶昕 <yexin(a)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