Exception thrown

[jskt89]

Dear,

I run Black on the top of some experiments around LTL. In the process we've found the following bug in the experiment:

Blacks run many hours (4h) and throw the message: Killed.

My manual analysis shows a non-explaneable behaviour to request memory. Among them, the execution continuously increases the memory space.

However, Black often stabilizes the memory request. By the Black design, I consider that the pruning rules reduce the memory stored during the execution, and then I consider it as the potential root cause.

The input is:

((!r1) & (!r2) & (!g1) & (!g2) & (G(((F(!r1)) | (F(!g1))))) & (G(((F(!r2)) | (F(!g2))))) & (G(((X(!g1)) | (X(!g2))))) & (((g1) | (X(g2)) | (F(G(((r1) | (g2))))))) & (G(((F(((r1) & (g1)))) | (F(((!r1) & (!g1))))))) & (G(((F(((r2) & (g2)))) | (F(((!r2) & (!g2))))))) & (G(((((r1) & (X(r1)))) | (((!r1) & (X(!r1)))) | (((((r1) | (!g1))) & (((!r1) | (g1)))))))) & (G(((((r2) & (X(r2)))) | (((!r2) & (X(!r2)))) | (((((r2) | (!g2))) & (((!r2) | (g2)))))))) & (G(((((g1) & (X(g1)))) | (((!g1) & (X(!g1)))) | (((((r1) | (g1))) & (((!r1) | (!g1)))))))) & (G(((((g2) & (X(g2)))) | (((!g2) & (X(!g2)))) | (((((r2) | (g2))) & (((!r2) | (!g2)))))))))

I ran in the versions 0.92, 0.74, and 0.52. My computer is a conventional desktop: Core i7, 16Gb of memory, and SSD.

If you need to have additional information (e.g., I have other inputs with the same behaviour). Let me know.

By the way, thank you for the new LTL solver.

[nicola-gigante]

Hi, thanks for reporting!

BLACK's memory usage is a bit unpredictable because it depends on many things: the length of the models for satisfiable formulas, or the depth of the tableau tree for unsatisfiable ones; the size of the encoding formulas and their effect on the underlying SAT solver.

I do not have a ready recipe to solve these cases, unfortunately.

Do you expect this formula to be satisfiable or not? If yes, do you have an idea of how long should the model be?

[jskt89]

Hello Nicola.

I checked with other solvers and the answer is UNSAT. However, I do not have an estimation of the model.

Thank you for your attention.

[nicola-gigante]

Hi, which solvers did you try?

[jskt89]

Hello again,

I tried NuSMV (BDD) and PLTL (BDD and tableau).

[nicola-gigante]

Tha's interesting, because a long running time for BLACK on an UNSAT formula suggests that the formula has a large tableau, but if PLTL terminates earlier, this is not the case. I'll have a deeper look, although I cannot make promises on the time :)

[jskt89]

Thank you again for the attention.