:: deftheorem defines has_Peterson_mutex_in PETERSON:def 23 :
for Values being Values_with_Bool
for DS being DistributedSysWithSharedMem of Values
for p being Process of DS
for tr being trace of DS
for e being Event of DS
for x1, x2, turn being Location of DS
for a1, a2 being Element of the carrier of Values holds
( e has_Peterson_mutex_in p,x1,x2,turn,a1,a2,tr iff ex e1, e2, e3 being Event of DS st
( e1 in p,tr & e2 in p,tr & e3 in p,tr & e1 < e2 & e2 < e3 & e3 < e & e1 writesto x1, the True of Values & not (e1,e) interval_in (p,tr) writesto x1 & e2 writesto turn,a2 & not (e2,e) interval_in (p,tr) writesto turn & ( e3 reads x2, the False of Values or e3 reads turn,a1 ) ) );