// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************



macro N = ?, U = ?, H = ?, get = ?, 
      dif = ?, off_temp = ?, on_temp = ?;
module SingleChange(
    [N][N]real ?a, real ?u_s, ?H_s,?Off_s, [N]real ?h, hybrid [N]real x, nat ?s
) {
    flow{ drv(x[s]) <- ((sum(i = 0..N-1) (a[s][i]*cont(x[i]))) + U[s]*u_s + H[s]*h[s]*(1.0 - Off_s));	  
    }until(
        // continuous evolution terminated 
        //1. when heater switch conditions hold 
        ( cont(x[s]) <= get[s] & h[s] == 0.0 & 
        (exists(j = 0..N-1)((cont(x[j])-cont(x[s]) >= dif[s]) & (h[j] == 1.0) & (a[j][s] != 0))) ) 
            
        |
        
        	// 2. when heater needs to be turned on/off
        ( (h[s] == 1.0) & (((Off_s == 1.0) & 
        (cont(x[s]) <= on_temp))|((Off_s ==0.0) & 
        (cont(x[s]) >= off_temp))) )
     );
}