//Generated by c2fsm -cut -nodiv -int
model main {
var n,tmp,x,y;
//parameters n;
states stop,start,lbl_7_2,lbl_4_2,cut;
transition t_17 :={
from := start;
to := stop;
guard := (x+1 <= 0);
action:=;
};
transition t_19 :={
from := start;
to := lbl_4_2;
guard := ( (0 <= x) && (0 <= y) );
action:= y' = y-1;
};
transition t_27 :={
from := start;
to := cut;
guard := (0 <= x);
action:= x' = x-1;
};
transition t_28 :={
from := start;
to := lbl_7_2;
guard := ( (y <= n) && (0 <= x) );
action:= tmp' = y, x' = x-1, y' = y+1;
};
transition t_23 :={
from := lbl_7_2;
to := cut;
guard := true;
action:=;
};
transition t_24 :={
from := lbl_7_2;
to := lbl_7_2;
guard := (y <= n);
action:= tmp' = y, y' = y+1;
};
transition t_14 :={
from := lbl_4_2;
to := lbl_4_2;
guard := (0 <= y);
action:= y' = y-1;
};
transition t_25 :={
from := lbl_4_2;
to := cut;
guard := true;
action:= x' = x-1;
};
transition t_26 :={
from := lbl_4_2;
to := lbl_7_2;
guard := (y <= n);
action:= tmp' = y, x' = x-1, y' = y+1;
};
transition t_20 :={
from := cut;
to := stop;
guard := (x+1 <= 0);
action:=;
};
transition t_22 :={
from := cut;
to := lbl_4_2;
guard := ( (0 <= x) && (0 <= y) );
action:= y' = y-1;
};
transition t_29 :={
from := cut;
to := cut;
guard := (0 <= x);
action:= x' = x-1;
};
transition t_30 :={
from := cut;
to := lbl_7_2;
guard := ( (y <= n) && (0 <= x) );
action:= tmp' = y, x' = x-1, y' = y+1;
};
}
strategy dumb {
Region init := { state = start };
}