Data race-freedom is specified and verified by the assert statements in Line 58 and 62:

Termination and deadlock-freedom is verified by specifying the following macros and verifying the progress property <> fin0: 

#define fin0  (main[0]@fin)
#define fin1  (main[1]@fin)
#define fin2  (main[2]@fin)
#define fin3  (main[3]@fin)

/*  <> fin0  */