bool wantp = false;
bool wantq = false; // global variables that shares the intention for entering critical section of the 2 processes
int turn = 1; // global variable that sets the priority to one process, intially set on process p

//process p
active proctype p()
{
    //outer while loop
    do
        ::true ->
        wantp = true; // process p shares its intetion to enter critical section
        do
            :: wantq == true -> // checks if process q is also inteding to enter critical section
            if
                :: turn == 2 -> // in the case when both processes intend to enter critical section, check for priority
                wantp = false; // if priority is set on process q then set off process p intention
                (turn == 1); // wait for priority to be set on process p
                wantp = true; // once priority set on process p, process p intention to enter critical section is set on true
            :: else -> skip // if priority not set on process q, then skip
            fi;
        :: else -> break // if process q not intending to enter critical section, than go to own critical section
        od;
        printf("critical section p"); // execute critical section
        turn = 2; // set priority to the other process
        wantp = false; // set off intention to enter critical section
    od;
 }

//process p
active proctype q()
{
//outer while loop
do
    ::true ->
    wantq = true; // process q shares its intetion to enter critical section
    do
        :: wantp == true -> // checks if process p is also inteding to enter critical section
        if
            :: turn == 1 -> // in the case when both processes intend to enter critical section, check for priority
            wantq = false; // if priority is set on process p then set off process q intention
            (turn == 2); // wait for priority to be set on process q
            wantq = true; // once priority set on process q, process q intention to enter critical section is set on true
        :: else -> skip // if priority not set on process p, then skip
        fi;
    :: else -> break // if process p not intending to enter critical section, than go to own critical section
    od;
    printf("critical section q"); // execute critical section
    turn = 1; // set priority to the other process
    wantq = false; // set off intention to enter critical section
od;
}