search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
429 stars 40 forks source link

Apalache and TLC Performance comparison #2203

Closed niuzhi closed 1 year ago

niuzhi commented 1 year ago

hello author I'm really doing apalache vs tlc to verify performance with large state space. From the article "TLA+ Model Checking Made Symbolic", I saw the author's comparison of apalache and tlc in verifying invariants. The comparison results are as follows. May I ask where can I get the apalache and tlc verification codes and configure file of the relevant protocols or algorithms? image

Secondly, how to adjust the steps when performing apalache verification, because the state in tlc is to search until the end of the search, which is a clear stop signal. In apalache, I don't know how many steps to adjust to verify all the states. Now the default steps are 10. How to adjust steps so that it can verify all states of the specification?

Kukovec commented 1 year ago

Hi, and thanks for reaching out! The artifacts associated with the paper can be found here: https://zenodo.org/record/3370063#.Y0VVaewWMUQ Note, however, that the current version of Apalache is different in many ways, and may not be compatible with the old files (though the artifact contains a VM with the old version and you should be able to run it as-is). If you're going to run experiments with Apalache, I'd strongly recomment looking at the current version, though: https://apalache.informal.systems/docs/index.html

Regarding your second question, this shows results for verifying inductive invariants. For those, you need to run Apalache twice, once with --length=0 --init=Init --inv=Inv (where Init is your initial state predicate and Inv your inductive invariant), and once with --length=1 --init=Inv --inv=Inv. Inductive invariants can be verified in one step of bounded model checking. If you're not verifying inductive invariants, its up to you to decide what a reasonable exploration depth is, as bounded model checking is generally incomplete.

niuzhi commented 1 year ago

@Kukovec Thank you very much for your reply. I can understand that apalache is better than tlc in verifying induction invariants, but if it is some state invariants, it may be necessary to adjust the steps to obtain the verification results

Kukovec commented 1 year ago

Since you don't seem to have an issue with the model checker itself I'm going to convert this into a discussion and/or close the issue. Please let us know if you have more questions.