It is kind of awesome that you can alter the
algorithm and immediately look at the
counter example (problem you just created).
spin_fan 10 hours ago [-]
Spin is a great learning tool. Spin is
so much more accessible than TLA+ Toolbox, for instance.
But for really serious work, there are
much more modern approaches that exploit
SMT solvers like Z3 (as TLA+ does) for vastly more
powerful model checking than Spin offers.
Also, the creator of Spin has retired it seems;
email to the spin list bounces. The "community"
forum has not accepted registrations for
several years. Basically it seems Spin was
a one man show, and he has not passed the
torch onto anyone else. The tool is still
incredible though, and a great place to start.
Just don't expect any help if you get stuck.
Get the Spin book if you want to understand
all the options.
Here, for example, EPR is a vastly more powerful formalism:
I just watched this video from 2017 work,
and was blown away. They can model check
FULL Vertical Paxos (not just a single round
of Synod) in that same couple of seconds;
that was done for the first time in this paper.
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017.
My writeup/getting started guide here (for checking Paxos) https://github.com/glycerine/spin_paxos
It is kind of awesome that you can alter the algorithm and immediately look at the counter example (problem you just created).
But for really serious work, there are much more modern approaches that exploit SMT solvers like Z3 (as TLA+ does) for vastly more powerful model checking than Spin offers.
Also, the creator of Spin has retired it seems; email to the spin list bounces. The "community" forum has not accepted registrations for several years. Basically it seems Spin was a one man show, and he has not passed the torch onto anyone else. The tool is still incredible though, and a great place to start. Just don't expect any help if you get stuck. Get the Spin book if you want to understand all the options.
Here, for example, EPR is a vastly more powerful formalism:
I just watched this video from 2017 work, and was blown away. They can model check FULL Vertical Paxos (not just a single round of Synod) in that same couple of seconds; that was done for the first time in this paper.
Paxos Made EPR: Decidable Reasoning about Distributed Protocols Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017.
(pdf) https://arxiv.org/pdf/1710.07191.pdf
(video) https://youtu.be/_suyrSMJeCo
(from the first author's homepage)