//Generated by c2fsm -cut -nodiv -int
model main {
var N,i,j,k,m,n;
//parameters N,m,n;
states stop,start,lbl_13_1,lbl_12_1,lbl_11_1;
transition t_25 :={
from := start;
to := stop;
guard := ( ( (N+1 <= 0) || (m+1 <= 0) ) || (n+1 <= 0) );
action:=;
};
transition t_33 :={
from := start;
to := stop;
guard := ( ( (0 <= N) && (0 <= m) ) && (0 = n) );
action:= i' = 0;
};
transition t_41 :={
from := start;
to := lbl_13_1;
guard := ( ( (0 <= N) && (0 = m) ) && (1 <= n) );
action:= i' = 1, j' = 0;
};
transition t_42 :={
from := start;
to := lbl_12_1;
guard := ( ( (0 = N) && (1 <= m) ) && (1 <= n) );
action:= i' = 0, j' = 1, k' = 0;
};
transition t_43 :={
from := start;
to := lbl_11_1;
guard := ( ( (1 <= N) && (1 <= m) ) && (1 <= n) );
action:= i' = 0, j' = 1, k' = 1;
};
transition t_31 :={
from := lbl_13_1;
to := stop;
guard := (n <= i);
action:=;
};
transition t_38 :={
from := lbl_13_1;
to := lbl_13_1;
guard := ( (i+1 <= n) && (m <= 0) );
action:= i' = i+1, j' = 0;
};
transition t_39 :={
from := lbl_13_1;
to := lbl_12_1;
guard := ( ( (N <= i) && (i+1 <= n) ) && (1 <= m) );
action:= i' = i, j' = 1, k' = i;
};
transition t_40 :={
from := lbl_13_1;
to := lbl_11_1;
guard := ( ( (i+1 <= N) && (i+1 <= n) ) && (1 <= m) );
action:= j' = 1, k' = i+1;
};
transition t_35 :={
from := lbl_12_1;
to := lbl_13_1;
guard := (m <= j);
action:= i' = i+1;
};
transition t_36 :={
from := lbl_12_1;
to := lbl_12_1;
guard := ( (N <= i) && (j+1 <= m) );
action:= i' = i, j' = j+1, k' = i;
};
transition t_37 :={
from := lbl_12_1;
to := lbl_11_1;
guard := ( (i+1 <= N) && (j+1 <= m) );
action:= j' = j+1, k' = i+1;
};
transition t_27 :={
from := lbl_11_1;
to := lbl_12_1;
guard := (N <= k);
action:= i' = k;
};
transition t_28 :={
from := lbl_11_1;
to := lbl_11_1;
guard := (k+1 <= N);
action:= k' = k+1;
};
}
strategy dumb {
Region init := { state = start };
}