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

0 Input
1 Graph rewriting system
- 1.0 Initial Configuration
- 1.1 Transitions
2 Cover
3 Numerical Abstraction
4 ARMC output

Input

//example from "Actors in Scala" chapter 9

//  def mapReduce[K, V, K2, V2](
//    input: List[(K, V)],
//    mapping: (K, V) => List[(K2, V2)],
//    reducing: (K2, List[V2]) => List[V2]
//  ): Map[K2, List[V2]] = {
//    case class Intermediate(list: List[(K2, V2)])
//    case class Reduced(key: K2, values: List[V2])
//    val master = self
//    val workers = for ((key, value) <- input) yield
//      actor {
//        master ! Intermediate(mapping(key, value))
//      }
//    var intermediates = List[(K2, V2)]()
//    for (_ <- 1 to input.length)
//      receive {
//        case Intermediate(list) => intermediates :::= list
//      }
//    var dict = Map[K2, List[V2]]() withDefault (k => List())
//    for ((key, value) <- intermediates)
//      dict += (key -> (value :: dict(key)))
//    val reducers = for ((key, values) <- dict) yield
//      actor {
//        master ! Reduced(key, reducing(key, values))
//      }
//    var result = Map[K2, List[V2]]()
//    for (_ <- 1 to dict.size)
//      receive {
//        case Reduced(key, values) =>
//          result += (key -> values)
//      }
//    result
//  }

init
    (m, master) -> (i, input)*

transition "master: make mappers"
pre
    (m, master) -> (i, input)
post
    (m, master) -> (w, mapper)
    (w, mapper) -> (i, input)
==>
    m -> m
    i -> i
<==

transition "master: mappers created"
pre
    node (m, master)
post
    node (m, master1)
==>
    m -> m
<==
no
    (m, master) -> (i, input)
==>
    m -> m

transition "master: mapping done"
pre
    node (m, master1)
post
    node (m, master2)
==>
    m -> m
<==
no
    (m, master1) -> (w, mapper)
    (w, mapper) -> (i, input)
==>
    m -> m

transition "master: reducer"
pre
    (m, master2) -> (k1, key) [inter]
post
    (m, master2) -> (w, reducer)
    (w, reducer) -> (k1, key)
==>
    m -> m
    k1 -> k1
<==

transition "master: reducers created"
pre
    node (m, master2)
post
    node (m, master3)
==>
    m -> m
<==
no
    (m, master2) -> (k, key) [inter]
==>
    m -> m

transition "master: done"
pre
    node (m, master3)
post
    node (m, master4)
==>
    m -> m
<==
no
    (m, master3) -> (w, reducer)
    (w, reducer) -> (k1, key)
==>
    m -> m

transition "mapper"
pre
    (m, _) -> (w, mapper)
    (w, mapper) -> (i, input)
post
    (m, _) -> (k, key)* [inter]
    (k, key)* -> (v, value)**
==>
<==
    m -> m

transition "reducer"
pre
    (m, _) -> (w, reducer)
    (w, reducer) -> (k1, key)
post
    (m, _) -> (k2, key) [result]
    (k2, key) -> (v1, value)
==>
<==
    m -> m
no
    (k1, key) -> (v2, value)
==>
    k1 -> k1

Graph rewriting system

Initial Configuration
Transitions

Cover

cover element 0
cover element 1
cover element 2
cover element 3
cover element 4

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(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)), [(Input_2, 'input$2'), (Reducer_1, 'reducer$1'), (Value_28, 'value$28'), (Input_20, 'input$20'), (Value_13, 'value$13'), (Key_1, 'key$1'), (Value_1, 'value$1'), (Mapper_1, 'mapper$1'), (Key_4, 'key$4'), (Key_11, 'key$11')]).

preds( p(_, data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)), []).

