Allow skipping minimization when transition count > MAX_INT (was "NegativeArraySizeException in ValmariDFA")

[pierreganty]

Dear devs,

I was running Walnut with the following pc6 predicate and it crashed close to completion.
To reproduce you need time (i.e. couple of hours) and a lot of memory (I ran Walnut with -Xmx128G).

eval pc6 "?lsd_2 (0 <= v0 & 0 <= v1 & 0 <= v2 & 0 <= v3 & 0 <= v4 & 0 <= v5 & 2 * v1 + 2 * v2 + 2 * v3 + 2 * v4 + 2 * v5 <= 40 * v0 & 3 * v0 + 3 * v2 + 3 * v3 + 3 * v4 + 3 * v5 <= 39 * v1 & 5 * v0 + 5 * v1 + 5 * v3 + 5 * v4 + 5 * v5 <= 37 * v2 & 7 * v0 + 7 * v1 + 7 * v2 + 7 * v4 + 7 * v5 <= 35 * v3 & 11 * v0 + 11 * v1 + 11 * v2 + 11 * v3 + 11 * v5 <= 31 * v4 & 13 * v0 + 13 * v1 + 13 * v2 + 13 * v3 + 13 * v4 <= 29 * v5 & 1 <= v0 + v1 + v2 + v3 + v4 + v5)" ::

Walnut reached a stage where it completes an &-product thereby generating an automaton with a bit more than 58 millions states.
Then Walnut runs the minimization procedure for that large automaton, where it crashes almost immediately.
I suspect there is an integer overflow when computing the number of transitions in ValmariDFA.java:

             // Pre-size the arrays.
        for(int q = 0; q != dfaD.size();++q){
            numTransitions += dfaD.get(q).keySet().size();
        }

After the loop numTransitions contains a negative value, hence the exception when declaring T right after.

Below I pasted the output of the crash I obtained:

                        Minimizing: 58138358 states.
java.lang.NegativeArraySizeException: -574112384
        at Automata.FA.ValmariDFA.<init>(ValmariDFA.java:51)
        at Automata.FA.FA.justMinimize(FA.java:877)
        at Automata.FA.ProductStrategies.crossProductAndMinimize(ProductStrategies.java:211)
        at Automata.AutomatonLogicalOps.and(AutomatonLogicalOps.java:55)
        at Token.LogicalOperator.act(LogicalOperator.java:74)
        at Main.Computer.compute(Computer.java:77)
        at Main.Computer.<init>(Computer.java:49)
        at Main.Prover.eval_def_commands(Prover.java:584)
        at Main.Prover.processCommand(Prover.java:457)
        at Main.Prover.dispatch(Prover.java:391)
        at Main.Prover.readBuffer(Prover.java:314)
        at Main.Prover.run(Prover.java:280)
        at Main.Prover.main(Prover.java:261)
java.lang.RuntimeException: -574112384
        : char at 351
        at Main.Computer.compute(Computer.java:95)
        at Main.Computer.<init>(Computer.java:49)
        at Main.Prover.eval_def_commands(Prover.java:584)
        at Main.Prover.processCommand(Prover.java:457)
        at Main.Prover.dispatch(Prover.java:391)
        at Main.Prover.readBuffer(Prover.java:314)
        at Main.Prover.run(Prover.java:280)
        at Main.Prover.main(Prover.java:261)

[dvberkel]

@pierreganty Thanks for reporting the bug.

We are in the process of setting up an community and a way of working. We haven't have a clear idea when we will be able to address the problem you are experiencing.

You could join us on Discord to join in the discussions

[jn1z]

Hi Pierre,

Thanks for the bug report!

Unfortunately it seems you've hit a hard limit in Walnut.
Even if this was converted to a long (to avoid the integer overflow), Java can't handle arrays above Integer max, so the next line would fail.

However, the transition count could be validated, allowing Walnut to fail quicker with a friendly message.

BTW, if this was a quantification step, I might suggest experimental determinization options other than SC. But Product Construction generally doesn't minimize much at all.

[pierreganty]

I would not mind that after realizing Walnut can't apply minimization, it just skips that step and carries on.
In my particular use case (the pc6 predicate), Walnut would skip minimization, write the non-minimized automaton on file and return to the prompt.

[jn1z]

I'll take a look and see if that's feasible. Unfortunately it's not as simple as just skipping minimization, since for purposes of memory optimization, the routines are not separate.

[jn1z]

Sorry, I do not see a robust way to ignore minimization when there's array overflow. Minimization is additionally converting the DFA structure into an NFA structure, which is used after minimization is finished.

It's possible this could be revisited when there's a clean separation between DFA and NFA in the code.

BTW, most users would want this to fail early (and in fact if it wasn't the last command, that would probably be best in this scenario too).

[shallit43]

This isn't really the kind of problem that Walnut is designed to be useful for, for two reasons: it's only using Presburger arithmetic, not Buchi arithmetic, and it's not using any quantifiers. Walnut was designed to be useful for quantified statements in the larger logic of Buchi arithmetic; it is not optimized for the question you posed. By the way, there is no need at all to include statements like v1 >= 0, because the default domain for integers in Walnut is the non-negative integers, so this does nothing at all.

I suggest you look into Integer Programming packages, which are specifically designed to handle systems of linear equations and inequalities. I am not familiar with what is available, although I did find this paper: https://www.csd.uwo.ca/~mmorenom/Publications/The_Z_Polyhedra_library_in_Maple.pdf

[pierreganty]

Thanks for your input, Jeffrey. We are aware that we are not using Walnut the way it was intended, and you are correct that there are better tools out there for Presburger arithmetic (PA) formulas or even QF_LIA formulas like the one I posted.
However, we are primarily interested in the automata-based approach applied to QF_LIA, and it turns out that Walnut is a state-of-the art tool for that application domain. The competitors we are aware of are LASH (last release is more than 2 decades old), and Amaya from CAV'24.
On the above example, Amaya returns no results after 6 days of compute time, but Walnut manages to compute an automaton with 50+ millions states within hours. That is the only tool we are aware of that can reach such a high number, hence we are interested in it.

[jn1z]

Very interesting, @pierreganty , thank you. I wondered if Amaya wasn't always as performant as advertised ;-)

Don't know if we have this capability with GitHub issues, but I consider this dependent on fixing #25 (that is a pretty large task, however).
At that point, this would be as simple as returning instead of minimizing.