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.

[adl]

I came here to report the same problem: formula X(0) is realizable by any trace of length 1, but lisa outputs UNREALIZABLE.

From a very quick look around in the code, X(0) gets translated to the following WDBA:

but then the code that interprets this as a DFA fails to record state 0 as final.

void
compute_final_states(twa_graph_ptr A, set<unsigned>& finals)
{
	bdd p2 = bdd_ithvar(A->register_ap(ALIVE_AP));
	for(unsigned s = 0; s < A->num_states(); s ++)
	{
		for (auto& e: A->out(s))
		{
			if((e.cond & !p2) != bddfalse && s != e.dst)
			{
				finals.insert(s);
			}
		}
	}
}

The condition s != e.dst seems incorrect in this case. A state can be considered as final if it has an outgoing edge compatible with !alive and if it is reachable using only edges compatible with alive.