136 lines
2.6 KiB
Text
136 lines
2.6 KiB
Text
|
|
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> () { }
|