sort Id = struct id1 | id2; sort Job = struct easy | hard | normal; Done = struct done_easy | done_hard | done_normal; map process: Job -> Done; eqn process(easy) = done_easy; process(hard) = done_hard; process(normal) = done_normal; act getH, getH0, getH1: Id; putH, putH0, putH1: Id; getM, getM0, getM1: Id; putM, putM0, putM1: Id; input: Id # Job; output: Id # Done; proc Hammer = sum id:Id . getH0(id) . putH0(id) . Hammer ; Mallet = sum id:Id . getM0(id) . putM0(id) . Mallet ; Jobber(id:Id) = sum job:Job . input(id,job) . ((job == easy) -> output(id,process(job)) . Jobber(id) + (job == hard) -> getH1(id) . putH1(id) . Finish(id,job) + (job == normal) -> (getM1(id) . putM1(id) . Finish(id,job) + getH1(id) . putH1(id) . Finish(id,job))) ; Finish(id:Id,job:Job) = output(id,process(job)) . Jobber(id) ; init hide( { getH, putH }, allow( { input, output, getH, putH }, comm( { getH0|getH1->getH, putH0|putH1->putH, getM0|getM1->getM, putM0|putM1->putM }, Jobber(id1) || Jobber(id2) || Hammer || Mallet )));