Man2safe.pml

#define N_d 4  /* Number of processes in critical section */
#define N_u 4
#define P(S) do :: atomic { S > 0 -> S--; break } od
#define V(S) atomic { S++ }

int S_down = 1;
int S_up = 1;
int S_ally = 1;

int down = 0;
int up = 0;

byte critical = 0;
int incrit = 0;

active [N_d] proctype D() 
{
do ::
    skip;

    entry:
    P(S_down);
    
    
    if
    :: down == 0 -> P(S_ally);
    :: down != 0 -> skip;
    fi;
    down++;
    V(S_down);

    incrit:  // Move this label outside of the loop structure
    assert(down > 0 && up == 0);

    leave:
    P(S_down);
    down--;
    
    if
    :: down == 0 -> V(S_ally);
    :: down != 0 -> skip;
    fi;

    V(S_down);
od;
}

active [N_u] proctype U()
{
do ::
    skip;

    entry:
    P(S_up);
    
    
    if
    :: up == 0 -> P(S_ally);
    :: up != 0 -> skip;
    fi;
    up++;
    V(S_up);

    incrit:
    assert(up > 0 && down == 0);

    leave:
    P(S_up);
    up--;
    
    if
    :: up == 0 -> V(S_ally);
    :: up != 0 -> skip;
    fi;

    V(S_up);
    
od;
}