I'm really new to Modal Logic (and logic in general, actually) and currently playing with a tree proof generator just to see how some stuff work, but I can't read the countermodels that the algorithm gives me when my proposition is invalid. I (kinda) understand the concept of possible words and so on, I just can't read it there. Can someone explain to me?
Example: https://www.umsu.de/trees/#%E2%96%A1(a%E2%86%92b)%20|=%20%C2%AC%E2%97%87(a%E2%86%92%C2%ACb)
First it gives the set of worlds. Then it lists the propositional variables, and next to them the set of worlds at which they hold. Then they give $R$, the accessibility relation between the worlds. So, this one says, there is one world, $w_0,$ and $a$ and $b$ are both false there, and then that the accessibility relation has $w_0$ accessible from itself.
Since $a$ and $b$ are false there, $a\to b$ holds at $w_0,$ as does $a\to \lnot b,$ and since $w_0$ is accessible from itself and the only thing accessible from itself, $\square(a\to b)$ and $\lozenge(a\to\lnot b)$ both hold at the only world $w_0.$ So it follows that this is a counter model to $\square (a\to b)\models \lnot\lozenge(a\to\lnot b)$.