Raison de la différence de nombre d'états atteignables

Question

Je vérifie un additionneur 8 bits avec ce code. Quand j'imprime le nombre d'états atteignables sont 1 si le module principal est vide et 2^32 si le module principal entier est inclus. Qu'est-ce qui fait la différence dans le nombre déclaré d'états atteignables? Pour un additionneur de 4 bits, le nombre d'états atteignables était de 2^16. Il semble logique que les états d'entrée soient 2^n si n est le nombre de bits. D'où viennent tous les autres états? J'ai remarqué que c'est quand j'ajoute la ligne a : adder (in1, in2); que les états augmentent, mais cela n'a été vérifié qu'expérimentalement que c'est ce qui augmente le nombre d'états et non le module additionneur lui-même. Pourquoi?

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

Module principal vide. Si vous n'incluez pas (directement ou indirectement) quelque chose dans le module principal, il est simplement ignoré. Vous pouvez le penser comme définir une classe en C++ et ne jamais l'instancier/l'utiliser ailleurs: il peut être optimisé par le compilateur sans affecter l'exécution du système.

---

Additif 8 bits.

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

Ceci est mon avis sur l'exemple:

• Module bit-adder a deux variables boolean, les deux sont sans prendre aucune valeur juridique dans le domaine d'une variable boolean, en fonction des entrées spécifiques du module (c'est-à-dire les valeurs en in1, in2 et cin).

• Le module adder a huit sous-modules bit-adder et un certain nombre de champs définis, qui ne comptent pas vraiment lorsque l'objectif est d'estimer l'espace d'état. Ce module n'ajoute aucune contrainte particulière sur les états possibles assumés par les variables dans le bit-adders, donc la seule chose qui compte est qu'en combinant huit bit-adders ensemble il a un espace potentiel de 2^16 états. Le module main a un module adder et deux matrices 8-bit qui modélisent les entrées. Ces entrées sont arbitrairement choisies dans le premier état et restent fixes pour toujours, donc elles ajoutent 2^16 états initiaux possibles au système. Le adder lui-même a globalement 2^16 états atteignables. La combinaison des deux choses donne un espace de 2^32 états.

---

Addendum. Dans la sortie ci-dessus, nuXmv vous avertit que le système diamètre est seulement 1. Cela est dû au fait que les deux sum et cout peut prendre une valeur quelconque dans l'état initial, de sorte que pour tout choix de in1 et in2, il existe au moins un état initial dans lequel les valeurs de sum et cout de chaque bit-adder dans le le système coïncide avec la somme correcte, sans qu'aucun calcul ne soit nécessaire. C'est évidemment un tronçon irréaliste.Une meilleure approche serait de forcer les deux sum et cout étant initialisées à FALSE:

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

Vous pouvez voir que cette fois le diamètre du système a augmenté à 9. Ceci est évidemment dû au fait que dans ce codage très simple d'un additionneur de circuit le carry-bit est propagé le long de la diagonale, et chaque étape de propagation prend une transition. Le nombre d'états atteignables a également été réduit grâce au fait que nous avons abandonné certaines configurations en fixant les valeurs de cout et sum.