MODULE main
VAR
  k: 10..10;
  m0: process bottom(m5, k);
  m1: process machine(m0, k);
  m2: process machine(m1, k);
  m3: process machine(m2, k);
  m4: process machine(m3, k);
  m5: process machine(m4, k);
SPEC
  AG AF( (m0.s = m1.s) & (m1.s = m2.s) & (m2.s = m3.s) & (m3.s = m4.s) & (m4.s = m5.s) )

MODULE machine(l, k)
VAR
  s: 0..k;
ASSIGN
  init(s) := 0;
  next(s) := case
           !(l.s = s) : l.s;
           TRUE : s;
           esac;
FAIRNESS running
SPEC
   AG AF ( l.s != s )

MODULE bottom(l, k)
VAR
  s: 0..k;
ASSIGN
  init(s) := 0;
  next(s) := case
            (l.s = s) : (s+1) mod k;
            TRUE : s;
            esac;
FAIRNESS running