#cex.state[2:0] = 7  * cex.s2 = 1 * S.state[1:0] = 0 * EX(cex.state[2:0] = 2 *
# S.state[1:0] = 1) ;

#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 * S.state[1:0] = 0));
#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 0 ));
#cex.s2 = 1 * EX(cex.s2 = 1 * EX(cex.s3 = 1 ));
#cex.s2 = 1 * EX(cex.s2 = 0 * EX(cex.s3 = 1 ));
cex.state[2:0] = 7 * cex.s2 = 1 * S.state[1:0] = 0 * (EX(cex.state[2:0] = 2
* cex.s2 = 0 * S.state[1:0] = 1 * EX(cex.s2 = 0)));
 cex.s2 = 1 * S.state[1:0] = 0 * (EX( cex.s2 = 1 * S.state[1:0] = 0 * EX(S.state[1:0] = 0 * cex.s3 = 0 
* EX(S.state[1:0] =  0 * EX(S.state[1:0] = 1)))));