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.
16 lines
414 B
16 lines
414 B
// mutual exclusion
|
|
|
|
(!((p1=2) & (p2=2))) &
|
|
(!((p1=2) & (p3=2))) &
|
|
(!((p2=2) & (p3=2)))
|
|
|
|
// liveness
|
|
// if a process is trying then eventually a process enters the critical section
|
|
|
|
((p1=1) | (p2=1) | (p3=1)) =>
|
|
P>=1 [ true U (p1=2) | (p2=2) | (p3=2) ]
|
|
|
|
// if all processes are trying process 1 enters the critical section first
|
|
|
|
(p1=1) & (p2=1) & (p3=1) =>
|
|
P>=0.5 [ !(p2=2) & !(p3=2) U (p1=2) ]
|