3 ms·
I've used TLA+ professionally in a previous role and found it useful. I'd agree with the sentiments in the GG discussion: 1. A repl would be useful. 2. Better
by ausimian 10y ago
I've used TLA+ professionally in a previous role and found it useful. I'd agree with the sentiments in the GG discussion:
1. A repl would be useful.
2. Better documentation for the individual tools, allowing other editors and toolchains to hook them more easily.
I would say that I found the TLC model checker extremely valuable, but learning what subset of TLA+ it can actually handle (and structuring your specifications appropriately) takes time.
Not sure about enums - seems like something PlusCal would do (if it doesn't already), but I would leave TLA+ alone, I think its support for sets is sufficient.