// mutual exclusion

(!((p1=2) & (p2=2))) &
(!((p1=2) & (p3=2))) &
(!((p1=2) & (p4=2))) &
(!((p1=2) & (p5=2))) &
(!((p2=2) & (p3=2))) &
(!((p2=2) & (p4=2))) &
(!((p2=2) & (p5=2))) &
(!((p3=2) & (p4=2))) &
(!((p3=2) & (p5=2))) &
(!((p4=2) & (p5=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)) =>
P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) ]

// if all processes are trying process 1 enters the critical section first

(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) =>
P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) U (p1=2) ]