Especificación en Z de controlar_rinde

RINDE == N

VELOCIDAD == N

[SEMILLA]

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

®delta: RINDE
®calc_vel: RINDE x RINDE x VELOCIDAD f VELOCIDAD
®rinde_optimo: SEMILLA f RINDE

Considerar que el rinde actual debe ser exactamente igual al óptimo ocasionaría, debido a la naturaleza cambiante de la magnitud, constantes cambios en la velocidad. Para evitar esto, se considera un intervalo de tolerancia (rinde_optimo¹delta).

®vel_min, vel_max: SEMILLA f VELOCIDAD

Estas funciones dan los límites de velocidad aceptables para una semilla dada.

®controlar_rinde: SEMILLA x RINDE x VELOCIDAD x ESTADO f VELOCIDAD
Ç_______________
® As: SEMILLA; r: RINDE; v: VELOCIDAD; e: ESTADO
® ¥ controlar_rinde (s, r, v, e)
® = if e ä {cosechando, va_cos}
® v rinde_optimo s - delta ø r ø rinde_optimo s + delta
® then v
® else if calc_vel (r, (rinde_optimo s), v) < vel_min s
® then vel_min s
® else if calc_vel (r, (rinde_optimo s), v) > vel_max s
® then vel_max s
® else calc_vel (r, (rinde_optimo s), v)

GDES

Cálculo DFC