def explore(mp, maxTransitions):
    # some globals may not be needed; code only mutates collection *contents*, 
    # as in finished, deadend
    global anames, states, graph, accepting, frontier, unsafe
    anames = mp.anames
    explored = list() 
    fsm = list() # list of transitions with mp states not state numbers
    more_runs = True # TestSuite might have multiple runs
    while more_runs:
      initialState = mp.Current()
      frontier.append(initialState)
      states.append(initialState) # includes initial state even if no trans'ns
      iInitial = states.index(initialState) # might already be there
      runstarts.append(iInitial)
      if mp.Accepting(): # initial state might be accepting even if no trans'ns
        accepting.append(iInitial)
      if not mp.StateInvariant():
        unsafe.append(iInitial)
      while frontier:
        if len(graph) == maxTransitions:
            break
        current = frontier[0]   # head, keep in mind current might lead nowhere
        frontier = frontier[1:] # tail
        icurrent = states.index(current) # might already be there
        #print 'current %s' % current # DEBUG
        #print '   frontier %s' % frontier # DEBUG
        explored.append(current) # states we checked, some might lead nowhere
        mp.Restore(deepcopy(current)) # assign state in mp, need deepcopy here
        transitions = mp.EnabledTransitions(list()) # all actions, not cleanup
        if not transitions: # terminal state, no enabled transitions
          if icurrent in accepting:
            finished.append(icurrent)
          else:
            deadend.append(icurrent)
        # print 'current %s, transitions %s' % (current, transitions) # DEBUG
        for (aname, args, result, next, next_properties) in transitions:
          # EnabledTransitions doesn't return transitions where not statefilter
          # if next_properties['statefilter']: 
            if len(graph) < maxTransitions:
                if next not in explored and next not in frontier:
                    # append for breadth-first, push on head for depth-first
                    frontier.append(next) # frontier contents are already copies
                transition = (current, (aname, args, result), next)
                if transition not in fsm:
                    fsm.append(transition)
                    if current not in states:
                        states.append(current)
                    if next not in states:
                        states.append(next) # next might never be in explored
                    # icurrent = states.index(current) # might already be there
                    inext = states.index(next) # ditto
                    graph.append((icurrent, (aname,args,result), inext)) #tuple
                    if mp.Accepting() and icurrent not in accepting:
                        accepting.append(icurrent)
                    if not mp.StateInvariant() and icurrent not in unsafe:
                        unsafe.append(icurrent)
                    if next_properties['accepting'] and inext not in accepting:
                        accepting.append(inext)
                    if not next_properties['stateinvariant'] and inext not in unsafe:
                        unsafe.append(inext)
                    # TK likewise dead states ... ?
            else: # found transition that will not be included in graph
                frontier.insert(0,current) # not completely explored after all
                # explored.remove(current) # not necessary
                break
            # end if < ntransitions else ...
        # end for transitions
      # end while frontier
     
      # continue exploring test suite with multiple runs
      more_runs = False
      if mp.TestSuite:
          try:
              mp.Reset()
              more_runs = True
          except __HOLE__: # raised by TestSuite Reset after last run
              pass # no more runs, we're done
    # end while more_runs
dataset/ETHPy150Open jon-jacky/PyModel/pymodel/Analyzer.py/explore