MODULE counter_cell(carry_in)
 VAR
   value : boolean;
 ASSIGN
   init(value) := FALSE;
   next(value) := value xor carry_in;
 DEFINE
  carry_out := value & carry_in;
MODULE main
 VAR
   bit0 : counter_cell(TRUE);
   bit1 : counter_cell(bit0.carry_out);
   bit2 : counter_cell(bit1.carry_out);