nft/composition(fix): Skip recomputing synchronization types

[Adda0]

Skips recomputing synchronisation types of targets of transitions from states already computed.

Fixes #670. Fixes VeriFIT/z3-noodler#398.

[Adda0]

@koniksedy Does this make sense? There are two transitions over symbols that cause get_synchronization_types() to push the state 6 onto the stack twice. The first time it is popped, its successors are computed; the second time it is popped from the stack, it tries to compute the successors again.

"q0 48 q5\n"
"q0 49 q5\n"

I am, however, not sure how it could have ever worked before.

[koniksedy]

I definitely agree that this is a bug.

The proposed fix will work, but we should probably avoid pushing the same state onto the stack in the first place. I'm not sure whether that can be checked efficiently when pushing.

As for the question, "How could it ever work?": we probably hadn't worked with transducers where a state had multiple transitions to the same target. Also, the root state is pushed onto the stack only once, regardless of the number of outgoing transitions, which likely masked this issue.

[koniksedy]

I looked into it again, and I don't think it's worth carrying additional information about whether a state is already on the stack. Skipping states that appear on the stack multiple times is the appropriate fix. It just needs a comment explaining why this is necessary.

[Adda0]

Then we could merge this now and later consider an optimisation that properly fixes the root cause, not just mitigates the symptoms.

[Adda0]

Ah, OK. Wilco.