Süsteemide modelleerimine 2018/19 sügis

TLA Intro

Chapter 1 from Practical TLA+

"Alice and Bob have accounts at Bankgroup. Each account has 0 or more dollars in it. Bankgroup wants to add a new “wire” feature, where any user can transfer money to any other user... Wires can take an arbitrary amount of time. In other words, even if wire A starts before B, A may still finish after wire B. Your algorithm must guarantee that, even in those cases, we satisfy all of the requirements. Given that money is on the line, you should probably design this in advance."

Step 1: Install TLA

Install TLA... this is yet again an Eclipse-based tool.

• Binaries
• TLA Web Page
• Book repository

Step 2: Create the project

Create a new project under File > Open Spec > Add New Spec, set the root-module file to /your/path/wire.tla and set the specification name to “wire”. Insert the following code within the module blocks:

EXTENDS Integers
(*--algorithm wire

begin
    skip;
end algorithm;*) 

Step 3: Define the variables

Create variables! They go right before begin (line 3 above). Variables are separated with comma and end with semicolon, such as variables x = 5, y = 4; Add the following variables:

• The set of people people = {"Whatever", "Name"}.
• The state of their accounts acc = [p \in people |-> n] for your choice of n.
• The variable sender and receiver are strings that equal who sends whom.
• An integer variable amount should signify the amount to be transferred.

Step 4: Write the invariant

After the variables, declare your invariant:

define
    NoOverdrafts == ...
end define; 

This should state that for every person in people (based on syntax: \A x \in set : property), the money in their account (syntax: acc[person]) is greater than zero.

Step 5: Implement a single transfer

Replace the body of the algorithm (currently skip) with two statements to make a transfer:

    Withdraw:
        acc[sender] := ...;
    Deposit:
        acc[receiver] := ...;

Step 6: Translate to TLA and verify

To compile, to File > Translate PlusCal Algorithm (Ctrl-T) or right-click and set Eclipse to do this automatically. To create the model, go to TLC Model Checker > New Model. Find the drop-down labeled Invariants and click the Add button. Type in the name of the invariant we want to check (NoOverdrafts), save it, and run the model (the green button just under “Model Overview”). You should see 4 states found, 3 distinct states, and no error.

Step 7: Generalize the simulation!

This only tested a single transfer. Set the amount to be in the set 1..6. Try to verify. This should fail if your accounts started with less than 6. Change the upper bound to acc[sender] instead.

Step 8: Multiple processes.

Now declare two processes before the "begin" statement: process Wire \in 1..2 and make the variables sender, receiver and amount local variables of the processes. Also, you need to add end process;. Now run this! You should get an error! Fix it by introducing a check that account has the necessary funds.

• Does this work?
• Should it work?
• If not, how can you fix it?

Step 9: Towards Liveness.

Consider how to state the property "NoMoneyIsLost" that claims money in the bank will remain constant. Is this an invariant? Is it an invariant than must hold eventually?