#define race_0  (read_A[0] && write_A[0])
#define race_1  (read_A[1] && write_A[1])
#define race_2  (read_A[2] && write_A[2])


/* [] !race_0  */


#define fin_0  (main[0]@P)
#define fin_1  (main[1]@P)
#define fin_2  (main[2]@P)


/* <> fin0  */