3 ms·
> You're confusing TLC with TLA+. True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+. >
by sriram_malhar 7y ago
> You're confusing TLC with TLA+.
True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.
> TLA+ is not "too abstract". It is mathematics.
I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.
- pron 7y ago> 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.