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