Cómo deducir el número de estados posibles para un sumador

Si mi cálculo es correcto, un sumador de 4 bits tiene 65536 estados, que es exactamente 2¹⁶. ¿De dónde viene este número? Parece que debería haber algún trasfondo teórico por qué este número es exactamente 2¹⁶. ¿Es cierto, según una fórmula general o mi modelo es defectuoso?

Mi sumador se ve de acuerdo con la siguiente especificación.

MODULE bit-adder (in1, in2, cin)
VAR
    sum : boolean;
    cout : boolean;
ASSIGN
    next (sum) := (in1 xor in2) xor cin;
    next (cout) := (in1 & in2) | ((in1 | in2) & cin);
MODULE adder (in1, in2)
VAR
    bit0 : bit-adder (in1[0], in2[0], FALSE);
    bit1 : bit-adder (in1[1], in2[1], bit0.cout);
    bit2 : bit-adder (in1[2], in2[2], bit1.cout);
    bit3 : bit-adder (in1[3], in2[3], bit2.cout);
DEFINE
    sum0 := bit0.sum;
    sum1 := bit1.sum;
    sum2 := bit2.sum;
    sum3 := bit3.sum;
    overflow := bit3.cout;

Es el número de estados de mi módulo principal que se informa. Si no incluyo el módulo principal, entonces el número de estados es 1.

MODULE main

VAR
    in1 : array 0 .. 3 of boolean;
    in2 : array 0 .. 3 of boolean;
    a : adder (in1, in2);
ASSIGN
    next (in1[0]) := in1[0];
    next (in1[1]) := in1[1];
    next (in1[2]) := in1[2];
    next (in1[3]) := in1[3];
    next (in2[0]) := in2[0];
    next (in2[1]) := in2[1];
    next (in2[2]) := in2[2];
    next (in2[3]) := in2[3];
DEFINE
    op1 := toint (in1[0]) + 2 * toint (in1[1]) + 4 * toint (in1[2]) + 8 * toint
    (in1[3]);
    op2 := toint (in2[0]) + 2 * toint (in2[1]) + 4 * toint (in2[2]) + 8 * toint
    (in2[3]);
    sum := toint (a.sum0) + 2 * toint (a.sum1) + 4 * toint (a.sum2) + 8 * toint
    (a.sum3) + 16 * toint (a.overflow);

    LTLSPEC F op1 + op2 = sum

Es cuando agrego la fila a : adder (in1, in2); que el número de estados aumenta de 2 ^ 8 a 2 ^ 16. Así que es algo con el verificador de modelos y el módulo principal.