/* This is a model of the "correction of Figure 1 */ #define MAYCRASH if :: true -> endcrash: false :: true -> skip fi #define IF if :: #define FI :: else fi #define PB(sem) atomic{ (sem==1) -> sem=0 } #define VB(sem) sem=1 #define INITVAL 0 #define MAX_P 2 #define MAX_V 2 byte mutex = 1 ; byte delay = 0 ; short count = INITVAL; byte number_of_P = 0 ; byte number_of_V = 0 ; inline PC () { PB(mutex); count-- ; IF (count < 0) -> VB(mutex); MAYCRASH ; PB(delay) FI; VB(mutex) } inline VC () { PB(mutex); count++ ; if :: (count <= 0) -> VB(delay) :: else -> VB(mutex) fi } active[MAX_P] proctype TryPC() { PC() ; number_of_P++ } active[MAX_V] proctype TryVC() { number_of_V++ ; VC() } active proctype monitor() { endm: assert(number_of_P <= (number_of_V + INITVAL)) } /* active proctype monitor() { endm: atomic{ !(number_of_P <= (number_of_V + INITVAL)) -> assert(number_of_P <= (number_of_V + INITVAL)) } } */