I'm a little confused about some LTL syntax.
When the Global and Future operator (GFx) or <>x is used, what does it mean. In the lecture slides it is given as infinitely often. But I don't understand it.
When used as FGx or <>x, I understand it as eventually in the future something will be true forever. E.g. eventually x will become 3 (x = 3) and x will stay as 3 forever.
Can someone explain what GFx means?