Re:Learn TLA+ (2018)
by pron on Monday February 24, 2020 @07:59AM
(#22403623)
> I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.
Really? I personally have checked quite elaborate TLA+ specifications with TLC, and I know others have, too. Sure, like all verification tools it's got its limits, but even for a complex distributed system spec, TLC could reasonably check it with, say, four nodes.
> I'd wager that is the chief reason why most programmers don't even begin to investigate it.
I'm not sure Spin is used more than TLA+ these days, especially when it comes to "mainstream" software.
Really? I personally have checked quite elaborate TLA+ specifications with TLC, and I know others have, too. Sure, like all verification tools it's got its limits, but even for a complex distributed system spec, TLC could reasonably check it with, say, four nodes.
> I'd wager that is the chief reason why most programmers don't even begin to investigate it.
I'm not sure Spin is used more than TLA+ these days, especially when it comes to "mainstream" software.