$MAX=3; typedef data=0..$MAX-1; // A lossy buffer, with a single cell, that can hold a data. gal Buffer {
// MAX models an empty buffer int value=$MAX; /** Allows to write to the buffer, if it is empty */ transition put (data $d) [value==$MAX] label "send"($d) { value = $d; }
} composite Channel {
// the sender sends at most three messages BoundedCounter sender($BOUND=3); Buffer buff; synchronization sendData (data $d) { sender."inc"(1); buff."send"($d); }
} main Channel; property noDead [ctl] : AG (EX true);