# Model ackerman¶

Cited in: [BenAmramL07].

Tag: complexity.

## Source code¶

```model ack {

var m, n;

states start, cont1, a, b, stop3, stop2, stop1;

transition t0bis := {
from   := start;
to     := cont1;
guard  := m > 0;
action := ;
};

transition t0 := {
from   := start;
to     := stop1;
guard  := m <= 0;
action := ;
};

transition t2 := {
from   := cont1;
to     := a;
guard  := n > 0;
action := n' = n - 1;
};

transition t1 := {
from   := cont1;
to     := stop2;
guard  := n <= 0;
action := m' = m - 1, n' = 1;
};

transition t3 := {
from   := a;
to     := b;
guard  := true;
action := m' = m - 1, n' = ?;
};

transition t4bis := {
from   := b;
to     := stop3;
guard  := n < 0;
action := ;
};

transition t4 := {
from   := b;
to     := start;
guard  := n >= 0;
action := ;
};

}

strategy ack_s {

Region init := {state = start && n >= 0 && m >= 0};

}```

## Expected invariant¶

`{ b[v1, v2] : v1 >= 0; stop1[0, v2] : v2 >= 0; cont1[v1, v2] : v1 >= 1 and v2 >= 0; start[v1, v2] : v1 >= 0 and v2 >= 0; a[v1, v2] : v2 >= 0 and v1 >= 1; stop2[v1, 1] : v1 >= 0; stop3[v1, v2] : v2 <= -1 and v1 >= 0 }`

## Results¶

• With Aspic: { stop1[0, n] : n >= 0; stop2[m, 1] : m >= 0; b[m, n] : m >= 0; start[m, n] : m >= 0 and n >= 0; stop3[m, n] : n <= -1 and m >= 0; cont1[m, n] : m >= 1 and n >= 0; a[m, n] : n >= 0 and m >= 1 } (0.05s), OK.
• With ISL: { b[m__1, n__1] : m__1 >= 0; stop1[0, n__1] : n__1 >= 0 or n__1 >= 0; cont1[m__1, n__1] : (n__1 >= 0 and m__1 >= 1) or (n__1 >= 0 and m__1 >= 1); start[m__1, n__1] : (n__1 >= 0 and m__1 >= 0) or (n__1 >= 0 and m__1 >= 0); a[m__1, n__1] : (n__1 >= 0 and m__1 >= 1) or (n__1 >= 0 and m__1 >= 1); stop2[m__1, 1] : m__1 >= 0 or m__1 >= 0; stop3[m__1, n__1] : m__1 >= 0 and n__1 <= -1 } (0.02s), OK.