Computing Termination of core/src/test/resources/dbp_graph/termination/split_merge.dbp
Computing Termination of core/src/test/resources/dbp_graph/termination/split_merge.dbp
Input
init
node (m, master1)
(w, worker)* -> (m, master1) [M]
(m, master1) -> (w, worker)* [idle]
transition "send job"
pre
(m, master1) -> (w, worker) [idle]
post
(m, master1) -> (w, worker_working) [working]
==>
m -> m
w -> w
<==
transition "worker done"
pre
node (w, worker_working)
post
node (w, worker_done)
==>
w -> w
<==
transition "send mode to gather mode"
pre
node (m, master1)
post
node (m, master2)
==>
m -> m
<==
no
(m, master1) -> (w, _) [idle]
==>
m -> m
transition "gather result"
pre
(m, master2) -> (w, worker_done) [working]
post
node (m, master2)
==>
m -> m
<==
transition "done"
pre
node (m, master2)
post
node (m, master3)
==>
m -> m
<==
no
(m, master2) -> (w, _) [working]
==>
m -> m
Graph rewriting system
Initial Configuration
init
0
(worker,1)
1
(master1,0)
0->1
M
1->0
idle
Transitions
send job
trs
cluster_trslhs
LHS
cluster_trsrhs
RHS
trslhs0
(worker,0)
trsrhs0
(worker_working,0)
trslhs0->trsrhs0
trslhs1
(master1,0)
trslhs1->trslhs0
idle
trsrhs1
(master1,0)
trslhs1->trsrhs1
trsrhs1->trsrhs0
working
worker done
trs
cluster_trslhs
LHS
cluster_trsrhs
RHS
trslhs0
(worker_working,0)
trsrhs0
(worker_done,0)
trslhs0->trsrhs0
send mode to gather mode
trs
cluster_trsguard
GUARD
cluster_trslhs
LHS
cluster_trsrhs
RHS
trsguard0
(_,0)
trsguard1
(master1,0)
trsguard1->trsguard0
idle
trslhs0
(master1,0)
trslhs0->trsguard1
trsrhs0
(master2,0)
trslhs0->trsrhs0
gather result
trs
cluster_trslhs
LHS
cluster_trsrhs
RHS
trslhs0
(worker_done,0)
trslhs1
(master2,0)
trslhs1->trslhs0
working
trsrhs0
(master2,0)
trslhs1->trsrhs0
done
trs
cluster_trsguard
GUARD
cluster_trslhs
LHS
cluster_trsrhs
RHS
trsguard0
(_,0)
trsguard1
(master2,0)
trsguard1->trsguard0
working
trslhs0
(master2,0)
trslhs0->trsguard1
trsrhs0
(master3,0)
trslhs0->trsrhs0
Cover
cover element 0
cover
0
(worker_working,1)
1
(master2,0)
0->1
M
1->0
working
2
(worker_done,1)
1->2
working
2->1
M
cover element 1
cover
0
(worker,1)
1
(master1,0)
0->1
M
1->0
idle
2
(worker_working,1)
1->2
working
3
(worker_done,1)
1->3
working
2->1
M
3->1
M
cover element 2
cover
0
(master3,0)
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(Worker_1, Worker_working_1, Worker_done_1)), [(Worker_1, 'worker$1'), (Worker_working_1, 'worker_working$1'), (Worker_done_1, 'worker_done$1')]).
preds( p(_, data(Worker_1, Worker_working_1, Worker_done_1)), []).
trans_preds(
p(_, data(Worker_1, Worker_working_1, Worker_done_1)),
p(_, data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ 0 = Worker_1_prime,
0 =< Worker_1_prime,
Worker_1_prime < Worker_1,
Worker_1_prime = Worker_1,
0 = Worker_working_1_prime,
0 =< Worker_working_1_prime,
Worker_working_1_prime < Worker_working_1,
Worker_working_1_prime = Worker_working_1,
0 = Worker_done_1_prime,
0 =< Worker_done_1_prime,
Worker_done_1_prime < Worker_done_1,
Worker_done_1_prime = Worker_done_1
]).
start( pc(s__19)).
cutpoint(pc(s__3)).
cutpoint(pc(s__1)).
% unfolding; morphing, send job; folding; covering
r( p(pc(s__3), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__3), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ Worker_working_1 - Worker_working_1_prime = -1, Worker_1 - Worker_1_prime = 1, Worker_done_1 = Worker_done_1_prime, 1 =< Worker_working_1_prime, 0 =< Worker_1_prime, 0 =< Worker_done_1_prime ],
[], 0).
% unfolding; morphing, worker done; folding; covering
r( p(pc(s__3), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__3), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ Worker_working_1 - Worker_working_1_prime = 1, Worker_1 = Worker_1_prime, Worker_done_1 - Worker_done_1_prime = -1, 0 =< Worker_working_1_prime, 1 =< Worker_done_1_prime, 0 =< Worker_1_prime ],
[], 1).
% inhibiting; morphing, send mode to gather mode; covering
r( p(pc(s__3), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__1), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ Worker_done_1 = Worker_done_1_prime, Worker_working_1 = Worker_working_1_prime, Worker_1_prime = 0 ],
[], 2).
% initialize
r( p(pc(s__19), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__7), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ 0 = 0, Worker_1_prime = 0, Worker_working_1_prime = 0, Worker_done_1_prime = 0 ],
[], 3).
% initialize
r( p(pc(s__19), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__3), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ 0 =< Worker_1_prime, 0 =< Worker_working_1_prime, 0 =< Worker_done_1_prime ],
[], 4).
% initialize
r( p(pc(s__19), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__1), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ 0 =< Worker_working_1_prime, 0 =< Worker_done_1_prime, Worker_1_prime = 0 ],
[], 5).
% inhibiting; morphing, done; covering
r( p(pc(s__1), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__7), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ 0 = 0, Worker_1_prime = 0, Worker_working_1_prime = 0, Worker_done_1_prime = 0 ],
[], 6).
% unfolding; morphing, worker done; folding; covering
r( p(pc(s__1), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__1), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ Worker_done_1 - Worker_done_1_prime = -1, Worker_working_1 - Worker_working_1_prime = 1, 1 =< Worker_done_1_prime, 0 =< Worker_working_1_prime, Worker_1_prime = 0 ],
[], 7).
% unfolding; morphing, gather result; covering
r( p(pc(s__1), data(Worker_1, Worker_working_1, Worker_done_1)),
p(pc(s__1), data(Worker_1_prime, Worker_working_1_prime, Worker_done_1_prime)),
[ Worker_working_1 = Worker_working_1_prime, Worker_done_1 - Worker_done_1_prime = 1, 0 =< Worker_working_1_prime, 0 =< Worker_done_1_prime, Worker_1_prime = 0 ],
[], 8).
ARMC output
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.41wTcK4AvU
]
reading input from /tmp/tmp.41wTcK4AvU
...done.
--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4 5
==================================================
ARMC-LIVE: program is correct
abstract trans fixpoint
abstract_trans_state(0, pc(s__19), pc(s__19), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__19), pc(s__7), [1,2,5,6,9,10], stem, 2, (1,3)).
abstract_trans_state(1, pc(s__19), pc(s__3), [2,6,10], stem, 3, (1,4)).
abstract_trans_state(1, pc(s__19), pc(s__1), [1,2,6,10], stem, 4, (1,5)).
abstract_trans_state(2, pc(s__3), pc(s__3), [2,3,6,10,12], loop, 5, (3,0)).
abstract_trans_state(2, pc(s__3), pc(s__3), [2,4,6,7,10], loop, 6, (3,1)).
abstract_trans_state(2, pc(s__3), pc(s__1), [1,2,6,8,10,12], loop, 7, (3,2)).
abstract_trans_state(2, pc(s__1), pc(s__7), [1,2,4,5,6,9,10], loop, 8, (4,6)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,7,10], loop, 9, (4,7)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,8,10,11], loop, 10, (4,8)).
abstract_trans_state(3, pc(s__3), pc(s__3), [2,3,6,10], loop, 11, (5,1)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,3,6,10,12], loop, 12, (5,2)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,6,7,10], loop, 13, (6,2)).
abstract_trans_state(3, pc(s__3), pc(s__7), [1,2,5,6,9,10], loop, 14, (7,6)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,6,8,10,11], loop, 15, (7,8)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,3,6,10], loop, 16, (11,2)).
frontier 0: stem 1 (pc(s__19)->pc(s__19)) from 0 by applying 0: T
frontier 1: stem 2 (pc(s__19)->pc(s__7)) from 1 by applying 3: 0=worker$1', 0=<worker$1', 0=worker_working$1', 0=<worker_working$1', 0=worker_done$1', 0=<worker_done$1'
frontier 1: stem 3 (pc(s__19)->pc(s__3)) from 1 by applying 4: 0=<worker$1', 0=<worker_working$1', 0=<worker_done$1'
frontier 1: stem 4 (pc(s__19)->pc(s__1)) from 1 by applying 5: 0=worker$1', 0=<worker$1', 0=<worker_working$1', 0=<worker_done$1'
frontier 2: loop 5 (pc(s__3)->pc(s__3)) from 3 by applying 0: 0=<worker$1', worker$1'<worker$1, 0=<worker_working$1', 0=<worker_done$1', worker_done$1'=worker_done$1
frontier 2: loop 6 (pc(s__3)->pc(s__3)) from 3 by applying 1: 0=<worker$1', worker$1'=worker$1, 0=<worker_working$1', worker_working$1'<worker_working$1, 0=<worker_done$1'
frontier 2: loop 7 (pc(s__3)->pc(s__1)) from 3 by applying 2: 0=worker$1', 0=<worker$1', 0=<worker_working$1', worker_working$1'=worker_working$1, 0=<worker_done$1', worker_done$1'=worker_done$1
frontier 2: loop 8 (pc(s__1)->pc(s__7)) from 4 by applying 6: 0=worker$1', 0=<worker$1', worker$1'=worker$1, 0=worker_working$1', 0=<worker_working$1', 0=worker_done$1', 0=<worker_done$1'
frontier 2: loop 9 (pc(s__1)->pc(s__1)) from 4 by applying 7: 0=worker$1', 0=<worker$1', worker$1'=worker$1, 0=<worker_working$1', worker_working$1'<worker_working$1, 0=<worker_done$1'
frontier 2: loop 10 (pc(s__1)->pc(s__1)) from 4 by applying 8: 0=worker$1', 0=<worker$1', worker$1'=worker$1, 0=<worker_working$1', worker_working$1'=worker_working$1, 0=<worker_done$1', worker_done$1'<worker_done$1
frontier 3: loop 11 (pc(s__3)->pc(s__3)) from 5 by applying 1: 0=<worker$1', worker$1'<worker$1, 0=<worker_working$1', 0=<worker_done$1'
frontier 3: loop 12 (pc(s__3)->pc(s__1)) from 5 by applying 2: 0=worker$1', 0=<worker$1', worker$1'<worker$1, 0=<worker_working$1', 0=<worker_done$1', worker_done$1'=worker_done$1
frontier 3: loop 13 (pc(s__3)->pc(s__1)) from 6 by applying 2: 0=worker$1', 0=<worker$1', 0=<worker_working$1', worker_working$1'<worker_working$1, 0=<worker_done$1'
frontier 3: loop 14 (pc(s__3)->pc(s__7)) from 7 by applying 6: 0=worker$1', 0=<worker$1', 0=worker_working$1', 0=<worker_working$1', 0=worker_done$1', 0=<worker_done$1'
frontier 3: loop 15 (pc(s__3)->pc(s__1)) from 7 by applying 8: 0=worker$1', 0=<worker$1', 0=<worker_working$1', worker_working$1'=worker_working$1, 0=<worker_done$1', worker_done$1'<worker_done$1
frontier 4: loop 16 (pc(s__3)->pc(s__1)) from 11 by applying 2: 0=worker$1', 0=<worker$1', worker$1'<worker$1, 0=<worker_working$1', 0=<worker_done$1'
_5637->_5640: #12: 0=worker$1', 0=<worker$1', worker$1'<worker$1, worker$1'=worker$1, 0=worker_working$1', 0=<worker_working$1', worker_working$1'<worker_working$1, worker_working$1'=worker_working$1, 0=worker_done$1', 0=<worker_done$1', worker_done$1'<worker_done$1, worker_done$1'=worker_done$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