//Generated by c2fsm -cut -nodiv -int
model nd_loop {
var x,y;
//parameters;
states stop,start,lbl_5_1,cut;
transition t_22 :={
from := start;
to := lbl_5_1;
guard := true;
action:= x' = ?, y' = 0;
};
transition t_18 :={
from := lbl_5_1;
to := stop;
guard := ( (x <= y) || (y+3 <= x) );
action:=;
};
transition t_19 :={
from := lbl_5_1;
to := cut;
guard := ( ( (x <= y+2) && (x <= 9) ) && (y+1 <= x) );
action:=;
};
transition t_20 :={
from := lbl_5_1;
to := stop;
guard := ( ( (x <= y+2) && (y+1 <= x) ) && (10 <= x) );
action:=;
};
transition t_21 :={
from := cut;
to := lbl_5_1;
guard := true;
action:= x' = ?, y' = x;
};
}
strategy dumb {
Region init := { state = start };
}