//Generated by c2fsm -cut -nodiv -int
model gcd {
var x,y;
//parameters;
states stop,start,lbl_6,lbl_10_1,lbl_11_1,cut;
transition t_18 :={
from := start;
to := stop;
guard := (x <= 0);
action:=;
};
transition t_20 :={
from := start;
to := lbl_6;
guard := ( (1 <= x) && (y <= 0) );
action:=;
};
transition t_30 :={
from := start;
to := cut;
guard := ( (y = x) && (1 <= y) );
action:=;
};
transition t_31 :={
from := start;
to := lbl_10_1;
guard := ( (x+1 <= y) && (1 <= x) );
action:= y' = y-x;
};
transition t_32 :={
from := start;
to := lbl_11_1;
guard := ( (y+1 <= x) && (1 <= y) );
action:= x' = x-y;
};
transition t_2 :={
from := lbl_6;
to := stop;
guard := true;
action:=;
};
transition t_24 :={
from := lbl_10_1;
to := cut;
guard := (y = x);
action:=;
};
transition t_25 :={
from := lbl_10_1;
to := lbl_10_1;
guard := (x+1 <= y);
action:= y' = y-x;
};
transition t_26 :={
from := lbl_10_1;
to := lbl_11_1;
guard := (y+1 <= x);
action:= x' = x-y;
};
transition t_27 :={
from := lbl_11_1;
to := cut;
guard := (y = x);
action:=;
};
transition t_28 :={
from := lbl_11_1;
to := lbl_10_1;
guard := (x+1 <= y);
action:= y' = y-x;
};
transition t_29 :={
from := lbl_11_1;
to := lbl_11_1;
guard := (y+1 <= x);
action:= x' = x-y;
};
transition fromCut :={
from := cut;
to := stop;
guard := true;
action:=;
};
}
strategy dumb {
Region init := { state = start };
}