Why is GFp -> GFq false in LTL, even though GFp and GFq are false?

Consider the Kripke structure:
$$
\begin{array}{ccccccc}
\to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\
& \circlearrowright & & \circlearrowright & & \circlearrowright & \\
\end{array}
$$

where $(p, \neg q)$ means “$p$ and not $q$” and $\circlearrowright$ is a self loop. We number the states $s_1, s_2, s_3$ from left to right.
Now consider the three LTL properties:
$$
\begin{array}{ll}
M \vDash \mathbf{G}\,\mathbf{F}\,p \to \mathbf{G}\,\mathbf{F}\,q & \text{false} \\
M \vDash \mathbf{G}\,\mathbf{F}\,p & \text{false} \\
M \vDash \mathbf{G}\,\mathbf{F}\,q & \text{false} \\
\end{array}$$

The oddity is this: how can $\text{false} \to \text{false}$ be false?

P.S.: I am sure of the results because I used NuSMV with the following code:

MODULE main
VAR
   state : {a, b, c};
   p : boolean;
   q : boolean;

ASSIGN
   init(state) := a;
   next(state) := 
       case
         state=a : {a,b};
         state=b : c;
         state=c : c;
   esac;
p :=
  case
    state=a : TRUE;
    state=b : FALSE;
    state=c : FALSE;
  esac;
q :=
  case
    state=a : FALSE;
    state=b : FALSE;
    state=c : TRUE;
  esac;

LTLSPEC 
   ((G ( F p = TRUE)) ->  (G ( F q = TRUE)))
LTLSPEC 
   (G ( F p = TRUE))
LTLSPEC
   (G ( F q = TRUE))

This happens because of the way LTL formulae are evaluated over Kripke structures: Recall that LTL is first of all a logic of traces; when we say that a Kripke structure $S$ satisfies $\varphi$, we mean that all its traces do, i.e. we have an implicit universal quantification.

The consequence is that, for an LTL formula $\varphi$, it is possible that neither $\varphi$ nor $\neg\varphi$ is true for $S$, because neither holds for all traces. Similarly, none of your three formulas above holds for every trace.

If you are more familiar with predicate calculus, this is just saying that $(\forall x.A)\vee(\forall x.\neg A)$ is not a tautology, and neither is $(\forall x.A)\vee(\forall x.B)\vee(\forall x.A\to B)$.

StackExchange Computer Science Q#2548, answer score: 5