:: deftheorem defines has_Peterson_mutex_in PETERSON:def 24 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for tr being trace of DS
for Es being set holds
( Es has_Peterson_mutex_in tr iff ex p1, p2 being Process of DS st
( ( for p being Process of DS holds
( p = p1 or p = p2 ) ) & ex flag1, flag2, turn being Location of DS st
( ( for e being Event of DS st e in p1,tr holds
( not e writesto flag2 & not e writesto turn, the False of Values ) ) & ( for e being Event of DS st e in p2,tr holds
( not e writesto flag1 & not e writesto turn, the True of Values ) ) & ( for e being Event of DS st e in Es holds
( e has_Peterson_mutex_in p1,flag1,flag2,turn, the False of Values, the True of Values,tr & e has_Peterson_mutex_in p2,flag2,flag1,turn, the True of Values, the False of Values,tr ) ) ) ) );