La gestión del peso de la caja la realiza la capsula Caja. Por tanto, el proceso Empaquetador no sabe nada del peso actual de la caja. La acción de almacenar una pasta en la caja se desdobla en dos:
----------------------------------------------- TASK Empaquetador; VAR pasta : TipoPasta; BEGIN LOOP Mostrador.TomarPasta (pasta); Caja.SiguientePasta (pasta); Caja.AlmacenarPasta (pasta); END (* LOOP *) END Empaquetador; -------------------------------------------------------------------------- CAPSULA Caja; VAR reponer : BOOLEAN (* valor inicial : FALSE *); VAR retirar : BOOLEAN (* valor inicial : FALSE *); OPERACION SiguientePasta (pasta : TipoPasta); PRE: TRUE POST: reponer = (pesoActual + Peso(pasta) > PesoMaximo) OPERACION AlmacenarPasta (pasta : TipoPasta); PRE: NOT (reponer) POST: pesoActual = pesoActual' + Peso(pasta) OPERACION ReponerCaja (); PRE: reponer POST: NOT (reponer) AND pesoActual = 0 OPERACION RetirarCaja (); PRE: retirar POST: NOT (retirar) AND reponer --------------------------------------------------------------------------