3 ms·

Always love seeing more examples of TLA+ in action! > One really nice feature of TLC is that (unlike a fuzz tester) it does a breadth-first search and therefor

Always love seeing more examples of TLA+ in action! > One really nice feature of TLC is that (unlike a fuzz tester) it does a breadth-first search and therefore finds minimal counter-examples for invariants. It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC.

im_down_w_otp 8y ago
It seems like an odd comparison though. Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. Making even moderately complex TLA+ models or minor iterations on a simple model's depth of representation often results in exploding the search space for TLC and consequently the time to perform checking. Both classes of tools are useful, but the comparison seemed odd since you wouldn't use TLA+ like a fuzzer, nor vice versa.
- pron 8y ago
  > Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. TLC checks the TLA+ specification, however detailed it is. In practice, it's true that it is usually much more useful to specify at a level well above the code, but it could be at the same abstraction level as the code (the specification could even be mechanically generated from the code), or even, in principle, much finer: you can refine the TLA+ specification to an arbitrary level, including down to the level of electronics in the CPU. However, very fine specifications are far less practical. > Making even moderately complex TLA+ models or minor iterations on a simple model's depth of representation often results in exploding the search space for TLC and consequently the time to perform checking. You can avoid the explosion by asking TLC to sample the behaviors in the same way a fuzzer does, but then you'll lose the exhaustiveness and the proof of absence of errors.
  - im_down_w_otp 8y ago
    I'm aware of both of these things. In either case the purpose and thus optimization of each kind of tool is fairly different, even if abstractly they're both "state space exploration", which made the comparison seem odd to me.
hwayne 8y ago
> It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC. While this is true for invariants, unfortunately it's not true for liveness properties. The currently implementation doesn't make any guarantees about the length of a minimum liveness counterexample, and in practice I find it's usually the _longest_ counterexample. Still super useful, I'm just being a little pedantic here :)

im_down_w_otp 8y ago

It seems like an odd comparison though. Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. Making even moderately complex TLA+ models or minor iterations on a simple model's depth of representation often results in exploding the search space for TLC and consequently the time to perform checking. Both classes of tools are useful, but the comparison seemed odd since you wouldn't use TLA+ like a fuzzer, nor vice versa.

pron 8y ago
> Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. TLC checks the TLA+ specification, however detailed it is. In practice, it's true that it is usually much more useful to specify at a level well above the code, but it could be at the same abstraction level as the code (the specification could even be mechanically generated from the code), or even, in principle, much finer: you can refine the TLA+ specification to an arbitrary level, including down to the level of electronics in the CPU. However, very fine specifications are far less practical. > Making even moderately complex TLA+ models or minor iterations on a simple model's depth of representation often results in exploding the search space for TLC and consequently the time to perform checking. You can avoid the explosion by asking TLC to sample the behaviors in the same way a fuzzer does, but then you'll lose the exhaustiveness and the proof of absence of errors.
- im_down_w_otp 8y ago
  I'm aware of both of these things. In either case the purpose and thus optimization of each kind of tool is fairly different, even if abstractly they're both "state space exploration", which made the comparison seem odd to me.

hwayne 8y ago

> It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC. While this is true for invariants, unfortunately it's not true for liveness properties. The currently implementation doesn't make any guarantees about the length of a minimum liveness counterexample, and in practice I find it's usually the _longest_ counterexample. Still super useful, I'm just being a little pedantic here :)