# Computing Termination of core/src/test/resources/dbp_graph/termination/stealing3.dbp

• Computing Termination of core/src/test/resources/dbp_graph/termination/stealing3.dbp
• ## Input

```// Work stealing.

init
(w1, worker)* -> (j, job)** [job]

// *****************************************************************************

transition "steal"
pre
(w1, worker) -> (j, job) [job]
node (w2, worker)
post
node (w1, worker)
(w2, worker) -> (j, stolen) [job]
==>
w1 -> w1
w2 -> w2
j -> j
<==

transition "consume"
pre
(w1, worker) -> (j, _) [job]
post
node (w1, worker)
==>
w1 -> w1
<==

// *****************************************************************************
```

## Numerical Abstraction

```% BEGIN FIXED PREAMBLE
cube_size/1,start/1,error/1,refinement/1,cutpoint/1,invgen_template/2,
invgen_template/1,cfg_exit_relation/1,stmtsrc/2,strengthening/2,globals/3,
bound_var/2,bounding_vars/2,transition_access/2,atomic/3.
refinement(inter).
cube_size(1).
% END FIXED PREAMBLE

var2names( p(_, data(Job_1, Worker_1, Stolen_1)), [(Job_1, 'job\$1'), (Worker_1, 'worker\$1'), (Stolen_1, 'stolen\$1')]).

preds( p(_, data(Job_1, Worker_1, Stolen_1)), []).

trans_preds(
p(_, data(Job_1, Worker_1, Stolen_1)),
p(_, data(Job_1_prime, Worker_1_prime, Stolen_1_prime)),
[ 0 = Job_1_prime,
0 =< Job_1_prime,
Job_1_prime < Job_1,
Job_1_prime = Job_1,
0 = Worker_1_prime,
0 =< Worker_1_prime,
Worker_1_prime < Worker_1,
Worker_1_prime = Worker_1,
0 = Stolen_1_prime,
0 =< Stolen_1_prime,
Stolen_1_prime < Stolen_1,
Stolen_1_prime = Stolen_1
]).

start( pc(s__11)).
cutpoint(pc(s__1)).

% unfolding; morphing, steal; folding; covering
r(  p(pc(s__1), data(Job_1, Worker_1, Stolen_1)),
p(pc(s__1), data(Job_1_prime, Worker_1_prime, Stolen_1_prime)),
[ Stolen_1 - Stolen_1_prime = -1, Worker_1 = Worker_1_prime, Job_1 - Job_1_prime = 1, 0 =< Job_1_prime, 2 =< Worker_1_prime, 1 =< Stolen_1_prime ],
[], 0).
% unfolding; morphing, consume; folding; covering
r(  p(pc(s__1), data(Job_1, Worker_1, Stolen_1)),
p(pc(s__1), data(Job_1_prime, Worker_1_prime, Stolen_1_prime)),
[ Stolen_1 = Stolen_1_prime, Job_1_prime - Job_1 = -1, Worker_1 = Worker_1_prime, 1 =< Job_1, 0 =< Stolen_1_prime, 1 =< Worker_1_prime ],
[], 1).
% unfolding; morphing, consume; folding; covering
r(  p(pc(s__1), data(Job_1, Worker_1, Stolen_1)),
p(pc(s__1), data(Job_1_prime, Worker_1_prime, Stolen_1_prime)),
[ Stolen_1 - Stolen_1_prime = 1, Worker_1 = Worker_1_prime, Job_1 = Job_1_prime, 1 =< Worker_1_prime, 0 =< Stolen_1_prime, 0 =< Job_1_prime ],
[], 2).
% initialize
r(  p(pc(s__11), data(Job_1, Worker_1, Stolen_1)),
p(pc(s__1), data(Job_1_prime, Worker_1_prime, Stolen_1_prime)),
[ 0 =< Job_1_prime, 0 =< Worker_1_prime, 0 =< Stolen_1_prime ],
[], 3).
```

## ARMC output

```ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.jKXRGyS5om
]
...done.

--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3

==================================================
ARMC-LIVE: program is correct

abstract trans fixpoint
abstract_trans_state(0, pc(s__11), pc(s__11), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__11), pc(s__1), [2,6,10], stem, 2, (1,3)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,3,6,8,10], loop, 3, (2,0)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,8,10,11], loop, 4, (2,2)).

frontier 0: stem 1 (pc(s__11)->pc(s__11)) from 0 by applying 0: 	T
frontier 1: stem 2 (pc(s__11)->pc(s__1)) from 1 by applying 3: 	0=<job\$1', 0=<worker\$1', 0=<stolen\$1'
frontier 2: loop 3 (pc(s__1)->pc(s__1)) from 2 by applying 0: 	0=<job\$1', job\$1'<job\$1, 0=<worker\$1', worker\$1'=worker\$1, 0=<stolen\$1'
frontier 2: loop 4 (pc(s__1)->pc(s__1)) from 2 by applying 2: 	0=<job\$1', job\$1'=job\$1, 0=<worker\$1', worker\$1'=worker\$1, 0=<stolen\$1', stolen\$1'<stolen\$1

_5385->_5388:	#12:	0=job\$1', 0=<job\$1', job\$1'<job\$1, job\$1'=job\$1, 0=worker\$1', 0=<worker\$1', worker\$1'<worker\$1, worker\$1'=worker\$1, 0=stolen\$1', 0=<stolen\$1', stolen\$1'<stolen\$1, stolen\$1'=stolen\$1
---------------------------------------------+----run(s)----+---wall(s)----+
Time on instantiating uf axioms              |     0.00     |     0.00     |
Time on cli constraint solving               |     0.00     |     0.00     |
Time on cli constraint preparation           |     0.00     |     0.00     |
Time on cli matrix parsing                   |     0.00     |     0.00     |
Time on cli preprocessing                    |     0.00     |     0.00     |
Time on concretizing trans rel               |     0.00     |     0.00     |
Time on concretizing from state              |     0.00     |     0.00     |
Time on computing the subsumer subtree       |     0.00     |     0.00     |
Time on finding the location of subsumer in queue|     0.00     |     0.00     |
Time on path invariant generation            |     0.00     |     0.00     |
Time on new predicate selection              |     0.00     |     0.00     |
Time on refinement preprocessing cut         |     0.00     |     0.00     |
Time on refinement cutting trace             |     0.00     |     0.00     |
Time on refinement finding unsat subtrace    |     0.00     |     0.00     |
Time on refinement                           |     0.00     |     0.00     |
Time on fixpoint abstraction                 |     0.00     |     0.00     |
Time on fixpoint test                        |     0.00     |     0.00     |
Time on abstract check                       |     0.00     |     0.00     |
Time on total including result checking      |     0.00     |     0.00     |
Time on check result                         |     0.00     |     0.00     |
Time on total                                |     0.00     |     0.00     |
---------------------------------------------+--------------+--------------+

==================================================
ARMC-LIVE: program is correct

```