Computing Termination of core/src/test/resources/dbp_graph/termination/clientserver.dbp
Computing Termination of core/src/test/resources/dbp_graph/termination/clientserver.dbp
Input
// client/server with an input queue
init
(c1, client)* -> (j, job)** [job]
node (n, in)
node (o, out)
node (s, server)
// *****************************************************************************
transition "enq"
pre
(c, client) -> (j, job) [job]
node (n, in)
post
node (c, client)
(n, in) -> (j, job) [job]
==>
c -> c
n -> n
j -> j
<==
transition "accept"
pre
(n, in) -> (j, job) [job]
node (s, server)
post
node (n, in)
(s, server) -> (j, job)
==>
s -> s
n -> n
j -> j
<==
no
(s, server) -> (j, _) [job]
==>
s -> s
transition "process"
pre
(s, server) -> (j, job)
node (n, out)
post
node (s, server)
(n, out) -> (j, job) [job]
==>
s -> s
n -> n
j -> j
<==
// *****************************************************************************
Graph rewriting system
-
Initial Configuration
-
Transitions
-
enq
-
accept
-
process
Cover
-
cover element 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(Job_4, Client_1, Job_1, Job_3, Job_2)), [(Job_4, 'job$4'), (Client_1, 'client$1'), (Job_1, 'job$1'), (Job_3, 'job$3'), (Job_2, 'job$2')]).
preds( p(_, data(Job_4, Client_1, Job_1, Job_3, Job_2)), []).
trans_preds(
p(_, data(Job_4, Client_1, Job_1, Job_3, Job_2)),
p(_, data(Job_4_prime, Client_1_prime, Job_1_prime, Job_3_prime, Job_2_prime)),
[ 0 = Job_4_prime,
0 =< Job_4_prime,
Job_4_prime < Job_4,
Job_4_prime = Job_4,
0 = Client_1_prime,
0 =< Client_1_prime,
Client_1_prime < Client_1,
Client_1_prime = Client_1,
0 = Job_1_prime,
0 =< Job_1_prime,
Job_1_prime < Job_1,
Job_1_prime = Job_1,
0 = Job_3_prime,
0 =< Job_3_prime,
Job_3_prime < Job_3,
Job_3_prime = Job_3,
0 = Job_2_prime,
0 =< Job_2_prime,
Job_2_prime < Job_2,
Job_2_prime = Job_2
]).
start( pc(s__12)).
cutpoint(pc(s__1)).
% initialize
r( p(pc(s__12), data(Job_4, Client_1, Job_1, Job_3, Job_2)),
p(pc(s__1), data(Job_4_prime, Client_1_prime, Job_1_prime, Job_3_prime, Job_2_prime)),
[ 0 =< Job_3_prime, 0 =< Job_2_prime, 0 =< Client_1_prime, 0 =< Job_1_prime, 0 =< Job_4_prime ],
[], 0).
% unfolding; morphing, enq; folding; covering
r( p(pc(s__1), data(Job_4, Client_1, Job_1, Job_3, Job_2)),
p(pc(s__1), data(Job_4_prime, Client_1_prime, Job_1_prime, Job_3_prime, Job_2_prime)),
[ Job_1 - Job_1_prime = 1, Client_1 = Client_1_prime, Job_3 = Job_3_prime, Job_4 = Job_4_prime, Job_2 - Job_2_prime = -1, 0 =< Job_1_prime, 1 =< Client_1_prime, 0 =< Job_3_prime, 0 =< Job_4_prime, 1 =< Job_2_prime ],
[], 1).
% unfolding; morphing, process; folding; covering
r( p(pc(s__1), data(Job_4, Client_1, Job_1, Job_3, Job_2)),
p(pc(s__1), data(Job_4_prime, Client_1_prime, Job_1_prime, Job_3_prime, Job_2_prime)),
[ Client_1_prime = Client_1, Job_1 = Job_1_prime, Job_3 - Job_3_prime = 1, Job_4 - Job_4_prime = -1, Job_2_prime = Job_2, 0 =< Client_1, 0 =< Job_1_prime, 0 =< Job_3_prime, 0 =< Job_2, 1 =< Job_4_prime ],
[], 2).
% unfolding; inhibiting; morphing, accept; folding; covering
r( p(pc(s__1), data(Job_4, Client_1, Job_1, Job_3, Job_2)),
p(pc(s__1), data(Job_4_prime, Client_1_prime, Job_1_prime, Job_3_prime, Job_2_prime)),
[ Job_1 = Job_1_prime, Client_1 = Client_1_prime, Job_3 - Job_3_prime = -1, Job_4 = Job_4_prime, Job_2 - Job_2_prime = 1, 0 =< Client_1_prime, 1 =< Job_3_prime, 0 =< Job_4_prime, 0 =< Job_1_prime, 0 =< Job_2_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.OCj12PIiyh
]
reading input from /tmp/tmp.OCj12PIiyh
...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__12), pc(s__12), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__12), pc(s__1), [2,6,10,14,18], stem, 2, (1,0)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,8,10,11,14,16,18], loop, 3, (2,1)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,6,8,10,12,14,15,18,20], loop, 4, (2,2)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,8,10,12,14,18,19], loop, 5, (2,3)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,6,8,10,11,14,15,18], loop, 6, (3,2)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,4,6,8,10,11,14,18], loop, 7, (3,3)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,6,8,10,12,14,18,19], loop, 8, (4,3)).
abstract_trans_state(4, pc(s__1), pc(s__1), [2,6,8,10,11,14,18], loop, 9, (6,3)).
frontier 0: stem 1 (pc(s__12)->pc(s__12)) from 0 by applying 0: T
frontier 1: stem 2 (pc(s__12)->pc(s__1)) from 1 by applying 0: 0=<job$4', 0=<client$1', 0=<job$1', 0=<job$3', 0=<job$2'
frontier 2: loop 3 (pc(s__1)->pc(s__1)) from 2 by applying 1: 0=<job$4', job$4'=job$4, 0=<client$1', client$1'=client$1, 0=<job$1', job$1'<job$1, 0=<job$3', job$3'=job$3, 0=<job$2'
frontier 2: loop 4 (pc(s__1)->pc(s__1)) from 2 by applying 2: 0=<job$4', 0=<client$1', client$1'=client$1, 0=<job$1', job$1'=job$1, 0=<job$3', job$3'<job$3, 0=<job$2', job$2'=job$2
frontier 2: loop 5 (pc(s__1)->pc(s__1)) from 2 by applying 3: 0=<job$4', job$4'=job$4, 0=<client$1', client$1'=client$1, 0=<job$1', job$1'=job$1, 0=<job$3', 0=<job$2', job$2'<job$2
frontier 3: loop 6 (pc(s__1)->pc(s__1)) from 3 by applying 2: 0=<job$4', 0=<client$1', client$1'=client$1, 0=<job$1', job$1'<job$1, 0=<job$3', job$3'<job$3, 0=<job$2'
frontier 3: loop 7 (pc(s__1)->pc(s__1)) from 3 by applying 3: 0=<job$4', job$4'=job$4, 0=<client$1', client$1'=client$1, 0=<job$1', job$1'<job$1, 0=<job$3', 0=<job$2'
frontier 3: loop 8 (pc(s__1)->pc(s__1)) from 4 by applying 3: 0=<job$4', 0=<client$1', client$1'=client$1, 0=<job$1', job$1'=job$1, 0=<job$3', 0=<job$2', job$2'<job$2
frontier 4: loop 9 (pc(s__1)->pc(s__1)) from 6 by applying 3: 0=<job$4', 0=<client$1', client$1'=client$1, 0=<job$1', job$1'<job$1, 0=<job$3', 0=<job$2'
_5600->_5603: #20: 0=job$4', 0=<job$4', job$4'<job$4, job$4'=job$4, 0=client$1', 0=<client$1', client$1'<client$1, client$1'=client$1, 0=job$1', 0=<job$1', job$1'<job$1, job$1'=job$1, 0=job$3', 0=<job$3', job$3'<job$3, job$3'=job$3, 0=job$2', 0=<job$2', job$2'<job$2, job$2'=job$2
---------------------------------------------+----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.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