Причина различий в количестве достижимых состояний

Question

Я проверяю 8-битный сумматор с этим кодом. Когда я печатаю, число достижимых состояний равно 1, если основной модуль пуст, и 2^32, если весь основной модуль включен. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для 4-разрядного сумматора зарегистрированное число достижимых состояний было 2^16. Кажется логичным, что входные состояния равны 2^n, если n - это число битов. Откуда берутся все остальные штаты? Я заметил, что это, когда я добавляю строку a : adder (in1, in2); что состояния увеличиваются, но это было только экспериментально подтверждено, что именно это увеличивает количество состояний, а не сам модуль сумматора. Зачем?

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);
    bit4 : bit-adder (in1[4], in2[4], bit3.cout);
    bit5 : bit-adder (in1[5], in2[5], bit4.cout);
    bit6 : bit-adder (in1[6], in2[6], bit5.cout);
    bit7 : bit-adder (in1[7], in2[7], bit6.cout);
DEFINE
    sum0 := bit0.sum;
    sum1 := bit1.sum;
    sum2 := bit2.sum;
    sum3 := bit3.sum;
    sum4 := bit4.sum;
    sum5 := bit5.sum;
    sum6 := bit6.sum;
    sum7 := bit7.sum;   
    overflow := bit7.cout;
MODULE main
VAR
    in1 : array 0 .. 7 of boolean;
    in2 : array 0 .. 7 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 (in1[4]) := in1[4];
    next (in1[5]) := in1[5];
    next (in1[6]) := in1[6];
    next (in1[7]) := in1[7];


    next (in2[0]) := in2[0];
    next (in2[1]) := in2[1];
    next (in2[2]) := in2[2];
    next (in2[3]) := in2[3];

    next (in2[4]) := in2[4];
    next (in2[5]) := in2[5];
    next (in2[6]) := in2[6];
    next (in2[7]) := in2[7];


DEFINE
    op1 := toint (in1[0]) + 2 * toint (in1[1]) + 4 * toint (in1[2]) + 8 * toint
    (in1[3]) + 16 * toint (in1[4]) + 32 * toint (in1[5]) + 64 * toint (in1[6]) + 128 * toint
    (in1[7]);
    op2 := toint (in2[0]) + 2 * toint (in2[1]) + 4 * toint (in2[2]) + 8 * toint
    (in2[3]) + 16* toint (in2[4]) + 32 * toint (in2[5]) + 64 * toint (in2[6]) + 128 * toint
    (in2[7]);
    sum := toint (a.sum0) + 2 * toint (a.sum1) + 4 * toint (a.sum2) + 8 * toint
    (a.sum3) +16 * toint (a.sum4) + 32 * toint (a.sum5) + 64 * toint (a.sum6) + 128 * toint
    (a.sum7) + 256 * toint (a.overflow);


    LTLSPEC F op1 + op2 = sum

Answer 1

Пустой главный модуль. Если вы не включаете (прямо или косвенно) что-либо в основной модуль, то это просто игнорируется. Вы можете думать об этом, как об определении класса в C++ и никогда не создавать его / не создавать его где-либо еще: он может быть оптимизирован компилятором, не влияя на работу системы.

---

8-битный сумматор.

nuXmv > print_reachable_states
######################################################################
system diameter: 1
reachable states: 4.29497e+09 (2^32) out of 4.29497e+09 (2^32)
######################################################################

Это мой пример:

• модуль bit-adder имеет два boolean переменные, оба они могут принимать любое законное значение в области boolean переменная, в зависимости от конкретных входов модуля (т. е. значений в in1, in2 а также cin).

• модуль adder имеет восемь bit-adder подмодули и ряд определенных полей, которые на самом деле не учитываются, когда целью является оценка пространства состояний. Этот модуль не добавляет никаких особых ограничений на возможные состояния, принимаемые переменными в bit-adders так что единственное, что имеет значение, это то, что, объединяя восемь bit-adders вместе это имеет потенциальное пространство 2^16 состояния.

• модуль main имеет один adder модуль и два 8-bit массивы, которые моделируют входы. Эти входы произвольно выбираются в первом состоянии и остаются неизменными навсегда, поэтому они добавляют 2^16 возможные начальные состояния в системе. adder сам в целом имеет 2^16 достижимые состояния. Сочетание обеих вещей дает пространство 2^32 состояния.

---

Добавление. В приведенном выше выводе nuXmv предупреждает, что диаметр системы 1, Это связано с тем, что оба sum а также cout может принимать произвольное значение в исходном состоянии, поэтому для любого выбора in1 а также in2 существует хотя бы одно начальное состояние, в котором значения sum а также cout каждого bit-adder в системе совпадают с правильной суммой, без необходимости каких-либо вычислений. Это явно нереально. Лучшим подходом было бы заставить оба sum а также cout инициализируется в FALSE:

nuXmv > print_reachable_states 
######################################################################
system diameter: 9
reachable states: 259539 (2^17.9856) out of 4.29497e+09 (2^32)
######################################################################

Вы можете видеть, что на этот раз диаметр системы увеличился до 9. Это, очевидно, связано с тем, что в этом очень простом кодировании схемы сумматора carry-bit распространяется по диагонали, и каждый шаг распространения занимает один переход. Количество достижимых состояний также было уменьшено благодаря тому, что мы отбросили некоторые конфигурации, зафиксировав значения cout а также sum,