#include "list.h"

/*@ type Has_cycle_variant */

/*@ logic Has_cycle_variant has_cycle_variant(list l, list l1, list l2)
  reads l->tl */

/*@ requires
  @   finite(l)
  @ ensures 
  @   \result <=> cyclic(l) 
  @*/
int cyclic(list l) {
  list l1 = l;
  list l2;
  if (!l1) return 0;
  l2 = l1->tl;
  /*@ invariant (\exists plist pl1; lpath(l,pl1,l1)) &&
    @           (\exists plist pl12; lpath(l1,pl12,l2) && pl12!=nil())
    @ variant has_cycle_variant(l,l1,l2) for has_cycle_order
    @*/
  while (l1 != l2) {
    if (!l1 || !l2 || !l2->tl) return 0;
    l1 = l1->tl;
    l2 = l2->tl->tl;
  }
  return 1;
}