data

sorts Attribute, File, FileAndAttribute, State

op setAttr: State * FileAndAttribute -> State;

getAttr: State * File ->? Attribute;

initial: State

channel

set: FileAndAttribute;

hugo: File;

reply: Attribute

process

set?fa -> P( setAttr(s,fa) )

[] hugo?f -> reply!getAttr(s,f) -> P(s)