//Generated by c2fsm -cut -nodiv -int
model main {
var N,j,k,m,tmp;
//parameters N;
states stop,start,lbl_20_1,lbl_21_1,lbl_4_3;
transition t_51 :={
from := start;
to := stop;
guard := (N <= 2);
action:=;
};
transition t_76 :={
from := start;
to := lbl_21_1;
guard := (3 <= N);
action:= j' = N, k' = 0, m' = 1;
};
transition t_77 :={
from := start;
to := lbl_20_1;
guard := (3 <= N);
action:= j' = 1, k' = 0, m' = 1;
};
transition t_78 :={
from := start;
to := lbl_21_1;
guard := (4 <= N);
action:= j' = N, k' = 0, m' = 2;
};
transition t_79 :={
from := start;
to := lbl_20_1;
guard := (4 <= N);
action:= j' = 2, k' = 0, m' = 2;
};
transition t_60 :={
from := lbl_20_1;
to := lbl_4_3;
guard := (N <= 2j+k+2);
action:= k' = k+1, tmp' = k;
};
transition t_61 :={
from := lbl_20_1;
to := lbl_21_1;
guard := (2j+k+3 <= N);
action:= j' = N, m' = 2j+1;
};
transition t_62 :={
from := lbl_20_1;
to := lbl_20_1;
guard := (2j+k+3 <= N);
action:= j' = 2j+1, m' = 2j+1;
};
transition t_63 :={
from := lbl_20_1;
to := lbl_21_1;
guard := (2j+k+4 <= N);
action:= j' = N, m' = 2j+2;
};
transition t_64 :={
from := lbl_20_1;
to := lbl_20_1;
guard := (2j+k+4 <= N);
action:= j' = 2j+2, m' = 2j+2;
};
transition t_65 :={
from := lbl_21_1;
to := lbl_4_3;
guard := (N <= 2j+k+2);
action:= k' = k+1, tmp' = k;
};
transition t_66 :={
from := lbl_21_1;
to := lbl_21_1;
guard := (2j+k+3 <= N);
action:= j' = N, m' = 2j+1;
};
transition t_67 :={
from := lbl_21_1;
to := lbl_20_1;
guard := (2j+k+3 <= N);
action:= j' = 2j+1, m' = 2j+1;
};
transition t_68 :={
from := lbl_21_1;
to := lbl_21_1;
guard := (2j+k+4 <= N);
action:= j' = N, m' = 2j+2;
};
transition t_69 :={
from := lbl_21_1;
to := lbl_20_1;
guard := (2j+k+4 <= N);
action:= j' = 2j+2, m' = 2j+2;
};
transition t_56 :={
from := lbl_4_3;
to := stop;
guard := (N <= k+1);
action:=;
};
transition t_70 :={
from := lbl_4_3;
to := lbl_4_3;
guard := (k+2 = N);
action:= j' = 0, k' = k+1, m' = 0, tmp' = k;
};
transition t_71 :={
from := lbl_4_3;
to := lbl_21_1;
guard := (k+3 <= N);
action:= j' = N, m' = 1;
};
transition t_72 :={
from := lbl_4_3;
to := lbl_20_1;
guard := (k+3 <= N);
action:= j' = 1, m' = 1;
};
transition t_73 :={
from := lbl_4_3;
to := lbl_21_1;
guard := (k+4 <= N);
action:= j' = N, m' = 2;
};
transition t_74 :={
from := lbl_4_3;
to := lbl_20_1;
guard := (k+4 <= N);
action:= j' = 2, m' = 2;
};
}
strategy dumb {
Region init := { state = start };
}