#define D_NORTH 0
#define D_SOUTH 1

#define N 2
#define getDirection(no) ((no < N/2) -> D_NORTH : D_SOUTH)
#define P(s) atomic { s > 0 -> s = s - 1 }
#define V(s) atomic { s = s + 1 }

byte mutex = 1;
byte queue = 0;
byte inCrit = 0;
byte direction = 0;
byte waiting = 0, inAlley = 0;

byte carsInDirection[2];
pid cars[N];

proctype Car(int no)
{
    byte temp;

    do
     ::
        skip;

enter:
        P(mutex);
        inCrit++;

        if
         :: (0 == inAlley) -> direction = getDirection(no);
         :: else -> skip;
        fi;

        if
         :: (getDirection(no) == direction) ->
            temp = inAlley;
            inAlley = temp + 1;

            carsInDirection[getDirection(no)]++;
            inCrit--;

            V(mutex);
         :: else ->
            temp = waiting;
            waiting = temp + 1;

            inCrit--;
            V(mutex);
            P(queue);

            direction = getDirection(no);

            temp = inAlley;
            inAlley = temp + 1;

            temp = waiting;
            waiting = temp - 1;

            carsInDirection[getDirection(no)]++;

            if
             :: (0 < waiting) -> V(queue)
             :: else -> inCrit--; V(mutex);
            fi;
        fi;

in_alley:
        skip;

leave:
        P(mutex);
        inCrit++;
        carsInDirection[getDirection(no)]--;

        temp = inAlley;
        inAlley = temp - 1;

        if
         :: (0 == inAlley && 0 < waiting) -> V(queue);
         :: else -> inCrit--; V(mutex);
        fi;
    od;
}

#define CHECK(P) atomic { !(P) -> assert(P) }

active proctype Monitor()
{
    // Safety invariants

    if
     :: CHECK(inAlley <= N/2 && inAlley >= 0)
     :: CHECK(inCrit == 0 || inCrit == 1)
     :: CHECK(!(carsInDirection[D_SOUTH] && carsInDirection[D_NORTH]))
    fi
}


init {
    atomic {
        int i = 0;

        for (i in cars) {
            cars[i] = run Car(i);
        }
    }
}