4 ms·
Loved the article. Well written. I'm working on a formal model now and I'm playing with spin and p-lang to see which is better. Not a fan of tla+
by scrubs 1y ago
Loved the article. Well written.
I'm working on a formal model now and I'm playing with spin and p-lang to see which is better. Not a fan of tla+
- hwayne 1y agoI 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.
- scrubs 1y agoSorry 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.