Hang Loop

[jskt89]

Hi.

For this formula, the memory behavior is unpredictable, as usually.

However, It runs for more than 24 hours in my conventional desktop (Core i7, 16Gb of memory, and SSD), and the execution does not end.

The formula 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))) & (((!g2) | (((!r2) & (g2)))))))))))

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

Thank you for your attention.