nikita.pml

/**
 Producer/Consumer by Nikita Yushchenko
 
 The Promela encoding by Igor Konnov.

 To check the property, run:
 
 spin -a nikita.pml && gcc -o pan pan.c && ./pan -f -a -N corr2 -m10000000
 */


/* the number of producers */
#define N 3

byte ACK;
byte DIRTY;

proctype Producer(byte n) {
    byte ack;
    do
        :: true ->
produced:
            ack = ACK;
            if
                :: (ack & (1 << n)) != 0 ->
                    // the atomic statements are redundant here
                    atomic { DIRTY = DIRTY & ~(1 << n); }
                :: else ->
                    // the atomic statements are redundant here
                    atomic { DIRTY = DIRTY | (1 << n); }
            fi

        :: true -> skip; /* do nothing */
    od
}

proctype Consumer() {
    byte tmp, dirty;
    do
        :: tmp = DIRTY;
            dirty = tmp ^ ACK;
            ACK = tmp;
            /* consume: add extra conditions for N > 3 */
            if
                :: (dirty & 1) != 0 ->
consumed0:              skip;
                :: else
            fi;
            if
                :: (dirty & 2) != 0 ->
consumed1:              skip;
                :: else
            fi;
            if
                :: (dirty & 4) != 0 ->
consumed2:              skip;
                :: else
            fi;
    od
}

init {
    run Producer(0);
    run Producer(1);
    run Producer(2);
    run Consumer();
}

ltl corr0 { ([](Producer[1]@produced -> <>Consumer@consumed0)) }
ltl corr1 { ([](Producer[2]@produced -> <>Consumer@consumed1)) }
ltl corr2 { ([](Producer[3]@produced -> <>Consumer@consumed2)) }