We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
The text was updated successfully, but these errors were encountered:
No branches or pull requests
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.
The text was updated successfully, but these errors were encountered: