You can try the model checker in the teaching tools with the following transition system
vars b,c;
init 0;
labels 0:c; 1:; 2:b;
transitions 0->1; 1->2; 2->2;
and properties
c ∧ E X(b∧¬c);
c ∧ E X E F(b∧¬c);
You will then see that
- 〖b〗= {s2}
- 〖c〗= {s0}
- 〖!c〗= {s1;s2}
- 〖b & !c〗 = {s2}
- 〖EX(b & !c)〗 = {s1;s2}
- 〖c & EX(b & !c)〗 = {}
- 〖EF(b & !c)〗 = {s0;s1;s2}
- 〖EX EF (b & !c)〗 = {s0;s1;s2}
- 〖c & EX EF (b & !c)〗 = {s0}
The latter is clear since c holds on s0, and s0 has a next state, namely s1, such that EF(b & !c) holds there. Note that b & !c holds on s2, and that s2 can be reached from s0;s1;s2.
