Finite State Process - Modelling Concurrency Issue?

170 Views Asked by At

I've been assigned a task to come up with a LTSA modelling for the following scenario.

Customers need to buy tickets to watch a show in a theater. The tickets are only issued at the counter on the day
of the show. Ticket holders are then showed to their respective seats by an Usher. 
There are two ticket Counters. Tickets can be issued by any Counter
There is only one main door.
There are only 3 Ushers available to seat the clients.
Customers can arrive in any order.
The management need to ensure that each customer is treated fairly to avoid a possible gate-crash.

And this is the LTSA code I've been able to develop so far.

const T_M = 3 
const C_M = 2


range T_R = 1..T_M //Range of tickets available
range C_R= 1..C_M //Range of counters


HOLDCOUNTER = ( holdCounter[c:C_R]-> release[c] -> HOLDCOUNTER).
CUSTOMER = ( gotoCounter[c:C_R] -> holdCounter[c] -> buyTicket[c] -> releaseCounter[c] -> STOP).
COUNTER = ( holdCounter[c:C_R]-> buyTicket[c] -> issueTicket[c] -> COUNTER).

||CUSTOMERS = ([c:T_R]:CUSTOMER).

||THEATER = ( CUSTOMERS || [counter:C_R]:COUNTER || HOLDCOUNTER).

But when I run it, it appears that when a CUSTOMER 1 goes to COUNTER 1, COUNTER 1 is available for CUSTOMER 2 to be used, which is wrong. The outcome should be such that when a CUSTOMER is using a COUNTER, that COUNTER should be locked from other CUSTOMERS until the CUSTOMER is done with it.

I think re-labeling the action 'holdCounter' of the composite process CUSTOMERS could help, but I don't know how to do it properly.

Can someone help? Thanks in advance.

0

There are 0 best solutions below