3 ms·

The tool is also pretty abysmal at telling you why it can’t parse the thing you wrote. For me that was the reason #1 it’s hard to learn. The other reason I don

The tool is also pretty abysmal at telling you why it can’t parse the thing you wrote. For me that was the reason #1 it’s hard to learn. The other reason I don’t use it is that it’s very hard to inspect what you’re running. You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. It makes it really hard to convince yourself (and your peers) you haven’t assumed all of the state away.

pron 5y ago
> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818 https://youtu.be/TP3SY0EUV2A?t=818 But there often are easier ways to do sanity checks to "convince yourself you haven’t assumed all of the state away," usually either by asserting something believed to be false or by intentionally introducing an error in the spec, and letting TLC find a counterexample.
- smallpipe 5y ago
  I agree it’s workable, but it’s a bit of a hack. Commercial formal verification software for RTL has this built-in, and once you have 10+ people updating a spec, you need an automated way of checking for accidental constraints.
  - pron 5y ago
    I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. A mistake that could be automatically checked is specifying a system that is equivalent to FALSE (and so implies anything). I hope TLC adds a feature that allows you to check if your system implies FALSE. In the meantime, checking the invariant ¬Init has the same effect.
thisiscorrect 5y ago
TLA+ as a formal language for specifying systems is quite good. But the quasi-official toolchain for working with it [1] including TLC and the sanitizer are not well maintained. They were pretty resistant to outside contributions when I tried. I have hope that a better toolchain for working with the TLA+ language can come along. The underpinning language is well designed. Lamport is no slouch. [1] https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus
- noblethrasher 5y ago
  TLA+ really is quite nice. I write most of my TLA+ specifications longhand and only bother with the toolbox when I think that refinement might be useful. Even then, it's mostly for SANY rather than TLC. After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.

pron 5y ago

> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818 https://youtu.be/TP3SY0EUV2A?t=818 But there often are easier ways to do sanity checks to "convince yourself you haven’t assumed all of the state away," usually either by asserting something believed to be false or by intentionally introducing an error in the spec, and letting TLC find a counterexample.

smallpipe 5y ago
I agree it’s workable, but it’s a bit of a hack. Commercial formal verification software for RTL has this built-in, and once you have 10+ people updating a spec, you need an automated way of checking for accidental constraints.
- pron 5y ago
  I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. A mistake that could be automatically checked is specifying a system that is equivalent to FALSE (and so implies anything). I hope TLC adds a feature that allows you to check if your system implies FALSE. In the meantime, checking the invariant ¬Init has the same effect.

thisiscorrect 5y ago

TLA+ as a formal language for specifying systems is quite good. But the quasi-official toolchain for working with it [1] including TLC and the sanitizer are not well maintained. They were pretty resistant to outside contributions when I tried. I have hope that a better toolchain for working with the TLA+ language can come along. The underpinning language is well designed. Lamport is no slouch. [1] https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus

noblethrasher 5y ago
TLA+ really is quite nice. I write most of my TLA+ specifications longhand and only bother with the toolbox when I think that refinement might be useful. Even then, it's mostly for SANY rather than TLC. After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.