MODULE main
VAR
  p : boolean;
  q : boolean;
  r : boolean;
  state : {l0, l1, l2};

ASSIGN
  init(state) := l0;
  next(state) :=
    case
      state = l0 : {l1};
      state = l1 : {l0,l2};
      state = l2 : {l2};
    esac;

  init(p) := TRUE;
  init(q) := TRUE;
  init(r) := FALSE;

  next(p) := next(state) = l0;
  next(q) := next(state) = l0 | next(state) = l1;
  next(r) := next(state) = l1 | next(state) = l2;

LTLSPEC G(F(q));