point/.style={circle, draw=blue, thick, inner sep=3pt, minimum size=9mm},
        node distance=20mm]
      \node (3) [point] {};
      \node [lo=3] {$w_3$};
      \node (2) [point, below right of=3] {\alt<-2>{$\lab{q}$}{}};
      \node [aro=2] {$w_2$};

      \node (1) [point, below left of=3] {$\lab{q}$};
      \node [alo=1] {$w_1$};

      \begin{scope}[shorten <= 1mm, shorten >= 1mm, very thick,>=stealth]
        \draw [->] (1) to (3);
        \draw [->] (3) to (2);
        \draw [->] (3) to[out=45,in=45+90,looseness=4] (3);

      \draw [rounded corners=2mm, dashed] (-25mm,-20mm) rectangle (25mm,11mm);
      \node at (-25mm,8mm) [anchor=north east,inner sep=2mm] {$\mathcal{M}_{\alt<-2>{1}{2}}$};
      w_2 &\fc \all\some q \\
      w_3 &\fc q \to \all\some q \\
      w_2 &\fc q \\
      w_3 &\fc \some q \\
      w_1 &\fc \all\some q \\[1ex]
      \M_1  & \models  q \to \all\some q \\
      \mpause[2]{ \M_2  & \not\models  q \to \all\some q }
    Can you change the labelling such that such that
      \M \models q \to \all\some q
    is no longer valid?
  Yes, for example, by setting $\lab{L}(w_2) = \{\; \}$\;.