I think of the two P-lang probably has a brighter future. I don't know how many people are working on Spin besides Holzmann, while P has a lot of institutional support and development budget at AWS.
Sorry to disagree. I've put about 10 hrs into a P Lang model I started in spin. My experience so far: it's finicky, documentation subpar, missing basic operators (bitwise), cumbersome dragging in donet as a install prereq. I've sent all this to p-org.git.
Yes spin is older ... but it's the complete opposite: far far far better documented including books from springer Verlag (several) + 10s and 10s of academic articles on same.
C/c++/Unix are all older. Nobody denigrates them for age alone. Likewise spin cannot be knocked soley on age. This isnt the fashion sector. Good engineering then remains good now. State exploration + ltl if done right doesnt have a expiration date.
Spin btw has numerous optimizations for state exploration i don't think P or tla have. Maybe Amazon's internal tooling is better. But p-org.git is not mature stuff.
