VeriFIT / mata

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

Implement class `Levels` inheriting from `std::vector<Level>` #390

Closed Adda0 closed 7 months ago

Adda0 commented 7 months ago

This PR implements class levels inheriting from std::vector<Level> which adds a convenience function Levels::set(State, Level) which allows for easier setting of levels for new states.

Furthermore, this PR also renames and retypes Level Nft::levels_cnt to size_t Nft::num_of_levels. I decided to go against the idea of moving this variable into the Levels class. It became confusing how to get the number of levels (tracks) in the transducers (Nft::num_of_levels) and how to get the number of elements in the Levels Nft::levels class (Levels::size()):

Nft nft{};
// ...
if (nft.levels.num_of_levels != 2) { 
// ...
} else if (nft.levels.size() != 3) {
// ...
}

I think having these separate will make the distinction more clear:

Nft nft{};
// ...
if (nft.num_of_levels != 2) { 
// ...
} else if (nft.levels.size() != 3) {
// ...
}

What do you think about this? Should num_of_levels be a member of Levels?

Due to time constraints, the PR will be merged immediately. I ask the reviewers to do their reviews in their own time and any issues raised in the reviews will be resolved in later PRs.

Furthermore, the PR fixes compilation of Mata on GitHub Actions.

codecov[bot] commented 7 months ago

Codecov Report

Attention: Patch coverage is 91.17647% with 6 lines in your changes are missing coverage. Please review.

:exclamation: No coverage uploaded for pull request base (states_with_levels@3447f4d). Click here to learn what that means.

Files Patch % Lines
src/nft/operations.cc 73.33% 1 Missing and 3 partials :warning:
src/nft/nft.cc 93.93% 2 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## states_with_levels #390 +/- ## ===================================================== Coverage ? 73.63% ===================================================== Files ? 43 Lines ? 5150 Branches ? 1166 ===================================================== Hits ? 3792 Misses ? 921 Partials ? 437 ```

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

koniksedy commented 7 months ago

Overall, the implementation of the Levels class looks good to me. I also agree with the idea of keeping Nft::num_of_levels as an attribute of the Nft class.

However, does the Levels class prevent accessing the level of a state that is out of its range? This could potentially happen, and in that case, I would expect Levels to return DEFAULT_LEVEL.

Additionally, why not simply override the [] operator instead of creating a method Levels::set(State, Level)?

Adda0 commented 7 months ago

Additionally, why not simply override the [] operator instead of creating a method Levels::set(State, Level)?

The main idea here is that Levels::operator[]() is the most performant way to access or change a state if you know it already exists. This follows the standard implementation of STL containers. If you want to optionally handle adding states into Nft::levels and expanding the vector, a slower function set(State, Level), which performs checks and potentially allocates memory, can be used.

However, does the Levels class prevent accessing the level of a state that is out of its range? This could potentially happen, and in that case, I would expect Levels to return DEFAULT_LEVEL.

That did not work without the class either. It is a design decision, but I think you are right that, taking an inspiration from Nfa::StatePost, we can implement a similar approach here. I consider this a TODO for when there is some spare time. What do you think?

koniksedy commented 7 months ago

On second thought, the implementation that allows access to a state level not present in Levels could lead to unusual behavior. This situation can only occur when requesting a level of a state that was not created using the add_state method or its variants. This seems more like a programmer's error and, therefore, should raise an exception.