//Generated by c2fsm -cut -nodiv -int
model main {
var N,j,k,m,tmp,tmp_1,tmp_2,tmp_3,tmp_4,tmp_5;
//parameters N;
states stop,start,lbl_27_1,lbl_28_1,lbl_13_3,lbl_7_1,lbl_12_1,lbl_12_3,lbl_11_1
,lbl_10_1,lbl_4_3;
transition t_71 :={
from := start;
to := stop;
guard := (N <= 2);
action:=;
};
transition t_89 :={
from := start;
to := lbl_7_1;
guard := (3 <= N);
action:= j' = 1, k' = 1, tmp_1' = ?;
};
transition t_92 :={
from := lbl_27_1;
to := lbl_13_3;
guard := (N <= 2j+k+2);
action:= k' = k+1, tmp' = k;
};
transition t_93 :={
from := lbl_27_1;
to := lbl_28_1;
guard := (2j+k+3 <= N);
action:= j' = N, m' = 2j+1;
};
transition t_94 :={
from := lbl_27_1;
to := lbl_27_1;
guard := (2j+k+3 <= N);
action:= j' = 2j+1, m' = 2j+1;
};
transition t_95 :={
from := lbl_27_1;
to := lbl_28_1;
guard := (2j+k+4 <= N);
action:= j' = N, m' = 2j+2;
};
transition t_96 :={
from := lbl_27_1;
to := lbl_27_1;
guard := (2j+k+4 <= N);
action:= j' = 2j+2, m' = 2j+2;
};
transition t_97 :={
from := lbl_28_1;
to := lbl_13_3;
guard := (N <= 2j+k+2);
action:= k' = k+1, tmp' = k;
};
transition t_98 :={
from := lbl_28_1;
to := lbl_28_1;
guard := (2j+k+3 <= N);
action:= j' = N, m' = 2j+1;
};
transition t_99 :={
from := lbl_28_1;
to := lbl_27_1;
guard := (2j+k+3 <= N);
action:= j' = 2j+1, m' = 2j+1;
};
transition t_100 :={
from := lbl_28_1;
to := lbl_28_1;
guard := (2j+k+4 <= N);
action:= j' = N, m' = 2j+2;
};
transition t_101 :={
from := lbl_28_1;
to := lbl_27_1;
guard := (2j+k+4 <= N);
action:= j' = 2j+2, m' = 2j+2;
};
transition t_82 :={
from := lbl_13_3;
to := stop;
guard := (N <= k+1);
action:=;
};
transition t_102 :={
from := lbl_13_3;
to := lbl_13_3;
guard := (k+2 = N);
action:= j' = 0, k' = k+1, m' = 0, tmp' = k;
};
transition t_103 :={
from := lbl_13_3;
to := lbl_28_1;
guard := (k+3 <= N);
action:= j' = N, m' = 1;
};
transition t_104 :={
from := lbl_13_3;
to := lbl_27_1;
guard := (k+3 <= N);
action:= j' = 1, m' = 1;
};
transition t_105 :={
from := lbl_13_3;
to := lbl_28_1;
guard := (k+4 <= N);
action:= j' = N, m' = 2;
};
transition t_106 :={
from := lbl_13_3;
to := lbl_27_1;
guard := (k+4 <= N);
action:= j' = 2, m' = 2;
};
transition t_76 :={
from := lbl_7_1;
to := lbl_10_1;
guard := ( ( (j <= 2tmp_1+2) && (2tmp_1+1 <= j) ) && (1 <= j) );
action:= tmp_4' = ?;
};
transition t_77 :={
from := lbl_7_1;
to := lbl_4_3;
guard := ( (j <= 2tmp_1+2) && (2tmp_1+1 <= j) );
action:= k' = k+1, tmp_5' = k;
};
transition t_62 :={
from := lbl_12_1;
to := lbl_12_3;
guard := ( (j <= 2tmp_2+2) && (2tmp_2+1 <= j) );
action:= j' = tmp_2;
};
transition t_74 :={
from := lbl_12_3;
to := lbl_7_1;
guard := true;
action:= tmp_1' = ?;
};
transition t_64 :={
from := lbl_11_1;
to := lbl_12_1;
guard := ( (j <= 2tmp_3+2) && (2tmp_3+1 <= j) );
action:= tmp_2' = ?;
};
transition t_66 :={
from := lbl_10_1;
to := lbl_11_1;
guard := ( (j <= 2tmp_4+2) && (2tmp_4+1 <= j) );
action:= tmp_3' = ?;
};
transition t_86 :={
from := lbl_4_3;
to := lbl_7_1;
guard := (k+1 <= N);
action:= j' = k, tmp_1' = ?;
};
transition t_87 :={
from := lbl_4_3;
to := stop;
guard := ( (N <= k) && (N <= 1) );
action:= k' = 0;
};
transition t_107 :={
from := lbl_4_3;
to := lbl_13_3;
guard := ( (2 = N) && (2 <= k) );
action:= j' = 0, k' = 1, m' = 0, tmp' = 0;
};
transition t_108 :={
from := lbl_4_3;
to := lbl_28_1;
guard := ( (N <= k) && (3 <= N) );
action:= j' = N, k' = 0, m' = 1;
};
transition t_109 :={
from := lbl_4_3;
to := lbl_27_1;
guard := ( (N <= k) && (3 <= N) );
action:= j' = 1, k' = 0, m' = 1;
};
transition t_110 :={
from := lbl_4_3;
to := lbl_28_1;
guard := ( (N <= k) && (4 <= N) );
action:= j' = N, k' = 0, m' = 2;
};
transition t_111 :={
from := lbl_4_3;
to := lbl_27_1;
guard := ( (N <= k) && (4 <= N) );
action:= j' = 2, k' = 0, m' = 2;
};
}
strategy dumb {
Region init := { state = start };
}