Computing Termination of core/src/test/resources/dbp_graph/termination/stealing-3proc.dbp
Computing Termination of core/src/test/resources/dbp_graph/termination/stealing-3proc.dbp
Input
// Work stealing. 3 workers
init
(w1, worker) -> (j1, job)* [job]
(w2, worker) -> (j2, job)* [job]
(w3, worker) -> (j3, job)* [job]
// *****************************************************************************
transition "steal"
pre
node (w2, worker)
(w1, worker) -> (j, job) [job]
post
node (w1, worker)
(w2, worker) -> (j, stolen) [job]
==>
w1 -> w1
w2 -> w2
j -> j
<==
no
(w2, worker) -> (j, _) [job]
==>
w2 -> w2
transition "consume"
pre
(w1, worker) -> (j, _) [job]
post
node (w1, worker)
==>
w1 -> w1
<==
// *****************************************************************************
Graph rewriting system
-
Initial Configuration
-
Transitions
-
steal
-
consume
Cover
-
cover element 0
-
cover element 1
-
cover element 2
Numerical Abstraction
% BEGIN FIXED PREAMBLE
:- multifile r/5,implicit_updates/0,var2names/2,preds/2,trans_preds/3,
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_16, Stolen_5, Job_3, Stolen_1, Job_15)), [(Job_16, 'job$16'), (Stolen_5, 'stolen$5'), (Job_3, 'job$3'), (Stolen_1, 'stolen$1'), (Job_15, 'job$15')]).
preds( p(_, data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)), []).
trans_preds(
p(_, data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(_, data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16_prime + Job_3_prime + Job_15_prime < Job_16 + Job_3 + Job_15,
Job_16_prime + Job_3_prime + Job_15_prime = Job_16 + Job_3 + Job_15,
0 = Job_16_prime,
0 =< Job_16_prime,
Job_16_prime < Job_16,
Job_16_prime = Job_16,
0 = Stolen_5_prime,
0 =< Stolen_5_prime,
Stolen_5_prime < Stolen_5,
Stolen_5_prime = Stolen_5,
0 = Job_3_prime,
0 =< Job_3_prime,
Job_3_prime < Job_3,
Job_3_prime = Job_3,
0 = Stolen_1_prime,
0 =< Stolen_1_prime,
Stolen_1_prime < Stolen_1,
Stolen_1_prime = Stolen_1,
0 = Job_15_prime,
0 =< Job_15_prime,
Job_15_prime < Job_15,
Job_15_prime = Job_15
]).
start( pc(s__55)).
cutpoint(pc(s__7)).
cutpoint(pc(s__1)).
cutpoint(pc(s__3)).
% unfolding; morphing, consume; covering
r( p(pc(s__7), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Stolen_5_prime = 1, Job_16 = Job_15_prime, Stolen_5 = 1, Job_16_prime - Job_15 = -1, 1 =< Job_15, 0 =< Job_15_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 0).
% morphing, consume; covering
r( p(pc(s__7), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15_prime = Job_16, Stolen_5 = 1, Job_16_prime = Job_15, Stolen_5_prime = 0, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 1).
% unfolding; morphing, consume; covering
r( p(pc(s__7), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16_prime = Job_15, Job_16 - Job_15_prime = 1, Stolen_5 = 1, Stolen_5_prime = 1, 0 =< Job_15, 0 =< Job_15_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 2).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__7), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Stolen_5_prime = 1, Job_16 - Job_16_prime = 1, Stolen_5 = 1, Stolen_1_prime = 1, 0 =< Job_16_prime, 0 =< Job_15, Job_3_prime = 0, Job_15_prime = 0 ],
[], 3).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__7), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Stolen_5_prime = 1, Stolen_5 = 1, Stolen_1_prime = 1, Job_15 - Job_16_prime = 1, 0 =< Job_16, 0 =< Job_16_prime, Job_3_prime = 0, Job_15_prime = 0 ],
[], 4).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16 - Job_15_prime = 1, Stolen_5_prime = 1, Job_16_prime = Job_3, 0 =< Job_15, 0 =< Job_15_prime, 0 =< Job_3, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 5).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 - Job_15_prime = 1, Job_3 = Job_16_prime, Stolen_5_prime = 1, 0 =< Job_16, 0 =< Job_15_prime, 0 =< Job_16_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 6).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 - Job_15_prime = 1, Job_16 = Job_16_prime, Stolen_5_prime = 1, 0 =< Job_16_prime, 0 =< Job_3, 0 =< Job_15_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 7).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 = Job_15_prime, Stolen_5_prime = 1, Job_3 - Job_16_prime = 1, 0 =< Job_16, 0 =< Job_15_prime, 0 =< Job_16_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 8).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 = Job_16_prime, Job_16 - Job_15_prime = 1, Stolen_5_prime = 1, 0 =< Job_3, 0 =< Job_15_prime, 0 =< Job_16_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 9).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16 = Job_15_prime, Stolen_5_prime = 1, Job_3 - Job_16_prime = 1, 0 =< Job_15, 0 =< Job_15_prime, 0 =< Job_16_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 10).
% unfolding; morphing, consume; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__3), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 = Job_3_prime, Job_16 = Job_15_prime, Job_16_prime - Job_3 = -1, 1 =< Job_3, 0 =< Job_15_prime, 0 =< Job_3_prime, Stolen_5_prime = 0, Stolen_1_prime = 0 ],
[], 11).
% unfolding; morphing, consume; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__3), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 = Job_3_prime, Job_16 - Job_16_prime = 1, Job_3 = Job_15_prime, 0 =< Job_16_prime, 0 =< Job_3_prime, 0 =< Job_15_prime, Stolen_5_prime = 0, Stolen_1_prime = 0 ],
[], 12).
% unfolding; morphing, consume; covering
r( p(pc(s__3), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__3), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_15 - Job_16_prime = 1, Job_16 = Job_3_prime, Job_3 = Job_15_prime, 0 =< Job_16_prime, 0 =< Job_3_prime, 0 =< Job_15_prime, Stolen_5_prime = 0, Stolen_1_prime = 0 ],
[], 13).
% morphing, consume; covering
r( p(pc(s__1), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16 = Job_16_prime, Stolen_1_prime = 1, Stolen_5 = 1, Stolen_1 = 1, Stolen_5_prime = 0, Job_3_prime = 0, Job_15_prime = 0 ],
[], 14).
% unfolding; inhibiting; morphing, steal; covering
r( p(pc(s__1), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16 - Job_16_prime = 1, Stolen_5_prime = 1, Stolen_5 = 1, Stolen_1_prime = 1, Stolen_1 = 1, 0 =< Job_16_prime, Job_3_prime = 0, Job_15_prime = 0 ],
[], 15).
% morphing, consume; covering
r( p(pc(s__1), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Job_16 = Job_16_prime, Stolen_1_prime = 0, Stolen_5 = 1, Stolen_1 = 1, Stolen_5_prime = 1, Job_3_prime = 0, Job_15_prime = 0 ],
[], 16).
% initialize
r( p(pc(s__55), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__7), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ 0 =< Job_16_prime, Stolen_5_prime = 1, 0 =< Job_15_prime, Job_3_prime = 0, Stolen_1_prime = 0 ],
[], 17).
% initialize
r( p(pc(s__55), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__3), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ 0 =< Job_3_prime, 0 =< Job_15_prime, 0 =< Job_16_prime, Stolen_5_prime = 0, Stolen_1_prime = 0 ],
[], 18).
% initialize
r( p(pc(s__55), data(Job_16, Stolen_5, Job_3, Stolen_1, Job_15)),
p(pc(s__1), data(Job_16_prime, Stolen_5_prime, Job_3_prime, Stolen_1_prime, Job_15_prime)),
[ Stolen_5_prime = 1, Stolen_1_prime = 1, 0 =< Job_16_prime, Job_3_prime = 0, Job_15_prime = 0 ],
[], 19).
ARMC output
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.U6289Vd0ug
]
reading input from /tmp/tmp.U6289Vd0ug
...done.
--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4
==================================================
ARMC-LIVE: program is correct
abstract trans fixpoint
abstract_trans_state(0, pc(s__55), pc(s__55), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__55), pc(s__7), [4,8,11,12,15,16,20], stem, 2, (1,17)).
abstract_trans_state(1, pc(s__55), pc(s__3), [4,7,8,12,15,16,20], stem, 3, (1,18)).
abstract_trans_state(1, pc(s__55), pc(s__1), [4,8,11,12,16,19,20], stem, 4, (1,19)).
abstract_trans_state(2, pc(s__7), pc(s__7), [1,4,8,10,11,12,14,15,16,18,20], loop, 5, (2,0)).
abstract_trans_state(2, pc(s__7), pc(s__7), [2,4,7,8,9,11,12,14,15,16,18,20], loop, 6, (2,1)).
abstract_trans_state(2, pc(s__7), pc(s__1), [1,4,5,8,10,11,12,14,16,19,20], loop, 7, (2,3)).
abstract_trans_state(2, pc(s__7), pc(s__1), [1,4,8,10,11,12,14,16,19,20,21], loop, 8, (2,4)).
abstract_trans_state(2, pc(s__3), pc(s__7), [1,4,8,11,12,15,16,18,20], loop, 9, (3,5)).
abstract_trans_state(2, pc(s__3), pc(s__3), [1,4,7,8,10,12,15,16,18,20], loop, 10, (3,11)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,7,8,9,11,12,14,16,18,19,20,22], loop, 11, (4,14)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,4,5,8,10,11,12,14,16,18,19,20,22], loop, 12, (4,15)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,8,10,11,12,14,15,16,17,19,20,22], loop, 13, (4,16)).
abstract_trans_state(3, pc(s__7), pc(s__7), [1,4,7,8,9,11,12,14,15,16,18,20], loop, 14, (5,1)).
abstract_trans_state(3, pc(s__7), pc(s__1), [1,4,8,10,11,12,14,16,19,20], loop, 15, (5,3)).
abstract_trans_state(3, pc(s__7), pc(s__1), [1,4,5,7,8,9,11,12,14,16,19,20], loop, 16, (7,14)).
abstract_trans_state(3, pc(s__7), pc(s__1), [1,4,7,8,9,11,12,14,16,19,20,21], loop, 17, (8,14)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,4,8,11,12,16,19,20], loop, 18, (9,3)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,4,5,7,8,9,11,12,14,16,18,19,20,22], loop, 19, (12,14)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,4,5,8,10,11,12,14,15,16,17,19,20,22], loop, 20, (12,16)).
abstract_trans_state(4, pc(s__7), pc(s__1), [1,4,7,8,9,11,12,14,16,19,20], loop, 21, (15,14)).
frontier 0: stem 1 (pc(s__55)->pc(s__55)) from 0 by applying 0: T
frontier 1: stem 2 (pc(s__55)->pc(s__7)) from 1 by applying 17: 0=<job$16', 0=<stolen$5', 0=job$3', 0=<job$3', 0=stolen$1', 0=<stolen$1', 0=<job$15'
frontier 1: stem 3 (pc(s__55)->pc(s__3)) from 1 by applying 18: 0=<job$16', 0=stolen$5', 0=<stolen$5', 0=<job$3', 0=stolen$1', 0=<stolen$1', 0=<job$15'
frontier 1: stem 4 (pc(s__55)->pc(s__1)) from 1 by applying 19: 0=<job$16', 0=<stolen$5', 0=job$3', 0=<job$3', 0=<stolen$1', 0=job$15', 0=<job$15'
frontier 2: loop 5 (pc(s__7)->pc(s__7)) from 2 by applying 0: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'=stolen$1, 0=<job$15'
frontier 2: loop 6 (pc(s__7)->pc(s__7)) from 2 by applying 1: job$16'+job$3'+job$15'=job$16+job$3+job$15, 0=<job$16', 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'=stolen$1, 0=<job$15'
frontier 2: loop 7 (pc(s__7)->pc(s__1)) from 2 by applying 3: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', job$16'<job$16, 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15'
frontier 2: loop 8 (pc(s__7)->pc(s__1)) from 2 by applying 4: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15', job$15'<job$15
frontier 2: loop 9 (pc(s__3)->pc(s__7)) from 3 by applying 5: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=<stolen$5', 0=job$3', 0=<job$3', 0=stolen$1', 0=<stolen$1', stolen$1'=stolen$1, 0=<job$15'
frontier 2: loop 10 (pc(s__3)->pc(s__3)) from 3 by applying 11: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=stolen$5', 0=<stolen$5', stolen$5'=stolen$5, 0=<job$3', 0=stolen$1', 0=<stolen$1', stolen$1'=stolen$1, 0=<job$15'
frontier 2: loop 11 (pc(s__1)->pc(s__1)) from 4 by applying 14: job$16'+job$3'+job$15'=job$16+job$3+job$15, 0=<job$16', job$16'=job$16, 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', stolen$1'=stolen$1, 0=job$15', 0=<job$15', job$15'=job$15
frontier 2: loop 12 (pc(s__1)->pc(s__1)) from 4 by applying 15: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', job$16'<job$16, 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', stolen$1'=stolen$1, 0=job$15', 0=<job$15', job$15'=job$15
frontier 2: loop 13 (pc(s__1)->pc(s__1)) from 4 by applying 16: job$16'+job$3'+job$15'=job$16+job$3+job$15, 0=<job$16', job$16'=job$16, 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'<stolen$1, 0=job$15', 0=<job$15', job$15'=job$15
frontier 3: loop 14 (pc(s__7)->pc(s__7)) from 5 by applying 1: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'=stolen$1, 0=<job$15'
frontier 3: loop 15 (pc(s__7)->pc(s__1)) from 5 by applying 3: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15'
frontier 3: loop 16 (pc(s__7)->pc(s__1)) from 7 by applying 14: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', job$16'<job$16, 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15'
frontier 3: loop 17 (pc(s__7)->pc(s__1)) from 8 by applying 14: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15', job$15'<job$15
frontier 3: loop 18 (pc(s__3)->pc(s__1)) from 9 by applying 3: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=<stolen$5', 0=job$3', 0=<job$3', 0=<stolen$1', 0=job$15', 0=<job$15'
frontier 3: loop 19 (pc(s__1)->pc(s__1)) from 12 by applying 14: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', job$16'<job$16, 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', stolen$1'=stolen$1, 0=job$15', 0=<job$15', job$15'=job$15
frontier 3: loop 20 (pc(s__1)->pc(s__1)) from 12 by applying 16: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', job$16'<job$16, 0=<stolen$5', stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'<stolen$1, 0=job$15', 0=<job$15', job$15'=job$15
frontier 4: loop 21 (pc(s__7)->pc(s__1)) from 15 by applying 14: job$16'+job$3'+job$15'<job$16+job$3+job$15, 0=<job$16', 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, 0=job$3', 0=<job$3', job$3'=job$3, 0=<stolen$1', 0=job$15', 0=<job$15'
_5873->_5876: #22: job$16'+job$3'+job$15'<job$16+job$3+job$15, job$16'+job$3'+job$15'=job$16+job$3+job$15, 0=job$16', 0=<job$16', job$16'<job$16, job$16'=job$16, 0=stolen$5', 0=<stolen$5', stolen$5'<stolen$5, stolen$5'=stolen$5, 0=job$3', 0=<job$3', job$3'<job$3, job$3'=job$3, 0=stolen$1', 0=<stolen$1', stolen$1'<stolen$1, stolen$1'=stolen$1, 0=job$15', 0=<job$15', job$15'<job$15, job$15'=job$15
---------------------------------------------+----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.01 | 0.01 |
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