// **************************************************************************
//
//    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
//
// **************************************************************************
// 
// The example has a if-else statement inside of which there is a flow statement.
// For verification
// ******************************************************************************




module FlowIfElseComplex(hybrid real b,a,c){

  loop{
     if (a==1.0) {
	  l1,l2:flow{
	      drv(a) <- 0.0;
	      drv(b) <- 0.0;
	      drv(c) <- 1.0;	    
	  }until(cont(c) >= 1.0);
      }
      else{
	  l3,l4:flow{
	      drv(a) <- 0.0;
	      drv(b) <- 0.0;
	      drv(c) <- -1.0;
	  }until(cont(c) <= 0.0);
      }
      next(b) = b+1;
      if (a==1.0) {next(a) = 0.0;}
      else{next(a) = 1.0;}
      flow{
	drv(a) <- 0.0;
	drv(b) <- 0.0;
	drv(c) <- 0.0;
      }until(true);
    }
}
satisfies{// Specify sequence property
  p1: assert (c > 0 -> (E F (c*b>=1.5 and a == 0.0)));
}
drivenby{
 b = 0;
 a = 1.0;
 b = 0.0;
pause;
 for(i = 0..3)
pause;
}