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