Suppose I have following structure M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan.
Clearly, from such model, we have X r is satisfied in s0 (the initial state), since r is satisfied in s1 and s2. My NuSMV code for the Kripke structure is as follows (as described here).
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};
ASSIGN
init(state) := s0;
next(state) :=
case
state = s0 : {s1, s2};
state = s1 : {s2};
state = s2 : {s2};
TRUE : state;
esac;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(p) :=
case
state = s1 | state = s2 : FALSE;
esac;
next(q) :=
case
state = s1 : TRUE;
state = s2 : FALSE;
TRUE : q;
esac;
next(r) :=
case
state = s1 : FALSE;
state = s2 : TRUE;
TRUE : r;
esac;
LTLSPEC
X r
But NuSMV returns that specification X r is false and yields a counterexample.