MODULE main
        VAR
          bit0 : counter_cell(1);
          bit1 : counter_cell(bit0.carry_out);
          bit2 : counter_cell(bit1.carry_out);
        LTLSPEC
          G F bit2.carry_out

        MODULE counter_cell(carry_in)
        VAR
          value : boolean;
        ASSIGN
          init(value) := 0;
          next(value) := (value + carry_in) mod 2;
        DEFINE
          carry_out := value & carry_in;