Code Multiple Sleeping Barber bằng Promela bị lỗi ra nhiều kết quả khác nhau

[Tvo]

Em chạy nhiều lần ra nhiều kết quả khác nhau. Em nghĩ là em bị sai logic nhưng mà không biết cách sửa mong mọi người góp ý ạ. Đây là những output mà em chạy.

1. both barbers are sleeping
2. customer remaining = 0, next_barber = 1
3. customer remaining = 1, next_barber = 0
4. customer remaining = 1, next_barber = 1
5. customer remaining = 0, next_barber = 0

#define NUM_BARBERS 2    // Number of barbers
#define NUM_CHAIRS 3     // Number of chairs in the waiting room
#define NUM_CUSTOMERS 5  // Total number of customers
chan waitingRoom = [NUM_CHAIRS] of {int};  // Bounded FIFO channel for waiting customers
chan barber[NUM_BARBERS] = [0] of {int};   // Synchronous channels for barber-customer interaction
chan finished[NUM_BARBERS] = [0] of {int}; // Synchronous channels to signal haircut completion
int customers_remaining = NUM_CUSTOMERS;  // Track the total number of customers left
int next_barber = 0;  // Keep track of the next barber to pick a customer (round-robin)
proctype Barber() {
    int barber_id = _pid - 1;
    int customer_id;
    do
    :: len(waitingRoom) > 0 ->  
        atomic {
            waitingRoom?customer_id;  
            printf("Barber %d is cutting hair for Customer %d.\n", barber_id, customer_id);
        }
        atomic {
            barber[barber_id]!customer_id;  
            finished[barber_id]?customer_id;  
            printf("Barber %d finished haircut for Customer %d.\n", barber_id, customer_id);
        }
    ::  atomic{
        customers_remaining == 0 && len(waitingRoom) == 0 ->
        printf("Barber %d is sleeping.\n", barber_id);
        break;  
        }
    od;
}
proctype Customer() {
    int customer_id = _pid - 1;
    int barber_id;
    if
    :: len(waitingRoom) < NUM_CHAIRS ->  
        atomic {
            waitingRoom!customer_id;  
            printf("Customer %d is waiting.\n", customer_id);
        }
        atomic {
            barber_id = next_barber;           // Assign to the next barber
            next_barber = (next_barber + 1) % NUM_BARBERS;  // Update for round-robin
           
        }
            barber[barber_id]?customer_id;  // Wait for the barber to accept
            printf("Customer %d is having a haircut with Barber %d.\n", customer_id, barber_id);
            finished[barber_id]!customer_id;  // Signal haircut completion
            printf("Customer %d is leaving after haircut from Barber %d.\n", customer_id, barber_id);
        atomic{
            customers_remaining--;
        }
    :: else ->  
        atomic {
            printf("Customer %d found no chair and left.\n", customer_id);
            customers_remaining--;  
        }
    fi;
}
init {
    atomic {
        printf("The barbers are sleeping\n");
        // Start barber processes
        int i;
        for (i : 1 .. NUM_BARBERS) {
            run Barber();
        }
        // Start customer processes
        for (i : 1 .. NUM_CUSTOMERS) {
            run Customer();
        }
    }
}

[Joe (Schwarz)]

Em chạy nhiều lần ra nhiều kết quả khác nhau. Em nghĩ là em bị sai logic nhưng mà không biết cách sửa

Boy, can you tell this poor forum exactly what you mean by “Em chạy nhiều lần ra nhiều kết quả khác nhau” ?
Is this an error? What does the error message say?
You’re using Promela, so you surely know what the acronym PROMELA stands for, right?

PRO(cess) ME(ta) LA(nguage) is a language for modeling concurrent (parallel) systems and NOT a programming language in the classical sense. Meaning:

• Multithreading
• Synchronization and message passing
• Few control structures, pure (no side effects) expressions
• Data structures with finite and fixed boundaries

The results of a concurrent (or multithreaded) process are and will be never the same. And this is exactly the same for every programming language. So why are you surprised by the result when you work with the “highest” level of a computer language? Maybe you should begin with the “primitive levels” (operating system, Paging, Thread, Concurrency, etc.) first before you try to climb the Mount Olympic.

[Tvo]

Dạ trường đại học của em bắt học môn này. Mà chạy nhiều lần mỗi lần lại ra kết quả có lúc đúng có lúc sai nên em không xác định được kết quả sẽ ra gì là đúng ạ.

[Joe (Schwarz)]

You still don’t tell us about the “lỗi”. Your terse explanation is useless. It’s probably in the atomic block. According to the documentation HERE. For example:

If any statement within the atomic sequence blocks, atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time, but not necessarily immediately. Before the process can resume the atomic execution of the remainder of the sequence, the process must first compete with all other active processes in the system to regain control, that is, it must first be scheduled for execution.

This is how concurrency works. Your university should teach you more about the effects of concurrency or parallelism.