trans_preds(
  p(_, data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),  
  p(_, data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),  
  [ 0 = Input_2_prime,
    0 =< Input_2_prime,
    Input_2_prime < Input_2,
    Input_2_prime = Input_2,
    0 = Reducer_1_prime,
    0 =< Reducer_1_prime,
    Reducer_1_prime < Reducer_1,
    Reducer_1_prime = Reducer_1,
    0 = Value_28_prime,
    0 =< Value_28_prime,
    Value_28_prime < Value_28,
    Value_28_prime = Value_28,
    0 = Input_20_prime,
    0 =< Input_20_prime,
    Input_20_prime < Input_20,
    Input_20_prime = Input_20,
    0 = Value_13_prime,
    0 =< Value_13_prime,
    Value_13_prime < Value_13,
    Value_13_prime = Value_13,
    0 = Key_1_prime,
    0 =< Key_1_prime,
    Key_1_prime < Key_1,
    Key_1_prime = Key_1,
    0 = Value_1_prime,
    0 =< Value_1_prime,
    Value_1_prime < Value_1,
    Value_1_prime = Value_1,
    0 = Mapper_1_prime,
    0 =< Mapper_1_prime,
    Mapper_1_prime < Mapper_1,
    Mapper_1_prime = Mapper_1,
    0 = Key_4_prime,
    0 =< Key_4_prime,
    Key_4_prime < Key_4,
    Key_4_prime = Key_4,
    0 = Key_11_prime,
    0 =< Key_11_prime,
    Key_11_prime < Key_11,
    Key_11_prime = Key_11
  ]).

start( pc(s__36)).
cutpoint(pc(s__3)).
cutpoint(pc(s__23)).
cutpoint(pc(s__1)).
cutpoint(pc(s__17)).

% unfolding; morphing, mapper; folding; covering
r(  p(pc(s__3), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__3), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Mapper_1 - Mapper_1_prime = 1, Input_2 = Input_2_prime, Input_20 - Input_20_prime = 1, Value_1 =< Value_1_prime, 0 =< Value_1, Key_4 =< Key_4_prime, 0 =< Input_20_prime, 0 =< Key_4, 0 =< Input_2_prime, 0 =< Mapper_1_prime, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 0).
% unfolding; morphing, master: make mappers; folding; covering
r(  p(pc(s__3), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__3), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Mapper_1 - Mapper_1_prime = -1, Value_1 = Value_1_prime, Input_2 - Input_2_prime = 1, Input_20_prime - Input_20 = 1, Key_4_prime = Key_4, 0 =< Input_20, 0 =< Value_1_prime, 0 =< Input_2_prime, 0 =< Key_4, 1 =< Mapper_1_prime, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 1).
% inhibiting; morphing, master: mappers created; covering
r(  p(pc(s__3), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__23), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_4 = Key_4_prime, Value_1 = Value_1_prime, Input_20 = Input_20_prime, Mapper_1 = Mapper_1_prime, Input_2_prime = 0, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 2).
% unfolding; morphing, mapper; folding; covering
r(  p(pc(s__23), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__23), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Input_20 - Input_20_prime = 1, Mapper_1 - Mapper_1_prime = 1, Key_4 =< Key_4_prime, 0 =< Key_4, Value_1 =< Value_1_prime, 0 =< Value_1, 0 =< Mapper_1_prime, 0 =< Input_20_prime, Input_2_prime = 0, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 3).
% inhibiting; morphing, master: mapping done; covering
r(  p(pc(s__23), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__17), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_4 = Key_4_prime, Value_28_prime = Value_1, Reducer_1_prime = 0, Key_11_prime = 0, Value_1_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Input_2_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0 ],
    [], 4).
% unfolding; inhibiting; morphing, reducer; folding; covering
r(  p(pc(s__1), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__1), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_1 - Key_1_prime = 1, Reducer_1 - Reducer_1_prime = 1, Key_11 - Key_11_prime = -1, Value_13 - Value_13_prime = -1, Value_1_prime =< Value_1, 0 =< Value_1_prime, 0 =< Reducer_1_prime, 1 =< Value_13_prime, 1 =< Key_11_prime, 0 =< Key_1_prime, Input_2_prime = 0, Value_28_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
    [], 5).
% inhibiting; morphing, master: done; folding; covering
r(  p(pc(s__1), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__9), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ (Value_1 + Value_13) - Value_13_prime = 0, Key_11 = Key_11_prime, Input_2_prime = 0, Reducer_1_prime = 0, Value_28_prime = 0, Input_20_prime = 0, Key_1_prime = 0, Value_1_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
    [], 6).
