Especificación en Z de controlar_estado_tolva

El resultado obtenido en el cálculo de cohesión es tal, ya que se había diseñado este método para que se encargue de dos tareas no relacionadas estrechamente: controlar el estado de la tolva y calcular y mostrar por pantalla el tiempo restante hasta el llenado (en función del espacio y el rinde actual). Se decide entonces dividir estas funciones en dos métodos separados: controlar_estado_tolva y calc_tr (de este último sólo se da la signatura en Z, no se especifica su comportamiento).

ESPACIO == N

TIEMPO == N

VELOCIDAD ::= nula | sin_cambio

ESTADO ::= vaciando | cosechando | lista | tolva_llena | va_cos

TOLVA ::= abierta | cerrada

COSECHA ::= detenida | no_cambia

®e_max, e_min: ESPACIO

®controlar_estado_tolva: ESTADO x ESPACIO
® § ESTADO x VELOCIDAD x TOLVA x COSECHA
Ç_______________
® Ae: ESTADO; esp: ESPACIO | esp e 0 .. 100
® ¥ controlar_estado_tolva (e, esp)
® = if e e {vaciando, va_cos}
® then if esp < e_max
® then (e, sin_cambio, abierta, no_cambia)
® else (if e = vaciando then lista else cosechando, sin_cambio,
® cerrada, no_cambia)
® else if e = lista
® then (e, sin_cambio, cerrada, no_cambia)
® else if e = cosechando
® then if esp > e_min
® then (e, sin_cambio, cerrada, no_cambia)
® else (tolva_llena, nula, cerrada, detenida)
® else (tolva_llena, nula, cerrada, detenida)

RINDE == N

®calc_tr: ESPACIO x RINDE x TOLVA f TIEMPO

GDES

Cálculo DFC