I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before.
I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software.
It really is just math and proofs, it shouldn't be so hard... to start.
Well, that's my take. Could be wrong. Might just need to hit the books.
P is very nice indeed, be advised that it is not an exhaustive checker like TLC (TLA+'s model checker, or Apalache, the symbolic tester). It is more like a higher-level testing framework.
That said, since non-deterministic choices are equi-probable in P, failure conditions are triggered at much higher frequencies than in a conventional testing scenario.
I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software.
It really is just math and proofs, it shouldn't be so hard... to start.
Well, that's my take. Could be wrong. Might just need to hit the books.