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

// 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
<==

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

• Initial Configuration

• Transitions

  • steal

  • consume

• cover element 0

% 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_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).

ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.jKXRGyS5om
]
reading input from /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