Computing Termination of mapReduce.dbp

  • Computing Termination of mapReduce.dbp
  • 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)
        (w, reducer) -> (v1, value)
    ==>
        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)
        (w, reducer) -> (v1, value)
    post
        (m, _) -> (k2, key) [result]
        (k2, key) -> (v1, value)
    ==>
        k1 -> k2
        v1 -> v1
    <==
        m -> m
    no
        (k1, key) -> (v2, value)
    ==>
        k1 -> k1
    

    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(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)), [(Key_25, 'key$25'), (Key_2, 'key$2'), (Value_16, 'value$16'), (Input_7, 'input$7'), (Reducer_1, 'reducer$1'), (Value_35, 'value$35'), (Value_3, 'value$3'), (Value_1, 'value$1'), (Input_6, 'input$6'), (Mapper_1, 'mapper$1'), (Key_26, 'key$26')]).
    
    preds( p(_, data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)), []).
    
    trans_preds(
      p(_, data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),  
      p(_, data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),  
      [ 0 = Key_25_prime,
        0 =< Key_25_prime,
        Key_25_prime < Key_25,
        Key_25_prime = Key_25,
        0 = Key_2_prime,
        0 =< Key_2_prime,
        Key_2_prime < Key_2,
        Key_2_prime = Key_2,
        0 = Value_16_prime,
        0 =< Value_16_prime,
        Value_16_prime < Value_16,
        Value_16_prime = Value_16,
        0 = Input_7_prime,
        0 =< Input_7_prime,
        Input_7_prime < Input_7,
        Input_7_prime = Input_7,
        0 = Reducer_1_prime,
        0 =< Reducer_1_prime,
        Reducer_1_prime < Reducer_1,
        Reducer_1_prime = Reducer_1,
        0 = Value_35_prime,
        0 =< Value_35_prime,
        Value_35_prime < Value_35,
        Value_35_prime = Value_35,
        0 = Value_3_prime,
        0 =< Value_3_prime,
        Value_3_prime < Value_3,
        Value_3_prime = Value_3,
        0 = Value_1_prime,
        0 =< Value_1_prime,
        Value_1_prime < Value_1,
        Value_1_prime = Value_1,
        0 = Input_6_prime,
        0 =< Input_6_prime,
        Input_6_prime < Input_6,
        Input_6_prime = Input_6,
        0 = Mapper_1_prime,
        0 =< Mapper_1_prime,
        Mapper_1_prime < Mapper_1,
        Mapper_1_prime = Mapper_1,
        0 = Key_26_prime,
        0 =< Key_26_prime,
        Key_26_prime < Key_26,
        Key_26_prime = Key_26
      ]).
    
    start( pc(s__36)).
    cutpoint(pc(s__16)).
    cutpoint(pc(s__3)).
    cutpoint(pc(s__1)).
    cutpoint(pc(s__17)).
    
    % unfolding; morphing, master: reducer; folding; covering
    r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_2 - Key_2_prime = -1, (Value_3 + Value_1 + 0 - Value_1_prime) - Value_3_prime = 0, Key_26_prime - Key_26 = -1, Key_25 = Key_25_prime, Value_16_prime = Value_16, Value_35 - Value_35_prime = -1, Reducer_1_prime - Reducer_1 = 1, Value_1 =< Value_1_prime + Value_3_prime, Value_1_prime =< Value_1, 1 =< Key_2_prime, 1 =< Key_26, 0 =< Value_16, 1 =< Value_35_prime, 0 =< Value_1_prime, 0 =< Reducer_1, 0 =< Key_25_prime, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
        [], 0).
    % unfolding; inhibiting; morphing, reducer; folding; covering
    r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_2 - Key_2_prime = 1, Value_1 = Value_1_prime, Key_25 - Key_25_prime = -1, Key_26_prime = Key_26, Value_35 - Value_35_prime = 1, Reducer_1_prime - Reducer_1 = -1, Value_16_prime - Value_16 = 1, Value_3_prime =< Value_3, 1 =< Key_25_prime, 0 =< Key_26, 0 =< Key_2_prime, 0 =< Value_16, 0 =< Value_1_prime, 0 =< Value_35_prime, 0 =< Value_3_prime, 1 =< Reducer_1, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
        [], 1).
    % inhibiting; morphing, master: reducers created; folding; covering
    r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_2 = Key_2_prime, (Value_1_prime + 0 - Value_1) - Value_35 = 0, Value_3 = Value_3_prime, Value_16_prime = Value_16, Key_25 = Key_25_prime, Reducer_1_prime = Reducer_1, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
        [], 2).
    % inhibiting; morphing, master: mapping done; covering
    r(  p(pc(s__3), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_25 = Key_26_prime, Value_1 = Value_1_prime, Key_25_prime = 0, Value_35_prime = 0, Key_2_prime = 0, Value_3_prime = 0, Reducer_1_prime = 0, Value_16_prime = 0, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
        [], 3).
    % unfolding; morphing, mapper; folding; covering
    r(  p(pc(s__3), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Input_7_prime - Input_7 = -1, Mapper_1_prime - Mapper_1 = -1, Key_25 =< Key_25_prime, 0 =< Key_25, Value_1 =< Value_1_prime, 0 =< Value_1, 1 =< Input_7, 1 =< Mapper_1, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
        [], 4).
    % unfolding; inhibiting; morphing, reducer; folding; covering
    r(  p(pc(s__1), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_25 - Key_25_prime = -1, Reducer_1 - Reducer_1_prime = 1, Value_1 - Value_1_prime = 1, Key_2 - Key_2_prime = 1, Value_16 - Value_16_prime = -1, Value_3_prime =< Value_3, 0 =< Value_3_prime, 0 =< Value_1_prime, 0 =< Reducer_1_prime, 0 =< Key_2_prime, 1 =< Value_16_prime, 1 =< Key_25_prime, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
        [], 5).
    % inhibiting; morphing, master: done; folding; covering
    r(  p(pc(s__1), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__9), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Key_25 = Key_25_prime, (Value_1 + Value_16 + Value_3) - Value_16_prime = 0, Key_2_prime = 0, Input_7_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Value_1_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
        [], 6).
    % initialize
    r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ 0 =< Key_26_prime, 0 =< Value_3_prime, 0 =< Reducer_1_prime, 0 =< Key_25_prime, 0 =< Value_1_prime, 0 =< Value_16_prime, 0 =< Key_2_prime, 0 =< Value_35_prime, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
        [], 7).
    % initialize
    r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ 0 =< Input_7_prime, 0 =< Value_1_prime, 0 =< Key_25_prime, 0 =< Mapper_1_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
        [], 8).
    % initialize
    r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ 0 =< Key_25_prime, 0 =< Key_2_prime, 0 =< Reducer_1_prime, 0 =< Value_1_prime, 0 =< Value_16_prime, 0 =< Value_3_prime, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
        [], 9).
    % initialize
    r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__9), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ 0 =< Key_25_prime, 0 =< Value_16_prime, Key_2_prime = 0, Input_7_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Value_1_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
        [], 10).
    % initialize
    r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ 0 =< Input_6_prime, 0 =< Value_1_prime, 0 =< Input_7_prime, 0 =< Key_25_prime, 0 =< Mapper_1_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_prime = 0 ],
        [], 11).
    % inhibiting; morphing, master: mappers created; covering
    r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Mapper_1 = Mapper_1_prime, Key_25 = Key_25_prime, Value_1 = Value_1_prime, Input_6 = Input_7_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
        [], 12).
    % unfolding; morphing, master: make mappers; folding; covering
    r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Mapper_1 - Mapper_1_prime = -1, Input_7 - Input_7_prime = 1, Value_1_prime = Value_1, Key_25 = Key_25_prime, Input_6_prime - Input_6 = 1, 1 =< Mapper_1_prime, 0 =< Input_7_prime, 0 =< Value_1, 0 =< Input_6, 0 =< Key_25_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_prime = 0 ],
        [], 13).
    % unfolding; morphing, mapper; folding; covering
    r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
        p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
        [ Mapper_1 - Mapper_1_prime = 1, Input_7 = Input_7_prime, Input_6_prime - Input_6 = -1, Key_25 =< Key_25_prime, 0 =< Key_25, 0 =< Mapper_1_prime, Value_1 =< Value_1_prime, 0 =< Value_1, 0 =< Input_7_prime, 1 =< Input_6, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_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.O2fHhllD1y
    ]
    reading input from /tmp/tmp.O2fHhllD1y
    ...done.
    
    
    
    --------------------------------------------------
    abstraction refinement iteration 0:
    lfp iteration 0 1 2 3 4 5 6 7 
    
    
    ==================================================
    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__16), [2,6,10,13,14,18,22,26,30,33,34,37,38,42], stem, 2, (1,7)).
    abstract_trans_state(1, pc(s__36), pc(s__3), [2,5,6,9,10,14,17,18,21,22,25,26,30,33,34,38,41,42], stem, 3, (1,8)).
    abstract_trans_state(1, pc(s__36), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,37,38,41,42], stem, 4, (1,9)).
    abstract_trans_state(1, pc(s__36), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], stem, 5, (1,10)).
    abstract_trans_state(1, pc(s__36), pc(s__17), [2,5,6,9,10,14,17,18,21,22,25,26,30,34,38,41,42], stem, 6, (1,11)).
    abstract_trans_state(2, pc(s__16), pc(s__16), [2,4,6,10,12,13,14,16,18,22,26,30,33,34,36,37,38,40,42,43], loop, 7, (2,0)).
    abstract_trans_state(2, pc(s__16), pc(s__16), [2,6,7,10,13,14,16,18,19,22,23,26,30,32,33,34,36,37,38,40,42,44], loop, 8, (2,1)).
    abstract_trans_state(2, pc(s__16), pc(s__1), [2,4,6,8,10,12,13,14,16,18,20,21,22,26,28,30,33,34,36,37,38,40,41,42], loop, 9, (2,2)).
    abstract_trans_state(2, pc(s__3), pc(s__16), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,36,37,38,42], loop, 10, (3,3)).
    abstract_trans_state(2, pc(s__3), pc(s__3), [2,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,33,34,36,38,39,41,42,44], loop, 11, (3,4)).
    abstract_trans_state(2, pc(s__1), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,24,26,30,31,33,34,36,37,38,40,41,42,44], loop, 12, (4,5)).
    abstract_trans_state(2, pc(s__1), pc(s__9), [2,4,5,6,10,13,14,16,17,18,21,22,24,25,26,29,30,33,34,36,37,38,40,41,42,44], loop, 13, (4,6)).
    abstract_trans_state(2, pc(s__17), pc(s__3), [2,4,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,32,33,34,38,40,41,42,44], loop, 14, (6,12)).
    abstract_trans_state(2, pc(s__17), pc(s__17), [2,4,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,32,34,38,41,42,44], loop, 15, (6,13)).
    abstract_trans_state(2, pc(s__17), pc(s__17), [2,5,6,8,9,10,12,14,16,17,18,20,21,22,24,25,26,28,30,34,35,38,39,41,42,44], loop, 16, (6,14)).
    abstract_trans_state(3, pc(s__16), pc(s__16), [2,6,10,13,14,16,18,22,26,30,33,34,36,37,38,40,42,43], loop, 17, (7,1)).
    abstract_trans_state(3, pc(s__16), pc(s__1), [2,4,6,10,12,13,14,16,18,21,22,26,30,33,34,36,37,38,40,41,42,43], loop, 18, (7,2)).
    abstract_trans_state(3, pc(s__16), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,23,26,30,33,34,36,37,38,40,41,42], loop, 19, (8,2)).
    abstract_trans_state(3, pc(s__16), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,26,30,33,34,36,37,38,40,41,42], loop, 20, (9,5)).
    abstract_trans_state(3, pc(s__16), pc(s__9), [2,4,5,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,36,37,38,40,41,42], loop, 21, (9,6)).
    abstract_trans_state(3, pc(s__3), pc(s__16), [1,2,6,9,10,12,13,14,18,22,26,30,33,34,36,37,38,42], loop, 22, (10,0)).
    abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,36,37,38,41,42], loop, 23, (10,2)).
    abstract_trans_state(3, pc(s__1), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,24,25,26,29,30,31,33,34,36,37,38,40,41,42,44], loop, 24, (12,6)).
    abstract_trans_state(3, pc(s__17), pc(s__16), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,37,38,42], loop, 25, (14,3)).
    abstract_trans_state(3, pc(s__17), pc(s__3), [2,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,33,34,38,39,41,42,44], loop, 26, (14,4)).
    abstract_trans_state(3, pc(s__17), pc(s__3), [2,4,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,32,33,34,38,41,42,44], loop, 27, (15,12)).
    abstract_trans_state(3, pc(s__17), pc(s__17), [2,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,34,38,41,42,44], loop, 28, (15,14)).
    abstract_trans_state(4, pc(s__16), pc(s__1), [2,6,10,13,14,16,18,21,22,26,30,33,34,36,37,38,40,41,42,43], loop, 29, (17,2)).
    abstract_trans_state(4, pc(s__16), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,23,25,26,29,30,33,34,36,37,38,40,41,42], loop, 30, (19,6)).
    abstract_trans_state(4, pc(s__16), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,25,26,29,30,33,34,36,37,38,40,41,42], loop, 31, (20,6)).
    abstract_trans_state(4, pc(s__3), pc(s__16), [2,6,10,13,14,18,22,26,30,33,34,36,37,38,42], loop, 32, (22,1)).
    abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,6,9,10,12,13,14,18,21,22,26,30,33,34,36,37,38,41,42], loop, 33, (22,2)).
    abstract_trans_state(4, pc(s__3), pc(s__9), [1,2,5,6,8,10,13,14,17,18,20,21,22,24,25,26,28,29,30,33,34,36,37,38,41,42], loop, 34, (23,6)).
    abstract_trans_state(4, pc(s__17), pc(s__16), [1,2,6,9,10,12,13,14,18,22,26,30,33,34,37,38,42], loop, 35, (25,0)).
    abstract_trans_state(4, pc(s__17), pc(s__1), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,37,38,41,42], loop, 36, (25,2)).
    abstract_trans_state(4, pc(s__17), pc(s__3), [2,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,33,34,38,41,42,44], loop, 37, (27,4)).
    abstract_trans_state(5, pc(s__16), pc(s__9), [2,5,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,36,37,38,40,41,42,43], loop, 38, (29,6)).
    abstract_trans_state(5, pc(s__3), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,36,37,38,41,42], loop, 39, (32,2)).
    abstract_trans_state(5, pc(s__3), pc(s__9), [1,2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,36,37,38,41,42], loop, 40, (33,6)).
    abstract_trans_state(5, pc(s__17), pc(s__16), [2,6,10,13,14,18,22,26,30,33,34,37,38,42], loop, 41, (35,1)).
    abstract_trans_state(5, pc(s__17), pc(s__1), [1,2,6,9,10,12,13,14,18,21,22,26,30,33,34,37,38,41,42], loop, 42, (35,2)).
    abstract_trans_state(5, pc(s__17), pc(s__9), [1,2,5,6,8,10,13,14,17,18,20,21,22,24,25,26,28,29,30,33,34,37,38,41,42], loop, 43, (36,6)).
    abstract_trans_state(6, pc(s__3), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,36,37,38,41,42], loop, 44, (39,6)).
    abstract_trans_state(6, pc(s__17), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,37,38,41,42], loop, 45, (41,2)).
    abstract_trans_state(6, pc(s__17), pc(s__9), [1,2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], loop, 46, (42,6)).
    abstract_trans_state(7, pc(s__17), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], loop, 47, (45,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__16)) from 1 by applying 7: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 1: stem 3 (pc(s__36)->pc(s__3)) from 1 by applying 8: 	0=<key$25', 0=key$2', 0=<key$2', 0=value$16', 0=<value$16', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 1: stem 4 (pc(s__36)->pc(s__1)) from 1 by applying 9: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 1: stem 5 (pc(s__36)->pc(s__9)) from 1 by applying 10: 	0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 1: stem 6 (pc(s__36)->pc(s__17)) from 1 by applying 11: 	0=<key$25', 0=key$2', 0=<key$2', 0=value$16', 0=<value$16', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=<value$1', 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 2: loop 7 (pc(s__16)->pc(s__16)) from 2 by applying 0: 	0=<key$25', key$25'=key$25, 0=<key$2', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$26', key$26'<key$26
    frontier 2: loop 8 (pc(s__16)->pc(s__16)) from 2 by applying 1: 	0=<key$25', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', reducer$1'<reducer$1, 0=<value$35', value$35'<value$35, 0=<value$3', 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$26', key$26'=key$26
    frontier 2: loop 9 (pc(s__16)->pc(s__1)) from 2 by applying 2: 	0=<key$25', key$25'=key$25, 0=<key$2', key$2'=key$2, 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', 0=<value$3', value$3'=value$3, 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 2: loop 10 (pc(s__3)->pc(s__16)) from 3 by applying 3: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 2: loop 11 (pc(s__3)->pc(s__3)) from 3 by applying 4: 	0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', input$7'<input$7, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=<mapper$1', mapper$1'<mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 2: loop 12 (pc(s__1)->pc(s__1)) from 4 by applying 5: 	0=<key$25', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=<value$3', 0=<value$1', value$1'<value$1, 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 2: loop 13 (pc(s__1)->pc(s__9)) from 4 by applying 6: 	0=<key$25', key$25'=key$25, 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 2: loop 14 (pc(s__17)->pc(s__3)) from 6 by applying 12: 	0=<key$25', key$25'=key$25, 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 2: loop 15 (pc(s__17)->pc(s__17)) from 6 by applying 13: 	0=<key$25', key$25'=key$25, 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', input$7'<input$7, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26', key$26'=key$26
    frontier 2: loop 16 (pc(s__17)->pc(s__17)) from 6 by applying 14: 	0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', 0=<input$6', input$6'<input$6, 0=<mapper$1', mapper$1'<mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 3: loop 17 (pc(s__16)->pc(s__16)) from 7 by applying 1: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$26', key$26'<key$26
    frontier 3: loop 18 (pc(s__16)->pc(s__1)) from 7 by applying 2: 	0=<key$25', key$25'=key$25, 0=<key$2', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'<key$26
    frontier 3: loop 19 (pc(s__16)->pc(s__1)) from 8 by applying 2: 	0=<key$25', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', value$35'<value$35, 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 3: loop 20 (pc(s__16)->pc(s__1)) from 9 by applying 5: 	0=<key$25', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 3: loop 21 (pc(s__16)->pc(s__9)) from 9 by applying 6: 	0=<key$25', key$25'=key$25, 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 3: loop 22 (pc(s__3)->pc(s__16)) from 10 by applying 0: 	0=key$25', 0=<key$25', 0=<key$2', 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 3: loop 23 (pc(s__3)->pc(s__1)) from 10 by applying 2: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 3: loop 24 (pc(s__1)->pc(s__9)) from 12 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', value$1'<value$1, 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 3: loop 25 (pc(s__17)->pc(s__16)) from 14 by applying 3: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 3: loop 26 (pc(s__17)->pc(s__3)) from 14 by applying 4: 	0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', 0=input$6', 0=<input$6', 0=<mapper$1', mapper$1'<mapper$1, 0=key$26', 0=<key$26', key$26'=key$26
    frontier 3: loop 27 (pc(s__17)->pc(s__3)) from 15 by applying 12: 	0=<key$25', key$25'=key$25, 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26', key$26'=key$26
    frontier 3: loop 28 (pc(s__17)->pc(s__17)) from 15 by applying 14: 	0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', input$7'<input$7, 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26', key$26'=key$26
    frontier 4: loop 29 (pc(s__16)->pc(s__1)) from 17 by applying 2: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'<key$26
    frontier 4: loop 30 (pc(s__16)->pc(s__9)) from 19 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', value$35'<value$35, 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 4: loop 31 (pc(s__16)->pc(s__9)) from 20 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', key$2'<key$2, 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26'
    frontier 4: loop 32 (pc(s__3)->pc(s__16)) from 22 by applying 1: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 4: loop 33 (pc(s__3)->pc(s__1)) from 22 by applying 2: 	0=key$25', 0=<key$25', 0=<key$2', 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 4: loop 34 (pc(s__3)->pc(s__9)) from 23 by applying 6: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 4: loop 35 (pc(s__17)->pc(s__16)) from 25 by applying 0: 	0=key$25', 0=<key$25', 0=<key$2', 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 4: loop 36 (pc(s__17)->pc(s__1)) from 25 by applying 2: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', value$1'=value$1, 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 4: loop 37 (pc(s__17)->pc(s__3)) from 27 by applying 4: 	0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=value$16', 0=<value$16', value$16'=value$16, 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=<value$1', 0=input$6', 0=<input$6', 0=<mapper$1', 0=key$26', 0=<key$26', key$26'=key$26
    frontier 5: loop 38 (pc(s__16)->pc(s__9)) from 29 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', input$7'=input$7, 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'<key$26
    frontier 5: loop 39 (pc(s__3)->pc(s__1)) from 32 by applying 2: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 5: loop 40 (pc(s__3)->pc(s__9)) from 33 by applying 6: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 5: loop 41 (pc(s__17)->pc(s__16)) from 35 by applying 1: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=<key$26'
    frontier 5: loop 42 (pc(s__17)->pc(s__1)) from 35 by applying 2: 	0=key$25', 0=<key$25', 0=<key$2', 0=value$16', 0=<value$16', value$16'=value$16, 0=input$7', 0=<input$7', 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 5: loop 43 (pc(s__17)->pc(s__9)) from 36 by applying 6: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', key$2'=key$2, 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'=value$35, 0=value$3', 0=<value$3', value$3'=value$3, 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 6: loop 44 (pc(s__3)->pc(s__9)) from 39 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', input$6'=input$6, 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 6: loop 45 (pc(s__17)->pc(s__1)) from 41 by applying 2: 	0=<key$25', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=<reducer$1', 0=value$35', 0=<value$35', 0=<value$3', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 6: loop 46 (pc(s__17)->pc(s__9)) from 42 by applying 6: 	0=key$25', 0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    frontier 7: loop 47 (pc(s__17)->pc(s__9)) from 45 by applying 6: 	0=<key$25', 0=key$2', 0=<key$2', 0=<value$16', 0=input$7', 0=<input$7', 0=reducer$1', 0=<reducer$1', 0=value$35', 0=<value$35', 0=value$3', 0=<value$3', 0=value$1', 0=<value$1', 0=input$6', 0=<input$6', 0=mapper$1', 0=<mapper$1', 0=key$26', 0=<key$26'
    
    _6498->_6501:	#44:	0=key$25', 0=<key$25', key$25'<key$25, key$25'=key$25, 0=key$2', 0=<key$2', key$2'<key$2, key$2'=key$2, 0=value$16', 0=<value$16', value$16'<value$16, value$16'=value$16, 0=input$7', 0=<input$7', input$7'<input$7, input$7'=input$7, 0=reducer$1', 0=<reducer$1', reducer$1'<reducer$1, reducer$1'=reducer$1, 0=value$35', 0=<value$35', value$35'<value$35, value$35'=value$35, 0=value$3', 0=<value$3', value$3'<value$3, value$3'=value$3, 0=value$1', 0=<value$1', value$1'<value$1, value$1'=value$1, 0=input$6', 0=<input$6', input$6'<input$6, input$6'=input$6, 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, mapper$1'=mapper$1, 0=key$26', 0=<key$26', key$26'<key$26, key$26'=key$26
    ---------------------------------------------+----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.02     |     0.02     |
    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