TLA+ Part 2 — TLA+ to ILP Part 2 — Performance check

This is the second part of the TLA+ series. For your convenience you can find other parts in the table of contents in Part 1 — TLA+ to ILP Part 1 — Reducing problem

Let’s now carry on with adding more invariants. Tutorial says to reorder the operations, so let’s first update the db and then send the message. Now we get the following output:

Great, it took 0.02 second to show that the invariant holds. Let’s now do it for 3 messages and at most 3 processing attempts:

5000 seconds, that’s almost 85 minutes to prove that the invariant holds. The same takes around 2 seconds for TLA+.