Add residual reduction algorithm

[notValord]

Two implementations of residual reductions were added to the reduction function. There is possible parametrization using the ParameterMap to select the type of implementation and its direction. The types differ in whether the construction of residual automaton is done after the final determinization or during. Generally the algorithm of residual reduction consist of backward determinization followed by forward residual construction, which can be described as a determinization with removal of covered states. For backward canonical residual automaton the direction of these operations are revered. Both implementations had similar results in effectivity and the result automata are mostly the same, but the approaches may provide further inspiration and different optimizations.

However, we were not able to find a way to utilize StateRenaming as it is done for simulation, as for residual reduction the automaton is reverted and determinized twice and there is no possible direct connection between the state of the original and tthe result automaton. For this reason, the parameter is not used. We are not sure how to modify the general interface for automata reduction, so that it would suit different algorithms and would appreciate any opinions on this topic.

Testing of this new functionality is also provided on various-sized automaton, checking the result construction. In every case, the size of both approaches should be the same(applies only for the same direction) and on some automata the results are identical.

[Adda0]

Hello. Thank you for the PR. Hopefully we will be able to have a look at it in a reasonable timeframe.

Have a look at the issues raised by Codacy. Otherwise, at a first glance, things look good to me.

Will there be any additional subsequent PRs? How urgently do you need this PR to be merged?

[notValord]

Hi, thanks for the quick response, I checked the Codacy issues, quickly fixed the discovered memory leak and will rework the other issues as well, however there still will be the unused variable problem as it was mentioned in the initial commit.

The PR is not urgent, just wanted to put up something so that if there will be any problems that would need reworking I could address them as soon as possible. For now there won't be any additional PRs, but I would also like to add reduction utilizing SAT and QBF solvers, but that is another whole feature so maybe it could be addressed in another PR in the future.

[Adda0]

Great. Thank you.

so maybe it could be addressed in another PR in the future.

Definitely. If this PR is still open then (hopefully not) and the next PR is depending on it, just stack the other PR onto this current one and the new PR will be rebased onto master once this PR is merged.

[ondrik]

Thanks @notValord for opening the PR. I wanted to raise the issue of a good interface for various reduction operations in mata. Currently, the interface is

void reduce(Nfa* result, const Nfa &aut, StateRenaming *state_renaming = nullptr,
                   const ParameterMap& params = {{ "algorithm", "simulation"}}) {

where state_renaming only makes sense for some algorithms. Even for simulation, the current parameter value simulation could be improved (e.g., should it be forward simulation? backward simulation? iterate? etc.)

Any ideas?

Ondra

[Adda0]

I wanted to raise the issue of a good interface for various reduction operations in mata.

I think it would be better to not pollute the discussion about this PR with our favourite discussion about interfaces (which we should really try to resolve...). There are already two issues open which raise these issues (#197 and #113), and we should discuss there how to ideally improve the interface. If we come to a conclusion, the appropriate changes will have to be implemented in another PR, anyway, since it will break all dependant projects that I know of.

[vhavlena]

I am not involved in this PR (thanks for that), but if there is someone who puts some nontrivial effort in an extension of Mata's functionality, we could do something more than just to ignore it. Everyone is super-busy with various stuff I know. Maybe we could think about a refinement of the reviewing process.

[ondrik]

I'm adding some graphs for performance and effectivity comparison with the simulation currently used in reduce for reference

[Adda0]

Hello, @notValord. What is the current status of this PR? Have you addressed all the discussions from above, or are you planning to work on anything some more? Is there anything left unresolved?

Feel free to resolve the conversations that you have already addressed.

[notValord]

Sorry for the late reply, yes all of the mentioned discussions should be resolved now, mostly forgot to resolve them at the time. There is no additional work planned on this PR so if everything checks out then it should be good to be merged and closed.

[Adda0]

Great. I already talked to @ondrik who agrees with merging the PR. Therefore, once the tests pass, I will merge the PR. Thanks for the PR and your help with resolving the suggested issues.