//Insert declarations of global clocks, variables, constants and channels.
int NSlight;
int SNlight;
int WElight;
int EWlight;
int NSreq;
int SNreq;
int WEreq;
int EWreq;
chan NSsync;
chan SNsync;
chan WEsync;
chan EWsync;
Lightint me; int me_req; int left; int left_req; int right; int right_req; chan sensor//Insert local declarations of clocks, variables and constants.
clock c;
redcargreenrequestingSensorchan lightNocarIscar//Insert process assignments.
NS := Light(NSlight, NSreq, EWlight, EWreq, WElight, WEreq, NSsync);
SN := Light(SNlight, SNreq, WElight, WEreq, EWlight, EWreq, SNsync);
WE := Light(WElight, WEreq, NSlight, NSreq, SNlight, SNreq, WEsync);
EW := Light(EWlight, EWreq, SNlight, SNreq, NSlight, NSreq, EWsync);
NSsensor := Sensor(NSsync);
SNsensor := Sensor(SNsync);
WEsensor := Sensor(WEsync);
EWsensor := Sensor(EWsync);
//Edit system definition.
system NS, SN, WE, EW, NSsensor, SNsensor, WEsensor, EWsensor;