type Node = {
  bool next_ge, # true = next is greater or equal, false = next is less
       next_le; # true = next is less or equal, false = next is greater
  data next:Node;
}

pred inorder(pointer x:Node) = 
  allpos p of Node: x<next*>p & p.next!=null => p.next_ge=true;

pred inorder2(pointer x,y:Node) = 
  (y=null => inorder(x)) &
  (y!=null => allpos p of Node: x<next*>p & p<next.next*>y => p.next_ge=true);

pred consistent(pointer x:Node) = 
  allpos p of Node: x<next*>p & p.next!=null => p.next_ge | p.next_le;

proc bubblesort(data x:Node):Node
[consistent(x)]
{
  bool yn_le_y, yn_ge_y;
  pointer p,y,yn,t:Node;
  bool change;
  change = true;
  while [consistent(x) & (!change => inorder(x))] (change) {
    p = null;
    change = false;
    y = x;
    if (x!=null) {
      yn = y.next, yn_le_y = y.next_le, yn_ge_y = y.next_ge;
    }
    else { /*BUG FIX!*/
      yn = null;
    }
    while [(x!=null => y!=null & yn=y.next & (y!=x => p.next=y) & (y=x => p=null) & x<next*>y) &
           (x=null => yn=null) &
           consistent(x) & 
           (!change => inorder2(x,y)) &
           (yn!=null => yn_le_y=y.next_le & yn_ge_y=y.next_ge)]
          (yn!=null) {
      if (yn_le_y & !yn_ge_y /* y.value > yn.value */) {
        t = yn.next;
        change = true;
        y.next = t, y.next_le = ?, y.next_ge = ?; # don't know
        y.next_ge = y.next_ge | !y.next_le; # but the answer must be consistent
        yn.next = y, 
          yn.next_ge = yn_le_y, yn.next_le = yn_ge_y, yn_le_y = yn_ge_y, yn_ge_y = yn_le_y; # update
        if (p=null) {
          x = yn;
        }
        else {
          p.next = yn;
        }
        p = yn;
        yn = t, 
          yn_le_y = y.next_le, yn_ge_y = y.next_ge; # update
      }
      else {
        p = y;
        y = yn;
        yn = y.next, 
          yn_le_y = y.next_le, yn_ge_y = y.next_ge; # update
      }
    }
  }
  return x;
}
[inorder(return)]