Modeling and debugging a transfer between bank accounts

We consider the following Python function that is supposed to transfer amount euros from account from to account to.

def transfer(from, to, amount):
   from -= amount
   to += amount

Our goal is to debug this function using the TLC model-checker. Some indications can be found here.

Part 1: modeling the function transfer

The file transfer1.tla contains a model of the function transfer above.

1. Draw the transition system defined by this model
2. Run the TLC model-checker and explain why the assertion holds. Justify using the transition system.
3. Replace initialization from = 10 by from \in Int. Parse the model and run the TLC model-checker again. Explain the error.

Part 2: debugging

1. Replace the initialization amount = 5 by amount = 20. Parse and model-check. What do you observe?
2. Copy the model in a file transfer2.tla and update the module name to transfer2. Fix the model in order to solve the bug.

Part 3: more debugging

Copy the file transfer2.tla into transfer3.tla, update the module name to transfer3, and set back initialization amount = 5. Then, add a new variable declared as account_total = from + to; after all the other variables. Finally, add the two properties below at the end of the file (immediately before the line =========):

VALID_AMOUNT == (amount >= 0)
MONEY_INVARIANT == (account_total = from + to)

Our goal is to check that both VALID_AMOUNT and MONEY_INVARIANT are invariants of the model (i.e. true in each state). To that purpose:

• if you are using Visual Code Studio: add INVARIANT VALID_AMOUNT and INVARIANT MONEY_AMOUNT to the file transfer3.cfg,
• if you are using the TLA+ toolbox: add VALID_AMOUNT and MONEY_AMOUNT in the Invariants box of the Model.

Then, answer the following questions:

1. Parse and model-check. Explain why MONEY_INVARIANT is not an invariant of your model. Draw the transition system of your model and use it to justify your answer.
2. We suggest to remove the label l1 from the model. Draw the transition system of the new model and explain why this modification makes MONEY_INVARIANT an invariant of your model.
3. Justify why removing the label l1 could be valid in the context of database operations.