#include <vcc.h>
#include <stdio.h>

typedef unsigned char task;

typedef struct delay {
  // abstract
  _(ghost \bool adelayed)
  _(ghost \natural tickcount)
  _(ghost \natural awaketime)
  _(ghost task adelayedtask)
  // abstract invariants
  _(invariant adelayed ==> ((tickcount <= awaketime) && (awaketime <= tickcount+60)))
  // concrete
  unsigned ctickcount; // clocked tick count
  task delayedtask;  // delayed task id
  unsigned delayed; // is there a delayed task to be woken in this clock cycle
  unsigned odelayed; // is there a delayed task to be woken in next clock cycle
  unsigned waketime; // time to wakeup delayed task
  unsigned owaketime; // overflowed wake time
  // concrete invariants
  _(invariant ctickcount < 60)
  _(invariant waketime < 60)
  _(invariant owaketime < 60)
  _(invariant delayed ==> ctickcount < waketime)
  _(invariant odelayed ==> owaketime <= ctickcount)
  _(invariant delayed ==> !odelayed)
  // gluing invariants
  _(invariant adelayed <==> (delayed || odelayed))
  _(invariant adelayed ==> (adelayedtask == delayedtask))
  // _(invariant ctickcount == tickcount % 60)
  // _(invariant delayed ==> (waketime == awaketime % 60))
  // _(invariant odelayed ==> (owaketime == awaketime % 60))
  _(invariant delayed ==> (awaketime - tickcount == waketime - ctickcount))
  _(invariant odelayed ==> (awaketime - tickcount == ((60 - ctickcount) + owaketime)))
} delay;

void init(delay *q)
  _(writes \span(q))
  _(ensures \wrapped(q))
 {
  _(ghost q->tickcount = 0)
  _(ghost q->adelayed = 0)
  _(ghost q->awaketime = 0)
  q->ctickcount = 0;
  q->delayedtask = 0;
  q->delayed = 0; // no task to be woken this cycle
  q->odelayed = 0; // no task to be woken next cycle
  q->waketime = 0;
  q->owaketime = 0;
  _(wrap q)
}

void delay(delay *q, task t, unsigned d)
  _(requires d > 0)
  _(requires \wrapped(q))
  _(requires d <= 60)
  _(writes q)
  _(ensures \wrapped(q))
{
  _(unwrap q)
  // abstract operation
  _(ghost
    if (!q->adelayed) {
      q->adelayed = \true;
      q->adelayedtask = t;
      q->awaketime = q->tickcount + d;
    }
   )
  // concrete operation
  unsigned p = 0;
  unsigned overflowed = 0;
  if (!(q->delayed || q->odelayed) && d <= 60) {
    q->delayedtask = t;
    p = q->ctickcount;
    while (d > 0)
      _(invariant d <= \old(d))
      _(invariant p == (q->ctickcount + (\old(d) - d)) % 60)
      _(invariant overflowed == 0 <==> ((q->ctickcount + (\old(d) - d)) < 60))
      _(invariant overflowed == 1 <==> ((q->ctickcount + (\old(d) - d)) >= 60))
    {
      if (p < 59)
        p++;
      else {
        p = 0;
        overflowed = 1;
      }
      d--;
    } 
    if (overflowed) {
      q->owaketime = p;
      q->odelayed = 1;
    }
    else {
      q->waketime = p;
      q->delayed = 1;
    }
  }
  _(wrap q)
}

task tick(delay *q)
_(requires \wrapped(q))
// _(requires q->adelayed && q->tickcount < q->awaketime - 1 && q->delayed && q->ctickcount == 59)
_(writes q)
_(ensures \wrapped(q))
{
  _(unwrap q)
  // abstract operation
  _(ghost q->tickcount = q->tickcount + 1)
  _(ghost
    if (q->awaketime == q->tickcount) {
      // arettask = q->adelayedtask
      q->adelayed = \false;
    }
   )
  _(assert !(q->delayed && q->odelayed))
   // concrete operation
  if (q->ctickcount < 59)
    q->ctickcount++;
  else {
    q->ctickcount = 0;
    q->delayed = q->odelayed;
    q->odelayed = 0;
    q->waketime = q->owaketime;
  }
  if (q->waketime == q->ctickcount) {
    q->delayed = 0;
    _(wrap q)
    return q->delayedtask;
  }
  else {
    _(wrap q)
    return 0;
  }
}