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

    Cover

    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