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




module thermostat_verification(
    hybrid real x,  y,  z, bool ? x_on, ? x_off, !on
){ 

    //Initialization
    x = 2.0 ; 
    y = 0.0 ; 
    z = 0.0 ;
  
    loop{

        // Heater is on
	on = true;
	flow{
	    drv(x) <- -cont(x) + 5.0;
	    drv(y) <- 1.0;
	    drv(z) <- 1.0;
	}until(cont(x) == 3.0 & x_off);
    
        // Heater is off
	on = false;
	flow{
	    drv(x) <- -cont(x);
	    drv(y) <- 1.0;
	    drv(z) <- 0.0;
	}until(cont(x) == 1.0 & x_on);
		
    }

} satisfies { 
  
    Safe : 
        assert A G 
            ((1.0 <= x) & (x <= 3.0)) ->
                ((y == 60.0) -> (z >= 2 * y / 3));
                
    StatesInvar : 
        assert A G 
            (1.0 <= x) & (x <= 3.0)  -> 
                (
                    on -> (2.0 <= drv(x)) & (drv(x) <= 4.0) & 
                    !on -> (-3.0 <= drv(x)) & (drv(x) <= -1.0)
                );

} drivenby Test01 {

    x_on = true;
    x_off = true;
    for(i=0..10)
        pause;
        
}