import std::data;

function ceil_log2 (pint a) : pint
{
  pint i;
  pint M;
  chp {
     i := 0;
     M := a-1;
    *[ M > 0 -> i := i + 1; M := M/2 ];
     self := i
  }
}


template<pbool reset; pint V; pint N>
defchan gen_a1of <: chan(enum<N>) (std::data::d1of?!<N> d; bool!? a)
{
  { 0 <= V & V < N : "Initial token value out of range" };

  
  methods {
    /*-- initialize channel, sender end --*/
    send_init {
      [ reset -> (,i:N: [ i != V -> d.d[i]- [] else -> d.d[i]+ ])
      [] else -> (,i:N: d.d[i]-)
      ]   
    }

    /*-- set output data --*/
    set {
      [([]i:N: self = i -> d.d[i]+)]
    }

    /*-- finish synchronization --*/
    send_up {
      [a]
    }

    /*-- reset part of the protocol --*/
    send_rest {
      (,i:N:d.d[i]-);[~a]
    }

    /*-- initialize channel, receiver end --*/
    recv_init {
      a-
    }

    /*-- get value --*/
    get {
      [([]i:N:d.d[i] -> self := i)]
    }

    /*-- finish synchronization action --*/
    recv_up {
      a+
    }

    /*-- reset part of the protocol --*/
    recv_rest {
      [(&i:N:~d.d[i])];a-
    }

    /*-- probe expression on receiver --*/
    recv_probe = (|i:N:d.d[i]);

    // no sender probe
  }
}
export defchan a1of <: gen_a1of<false,0> () { }
export defchan ar1of <: gen_a1of<true,0> () { }


template<pbool reset; pint V; pint M>
defchan gen_aMx1of2 <: chan(int<M>) (std::data::Mx1of2?!<M> d; bool!? a)
{
  { 0 <= V & ceil_log2(V) < M : "Initial token value out of range" };
  
  methods {
    /*-- initialize channel, sender end --*/
    send_init {
      [ reset -> (,i:M: [ ((V >> i) & 1) = 0 -> d.d[i].f+ [] else -> d.d[i].t+ ])
      [] else -> (,i:M: d.d[i].t-,d.d[i].f-)
      ]
    }

    /*-- set output data --*/
    set {
      (,i:M: [((self >> i) & 1) = 0 -> d.d[i].f+ [] else -> d.d[i].t+ ])
    }

    /*-- finish synchronization --*/
    send_up {
      [a]
    }

    /*-- reset part of the protocol --*/
    send_rest {
      (,i:M: d.d[i].t-,d.d[i].f-);[~a]
    }

    /*-- initialize channel, receiver end --*/
    recv_init {
      a-
    }

    /*-- get value --*/
    get {
      [(&i:M: d.d[i].t | d.d[i].f)];
      self := 0;
      (;i:M: [ d.d[i].t -> self := self | (1 << i)
	     [] else -> skip
	     ]
      )
    }

    /*-- finish synchronization action --*/
    recv_up {
      a+
    }

    /*-- reset part of the protocol --*/
    recv_rest {
      [(&i:M:~d.d[i].t & ~d.d[i].f)];a-
    }

    /*-- probe expression on receiver --*/
    recv_probe = (d.d[0].t|d.d[0].f);

    // no sender probe
  }
}
export defchan aMx1of2 <: gen_aMx1of2<false,0> () { }
export defchan arMx1of2 <: gen_aMx1of2<true,0> () { }