# The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile

## Simple-Minimondex

Author: Jim Woodcock

This CML model has been developed by Jim Woodcock inspired by the original work done with the Mondex secure card system (see [Stepney&00,Woodcock&08a]. In 1994, National Westminster Bank developed an electronic purse (or smart card) system, called Mondex. An electronic purse is a card-sized device intended to replace “real” coins with electronic cash. In contrast to a credit or debit card, an electronic purse stores its balance in itself, thus does not necessarily require any network access to update a remote database during a transaction. So, electronic purses can be used in small stores or shops, such as bakeries, where small amounts of money are involved. In the CML model here however, the different potential faults that could happen in these transactions are not taken into account.

When debugging the MiniMondex example one will get an option to select between ten different cards that wish to transfer an amount of money to another card. Here you can experiment with transferring money between cards and see how it can communicate either over the accept or the reject channel. Experiment with sending money from a card to itself and with transferring more money than the amount left on a particular Card.

### simpler_minimondex.cml

``````values
N: nat = 2
V: nat = 1
M: nat = N*V

types
Index = nat
inv i == i in set {1,...,N}

Money = nat
inv m == m in set {0,...,M}

channels
pay, transfer: Index * Index * Money
accept , reject: Index

process Card = val i: Index @
begin
state value: nat := 0

operations
Init: () ==> ()
Init() == value := V

Credit: nat ==> ()
Credit(n) == value := value + n

Debit: nat ==> ()
Debit(n) == value := value - n
pre value >= n

actions
Transfer = pay.i?j?n ->
( [n > value] & reject!i -> Skip
[]
[n <= value] & transfer.i.j!n -> accept!i -> Debit(n) )

Cycle = ( Transfer [] Receive ); Cycle

@ Init(); Cycle

end

process OneCard = Card(1)

--THE FOLLOWING PROCESSES MAKE THE ANALYSIS VERY SLOW AND THE MODEL CHECKER
--STILL HAS PROBLEMS TO HANDLE IT.
process Cards =
|| i: Index @
[ {| pay.i,transfer.i,accept.i, reject.i |} union {| transfer.j.i.n | j:Index,n:Money|} ] Card(i)

--the original description uses {| pay.i,transfer.i,accept.i, reject.i |} union {transfer.j.i.n | j <- Index, n <- Money}
-- but the construct var <- expression is not accepted by the parser

process Network = Cards \\ {|transfer|}
``````