% initialize
r(  p(pc(s__36), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__3), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ 0 =< Mapper_1_prime, 0 =< Key_4_prime, 0 =< Value_1_prime, 0 =< Input_20_prime, 0 =< Input_2_prime, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 7).
% initialize
r(  p(pc(s__36), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__23), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ 0 =< Key_4_prime, 0 =< Mapper_1_prime, 0 =< Value_1_prime, 0 =< Input_20_prime, Input_2_prime = 0, Reducer_1_prime = 0, Value_28_prime = 0, Value_13_prime = 0, Key_1_prime = 0, Key_11_prime = 0 ],
    [], 8).
% initialize
r(  p(pc(s__36), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__1), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ 0 =< Key_11_prime, 0 =< Key_1_prime, 0 =< Reducer_1_prime, 0 =< Value_1_prime, 0 =< Value_13_prime, Input_2_prime = 0, Value_28_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
    [], 9).
% initialize
r(  p(pc(s__36), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__9), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ 0 =< Value_13_prime, 0 =< Key_11_prime, Input_2_prime = 0, Reducer_1_prime = 0, Value_28_prime = 0, Input_20_prime = 0, Key_1_prime = 0, Value_1_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
    [], 10).
% initialize
r(  p(pc(s__36), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__17), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ 0 =< Value_28_prime, 0 =< Reducer_1_prime, 0 =< Value_1_prime, 0 =< Value_13_prime, 0 =< Key_11_prime, 0 =< Key_1_prime, 0 =< Key_4_prime, Input_2_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0 ],
    [], 11).
% inhibiting; morphing, master: reducers created; folding; covering
r(  p(pc(s__17), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__1), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_1 = Key_1_prime, Key_11 = Key_11_prime, Reducer_1 = Reducer_1_prime, (Value_1 + Value_28) - Value_1_prime = 0, Value_13 = Value_13_prime, Input_2_prime = 0, Value_28_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
    [], 12).
% unfolding; morphing, master: reducer; folding; covering
r(  p(pc(s__17), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__17), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_1 - Key_1_prime = -1, Key_11 = Key_11_prime, Key_4 - Key_4_prime = 1, (Value_1_prime + Value_28_prime) - Value_28 - Value_1 = 0, Value_13_prime = Value_13, Reducer_1_prime - Reducer_1 = 1, 0 =< Value_1, 1 =< Key_1_prime, 0 =< Key_4_prime, 0 =< Value_13, 0 =< Reducer_1, Value_28_prime =< Value_28, 0 =< Key_11_prime, 0 =< Value_28_prime, Input_2_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0 ],
    [], 13).
% unfolding; inhibiting; morphing, reducer; folding; covering
r(  p(pc(s__17), data(Input_2, Reducer_1, Value_28, Input_20, Value_13, Key_1, Value_1, Mapper_1, Key_4, Key_11)),
    p(pc(s__17), data(Input_2_prime, Reducer_1_prime, Value_28_prime, Input_20_prime, Value_13_prime, Key_1_prime, Value_1_prime, Mapper_1_prime, Key_4_prime, Key_11_prime)),
    [ Key_1 - Key_1_prime = 1, Key_11 - Key_11_prime = -1, Key_4 = Key_4_prime, Value_13 - Value_13_prime = -1, Reducer_1 - Reducer_1_prime = 1, Value_28_prime = Value_28, 1 =< Key_11_prime, Value_1_prime =< Value_1, 0 =< Value_1_prime, 1 =< Value_13_prime, 0 =< Value_28, 0 =< Reducer_1_prime, 0 =< Key_4_prime, 0 =< Key_1_prime, Input_2_prime = 0, Input_20_prime = 0, Mapper_1_prime = 0 ],
    [], 14).

ARMC output

ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.osGpZhpPeC
]
reading input from /tmp/tmp.osGpZhpPeC
...done.



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4 5 6 7 8 9 


==================================================
ARMC-LIVE: program is correct

