vvs

// Raúl Fernández Domínguez
// Javier Loureiro Pérez

// Global variables

#define N 3
#define CAP 7
short max[N] = {2, 4, 3};     // Maximum money needed by each client
short loan[N] = {0, 0, 0};    // Current amount lent to each client
short cash = CAP;             // Money in the bank (initially, the capital CAP)

active [N] proctype Client() {
    byte request;

    do
    :: (loan[_pid] < max[_pid]) ->  // Si el préstamo actual es menor que el máximo

        byte max_request = max[_pid] - loan[_pid];  // Cantidad máxima que puede pedir
        select (request: 1.. max_request);

        atomic {
            // Verificar si hay suficiente efectivo disponible
            (cash >= request) -> {
                cash = cash - request;      // Disminuye el efectivo del banco
                loan[_pid] = loan[_pid] + request;  // Aumenta el préstamo del cliente
            }
        }


    req:    printf("C%d requests %d. Cash: %d [%d,%d,%d]\n", _pid, request, cash, loan[0], loan[1], loan[2]);

        // Impresión de petición
        printf("C%d got the money %d. Cash: %d [%d,%d,%d]\n", _pid, request, cash, loan[0], loan[1], loan[2]);

        // Verificación de consistencia del sistema
        assert(cash >= 0 && cash <= CAP);
        assert(loan[_pid] >= 0 && loan[_pid] <= max[_pid]);
        assert(cash + loan[0] + loan[1] + loan[2] == CAP);

    :: (loan[_pid] > 0) ->  // Devolver el préstamo si tiene un préstamo activo
        short return_amount;
        return_amount = loan[_pid];  // Todo el préstamo

        atomic {
            cash = cash + return_amount;    // El efectivo en el banco aumenta
            loan[_pid] = 0;           // El préstamo del cliente se devuelve por completo
        }

        // Impresión de devolución
    pay:    printf("C%d returns loan %d. Cash: %d [%d,%d,%d]\n", _pid, return_amount, cash, loan[0], loan[1], loan[2]);

        // Verificación consistencia del sistema
        assert(cash >= 0 && cash <= CAP);
        assert(loan[_pid] == 0);
        assert(cash + loan[0] + loan[1] + loan[2] == CAP);
    od;
}