// **************************************************************************
//
//    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
//
// **************************************************************************



import RoomHeating.*;
macro N =?, A_init =?, U =?, H =?, noH =?, noA =?, get =?, dif =?, off_temp =?, on_temp =?;
      
module Multiple(
    [N]real ?u, [N]real ?x_init, h, int ? N_on, hybrid [N]real x
) {	
    [N][N]real a;  
    [N]real Off;
    a = A_init;
    x = x_init;
    
    // Initialization Configuration
    InitRoom(a);
    InitHeater(h, N_on, Off);
    
    // Temperature Change
    loop{    
        // Continuous Dynamics
        for(i = 0..N-1) do || 
	    
	    SingleChange(a, h, u[i], H[i], Off[i], x, i);	
	    
	    // Switch Heater
	    Reset(h, Off, x, n, a); 
	
	    // Turned On/Off Heater 
	    { 
	      for(i = 0..N-1) do || { 
	        if((h[i] == 1.0) & (Off[i] == 1.0) & ((x[i]) <= on_temp)){ 
	  	    next(Off[i]) = 0.0 ; flow{}until(true) ; 
		}
	      } 
	    } ||
	    { 
	      for(i = 0..N-1) do || { 
	        if((h[i] == 1.0) & (Off[i] == 0.0) & ((x[i]) >= off_temp)){ 
	  	    next(Off[i]) = 1.0 ; flow{}until(true) ;   
		}		    
              }
	    }  
    }
} satisfies {
    // Specify the safety and liveness properties
    P_1 : assert A (forall(i = 0..N-1) (G (x[i] >= u)));    
    P_2 : assert A (forall(i = 0..N-1) (F (h[i] == 1.0)));    
    P_3 : assert A (forall(i = 0..N-1) (F (h[i] == 0.0)));
}