abstract trans fixpoint
abstract_trans_state(0, pc(s__36), pc(s__36), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__36), pc(s__3), [2,5,6,9,10,14,17,18,21,22,26,30,34,37,38], stem, 2, (1,7)).
abstract_trans_state(1, pc(s__36), pc(s__23), [1,2,5,6,9,10,14,17,18,21,22,26,30,34,37,38], stem, 3, (1,8)).
abstract_trans_state(1, pc(s__36), pc(s__1), [1,2,6,9,10,13,14,18,22,26,29,30,33,34,38], stem, 4, (1,9)).
abstract_trans_state(1, pc(s__36), pc(s__9), [1,2,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,38], stem, 5, (1,10)).
abstract_trans_state(1, pc(s__36), pc(s__17), [1,2,6,10,13,14,18,22,26,29,30,34,38], stem, 6, (1,11)).
abstract_trans_state(2, pc(s__3), pc(s__3), [2,4,5,6,8,9,10,12,14,15,17,18,20,21,22,24,26,30,31,34,37,38,40], loop, 7, (2,0)).
abstract_trans_state(2, pc(s__3), pc(s__3), [2,3,5,6,8,9,10,12,14,17,18,20,21,22,24,26,28,30,34,36,37,38,40], loop, 8, (2,1)).
abstract_trans_state(2, pc(s__3), pc(s__23), [1,2,5,6,8,9,10,12,14,16,17,18,20,21,22,24,26,28,30,32,34,36,37,38,40], loop, 9, (2,2)).
abstract_trans_state(2, pc(s__23), pc(s__23), [1,2,4,5,6,8,9,10,12,14,15,17,18,20,21,22,24,26,30,31,34,37,38,40], loop, 10, (3,3)).
abstract_trans_state(2, pc(s__23), pc(s__17), [1,2,4,5,6,8,10,13,14,17,18,20,21,22,24,25,26,29,30,34,36,37,38,40], loop, 11, (3,4)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,7,9,10,12,13,14,16,18,22,23,26,29,30,32,33,34,36,38], loop, 12, (4,5)).
abstract_trans_state(2, pc(s__1), pc(s__9), [1,2,4,5,6,9,10,12,13,14,16,18,21,22,25,26,29,30,32,33,34,36,38,40], loop, 13, (4,6)).
abstract_trans_state(2, pc(s__17), pc(s__1), [1,2,4,6,8,9,10,13,14,16,18,20,22,24,26,29,30,32,33,34,38,40], loop, 14, (6,12)).
abstract_trans_state(2, pc(s__17), pc(s__17), [1,2,4,6,10,13,14,16,18,20,22,26,29,30,32,34,35,38,40], loop, 15, (6,13)).
abstract_trans_state(2, pc(s__17), pc(s__17), [1,2,4,6,7,10,12,13,14,16,18,22,23,26,29,30,32,34,36,38], loop, 16, (6,14)).
abstract_trans_state(3, pc(s__3), pc(s__3), [2,3,5,6,8,9,10,12,14,17,18,20,21,22,24,26,30,34,37,38,40], loop, 17, (7,1)).
abstract_trans_state(3, pc(s__3), pc(s__23), [1,2,5,6,8,9,10,12,14,15,17,18,20,21,22,24,26,30,31,34,37,38,40], loop, 18, (7,2)).
abstract_trans_state(3, pc(s__3), pc(s__23), [1,2,3,5,6,8,9,10,12,14,17,18,20,21,22,24,26,28,30,34,36,37,38,40], loop, 19, (8,2)).
abstract_trans_state(3, pc(s__3), pc(s__17), [1,2,5,6,8,10,13,14,17,18,20,21,22,24,25,26,29,30,34,36,37,38,40], loop, 20, (9,4)).
abstract_trans_state(3, pc(s__23), pc(s__17), [1,2,4,5,6,8,10,13,14,15,17,18,20,21,22,24,25,26,29,30,31,34,37,38,40], loop, 21, (10,4)).
abstract_trans_state(3, pc(s__23), pc(s__1), [1,2,4,5,6,8,9,10,13,14,17,18,20,21,22,24,26,29,30,33,34,37,38,40], loop, 22, (11,12)).
abstract_trans_state(3, pc(s__23), pc(s__17), [1,2,4,6,10,13,14,17,18,20,22,26,29,30,34,35,37,38,40], loop, 23, (11,13)).
abstract_trans_state(3, pc(s__1), pc(s__9), [1,2,4,5,6,7,9,10,12,13,14,16,18,21,22,23,25,26,29,30,32,33,34,36,38], loop, 24, (12,6)).
abstract_trans_state(3, pc(s__17), pc(s__1), [1,2,4,6,7,9,10,13,14,16,18,22,23,26,29,30,32,33,34,38], loop, 25, (14,5)).
abstract_trans_state(3, pc(s__17), pc(s__9), [1,2,4,5,6,9,10,13,14,16,18,21,22,25,26,29,30,32,33,34,38,40], loop, 26, (14,6)).
abstract_trans_state(3, pc(s__17), pc(s__1), [1,2,4,6,9,10,13,14,16,18,20,22,26,29,30,32,33,34,35,38,40], loop, 27, (15,12)).
abstract_trans_state(3, pc(s__17), pc(s__17), [1,2,4,6,10,13,14,16,18,22,26,29,30,32,34,35,38], loop, 28, (15,14)).
abstract_trans_state(4, pc(s__3), pc(s__23), [1,2,3,5,6,8,9,10,12,14,17,18,20,21,22,24,26,30,34,37,38,40], loop, 29, (17,2)).
abstract_trans_state(4, pc(s__3), pc(s__17), [1,2,5,6,8,10,13,14,15,17,18,20,21,22,24,25,26,29,30,31,34,37,38,40], loop, 30, (18,4)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,5,6,8,9,10,13,14,17,18,20,21,22,24,26,29,30,33,34,37,38,40], loop, 31, (20,12)).
abstract_trans_state(4, pc(s__3), pc(s__17), [1,2,6,10,13,14,17,18,20,22,26,29,30,34,35,37,38,40], loop, 32, (20,13)).
abstract_trans_state(4, pc(s__23), pc(s__17), [1,2,4,6,10,13,14,15,17,18,20,22,26,29,30,31,34,37,38,40], loop, 33, (21,13)).
abstract_trans_state(4, pc(s__23), pc(s__9), [1,2,4,5,6,8,9,10,13,14,18,21,22,24,25,26,29,30,33,34,37,38,40], loop, 34, (22,6)).
abstract_trans_state(4, pc(s__23), pc(s__1), [1,2,4,6,9,10,13,14,17,18,20,22,26,29,30,33,34,35,37,38,40], loop, 35, (23,12)).
abstract_trans_state(4, pc(s__23), pc(s__17), [1,2,4,6,10,13,14,18,22,26,29,30,34,35,38], loop, 36, (23,14)).
abstract_trans_state(4, pc(s__17), pc(s__9), [1,2,4,5,6,7,9,10,13,14,16,18,21,22,23,25,26,29,30,32,33,34,38], loop, 37, (25,6)).
abstract_trans_state(4, pc(s__17), pc(s__1), [1,2,4,6,9,10,13,14,16,18,22,26,29,30,32,33,34,35,38], loop, 38, (27,5)).
abstract_trans_state(5, pc(s__3), pc(s__17), [1,2,3,5,6,8,10,13,14,17,18,20,21,22,24,25,26,29,30,34,37,38,40], loop, 39, (29,4)).
abstract_trans_state(5, pc(s__3), pc(s__17), [1,2,6,10,13,14,15,17,18,20,22,26,29,30,31,34,37,38,40], loop, 40, (30,13)).
abstract_trans_state(5, pc(s__3), pc(s__9), [1,2,5,6,8,9,10,13,14,18,21,22,24,25,26,29,30,33,34,37,38,40], loop, 41, (31,6)).
abstract_trans_state(5, pc(s__3), pc(s__1), [1,2,6,9,10,13,14,17,18,20,22,26,29,30,33,34,35,37,38,40], loop, 42, (32,12)).
abstract_trans_state(5, pc(s__3), pc(s__17), [1,2,6,10,13,14,18,22,26,29,30,34,35,38], loop, 43, (32,14)).
abstract_trans_state(5, pc(s__23), pc(s__1), [1,2,4,6,9,10,13,14,15,17,18,20,22,26,29,30,31,33,34,37,38,40], loop, 44, (33,12)).
abstract_trans_state(5, pc(s__23), pc(s__17), [1,2,4,6,10,13,14,15,18,22,26,29,30,31,34,38], loop, 45, (33,14)).
abstract_trans_state(5, pc(s__23), pc(s__1), [1,2,4,6,9,10,13,14,18,22,26,29,30,33,34,35,38], loop, 46, (35,5)).
abstract_trans_state(5, pc(s__23), pc(s__9), [1,2,4,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,35,37,38,40], loop, 47, (35,6)).
abstract_trans_state(5, pc(s__17), pc(s__9), [1,2,4,5,6,9,10,13,14,16,18,21,22,25,26,29,30,32,33,34,35,38], loop, 48, (38,6)).
abstract_trans_state(6, pc(s__3), pc(s__17), [1,2,3,6,10,13,14,17,18,20,22,26,29,30,34,37,38,40], loop, 49, (39,13)).
abstract_trans_state(6, pc(s__3), pc(s__1), [1,2,6,9,10,13,14,15,17,18,20,22,26,29,30,31,33,34,37,38,40], loop, 50, (40,12)).
abstract_trans_state(6, pc(s__3), pc(s__17), [1,2,6,10,13,14,15,18,22,26,29,30,31,34,38], loop, 51, (40,14)).
abstract_trans_state(6, pc(s__3), pc(s__1), [1,2,6,9,10,13,14,18,22,26,29,30,33,34,35,38], loop, 52, (42,5)).
abstract_trans_state(6, pc(s__3), pc(s__9), [1,2,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,35,37,38,40], loop, 53, (42,6)).
abstract_trans_state(6, pc(s__23), pc(s__1), [1,2,4,6,9,10,13,14,15,18,22,26,29,30,31,33,34,38], loop, 54, (44,5)).
abstract_trans_state(6, pc(s__23), pc(s__9), [1,2,4,5,6,9,10,13,14,15,18,21,22,25,26,29,30,31,33,34,37,38,40], loop, 55, (44,6)).
abstract_trans_state(6, pc(s__23), pc(s__9), [1,2,4,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,35,38], loop, 56, (46,6)).
abstract_trans_state(7, pc(s__3), pc(s__1), [1,2,3,6,9,10,13,14,17,18,20,22,26,29,30,33,34,37,38,40], loop, 57, (49,12)).
abstract_trans_state(7, pc(s__3), pc(s__17), [1,2,3,6,10,13,14,18,22,26,29,30,34,38], loop, 58, (49,14)).
abstract_trans_state(7, pc(s__3), pc(s__1), [1,2,6,9,10,13,14,15,18,22,26,29,30,31,33,34,38], loop, 59, (50,5)).
abstract_trans_state(7, pc(s__3), pc(s__9), [1,2,5,6,9,10,13,14,15,18,21,22,25,26,29,30,31,33,34,37,38,40], loop, 60, (50,6)).
abstract_trans_state(7, pc(s__3), pc(s__9), [1,2,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,35,38], loop, 61, (52,6)).
abstract_trans_state(7, pc(s__23), pc(s__9), [1,2,4,5,6,9,10,13,14,15,18,21,22,25,26,29,30,31,33,34,38], loop, 62, (54,6)).
abstract_trans_state(8, pc(s__3), pc(s__1), [1,2,3,6,9,10,13,14,18,22,26,29,30,33,34,38], loop, 63, (57,5)).
abstract_trans_state(8, pc(s__3), pc(s__9), [1,2,3,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,37,38,40], loop, 64, (57,6)).
abstract_trans_state(8, pc(s__3), pc(s__9), [1,2,5,6,9,10,13,14,15,18,21,22,25,26,29,30,31,33,34,38], loop, 65, (59,6)).
abstract_trans_state(9, pc(s__3), pc(s__9), [1,2,3,5,6,9,10,13,14,18,21,22,25,26,29,30,33,34,38], loop, 66, (63,6)).

