#define N 4

byte total_time=0;
byte where_is_torch=0;
byte on_right=0;

chan wanna_go =[0] of {int};
chan lets_go =[0] of {int};

#define TORCH(MAX)\
active proctype torch()\
{\
byte time1=0;\
byte time2=0;\
free: if\
:: wanna_go?time1; goto one;\
fi;\
one: if\
:: wanna_go?time2; goto two;\
:: goto going;\
fi;\
two: if\
::  atomic {time1>=time2;lets_go!0;}  goto going;\
::  atomic {time1<time2;lets_go!0;time1 = time2;time2 = 0;}  goto going;\
fi;\
going: if\
::  atomic {total_time+time1<=MAX;lets_go!0;total_time = total_time+time1;time1 = 0;where_is_torch = 1-where_is_torch;}  goto free;\
fi;\
}

#define SOLDIER(NAME, TIME)\
active proctype NAME()\
{\
left: if\
::  atomic {where_is_torch==0;wanna_go!TIME;}  goto go_right;\
fi;\
go_right: if\
::  atomic {lets_go?0;on_right = on_right+1;}  goto right;\
fi;\
right: if\
::  atomic {where_is_torch==1;wanna_go!TIME;on_right = on_right-1;}  goto go_left;\
fi;\
go_left: if\
:: lets_go?0; goto left;\
fi;\
}

TORCH(60)

SOLDIER(soldier_0, 5)

SOLDIER(soldier_1, 10)

SOLDIER(soldier_2, 20)

SOLDIER(soldier_3, 25)

never
{
again:
  if
  :: true; goto again;
  :: on_right==N;
  fi;
}