Especificación en Z de controlar_estado_tolva

RINDE == N

ESPACIO == N

TIEMPO == N

VELOCIDAD ::= nula | sin_cambio

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

TOLVA ::= abierta | cerrada

COSECHA ::= detenida | no_cambia

®calc_tr: ESPACIO x RINDE x TOLVA f TIEMPO
®e_max, e_min: ESPACIO

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

cal_tr calcula el tiempo restante para el llenado de la tolva en función del espacio disponible, el rinde actual y el estado de la tolva (vaciando o no).
Los distintos valores que conforman el tipo ESTADO representan las diferentes modalidades en que puede estar trabajando la cosechadora en un momento dado. En vaciando la tolva estará descargando su contenido y la maquinaria de cosecha estará detenida; en cosechando el proceso de cosecha estará en marcha y la tolva permanecerá cerrada; en lista la maquinaria se encontrará detenida preparada para comenzar la cosecha; en tolva_llena la cosecha estará detenida pero, por no haber espacio en la tolva no será posible reanudarla; por último, va_cos es cuando la máquina está cosechando y la tolva se encuentra descargando su contenido.

GDES

Cálculo DFC