Hopcroft's minimization: Valmari and Lehtinen's variant for a partial transition function

[koniksedy]

This PR introduces the implementation of Valmaria and Lehtinin's variant of Hopcroft's minimization of deterministic finite automata with partial transition function.

The performance of this reduction method was tested against Brzozowski's minimization and simulation on determinized automata obtained from:

1. Abstract Regular Model Checking,
2. automata generated during the decision process of WS1S logic,
3. automata for regular expressions sourced from RegexLib,
4. automata for regular expressions used in email validation obtained as in MFPS'17 and in APLAS'21,
5. automata for string constraints derived from Norn and SyGuS-qgen and Others, and
6. Tabakov-Vardi random automata.

Timeouts

The timeout was set to 10 seconds.

Method	Timeout Count
Brzozowski	2,167
Simulation	2,308
Hopcroft	481

All Benchmarks

It can be seen that Hopcoroft's algorithm is, on average, 100x faster than Brzozowski or the simulation.

Cactus Plot

Scatter Plot Matrix

Abstract Regular Model Checking

Cactus Plot

Scatter Plot Matrix

WS1S logic

These automate have a binary alphabet.

Cactus Plot

Scatter Plot Matrix

RegexLib

Cactus Plot

Scatter Plot Matrix

Email Validation

Cactus Plot

Scatter Plot Matrix

Norn and SyGuS-qgen and Others

Cactus Plot

Scatter Plot Matrix

Tabakov-Vardi

Automata were generated with 10, 50, 100, and 200 states, for alphabets containing 2, 4, 8, and 16 symbols, and with a transitions-to-states ratio per symbol ranging from 0.1 to 1.

Cactus Plot

Scatter Plot Matrix

[codecov]

Codecov Report

Attention: Patch coverage is 94.77612% with 7 lines in your changes missing coverage. Please review.

Project coverage is 74.46%. Comparing base (a45f104) to head (094ad6a).
Report is 20 commits behind head on devel.

Files with missing lines	Patch %	Lines
src/nfa/operations.cc	94.77%	0 Missing and 7 partials ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##            devel     #475      +/-   ##
==========================================
+ Coverage   73.67%   74.46%   +0.78%     
==========================================
  Files          30       30              
  Lines        4251     4413     +162     
  Branches      968     1003      +35     
==========================================
+ Hits         3132     3286     +154     
- Misses        771      772       +1     
- Partials      348      355       +7     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[jurajsic]

That looks really good!

Just to be safe, can you also compare the size of minimized automata by Brzozowski and Hopcroft? If they are actually always same.

Also, maybe we should make it the default minimization algorithm (for the dispatcher function, if we have it + maybe have two versions of the dispatcher function, one take nfa, one dfa).

[Adda0]

Also, maybe we should make it the default minimization algorithm (for the dispatcher function, if we have it + maybe have two versions of the dispatcher function, one take nfa, one dfa).

I agree. Maybe we should have minimize() and minimize_dfa()?

Or even better, minimize() which has a enum class flag AutomatonType with possible values NFA and DFA, by default NFA. And two underlying functions called from this function minimize_nfa() and minimize_dfa(). This would solve all the issues, would be extensible, and allow for reusing the enum class for other functions as well.

[koniksedy]

Just to be safe, can you also compare the size of minimized automata by Brzozowski and Hopcroft? If they are actually always same.

I've already tested it. Apart from Brzozowski creating (for some reason) an automaton with one initial state for an empty automaton, the automata are indeed the same in language and size.

[Adda0]

The PR looks great. When we finish the discussion regarding the interface, I will approve and merge the PR.

[jurajsic]

Looks good to me, I would still make it a default minimization algorithm, but that can be further PR.