#define race_0 (read_t[0] && write_t[0])
#define race_1 (read_t[1] && write_t[1])
#define race_2 (read_t[2] && write_t[2])


/* [] !race_0  */


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


/* <> fin_0  */