You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
25 lines
680 B
25 lines
680 B
// theorem 1 (mutual exclusion)
|
|
|
|
!((p1>9) & (p2>9))
|
|
& !((p1>9) & (p3>9))
|
|
& !((p2>9) & (p3>9))
|
|
|
|
// lemma c
|
|
// if the crical section is occupied then eventually it becomes clear
|
|
|
|
(p1>9) | (p2>9) | (p3>9) => P>=1 [ true U (p1<10) & (p2<10) & (p3<10) ]
|
|
|
|
// lemma d
|
|
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
|
|
|
|
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) => P>=1 [ true U (p1=14) | (p2=14) | (p3=14) ]
|
|
|
|
|
|
// theorem 2 (liveness)
|
|
// if process 1 tries then eventually it enters the critical section
|
|
|
|
(p1=1) => P>=1 [ true U (p1=10) ]
|
|
|
|
// not probability 1
|
|
|
|
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]
|