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 high

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.