Question Regarding Unexpected Results

[CoriolisSP]

Hello,

I've been using Lisa to solve an LTLf synthesis problem and I've encountered some unexpected results that I hope you could help clarify. Below are the details.

Formula:

X (G ( (X[!] ((p3) || (p0)))))

Variables:

.inputs: p0
.outputs: p3

Command:

./lisa -syn -ltlf ./testFormula -part ./testVar

Given that the top-level operator in the formula is X (weak next), I think that any trace of length 1 should satisfy it, implying that it should be realizable. However, the output I received was unexpected:

Starting the decomposition phase
Breaking formula into small pieces...
Starting the composition phase
Finished constructing minimal dfa in 11.236ms ...
Number of states (or nodes) is: 2
Final result (or number of nodes): 2
Computing the transition relation...
Finished computing the transition relation...
Starting to synthesize 
System will play first
The number of nodes in T(0) is 0
The number of nodes in W(0) is 0
The number of nodes in pre_image(0) is 0
Finished synthesis after 1 iterations
The number of nodes in T(i+1) is 0
UNREALIZABLE
Finished synthesizing
0.085 ms
Total CPU time used: 0.085 ms
Total wall clock time passed: 0.223291 ms

Could you please help me understand if this is a potential bug or if I might be misunderstanding something about how to properly use the tool?

Thank you for your time and assistance.