acws-0116% nusmv  ferryman.smv
*** This is NuSMV 2.1.2 (compiled 2002-11-22 12:00:00)
*** For more information of NuSMV see <http://nusmv.irst.itc.it>
*** or email to <nusmv-users@irst.itc.it>.
*** Please report bugs to <nusmv-users@irst.itc.it>.
-- specification !(((goat = cabbage | goat = wolf) -> goat = ferryman)
                 U (((cabbage & goat) & wolf) & ferryman)) is false
-- as demonstrated by the following execution sequence
-- loop starts here --
-> State 1.1 <-
    ferryman = 0              -> State 1.8 <-
    goat = 0                      ferryman = 1
    cabbage = 0                   goat = 1
    wolf = 0                      carry = g
    carry = 0                 -> State 1.9 <-
-> State 1.2 <-               -> State 1.10 <-
    ferryman = 1                  ferryman = 0
    goat = 1                      cabbage = 0
    carry = g                     carry = c
-> State 1.3 <-               -> State 1.11 <-
    ferryman = 0                  ferryman = 1
    carry = 0                     carry = 0
-> State 1.4 <-               -> State 1.12 <-
    ferryman = 1                  ferryman = 0
    cabbage = 1                   wolf = 0
    carry = c                     carry = w
-> State 1.5 <-               -> State 1.13 <-
    ferryman = 0                  ferryman = 1
    goat = 0                      carry = 0
    carry = g                 -> State 1.14 <-
-> State 1.6 <-                   ferryman = 0
    ferryman = 1                  goat = 0
    wolf = 1                      carry = g
    carry = w                 -> State 1.15 <-
-> State 1.7 <-                   carry = 0
    ferryman = 0
    carry = 0