MODULE main

VAR
a1 : 0..2;
a2 : 0..2;
a3 : 0..3;

ASSIGN
  init(a1) := 0;
  init(a2) := 0;
  init(a3) := 0;

  next(a1) :=
    case
      a1 < 2 : a1 + 1;
      a1 = 2 : 0;
      TRUE   : a1;
    esac;

  next(a2) :=
    case
      a2 < 2 & a1 = 2 : a2 + 1;
      a2 = 2 & a1 = 2 : 0;
      TRUE            : a2;
    esac;

  next(a3) :=
    case
      a3 < 2 & a2 = 2 & a1 = 2 : a3 +1;
      a3 = 2 & a2 = 2 & a1 = 2 : 0;
      TRUE                     : a3;
    esac;

SPEC AG (! (a3 = 1 & a2 = 1 & a1 = 1))
SPEC AX (! AF (a3 = 0 & a2 = 0 & a1 = 0))
SPEC AG (AF (a3 = 0))