Composition without epsilon self-loops

[koniksedy]

This PR introduces:

• a new, more efficient way of computing the composition of two NFTs that does not use jump transitions,
• a third JumpMode – JumpMode::NoJump,
• an auxiliary function for creating a transition of length N,
• a fix for a bug in Nft::unify_nondet_with that did not update levels correctly,
• adds a dispatch function for composition that distinguishes between two composition modes (General and FastNoJump), and
• modifies calls to compose and apply within replace_reluctant and noodlify by passing JumpMode::NoJump as the jump_mode, because I believe that in these places the NFTs never contain jump transitions.

The new implementation of the composition works only on NFTs without jump transitions (with JumpMode::NoJump). Therefore, it does not need to unwind transitions or create local copies, unlike the general version of the composition. It also does not construct the “waiting loops” on zero-level states, which in the general version are used when the NFT cannot synchronize on epsilon and therefore has to wait.

[Adda0]

@koniksedy Hey, what is the status of this PR? We might potentially want to base our next research on what “shapes” of transducers are created by this composition approach. Are there any missing features left to implement in this PR?

[koniksedy]

There’s still a bug that needs to be fixed before it can be used. I haven’t had much time to work on it (I was also on vacation), but I can take a look at it. Hopefully, it should be done by the middle of next week.

But if you need a somewhat working version, you can use the commit 1282c59.

[jurajsic]

Current results for Z3-Noodler:

Benchmark transducer_plus
# of formulae: 91
--------------------------------------------------
tool                                ✅    ❌    time    avg    med     std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------------  ----  ----  ------  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-b9a6f44-a89bddc          43    48  316.44   7.36   0.31   15.35     39        4          0    40         8        0
z3-noodler-b9a6f44-ead2f90          44    47  431.10   9.80   0.31   21.63     40        4          0    36        11        0
z3-noodler-model-b9a6f44-a89bddc    42    49  291.56   6.94   0.43   15.51     38        4          0    40         9        0
z3-noodler-model-b9a6f44-ead2f90    44    47  435.24   9.89   0.49   21.31     40        4          0    37        10        0
--------------------------------------------------

There seems to be some formulae where there is degradation, but it is probably coming from Z3 randomness.

I called composition and apply with the default arguments, I assume it will automatically select the correct (no) jump mode?

[koniksedy]

I called composition and apply with the default arguments, I assume it will automatically select the correct (no) jump mode?

If they are called from replace_reluctant or noodlify, then yes. Otherwise, the no jump mode is not set and a slow composition is used.
PS: There is no apply call in those functions.

[jurajsic]

I called composition and apply with the default arguments, I assume it will automatically select the correct (no) jump mode?

If they are called from replace_reluctant or noodlify, then yes. Otherwise, the no jump mode is not set and a slow composition is used. PS: There is no apply call in those functions.

I meant inside Z3-Noodler, not in mata. We use apply there (and also compose I think). So if we do not set the jump mode argument, it can create jumps?

[jurajsic]

I just read properly what you said. What should I call it with if I want to use the fast composition then? mata::nft::JumpMode::NoJump?

[koniksedy]

Yes. Then it will automatically select the fast composition. But it is your responsibility to ensure that the provided transducers have no jumps (epsilon jumps are OK).

Also, there needs to be exactly one synchronization level at each transducer (LHS and RHS). If there are more synchronization levels (e.g., 1 and 3 on the LHS and 2 and 5 on the RHS), then the slower, more general composition is also selected.

[jurajsic]

There seems to be some problem with the new composition. When I take this automaton:

@NFT-explicit
%Alphabet-auto
%Initial q0 q2 q3
%Final q1
%Levels q0:0 q1:0 q2:0 q3:0
%LevelsNum 2
q0 50 q1
q1 50 q1
q1 51 q1
q1 52 q1
q2 51 q1
q3 52 q1

And compose it with this NFT (using mata::nft::compose(nfa, nft, 0, 0, true, mata::nft::JumpMode::NoJump):

@NFT-explicit
%Alphabet-auto
%Initial q0
%Final q0
%Levels q0:0 q1:1 q2:1 q3:0 q4:1 q5:0 q6:1 q7:0 q8:1 q9:1 q10:1 q11:1
%LevelsNum 2
q0 48 q1
q0 49 q2
q0 50 q4
q0 51 q8
q0 52 q10
q0 196608 q11
q1 48 q0
q2 49 q0
q3 4294967295 q6
q4 48 q3
q5 4294967295 q2
q6 49 q5
q7 4294967295 q9
q8 48 q7
q9 48 q5
q10 49 q3
q11 196608 q0

I get this:

@NFT-explicit
%Alphabet-auto
%Initial q0 q1 q2
%Final q12
%Levels q0:0 q1:0 q2:0 q3:1 q4:1 q5:1 q6:0 q7:0 q8:1 q9:0 q10:1 q11:1 q12:0
%LevelsNum 2
q0 50 q3
q0 51 q3
q0 52 q3
q1 50 q4
q1 51 q4
q1 52 q4
q2 50 q5
q2 51 q5
q2 52 q5
q3 48 q6
q4 48 q7
q5 49 q6
q6 4294967295 q8
q7 4294967295 q10
q8 49 q9
q9 4294967295 q11
q10 48 q9
q11 49 q12
q12 50 q3
q12 50 q4
q12 50 q5
q12 51 q3
q12 51 q4
q12 51 q5
q12 52 q3
q12 52 q4
q12 52 q5

There are too many transitions coming from the initial states, for example the symbol (52,48) should not be allowed as the first symbol of any accepted word.

The previous composition (run as mata::nft::compose(nfa, nft, 0, 0, true, mata::nft::JumpMode::RepeatSymbol) returns (seemingly) correct result:

@NFT-explicit
%Alphabet-auto
%Initial q0 q1 q2
%Final q8
%Levels q0:0 q1:0 q2:0 q3:1 q4:0 q5:1 q6:0 q7:1 q8:0 q9:1 q10:1 q11:0 q12:1 q13:1 q14:1 q15:1
%LevelsNum 2
q0 50 q15
q1 51 q14
q2 52 q3
q3 49 q4
q4 4294967295 q5
q5 49 q6
q6 4294967295 q7
q7 49 q8
q8 50 q13
q8 51 q10
q8 52 q9
q9 49 q4
q10 48 q11
q11 4294967295 q12
q12 48 q6
q13 48 q4
q14 48 q11
q15 48 q4

[jurajsic]

Should there also be check for rhs_sync_levels.size() == 1? In the previous case (CompositionMode::FastNoJump) there is a check for bot lhs and rhs.