Especificación en Z de temporizar

[CHAR]

FUNC == seq CHAR

HORA == N

FRECUENCIA == N

TABLA == P(FUNC x FRECUENCIA x HORA)

®temporizar: TABLA x HORA f TABLA x P(FUNC)
Ç_______________
®A t: TABLA; hact: HORA ¥ (let func_ejec == {e1: FUNC; e2: FRECUENCIA; e3: HORA
® | (e1,e2,e3) e t ¦ hact - e3 ù e2}) ¥
®temporizar(t, hact) = ((t\func_ejec) U {a: FUNC; b: FRECUENCIA; c: HORA | (a,b,c) e func_ejec ¥ (a,b,hact)},
®{p: FUNC; q: FRECUENCIA; r: HORA | (p,q,r) e func_ejec ¥ p})

Se especifica cómo funciona el temporizador en cada una de sus ejecuciones. Toma como entradas la tabla donde se indican las distintas funciones y el intervalo de temporización de cada una (TABLA en la especificación) y la hora actual y retorna la tabla actualizada. Quita de la misma el conjunto de entradas cuya frecuencia de ejecución resulte menor al tiempo transcurrido desde la última vez que fueron invocadas (func_ejec) y las reemplaza por correspondientes ternas donde la componente HORA (de última ejecución) iguala a la actual. También retorna el conjunto de las funciones que deben ser invocadas (son las primeras componentes de las ternas que conforman func_ejec). Esta salida representa la ejecución de dichas funciones.

GDES

Cálculo DFC