VeriFIT / mata

A fast and simple automata library
MIT License
20 stars 13 forks source link

Refactor string solving operations #398

Closed Adda0 closed 6 months ago

Adda0 commented 6 months ago

This PR allows inserting word from states with levels different from 0. The level to start from is read from the source since the source must already exist in the NFT anyway. No need for an additional parameter.

Furthermore, the PR applies this improvement in some string operations. Further PRs to simplify the string operation functions will come in the future.

Adda0 commented 6 months ago

@koniksedy Could you have a look at the changes to insert word and see whether all looks good?

Adda0 commented 6 months ago

Hmm, never mind. Something broke. Wait with the review until I resolve the issue, please.

koniksedy commented 6 months ago

Hmm, never mind. Something broke. Wait with the review until I resolve the issue, please.

Too late. :smile: Overall, it looks good to me. I only have minor comments.

Adda0 commented 6 months ago

The reason it broke is that the latest changes to insert_identity() allowed for symbol jump transitions. Previously we agreed that transducers will not have symbol jump transitions, so I implemented the whole of string operations on NFTs with this assumption. When operations start adding symbol jump transitions, everything breaks. Therefore, I will disable creating symbol jump transitions in create_identity() for now. The operations that we implement may support them, but no operation should create them for now. When there is time to refactor the string solving, These symbol jump transitions can be enabled again.

codecov[bot] commented 6 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 74.31%. Comparing base (5a94d88) to head (85d9cc8). Report is 1 commits behind head on states_with_levels.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## states_with_levels #398 +/- ## ====================================================== - Coverage 74.51% 74.31% -0.20% ====================================================== Files 43 43 Lines 5509 5474 -35 Branches 1221 1213 -8 ====================================================== - Hits 4105 4068 -37 - Misses 958 964 +6 + Partials 446 442 -4 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

Adda0 commented 6 months ago

What do you think about the temporary fix for symbol jump transitions?

koniksedy commented 6 months ago

The operations that we implement may support them, but no operation should create them for now.

Well, then I have bad news for you. The function nft::insert_levels() does the exact same thing. It uses jump transitions to simplify the transducer. Thought, this behavior will not show on transducers with up to 2 levels, so your implementation should be fine, we need to keep it in mind.

Adda0 commented 6 months ago

I noticed, but as you said, unless one is creating an identity from level 0 to level 0, it does not matter for string solving. I will make a note to resolve this in the future, however.

koniksedy commented 6 months ago

OK. We can merge the PR.