Computing Termination of core/src/test/resources/dbp_graph/termination/simple_non_blocking.dbp
Computing Termination of core/src/test/resources/dbp_graph/termination/simple_non_blocking.dbp
Input
/* Compact encoding of:
* S(x, head) = out(x)(head).S(x, head)
* + in(x)(h2, h, succ, fail).([head = h].out(succ)().S(x, h2) |
* [head != h].out(fail)().S(x, head))
*
* Op1(x) = in(x)(h).Op2(x,h)
* Op2(x,h) = (\nu h2,succ,fail) out(x)(h2, h, succ, fail).(in(succ)().0 | in(fail)().Op1(x))
*/
init
(s, S) -> (h, head) [head]
(o, Op1)* -> (s, S) [x]
transition "client: Op1 -> Op2"
pre
(s, S) -> (h, head) [head]
(o, Op1) -> (s, S) [x]
post
(s, S) -> (h, head) [head]
(o, Op2) -> (s, S) [x]
(o, Op2) -> (h, head) [h]
(o, Op2) -> (h2, head) [h2]
==>
s -> s
o -> o
h -> h
<==
transition "client: Op2 Success"
pre
(s, S) -> (h, head) [head]
(o, Op2) -> (s, S) [x]
(o, Op2) -> (h, head) [h]
(o, Op2) -> (h2, head) [h2]
post
(s, S) -> (h2, head) [head]
node (h, head)
==>
s -> s
h -> h
h2 -> h2
<==
transition "client: Op2 Fail"
pre
(s, S) -> (h, head) [head]
(o, Op2) -> (s, S) [x]
(o, Op2) -> (h3, head) [h]
(o, Op2) -> (h2, head) [h2]
post
(s, S) -> (h, head) [head]
(o, Op1) -> (s, S) [x]
node (h2, head)
node (h3, head)
==>
s -> s
o -> o
h -> h
h2 -> h2
h3 -> h3
<==
Graph rewriting system
-
Initial Configuration
-
Transitions
-
client: Op1 -> Op2
-
client: Op2 Success
-
client: Op2 Fail
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(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)), [(Head_2, 'head$2'), (Op2_2, 'Op2$2'), (Op2_1, 'Op2$1'), (Head_4, 'head$4'), (Op1_1, 'Op1$1'), (Head_1, 'head$1')]).
preds( p(_, data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)), []).
trans_preds(
p(_, data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)),
p(_, data(Head_2_prime, Op2_2_prime, Op2_1_prime, Head_4_prime, Op1_1_prime, Head_1_prime)),
[ Op2_2_prime + Op2_1_prime + Op1_1_prime < Op2_2 + Op2_1 + Op1_1,
Op2_2_prime + Op2_1_prime + Op1_1_prime = Op2_2 + Op2_1 + Op1_1,
0 = Head_2_prime,
0 =< Head_2_prime,
Head_2_prime < Head_2,
Head_2_prime = Head_2,
0 = Op2_2_prime,
0 =< Op2_2_prime,
Op2_2_prime < Op2_2,
Op2_2_prime = Op2_2,
0 = Op2_1_prime,
0 =< Op2_1_prime,
Op2_1_prime < Op2_1,
Op2_1_prime = Op2_1,
0 = Head_4_prime,
0 =< Head_4_prime,
Head_4_prime < Head_4,
Head_4_prime = Head_4,
0 = Op1_1_prime,
0 =< Op1_1_prime,
Op1_1_prime < Op1_1,
Op1_1_prime = Op1_1,
0 = Head_1_prime,
0 =< Head_1_prime,
Head_1_prime < Head_1,
Head_1_prime = Head_1
]).
start( pc(s__11)).
cutpoint(pc(s__1)).
% unfolding; morphing, client: Op2 Success; folding; covering
r( p(pc(s__1), data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)),
p(pc(s__1), data(Head_2_prime, Op2_2_prime, Op2_1_prime, Head_4_prime, Op1_1_prime, Head_1_prime)),
[ Head_4_prime - Head_4 = 1, (Op2_1 + Op2_2) - Op2_2_prime = 1, (Head_1 + Head_2) - Head_1_prime = 1, Op1_1_prime = Op1_1, Op2_1_prime = 0, Head_2_prime = 0, Op2_2 =< Op2_2_prime, 0 =< Op2_2, -1 =< Head_1_prime - Head_2, 1 =< Head_2, 0 =< Head_4, 0 =< Op1_1 ],
[], 0).
% unfolding; morphing, client: Op1 -> Op2; folding; covering
r( p(pc(s__1), data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)),
p(pc(s__1), data(Head_2_prime, Op2_2_prime, Op2_1_prime, Head_4_prime, Op1_1_prime, Head_1_prime)),
[ Op2_1_prime - Op2_1 = 1, Head_1 = Head_1_prime, Op2_2 = Op2_2_prime, Head_2 - Head_2_prime = -1, Head_4 = Head_4_prime, Op1_1_prime - Op1_1 = -1, 0 =< Op2_1, 0 =< Op2_2_prime, 0 =< Head_1_prime, 0 =< Head_4_prime, 1 =< Head_2_prime, 1 =< Op1_1 ],
[], 1).
% unfolding; morphing, client: Op2 Fail; folding; covering
r( p(pc(s__1), data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)),
p(pc(s__1), data(Head_2_prime, Op2_2_prime, Op2_1_prime, Head_4_prime, Op1_1_prime, Head_1_prime)),
[ Op2_2_prime - Op2_2 = -1, Op2_1 = Op2_1_prime, Head_1 = Head_1_prime, Head_4_prime = Head_4, Head_2 = Head_2_prime, Op1_1_prime - Op1_1 = 1, 1 =< Op2_2, 1 =< Head_4, 1 =< Head_1_prime, 0 =< Op2_1_prime, 0 =< Op1_1, 0 =< Head_2_prime ],
[], 2).
% initialize
r( p(pc(s__11), data(Head_2, Op2_2, Op2_1, Head_4, Op1_1, Head_1)),
p(pc(s__1), data(Head_2_prime, Op2_2_prime, Op2_1_prime, Head_4_prime, Op1_1_prime, Head_1_prime)),
[ 0 =< Op2_1_prime, 0 =< Op2_2_prime, 0 =< Op1_1_prime, 0 =< Head_1_prime, 0 =< Head_2_prime, 0 =< Head_4_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.znHIZqKNqa
]
reading input from /tmp/tmp.znHIZqKNqa
...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__11), pc(s__11), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__11), pc(s__1), [4,8,12,16,20,24], stem, 2, (1,3)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,3,4,5,8,11,12,13,16,20,22,24], loop, 3, (2,0)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,8,10,12,16,18,20,21,24,26], loop, 4, (2,1)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,8,9,12,14,16,18,20,24,26], loop, 5, (2,2)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,4,8,12,16,20,21,24], loop, 6, (3,1)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,3,4,5,8,11,12,13,16,20,24], loop, 7, (3,2)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,4,8,9,12,16,18,20,24,26], loop, 8, (4,2)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,4,8,12,16,20,24], loop, 9, (6,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=<head$2', 0=<Op2$2', 0=<Op2$1', 0=<head$4', 0=<Op1$1', 0=<head$1'
frontier 2: loop 3 (pc(s__1)->pc(s__1)) from 2 by applying 0: Op2$2'+Op2$1'+Op1$1'<Op2$2+Op2$1+Op1$1, 0=head$2', 0=<head$2', head$2'<head$2, 0=<Op2$2', 0=Op2$1', 0=<Op2$1', Op2$1'<Op2$1, 0=<head$4', 0=<Op1$1', Op1$1'=Op1$1, 0=<head$1'
frontier 2: loop 4 (pc(s__1)->pc(s__1)) from 2 by applying 1: Op2$2'+Op2$1'+Op1$1'=Op2$2+Op2$1+Op1$1, 0=<head$2', 0=<Op2$2', Op2$2'=Op2$2, 0=<Op2$1', 0=<head$4', head$4'=head$4, 0=<Op1$1', Op1$1'<Op1$1, 0=<head$1', head$1'=head$1
frontier 2: loop 5 (pc(s__1)->pc(s__1)) from 2 by applying 2: Op2$2'+Op2$1'+Op1$1'=Op2$2+Op2$1+Op1$1, 0=<head$2', head$2'=head$2, 0=<Op2$2', Op2$2'<Op2$2, 0=<Op2$1', Op2$1'=Op2$1, 0=<head$4', head$4'=head$4, 0=<Op1$1', 0=<head$1', head$1'=head$1
frontier 3: loop 6 (pc(s__1)->pc(s__1)) from 3 by applying 1: Op2$2'+Op2$1'+Op1$1'<Op2$2+Op2$1+Op1$1, 0=<head$2', 0=<Op2$2', 0=<Op2$1', 0=<head$4', 0=<Op1$1', Op1$1'<Op1$1, 0=<head$1'
frontier 3: loop 7 (pc(s__1)->pc(s__1)) from 3 by applying 2: Op2$2'+Op2$1'+Op1$1'<Op2$2+Op2$1+Op1$1, 0=head$2', 0=<head$2', head$2'<head$2, 0=<Op2$2', 0=Op2$1', 0=<Op2$1', Op2$1'<Op2$1, 0=<head$4', 0=<Op1$1', 0=<head$1'
frontier 3: loop 8 (pc(s__1)->pc(s__1)) from 4 by applying 2: Op2$2'+Op2$1'+Op1$1'=Op2$2+Op2$1+Op1$1, 0=<head$2', 0=<Op2$2', Op2$2'<Op2$2, 0=<Op2$1', 0=<head$4', head$4'=head$4, 0=<Op1$1', 0=<head$1', head$1'=head$1
frontier 4: loop 9 (pc(s__1)->pc(s__1)) from 6 by applying 2: Op2$2'+Op2$1'+Op1$1'<Op2$2+Op2$1+Op1$1, 0=<head$2', 0=<Op2$2', 0=<Op2$1', 0=<head$4', 0=<Op1$1', 0=<head$1'
_5683->_5686: #26: Op2$2'+Op2$1'+Op1$1'<Op2$2+Op2$1+Op1$1, Op2$2'+Op2$1'+Op1$1'=Op2$2+Op2$1+Op1$1, 0=head$2', 0=<head$2', head$2'<head$2, head$2'=head$2, 0=Op2$2', 0=<Op2$2', Op2$2'<Op2$2, Op2$2'=Op2$2, 0=Op2$1', 0=<Op2$1', Op2$1'<Op2$1, Op2$1'=Op2$1, 0=head$4', 0=<head$4', head$4'<head$4, head$4'=head$4, 0=Op1$1', 0=<Op1$1', Op1$1'<Op1$1, Op1$1'=Op1$1, 0=head$1', 0=<head$1', head$1'<head$1, head$1'=head$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.01 | 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