//This file was generated from (Academic) UPPAAL 4.1.1 (rev. 4276), March 2009 /* Mutual exclusion */ A[] (forall (pid1 : pid_t) (forall (pid2 : pid_t) (((Thread(pid1).HasTheLock1 or Thread(pid1).HasTheLock2 or Thread(pid1).HasTheLock3) and (Thread(pid2).HasTheLock1 or Thread(pid2).HasTheLock2 or Thread(pid2).HasTheLock3)) imply pid1 == pid2)))