TVT Example: Cash Dispenser

This example includes files that were used in a cash dispenser presentation. Slides of the presentation can be found in http://www.cs.tut.fi/ohj/VARG/TVT/AK_cashdispenser.ps.

Contents

In this example, there are two versions of the systems. The first version is very coarse and it does not satisfy the requirements stated in the slides. However, it gives us valuable information about the behaviour of the systems based on this design.

The final version meets the requirements. The ideas behind these versions are described later.

This example consists of following files:

You can obtain the files from bank.tar.gz package.

Building the system

Most often you want to make a reduced state space of the system. With these files you can make it with the command
gmake system.lsts
Then you may examine the result visually by executing
tvt.illux system.lsts stylefile.col
. Executing the commands above has the same effect as the following use of TVT tools
tvt.extendedrules system.xrules | tvt.parallel - | tvt.lsts2ag - | tvt.detlsts - | tvt.ag2lsts - | tvt.SBreduction - | tvt.illux - stylefile.col
Sometimes you may also want to have intermediary files. You can (g)make following files:

Requirements for the system

In the presentation there were three requirements which the system should satisfy.

  1. Card is always returned to the customer.
  2. When money is given, the withdrawal must be recorded.
  3. If money is not given, withdrawal must not be committed.

Recording a withdrawal means that the withdrawn money is taken from the account or, if the bank is not sure whether or not the money was given to the customer, some kind of sign is left to database that the withdrawal should be checked later. It is not generally possible to make sure that the money of the last withdrawal was given to the customer. The uncertainity can be caused, for example, by a bulldozer or earthquake, which cuts the cable and thus the connection between the ATM and the bank.

First version

Process descriptions

Initially ATM process waits for the user to insert a card (ATM:card in) and initiate a withdrawal (ATM:withdraw). After that ATM sends a query to the bank (ATM:send query) to check if money can be given to the customer (if there is enough money in customer's account). Now there are three possibilities:

  1. ``Withdrawal is allowed'' message is received (ATM:rec allow). ATM returns the card (ATM:card out), gives the money to the customer (ATM:give money) and is back in its initial state.
  2. ``Withdrawal is not allowed'' message is received (ATM:rec refuce). ATM tells the customer that there is no money (ATM:no money) and continues to its initial state by returning the card.
  3. ATM does not receive any message before it decides that it cannot wait any longer (ATM:timeout). ATM announces an error (ATM:error) and stops.

Bank waits in its initial state a query to be received (BANK:rec query). After that it decides that either

After these choises the bank process is again in its initial state waiting for another query.

Channel is unreliable first-in-first-out buffer with capacity one. It can convey at most two different messages from a sender to a receiver. When a message is put in to the channel (CH:in1 or CH:in2) it either can be lost (CH:lose) or passed through (CH:out1 or CH:out2).

Parallel composition

There are four processes put in parallel in the composition of the whole system. Process number one is ATM which synchronises with two channel processes, numbered two and three (see system.xrules). Process number two is a channel which carries query messages from ATM to bank. Process number three is another channel from which ATM receives both ``withdrawal is allowed'' and ``bank refused to withdraw'' messages.

The fourth process is the bank, which is accordingly synchronised to the channel processes. It receives queries from process two and sends acceptance information of withdrawal to process three.

Why the system does not work

It is stated in the requirements that the inserted card should always be eventually given back to the customer. This does not hold in the system, because ATM deadlocks after error.

The system would not meet the requirements even if the card was given out after the error and ATM was reset to its initial state. The reason is that the bank may commit withdrawal (take the money from customer's account) even if the money is not given to the customer. This is fixed in the final version.

Final version

Changes to processes

The main difference between the final and the first version is that the withdrawal is not committed before ATM has desided to give the money. This is ensured so that when ATM receives the ``withdrawal is allowed'' message, it sends acknowledgement (ATM:send done).

On the other hand, bank waits for the acknowledgement (BANK:rec done) and commits the withdrawal only when it is received.

If the bank does not receive an acknowledgement before it receives a new query or timeout occurs, it records an unclear withdrawal. In reality this would be a very unlikely situation.

Channel processes, as well as ATM and bank, can also consume time (execute CH:timeout actions) in their initial states.

Notes on parallel composition

Timeout actions of all processes are synchronised in parallel composition. Executing timeout action means that a certain amount of time passes. The time is long enough for underlying protocol to consider connection lost and give up sending messages that may be requested to sent.


Return to TVT project homepage.


Antti Kervinen
Last modified: Thu Nov 7 16:37:36 EET 2002