MODULE main
  VAR state : { s0,s1,s2,s3,s4,s5,s6 };
  DEFINE
    p := state=s0 | state=s2;
    q := state=s1;
    r := state=s3 | state=s4 | state=s6;
    s := state=s1 | state=s5 | state=s6;
    t := state=s3;
  ASSIGN
    init(state) := s0;
    next(state) :=
      case
        state=s0 : s1;
        state=s1 : { s2, s3 };
        state=s2 : s0;
        state=s3 : s4;
        state=s4 : { s5, s6 };
        state=s5 : s3;
        state=s6 : s3;
      esac;
  
  -- 1.
  SPEC AG (t -> r)
  -- 2.
  SPEC AG (s -> r)
  -- 3.
  SPEC A[ 0 U p ]
  -- 4.
  SPEC E[ 0 U p ]
  -- 5.
  SPEC AG E[ 0 U p ]
  -- 6.
  SPEC AG (q -> EG (r | q))
  -- 7.
  SPEC AG (q -> AG (r | q))
  -- 8.
  SPEC AG EF p
  -- 9.
  SPEC EG EF p
  -- 10.
  SPEC AG (E[ r U t] -> r)
  -- 11.
  SPEC EG (!r -> EG EF p)
  -- 12.
  SPEC EG (!r -> AG EF p)