MODULE main
VAR
  a : boolean;
  b : boolean;
  c : boolean;
  at : boolean;
  bt : boolean;
  ct : boolean;
  i : boolean;
  v : boolean;
ASSIGN
  init (a) := FALSE;
  next (a) := at;
  init (b) := FALSE;
  next (b) := bt;
  init (c) := FALSE;
  next (c) := ct;
  init (i) := FALSE;
  next (i) := TRUE;
  init (v) := FALSE;
  next (v) := 
   (!i & ((at = ct) & (bt != ct))) | 
   (v & ((at = bt) -> (a = b)));
SPEC
  AG (v -> (a != b))