/*

Digital filter example from ASTREE webpage:

typedef enum  {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN INIT; float P, X;
void filter ()  {
  static float E[2], S[2];
  if (INIT)  { 
    S[0] = X; P = X; E[0] = X; 
  } else { 
    P = ((((
	    (0.5 * X) - (E[0] * 0.7)
	    ) + 
	   (E[1] * 0.4)
	   ) + 
	  (S[0] * 1.5)) 
	 - (S[1] * 0.7)
	 ); 
  }
  E[1] = E[0]; 
  E[0] = X; 
  S[1] = S[0]; 
  S[0] = P;
  // S[0], S[1] in [-1327.02698354, 1327.02698354] 
}
void main ()  { X = 0.2 * X + 5; INIT = TRUE;
  while (1)  {
    X = 0.9 * X + 35; // simulated filter input 
    filter (); INIT = FALSE; }
}
*/

:- multifile r/5, implicit_updates/0, var2names/2, preds/2, cube_size/1, start/1, refinement/1, error/1.
refinement(inter).
cube_size(1).
start(pc(init)).
error(pc(error)).

var2names(p(_, data(P, X, E0, E1, S0, S1)),
	  [(P, 'p'), (X, 'x'), (E0, 'e[0]'), (E1, 'e[1]'), (S0, 's[0]'), (S1, 's[1]')]).
preds(p(_, data(P, X, E0, E1, S0, S1)), []).		

r(p(pc(init), data(P, X, E0, E1, S0, S1)),  p(pc(start),    data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp=0, Xp=0, E0p=0, E1p=0, S0p=0, S1p=0],  [], 1000).

r(p(pc(start), data(P, X, E0, E1, S0, S1)),  p(pc(first_input_X),    data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = 0.2 * X + 5, E0p = E0, E1p = E1, S0p = S0, S1p = S1],  [], 0).

r(p(pc(first_input_X),  data(P, X, E0, E1, S0, S1)), p(pc(filter_init), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = 0.9 * X + 35, E0p = E0, E1p = E1, S0p = S0, S1p = S1],  [], 1).

r(p(pc(filter_init), data(P, X, E0, E1, S0, S1)), p(pc(filter_E1), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = X, Xp = X, E0p = X, E1p = E1, S0p = X, S1p = S1],  [], 2).

r(p(pc(filter_P), data(P, X, E0, E1, S0, S1)), p(pc(filter_E1), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = (((((0.5 * X) - (E0 * 0.7)) + (E1 * 0.4)) + (S0 * 1.5)) - (S1 * 0.7)),
   Xp = X, E0p = E0, E1p = E1, S0p = S0, S1p = S1], [], 3).

r(p(pc(filter_E1),  data(P, X, E0, E1, S0, S1)), p(pc(filter_E0), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = X, E0p = E0, E1p = E0, S0p = S0, S1p = S1], [], 4).

r(p(pc(filter_E0),  data(P, X, E0, E1, S0, S1)), p(pc(filter_S1), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = X, E0p = X, E1p = E1, S0p = S0, S1p = S1], [], 5).

r(p(pc(filter_S1),  data(P, X, E0, E1, S0, S1)), p(pc(filter_S0), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = X, E0p = E0, E1p = E1, S0p = S0, S1p = S0], [], 6).

r(p(pc(filter_S0),  data(P, X, E0, E1, S0, S1)), p(pc(filter_P), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [Pp = P, Xp = X, E0p = E0, E1p = E1, S0p = P, S1p = S1], [], 7).

r(p(pc(filter_P),  data(P, X, E0, E1, S0, S1)), p(pc(error), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [S0 =< -1327.02698354], [], 8).

r(p(pc(filter_P),  data(P, X, E0, E1, S0, S1)), p(pc(error), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [S0 >= 1327.02698354], [], 9).

r(p(pc(filter_P),  data(P, X, E0, E1, S0, S1)), p(pc(error), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [S1 =< -1327.02698354], [], 10).

r(p(pc(filter_P),  data(P, X, E0, E1, S0, S1)), p(pc(error), data(Pp, Xp, E0p, E1p, S0p, S1p)),
  [S1 >= 1327.02698354], [], 11).