(#create)(#null) (*create?[d] (# cell)(#write)(# read)(# mutex)(# nomutex)(# lock)(# unlock) (cell![null] | mutex![] | d![read,write,lock,unlock] | read?[port]cell?[u](cell![u]|port![u]) |write?[u,ack]cell?[v](cell![u]|ack![]) |*lock?[ack]mutex?[](ack![]|nomutex![]) |*unlock?[ack]nomutex?[](ack![]|mutex![])) | *rec?[](#data)(#add1)(#add2)(#trace)(#ack1)(#ack2)(#ack3) (create![add1]add1?[r,w,m,n]m![ack1]ack1?[]w![data,ack2] ack2?[]r![add2]n![ack3]ack3?[]add2?[d]trace![d]) | context?[d]create![d])