frontier 0: stem 1 (pc(s__36)->pc(s__36)) from 0 by applying 0: 	T
frontier 1: stem 2 (pc(s__36)->pc(s__3)) from 1 by applying 7: 	0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=<input$20', 0=value$13', 0=<value$13', 0=key$1', 0=<key$1', 0=<value$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11'
frontier 1: stem 3 (pc(s__36)->pc(s__23)) from 1 by applying 8: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=<input$20', 0=value$13', 0=<value$13', 0=key$1', 0=<key$1', 0=<value$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11'
frontier 1: stem 4 (pc(s__36)->pc(s__1)) from 1 by applying 9: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=<key$11'
frontier 1: stem 5 (pc(s__36)->pc(s__9)) from 1 by applying 10: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=<key$11'
frontier 1: stem 6 (pc(s__36)->pc(s__17)) from 1 by applying 11: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', 0=<key$11'
frontier 2: loop 7 (pc(s__3)->pc(s__3)) from 2 by applying 0: 	0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 2: loop 8 (pc(s__3)->pc(s__3)) from 2 by applying 1: 	0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', value$1'=value$1, 0=<mapper$1', 0=<key$4', key$4'=key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 2: loop 9 (pc(s__3)->pc(s__23)) from 2 by applying 2: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', input$20'=input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', value$1'=value$1, 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 2: loop 10 (pc(s__23)->pc(s__23)) from 3 by applying 3: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 2: loop 11 (pc(s__23)->pc(s__17)) from 3 by applying 4: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'=key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 2: loop 12 (pc(s__1)->pc(s__1)) from 4 by applying 5: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', reducer$1'<reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=<key$1', key$1'<key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'=key$4, 0=<key$11'
frontier 2: loop 13 (pc(s__1)->pc(s__9)) from 4 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', value$28'=value$28, 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'=key$4, 0=<key$11', key$11'=key$11
frontier 2: loop 14 (pc(s__17)->pc(s__1)) from 6 by applying 12: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', value$13'=value$13, 0=<key$1', key$1'=key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', 0=<key$11', key$11'=key$11
frontier 2: loop 15 (pc(s__17)->pc(s__17)) from 6 by applying 13: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4, 0=<key$11', key$11'=key$11
frontier 2: loop 16 (pc(s__17)->pc(s__17)) from 6 by applying 14: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', reducer$1'<reducer$1, 0=<value$28', value$28'=value$28, 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=<key$1', key$1'<key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4, 0=<key$11'
frontier 3: loop 17 (pc(s__3)->pc(s__3)) from 7 by applying 1: 	0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 18 (pc(s__3)->pc(s__23)) from 7 by applying 2: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 19 (pc(s__3)->pc(s__23)) from 8 by applying 2: 	0=input$2', 0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', value$1'=value$1, 0=<mapper$1', 0=<key$4', key$4'=key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 20 (pc(s__3)->pc(s__17)) from 9 by applying 4: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'=key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 21 (pc(s__23)->pc(s__17)) from 10 by applying 4: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 22 (pc(s__23)->pc(s__1)) from 11 by applying 12: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 23 (pc(s__23)->pc(s__17)) from 11 by applying 13: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 3: loop 24 (pc(s__1)->pc(s__9)) from 12 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=key$1', 0=<key$1', key$1'<key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'=key$4, 0=<key$11'
frontier 3: loop 25 (pc(s__17)->pc(s__1)) from 14 by applying 5: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', reducer$1'<reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=<key$1', key$1'<key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 3: loop 26 (pc(s__17)->pc(s__9)) from 14 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', 0=<key$11', key$11'=key$11
frontier 3: loop 27 (pc(s__17)->pc(s__1)) from 15 by applying 12: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11', key$11'=key$11
frontier 3: loop 28 (pc(s__17)->pc(s__17)) from 15 by applying 14: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 4: loop 29 (pc(s__3)->pc(s__23)) from 17 by applying 2: 	0=input$2', 0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'=value$28, 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 30 (pc(s__3)->pc(s__17)) from 18 by applying 4: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 31 (pc(s__3)->pc(s__1)) from 20 by applying 12: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 32 (pc(s__3)->pc(s__17)) from 20 by applying 13: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 33 (pc(s__23)->pc(s__17)) from 21 by applying 13: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 34 (pc(s__23)->pc(s__9)) from 22 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 35 (pc(s__23)->pc(s__1)) from 23 by applying 12: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 4: loop 36 (pc(s__23)->pc(s__17)) from 23 by applying 14: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 4: loop 37 (pc(s__17)->pc(s__9)) from 25 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=key$1', 0=<key$1', key$1'<key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 4: loop 38 (pc(s__17)->pc(s__1)) from 27 by applying 5: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 5: loop 39 (pc(s__3)->pc(s__17)) from 29 by applying 4: 	0=input$2', 0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 40 (pc(s__3)->pc(s__17)) from 30 by applying 13: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 41 (pc(s__3)->pc(s__9)) from 31 by applying 6: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', key$1'=key$1, 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 42 (pc(s__3)->pc(s__1)) from 32 by applying 12: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 43 (pc(s__3)->pc(s__17)) from 32 by applying 14: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 5: loop 44 (pc(s__23)->pc(s__1)) from 33 by applying 12: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 45 (pc(s__23)->pc(s__17)) from 33 by applying 14: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=<key$11'
frontier 5: loop 46 (pc(s__23)->pc(s__1)) from 35 by applying 5: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 5: loop 47 (pc(s__23)->pc(s__9)) from 35 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 5: loop 48 (pc(s__17)->pc(s__9)) from 38 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'=input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 6: loop 49 (pc(s__3)->pc(s__17)) from 39 by applying 13: 	0=input$2', 0=<input$2', input$2'<input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 6: loop 50 (pc(s__3)->pc(s__1)) from 40 by applying 12: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 6: loop 51 (pc(s__3)->pc(s__17)) from 40 by applying 14: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4', 0=<key$11'
frontier 6: loop 52 (pc(s__3)->pc(s__1)) from 42 by applying 5: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 6: loop 53 (pc(s__3)->pc(s__9)) from 42 by applying 6: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=key$11', 0=<key$11', key$11'=key$11
frontier 6: loop 54 (pc(s__23)->pc(s__1)) from 44 by applying 5: 	0=input$2', 0=<input$2', input$2'=input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 6: loop 55 (pc(s__23)->pc(s__9)) from 44 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 6: loop 56 (pc(s__23)->pc(s__9)) from 46 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 7: loop 57 (pc(s__3)->pc(s__1)) from 49 by applying 12: 	0=input$2', 0=<input$2', input$2'<input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=value$13', 0=<value$13', value$13'=value$13, 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 7: loop 58 (pc(s__3)->pc(s__17)) from 49 by applying 14: 	0=input$2', 0=<input$2', input$2'<input$2, 0=<reducer$1', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=<key$4', 0=<key$11'
frontier 7: loop 59 (pc(s__3)->pc(s__1)) from 50 by applying 5: 	0=input$2', 0=<input$2', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 7: loop 60 (pc(s__3)->pc(s__9)) from 50 by applying 6: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 7: loop 61 (pc(s__3)->pc(s__9)) from 52 by applying 6: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'<key$4, 0=<key$11'
frontier 7: loop 62 (pc(s__23)->pc(s__9)) from 54 by applying 6: 	0=input$2', 0=<input$2', input$2'=input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 8: loop 63 (pc(s__3)->pc(s__1)) from 57 by applying 5: 	0=input$2', 0=<input$2', input$2'<input$2, 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=<key$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=<key$11'
frontier 8: loop 64 (pc(s__3)->pc(s__9)) from 57 by applying 6: 	0=input$2', 0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=key$11', 0=<key$11', key$11'=key$11
frontier 8: loop 65 (pc(s__3)->pc(s__9)) from 59 by applying 6: 	0=input$2', 0=<input$2', 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', input$20'<input$20, 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', 0=<key$11'
frontier 9: loop 66 (pc(s__3)->pc(s__9)) from 63 by applying 6: 	0=input$2', 0=<input$2', input$2'<input$2, 0=reducer$1', 0=<reducer$1', 0=value$28', 0=<value$28', 0=input$20', 0=<input$20', 0=<value$13', 0=key$1', 0=<key$1', 0=value$1', 0=<value$1', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', 0=<key$11'

_6692->_6695:	#40:	0=input$2', 0=<input$2', input$2'<input$2, input$2'=input$2, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, reducer$1'=reducer$1, 0=value$28', 0=<value$28', value$28'<value$28, value$28'=value$28, 0=input$20', 0=<input$20', input$20'<input$20, input$20'=input$20, 0=value$13', 0=<value$13', value$13'<value$13, value$13'=value$13, 0=key$1', 0=<key$1', key$1'<key$1, key$1'=key$1, 0=value$1', 0=<value$1', value$1'<value$1, value$1'=value$1, 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4, key$4'=key$4, 0=key$11', 0=<key$11', key$11'<key$11, key$11'=key$11
---------------------------------------------+----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.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

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

Input

Graph rewriting system

Initial Configuration

Transitions

master: make mappers

master: mappers created

master: mapping done

master: reducer

master: reducers created

master: done

mapper

reducer

Cover

cover element 0

cover element 1

cover element 2

cover element 3

cover element 4

Numerical Abstraction

ARMC output