-- simple counter: count from 1 to 4 and then start again
MODULE Proc
VAR
  n : {1, 2, 3, 4};

ASSIGN
  init(n) := 1;

  next(n) := case
               n=4: 1;
               n<4: n+1;
               TRUE: n;
             esac;
-- END MODULE Proc

MODULE main
VAR
  p : Proc;
-- END MODULE main

SPEC
  AG !(p.n=4)
-- "along all paths, in every state, n=4"
-- false. To get a scenario

SPEC
  AG (p.n=1 -> AF p.n=4)
-- "along all paths, in every state, whenever n=1, then along all paths eventually n=4"
-- true

SPEC
  AG AF p.n=1
-- "along all paths, in every state, always eventually n=1"
-- true