const int B; // time bound
// timer
module timer

	t : [0..B+1];
	
	[time] t<=B -> t'=min(t+1,B+1);
	[done] l=4 -> t'=T+1;
	
endmodule