Conversation
|
@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? |
|
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. |
Co-authored-by: David Chocholatý <chocholaty.david@protonmail.com>
|
Current results for Z3-Noodler: 
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? |
If they are called from |
I meant inside Z3-Noodler, not in mata. We use |
|
I just read properly what you said. What should I call it with if I want to use the fast composition then? |
|
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. |
|
There seems to be some problem with the new composition. When I take this automaton: 
And compose it with this NFT (using 
I get this: 
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 
|
| } | ||
| return algorithms::compose_fast_no_jump(lhs, rhs, lhs_sync_levels.front(), rhs_sync_levels.front(), project_out_sync_levels); | ||
| case CompositionMode::Auto: | ||
| if (jump_mode == JumpMode::NoJump && lhs_sync_levels.size() == 1) { |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
I see the confusion this can cause.
The previous if statement lhs_sync_levels.size() != 1 || rhs_sync_levels.size() != 1 is there to throw an early exception, since FastNoJump can only be used when the number of sync levels is exactly 1. It does not check whether the number of sync levels matches between lhs and rhs (that case would be an error and is handled by an assert in the composition).
The if statement jump_mode == JumpMode::NoJump && lhs_sync_levels.size() == 1
implicitly expects rhs_sync_levels to also have size 1, just like lhs_sync_levels. It could explicitly check this, but I left that validation to the composition assert.
We can either:
- add an explicit check and throw a "number of sync levels mismatch" error as in the case of the first if, or
- remove the condition
rhs_sync_levels.size() != 1from the previous if statement.
PS: We should consider whether to replace the assert that checks lhs_sync_levels and rhs_sync_levels have the same size with an exception.
There was a problem hiding this comment.
I would remove rhs_sync_levels.size() != 1 so it is not confusing. I would also add the check for the number of sync levels mismatch, either at the beginning of this general compose function, or at the beginning of the compose functions implementations.
There was a problem hiding this comment.
@jurajsic Do you want to act on this in a future PR?
You can ignore this problem, the first automaton had 2 levels instead of one, so there were jumps. That is why the no jump version did not work. |
|
Current results: 
The small differences stem from Z3' randomness I think, so we can ignore it. |
|
I think we can merge. |
|
Now it just needs rebasing onto devel... I feel like we should first squash those 70 commits, then try to rebase. |
3 participants
This PR introduces:
JumpMode–JumpMode::NoJump,Nft::unify_nondet_withthat did not update levels correctly,GeneralandFastNoJump), andcomposeandapplywithinreplace_reluctantandnoodlifyby passingJumpMode::NoJumpas thejump_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.