NuSMV - ET modèle

Question

Je suis en train d'écrire le modèle suivant dans NuSMV

En d'autres termes, z devient mauvaise que lorsque x et y sont en mauvais état aussi. Ceci est le code que j'ai écrit

MODULE singleton 
    VAR state: {good, bad}; 
    INIT state = good 
    TRANS (state = good) -> next(state) = bad 
    TRANS (state = bad) -> next(state) = bad 

MODULE effect(cond) 
    VAR state: {good, bad}; 
    ASSIGN 
    init(state) := good; 
    next(state) := case 
     (state = bad) : bad; 
     (state = good & cond) : bad; 
     (!cond) : good; 
     TRUE : state; 
     esac; 

MODULE main 
    VAR x : singleton; 
    VAR y : singleton; 
    VAR z : effect((x.state = bad) & (y.state = bad)); 

Mais je me suis seulement ces états atteignables

NuSMV > print_reachable_states -v 
###################################################################### 
system diameter: 3 
reachable states: 3 (2^1.58496) out of 8 (2^3) 
    ------- State 1 ------ 
    x.state = good 
    y.state = good 
    z.state = good 
    ------- State 2 ------ 
    x.state = bad 
    y.state = bad 
    z.state = bad 
    ------- State 3 ------ 
    x.state = bad 
    y.state = bad 
    z.state = good 
    ------------------------- 
###################################################################### 

Comment puis-je modifier mon code pour obtenir également

x.state = good 
y.state = bad 
z.state = good 

x.state = bad 
y.state = good 
z.state = good 

dans les états atteignables? En outre, je ne suis pas sûr si je dois ajouter ou non cette flèche rouge imprimée dans l'image du modèle: si x et y sont en état mauvais, je veux que pour sûr, tôt ou tard aussi z devient mauvais .

Merci beaucoup d'avoir aidé!

Answer 1

Les états

x.state = good 
y.state = bad 
z.state = good 

x.state = bad 
y.state = good 
z.state = good 

ne sont pas accessibles parce que chaque sous-module de main effectue une transition en même temps des autres et parce que vous la force une transition déterministe pour vos variables d'état ; En d'autres termes, dans votre modèle, x et y changez l'état de good à bad en même temps. De plus, contrairement à votre belle image, votre code smv n'autorise aucune auto-boucle sauf celle sur l'état final.

---

Pour fixer votre modèle, il vous suffit de dire que le cas --En x (resp y.) Est good - vous voulez next(x) (resp next(y).) Pour être soit good ou bad, mais pas forcer soit une décision. par exemple.

MODULE singleton 
VAR 
    state: { good, bad }; 

ASSIGN 
    init(state) := good; 
    next(state) := case 
     state = good : { good, bad }; 
     TRUE   : bad; 
    esac; 


MODULE effect(cond) 
VAR 
    state: { good, bad }; 

ASSIGN 
    init(state) := good; 
    next(state) := case 
     (state = bad | cond) : bad; 
     TRUE     : state; 
    esac; 


MODULE main 
VAR 
    x : singleton; 
    y : singleton; 
    z : effect((x.state = bad) & (y.state = bad)); 

Note: i également simplifié les règles pour le module effect, bien que cela était inutile.

Vous pouvez tester le modèle comme suit:

nuXmv > reset; read_model -i test.smv ; go; print_reachable_states -v 
###################################################################### 
system diameter: 3 
reachable states: 5 (2^2.32193) out of 8 (2^3) 
    ------- State 1 ------ 
    x.state = good 
    y.state = bad 
    z.state = good 
    ------- State 2 ------ 
    x.state = good 
    y.state = good 
    z.state = good 
    ------- State 3 ------ 
    x.state = bad 
    y.state = good 
    z.state = good 
    ------- State 4 ------ 
    x.state = bad 
    y.state = bad 
    z.state = bad 
    ------- State 5 ------ 
    x.state = bad 
    y.state = bad 
    z.state = good 
    ------------------------- 
###################################################################### 

---

En ce qui concerne votre deuxième question, l'exemple de code I fourni vous garantit la propriété que vous souhaitez vérifier:

nuXmv > check_ltlspec -p "G ((x.state = bad & y.state = bad) -> F z.state = bad)" 
-- specification G ((x.state = bad & y.state = bad) -> F z.state = bad) is true 

Ceci est évidemment le cas parce que le auto-boucle es e bord rouge dans votre image n'est pas présent.Si vous pensez à ce sujet, cette transition permettrait au moins une exécution dans laquelle l'état actuel reste égal à

x.state = bad 
y.state = bad 
z.state = good 

indéfiniment, et ce serait un contre-exemple à votre cahier des charges.

---

EDIT:

Vous pouvez également corriger le code en écrivant ceci:

MODULE singleton 
    VAR state: {good, bad}; 
    INIT state = good 
    TRANS (state = bad) -> next(state) = bad 

Retrait de la ligne TRANS (state = good) -> next(state) = bad permet x et y de changer arbitrairement quand state = good, ce qui signifie qu'ils peut rester non-déterministe good ou devenir bad. Ceci est complètement équivalent au code que je vous ai fourni, bien que moins clair à première vue puisqu'il cache non-déterminisme sous les hottes au lieu de le rendre explicite.