NuSMV -int esercizio.smv [modalita interattiva]
read_model -i esercizio.smv [leggo il file]
go
pick_state
pick_state -i
simulate -v -i 5

NuSMV
Mi permette di vedere il controesempio se la formula è falsa.
C'è la possibilita di vedere n passi che il programma fa se la formula è vera?


NuSMV esercizio.smv