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.
79 lines
2.3 KiB
79 lines
2.3 KiB
// mutual exclusion
|
|
|
|
(!((p1=2) & (p2=2))) &
|
|
(!((p1=2) & (p3=2))) &
|
|
(!((p1=2) & (p4=2))) &
|
|
(!((p1=2) & (p5=2))) &
|
|
(!((p1=2) & (p6=2))) &
|
|
(!((p1=2) & (p7=2))) &
|
|
(!((p1=2) & (p8=2))) &
|
|
(!((p1=2) & (p9=2))) &
|
|
(!((p1=2) & (p10=2))) &
|
|
(!((p1=2) & (p11=2))) &
|
|
(!((p1=2) & (p12=2))) &
|
|
(!((p2=2) & (p3=2))) &
|
|
(!((p2=2) & (p4=2))) &
|
|
(!((p2=2) & (p5=2))) &
|
|
(!((p2=2) & (p6=2))) &
|
|
(!((p2=2) & (p7=2))) &
|
|
(!((p2=2) & (p8=2))) &
|
|
(!((p2=2) & (p9=2))) &
|
|
(!((p2=2) & (p10=2))) &
|
|
(!((p2=2) & (p11=2))) &
|
|
(!((p2=2) & (p12=2))) &
|
|
(!((p3=2) & (p4=2))) &
|
|
(!((p3=2) & (p5=2))) &
|
|
(!((p3=2) & (p6=2))) &
|
|
(!((p3=2) & (p7=2))) &
|
|
(!((p3=2) & (p8=2))) &
|
|
(!((p3=2) & (p9=2))) &
|
|
(!((p3=2) & (p10=2))) &
|
|
(!((p3=2) & (p11=2))) &
|
|
(!((p3=2) & (p12=2))) &
|
|
(!((p4=2) & (p5=2))) &
|
|
(!((p4=2) & (p6=2))) &
|
|
(!((p4=2) & (p7=2))) &
|
|
(!((p4=2) & (p8=2))) &
|
|
(!((p4=2) & (p9=2))) &
|
|
(!((p4=2) & (p10=2))) &
|
|
(!((p4=2) & (p11=2))) &
|
|
(!((p4=2) & (p12=2))) &
|
|
(!((p5=2) & (p6=2))) &
|
|
(!((p5=2) & (p7=2))) &
|
|
(!((p5=2) & (p8=2))) &
|
|
(!((p5=2) & (p9=2))) &
|
|
(!((p5=2) & (p10=2))) &
|
|
(!((p5=2) & (p11=2))) &
|
|
(!((p5=2) & (p12=2))) &
|
|
(!((p6=2) & (p7=2))) &
|
|
(!((p6=2) & (p8=2))) &
|
|
(!((p6=2) & (p9=2))) &
|
|
(!((p6=2) & (p10=2))) &
|
|
(!((p6=2) & (p11=2))) &
|
|
(!((p6=2) & (p12=2))) &
|
|
(!((p7=2) & (p8=2))) &
|
|
(!((p7=2) & (p9=2))) &
|
|
(!((p7=2) & (p10=2))) &
|
|
(!((p7=2) & (p11=2))) &
|
|
(!((p7=2) & (p12=2))) &
|
|
(!((p8=2) & (p9=2))) &
|
|
(!((p8=2) & (p10=2))) &
|
|
(!((p8=2) & (p11=2))) &
|
|
(!((p8=2) & (p12=2))) &
|
|
(!((p9=2) & (p10=2))) &
|
|
(!((p9=2) & (p11=2))) &
|
|
(!((p9=2) & (p12=2))) &
|
|
(!((p10=2) & (p11=2))) &
|
|
(!((p10=2) & (p12=2))) &
|
|
(!((p11=2) & (p12=2)))
|
|
|
|
// liveness
|
|
// if a process is trying then eventually a process enters the critical section
|
|
|
|
((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1) | (p6=1) | (p7=1) | (p8=1) | (p9=1) | (p10=1) | (p11=1) | (p12=1)) =>
|
|
P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) | (p6=2) | (p7=2) | (p8=2) | (p9=2) | (p10=2) | (p11=2) | (p12=2) ]
|
|
|
|
// if all processes are trying process 1 enters the critical section first
|
|
|
|
(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) & (p6=1) & (p7=1) & (p8=1) & (p9=1) & (p10=1) & (p11=1) & (p12=1) =>
|
|
P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) & !(p6=2) & !(p7=2) & !(p8=2) & !(p9=2) & !(p10=2) & !(p11=2) & !(p12=2) U (p1=2) ]
|