from automata import weighted_structure,progressivetimeoptimalsynthesis,tau_abstraction, collection, weighted_frontend, \
                     data_structure
import random
import time
import heapq
import collections
import numpy

attempts = 1

resultsfiles = [file('resultsattempt' + str(i), 'w') for i in range(1, attempts+1)]

def remove_colision_states(aut):
    states_to_remove = []
    for state in aut.get_states():
        dict = {}
        states = set()
        for edge in state.get_incoming():
            split = edge.label.name.split('-')
            if split[0] in dict:
                assert(dict[split[0]] == split[2])
            else:
                if split[2] in states:
                    states_to_remove.append(state)
                    break
                dict[split[0]] = split[2]
                states.add(split[2])
    for state in states_to_remove:
        aut.remove_state(state)

def set_collision_states(aut):
    collisions = {}
    for state in aut.get_states():
        for edge in state.get_incoming():
            split = edge.label.name.split('-')
            collisions[state] = set([int(split[2])])
            #state.collisions = set([int(split[2])])
    collisions[aut.initial] = set([int(aut.initial.get_outgoing()[0].label.name.split('-')[1])])
    return collisions

def create_run(index, startstop = None):
    if startstop != None:
        for i, (start, stop) in enumerate(startstop):
            if (start == 35 or start == 36):
                start += 2
            if (stop == 35 or stop == 36):
                stop += 2
            startstop[i] = (start, stop)
    names, state_resources = make_epucks(index, startstop)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts] + make_resources(index, auts[0].collection)
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    resources = map(frozenset, resources)
    return make_path(auts, resources, state_resources)

def create_run_numpy(startstop, conservative = True, blocked = [], notintersection = []):
    for i, (pid, start, stop) in enumerate(startstop):
        if (start == 35 or start == 36):
            start += 2
        if (stop == 35 or stop == 36):
            stop += 2
        startstop[i] = (pid, start, stop)
    def event_to_stringcorrect(event):
        split = event.name.split('-')
        source, too = int(split[1]), int(split[2])
        if source == 37 or source == 38:
            source -= 2
        if too == 37 or too == 38:
            source -= 2
        return '{}-{}-{}'.format(split[0],source,too)
    names, state_resources = make_epucks_indexed(startstop, blocked, notintersection)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts]
    resources.extend(make_resources_indexs([pid for pid, _, _ in startstop], auts[0].collection))
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    state_resource_map = collections.defaultdict(list)
    if not conservative:
        for i, sres in enumerate(state_resources):
            for event in sres:
                state_resource_map[event].append(i)
    else:
        resources.extend(state_resources)
    resources = map(frozenset, resources)
    #handle = file('mutex12.txt', 'w')
    #mutpairs = set()
    #for res in resources:
    #    for ev1 in res:
    #        for ev2 in res:
    #            mutpairs.add('({},{})'.format(event_to_stringcorrect(ev1), event_to_stringcorrect(ev2)))
    #handle.write('{{{}}}'.format(','.join(mutpairs)))
    #handle.close()
    alphabet = set()
    for aut in auts:
        alphabet.update(aut.alphabet)
    resource_int_map = {}
    for i, res in enumerate(resources):
        resource_int_map[res] = i
    event_resource_map = {}
    numpy_array_map = {}

    for event in alphabet:
        event_resource_map[event] = [resource_int_map[res] for res in resources if event in res]
        indexs = set(event_resource_map[event])
        numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(len(resources))], numpy.int8)
    epuck_res = [resource_int_map[frozenset(aut.alphabet)] for aut in auts]
    int_resources = set(resource_int_map.values())
    epuck_res = int_resources
    #make_path(auts, resources, state_resources)
    path, etime = make_path_epucks(auts, resources, state_resources, event_resource_map, epuck_res,
                          int_resources, resource_int_map, state_resource_map, numpy_array_map, 10)
    if path != None:
        for i, event in enumerate(path):
            path[i] = event_to_stringcorrect(event.label)
        handle = file('epuckevents.txt', 'w')
        handle.write('{}\n'.format(etime))
        handle.write('{}'.format(','.join(path)))
        handle.close()

def create_run_width(index, width, startstop = None):
    names, state_resources = make_epucks_width(index, startstop, width)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts] + make_resources_varied_width(index, auts[0].collection, width)
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    resources = map(frozenset, resources)
    make_path(auts, resources, state_resources)

def make_path(auts, resources, state_resources):
    handle = file('resultsepuck', 'w')
    for arbitrary in [1]:
        autweights = []
        dur = -time.clock()
        state_resources = set(state_resources)
        for aut in auts:
            collisions = set_collision_states(aut)
            heur = mark_aut_reverse_djikstra(aut)
            #autweights.append((aut, aut.initial.heur[0][1]))
            autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        autweights.sort(key= lambda x: x[1])
        autweights.reverse()
        lbe = autweights[0][1]
        numepucks = len(autweights)
        size = auts[0].get_num_states()
        #path.initial.collisions = []
        #path.initial.heur = []
        bestorigweight = float('inf')
        bestcompressweight = float('inf')
        for trie in range(attempts):
            path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
            path.initial = path.add_new_state(True)
            pathcoll = {}
            pathheur = {}
            pathcoll[path.initial] = []
            pathheur[path.initial] = []
            if trie == 1:
                autweights.reverse()
            elif trie > 1:
                random.shuffle(autweights)
            for (i, (aut,_,collA,heurA)) in enumerate(autweights):
                path, weight, pathcoll, pathheur = a_star_search(aut, path, resources, collA, pathcoll, heurA, pathheur)
                if path == None:
                    break
                #product = progressivetimeoptimalsynthesis.synchronousproduct_weighted_epucks([aut, path], 0)
                #product, weight = progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([product],
                #                                                                                        frozenset(product.alphabet), resources)
                #product, weight = progressivetimeoptimalsynthesis.make_greedy_prog_supervisor_all_controllable_epuck(product,
                #                                                                                               frozenset(product.alphabet), resources)
                #print "weight: " + str(weight)
                #product.save_as_dot("product.dot")
                #path = tau_abstraction.restrictpath(product)
                #print "restricted"
            if path == None:
                origweight = float('inf')
                compressweight = float('inf')
            else:
                origweight = weight
                trace = []
                state = path.initial
                while not state.marked:
                    edge = state.get_outgoing()[0]
                    trace.append(edge)
                    state = edge.succ
                trace, compressweight = compress_path(trace, resources, state_resources)
            bestorigweight = min(bestorigweight, origweight)
            bestcompressweight = min(bestcompressweight, compressweight)
            tim = dur + time.clock()
            resultsfiles[trie].write('epucks:{},size:{},lbe:{},weight:{},cweight:{},bweight:{},bcweight{},time:{}\n'.format(
                numepucks, size, lbe, origweight, compressweight, bestorigweight, bestcompressweight, tim
            ))
            resultsfiles[trie].flush()

def trace_to_path(trace, alphabet, coll, event_resource_map, fin_coll, puck_res):
    path = weighted_structure.WeightedAutomaton(alphabet, coll)
    prevstate = None
    state = path.add_new_state(True)
    contour = collections.defaultdict(lambda: 0)
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = fin_coll
    heur[state] = [(res, 0) for res in puck_res]
    for edge in reversed(trace):
        event, weight = edge.label, edge.weight
        prevstate = path.add_new_state(False)
        edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
        path.add_edge(edge)
        contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
        heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
        new_coll = set(collisions[state])
        split = event.name.split('-')
        prev, succ = int(split[1]), int(split[2])
        new_coll.remove(succ)
        new_coll.add(prev)
        collisions[prevstate] = new_coll
        state = prevstate
    path.initial = state
    return path, heur, collisions

def trace_to_path_numpy(trace, alphabet, coll, numpy_resource_map, fin_coll, puck_res, num_resources):
    path = weighted_structure.WeightedAutomaton(alphabet, coll)
    prevstate = None
    state = path.add_new_state(True)
    contour = numpy.array([0 for i in range(num_resources)], numpy.int8)
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = fin_coll
    heur[state] = contour
    for edge in reversed(trace):
        event, weight = edge.label, edge.weight
        prevstate = path.add_new_state(False)
        edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
        path.add_edge(edge)
        contour = numpy_rev_stack(contour, numpy_resource_map[event], weight)
        heur[prevstate] = contour
        new_coll = set(collisions[state])
        split = event.name.split('-')
        prev, succ = int(split[1]), int(split[2])
        assert (succ in new_coll)
        new_coll.remove(succ)
        assert (prev not in new_coll)
        new_coll.add(prev)
        collisions[prevstate] = new_coll
        state = prevstate
    path.initial = state
    return path, heur, collisions

def trace_to_path_numpy_drop(trace, alphabet, coll, numpy_resource_map, fin_coll, puck_res, num_resources):
    path = weighted_structure.WeightedAutomaton(alphabet, coll)
    prevstate = None
    state = path.add_new_state(True)
    contour = numpy.array([0 for i in range(num_resources)], numpy.int8)
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = fin_coll
    heur[state] = contour
    for edge in reversed(trace):
        event, weight = edge.label, edge.weight
        prevstate = path.add_new_state(False)
        edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
        path.add_edge(edge)
        contour = numpy_rev_stack_drop(contour, numpy_resource_map[event], weight)
        heur[prevstate] = contour
        new_coll = set(collisions[state])
        split = event.name.split('-')
        prev, succ = int(split[1]), int(split[2])
        assert (succ in new_coll)
        new_coll.remove(succ)
        assert (prev not in new_coll)
        new_coll.add(prev)
        collisions[prevstate] = new_coll
        state = prevstate
    path.initial = state
    return path, heur, collisions

def trace_to_path_wafer(trace, alphabet, coll, event_resource_map, fin_coll, puck_res):
    path = weighted_structure.WeightedAutomaton(alphabet, coll)
    prevstate = None
    state = path.add_new_state(True)
    contour = collections.defaultdict(lambda: 0)
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = fin_coll
    heur[state] = [(res, 0) for res in puck_res]
    for edge in reversed(trace):
        event, weight = edge.label, edge.weight
        prevstate = path.add_new_state(False)
        edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
        path.add_edge(edge)
        contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
        heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
        new_coll = set(collisions[state])
        split = event.name.split('-')
        prev, succ = split[1].split('_')[1], split[2].split('_')[1]
        if succ != '':
            new_coll.remove(succ)
        if prev != '':
            new_coll.add(prev)
        collisions[prevstate] = new_coll
        state = prevstate
    path.initial = state
    return path, heur, collisions

def make_path_epucks(auts, resources, state_resources, event_resource_map, puck_res, int_resources, resource_to_int,
                     event_state_resource_map, numpy_array_map, attempts = 1):
    autweights = []
    dur = -time.clock()
    state_resources = set(state_resources)
    for aut in auts:
        collisions = set_collision_states(aut)
        heur = mark_aut_reverse_djikstra_default(aut, resource_to_int[frozenset(aut.alphabet)])
        #autweights.append((aut, aut.initial.heur[0][1]))
        autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
        #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
    autweights.sort(key= lambda x: x[1])
    autweights.reverse()
    lbe = autweights[0][1]
    numepucks = len(autweights)
    size = auts[0].get_num_states()
    #path.initial.collisions = []
    #path.initial.heur = []
    bestorigweight = float('inf')
    bestcompressweight = float('inf')
    comptime = 0
    astar_time = 0
    #p1 = cp.Profile()
    #p2 = cp.Profile()
    for trie in range(attempts):
        path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
        path.initial = path.add_new_state(True)
        pathcoll = {}
        pathheur = {}
        pathcoll[path.initial] = set([])
        pathheur[path.initial] = numpy.array([0 for i in range(len(resources))], numpy.int8)
        if trie == 1:
            autweights.reverse()
        elif trie > 1:
            random.shuffle(autweights)
        for (i, (aut,aw,collA,heurA)) in enumerate(autweights):
            path, weight, pathcoll, _ = a_star_search_numpy(aut, path, int_resources, collA,
                                                            pathcoll, heurA, pathheur,
                                                            numpy_array_map, puck_res)
            if path == None:
                break
            for state in path.get_states():
                if state.marked:
                    fin_state = state
                    break
            fin_coll = pathcoll[fin_state]
            trace = []
            state = path.initial
            while not state.marked:
                edge = state.get_outgoing()[0]
                trace.append(edge)
                state = edge.succ
            trace, compressweight = compress_path_better(trace, event_resource_map, event_state_resource_map)
            path, pathheur, pathcoll = trace_to_path_numpy(trace, path.alphabet, path.collection, numpy_array_map,
                                                           fin_coll, puck_res, len(resources))
        if path == None:
            origweight = float('inf')
            compressweight = float('inf')
        else:
            origweight = weight
            print compressweight
            return trace,compressweight
        bestorigweight = min(bestorigweight, origweight)
        bestcompressweight = min(bestcompressweight, compressweight)
        tim = dur + time.clock()
    return None, None

def make_path_default(auts, resources, state_resources, event_resource_map, puck_res, int_resources, resource_to_int,
                      event_state_resource_map, numpy_array_map):
    handle = file('resultsepuck', 'w')
    for arbitrary in [1]:
        autweights = []
        dur = -time.clock()
        state_resources = set(state_resources)
        for aut in auts:
            collisions = set_collision_states(aut)
            heur = mark_aut_reverse_djikstra_default(aut, resource_to_int[frozenset(aut.alphabet)])
            #autweights.append((aut, aut.initial.heur[0][1]))
            autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        autweights.sort(key= lambda x: x[1])
        autweights.reverse()
        lbe = autweights[0][1]
        numepucks = len(autweights)
        size = auts[0].get_num_states()
        #path.initial.collisions = []
        #path.initial.heur = []
        bestorigweight = float('inf')
        bestcompressweight = float('inf')
        comptime = 0
        astar_time = 0
        #p1 = cp.Profile()
        #p2 = cp.Profile()
        for trie in range(attempts):
            path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
            path.initial = path.add_new_state(True)
            pathcoll = {}
            pathheur = {}
            pathcoll[path.initial] = set([])
            pathheur[path.initial] = numpy.array([0 for i in range(len(resources))], numpy.int8)
            if trie == 1:
                autweights.reverse()
            elif trie > 1:
                random.shuffle(autweights)
            for (i, (aut,aw,collA,heurA)) in enumerate(autweights):
                #p2.enable()
                #path, weight, pathcoll, pathheur = a_star_search_default(aut, path, int_resources, collA,
                #                                                         pathcoll, heurA, pathheur,
                #                                                         event_resource_map, puck_res)
                #p2.disable()
                #p2.enable()
                #astar_time -= time.clock()
                path, weight, pathcoll, _ = a_star_search_numpy(aut, path, int_resources, collA,
                                                                pathcoll, heurA, pathheur,
                                                                numpy_array_map, puck_res)
                #astar_time += time.clock()
                #p2.disable()
                if path == None:
                    break
                for state in path.get_states():
                    if state.marked:
                        fin_state = state
                        break
                fin_coll = pathcoll[fin_state]
                trace = []
                state = path.initial
                while not state.marked:
                    edge = state.get_outgoing()[0]
                    trace.append(edge)
                    state = edge.succ
                #comptime -= time.clock()
                #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
                #compressweight = weight
                trace, compressweight = compress_path_better(trace, event_resource_map, event_state_resource_map)
                #comptime += time.clock()
                #path, pathheur, pathcoll = trace_to_path(trace, path.alphabet, path.collection,
                #                                         event_resource_map, fin_coll, puck_res)
                path, pathheur, pathcoll = trace_to_path_numpy(trace, path.alphabet, path.collection, numpy_array_map,
                                                               fin_coll, puck_res, len(resources))
                #path, pathheur, pathcoll = trace_to_path_numpy_drop(trace, path.alphabet, path.collection, numpy_array_map,
                #                                               fin_coll, puck_res, len(resources))
                #product = progressivetimeoptimalsynthesis.synchronousproduct_weighted_epucks([aut, path], 0)
                #product, weight = progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([product],
                #                                                                                        frozenset(product.alphabet), resources)
                #product, weight = progressivetimeoptimalsynthesis.make_greedy_prog_supervisor_all_controllable_epuck(product,
                #                                                                                               frozenset(product.alphabet), resources)
                #print "weight: " + str(weight)
                #product.save_as_dot("product.dot")
                #path = tau_abstraction.restrictpath(product)
                #print "restricted"
            if path == None:
                origweight = float('inf')
                compressweight = float('inf')
            else:
                origweight = weight
                #trace = []
                #state = path.initial
                #while not state.marked:
                #    edge = state.get_outgoing()[0]
                #    trace.append(edge)
                #    state = edge.succ
                #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
            bestorigweight = min(bestorigweight, origweight)
            bestcompressweight = min(bestcompressweight, compressweight)
            #bestcompressweight = comp
            #compressweight = origweight
            tim = dur + time.clock()
            resultsfiles[trie].write('epucks:{},size:{},lbe:{},weight:{},cweight:{},bweight:{},bcweight{},time:{},tncomp:{}\n'.format(
                numepucks, size, lbe, origweight, compressweight, bestorigweight, bestcompressweight, tim, comptime
            ))
            resultsfiles[trie].flush()
    #print 'default'
    #s = StringIO.StringIO()
    #sortby = 'cumulative'
    #ps = pstats.Stats(p1, stream=s).sort_stats(sortby)
    #ps.print_stats()

def make_epuck_varied_width(index, initial, marked, width):
    total = ((width * 2)-1) * (width-1) + width-1
    not_used = set()
    string = "[weighted-automaton]\n"
    string += "states = " + ",".join(map(lambda x: str(x).zfill(2), range(1,total + 1))) + "\n"
    puck = "P" + str(index)
    state_resources = {}
    def destinations(index):
        mod = ((width * 2)-1)
        dests = []
        if (index-1) % mod < (width - 1):
            if index % mod != 1:
                dests.append(-1)
            if index % mod != (width - 1):
                dests.append(1)
            dests += [-width,-width+1,width-1,width]
        else:
            dests += [-mod, mod]
            if index % mod != width:
                dests += [-width,width-1]
            if index % mod != 0:
                dests += [-width+1,width]
        return dests
    alphabet = []
    for i in range(1, total+1):
        if i in not_used:
            continue
        place = str(i).zfill(2)
        state_resources[place] = []
        out_going = [puck + "-" + place + "-" + str(i + val).zfill(2) for val in destinations(i) if
                     (i + val > 0) and (i + val <= total) and ((i+val) not in not_used)]
        alphabet += out_going
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(event):
        split = event.split('-')
        state_resources[split[1]].append(event)
        state_resources[split[2]].append(event)
        return "(" + split[1] + "," + split[2] + "," + event + ",1)"
    string += "transitions = " + ','.join(map(transition, alphabet)) + "\n"
    string += "initial-state = " + str(initial).zfill(2) + "\n"
    string += "marker-states = " + str(marked).zfill(2) + "\n"
    return string, state_resources


# note this is only for use with the epuck model. As it takes into account the fact that all events are local
def a_star_search(autA, autB, resources, collA, collB, heurA, heurB, state_resources = []):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = {}
    for res in resources:
        zerocontour[res] = 0
    for res in state_resources:
        zerocontour[res] = 0
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = {}
    for r in resources:
        contour[r] = 0
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            if (state_resources == []):
                contour = progressivetimeoptimalsynthesis.rev_res_plus(contour, edge)
            else:
                contour = progressivetimeoptimalsynthesis.rev_res_plus_drop(contour, edge, state_resources)
            #prevstate.heur = [(res, time) for res, time in contour.iteritems()]
            #prevstate.collisions = prevtuple[0].collisions.union(prevtuple[1].collisions)
            heur[prevstate] = [(res, time) for res, time in contour.iteritems()]
            collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def a_star_search_default(autA, autB, resources, collA, collB, heurA, heurB, event_resource_map, puck_res):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = collections.defaultdict(lambda: 0)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = zerocontour
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
            heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
            collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def numpy_stack(c, a, w):
    early = numpy.amax(numpy.multiply(c, a))
    addarr = numpy.add(numpy.multiply(a, w), early)
    return numpy.maximum(c, addarr)

def numpy_stack_keep_early(c, a, w):
    early = numpy.amax(numpy.multiply(c, a))
    addarr = numpy.add(numpy.multiply(a, w), early)
    return numpy.maximum(c, addarr), early

def numpy_stack_drop(c, a, w):
    early = numpy.amax(numpy.multiply(c, a)) + w
    early = numpy.multiply(a, early)
    return numpy.maximum(c, early)

def numpy_rev_stack(c, a, w):
    late = numpy.amax(numpy.add(c, numpy.multiply(a, w)))
    return numpy.maximum(numpy.multiply(a, late), c)

def numpy_rev_stack_drop(c, a, w):
    late = numpy.amax(numpy.multiply(c, a)) + w
    return numpy.maximum(numpy.multiply(a, late), c)

def a_star_search_numpy(autA, autB, resources, collA, collB, heurA, heurB, numpy_array_map, puck_res):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    ha, hb = init()
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[autB.initial])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(len(resources))], numpy.int16)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    def heur(sa, sb):
        res, timen = ha[sa]
        heuristica = newcontour[res] + timen
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb)
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            #res, timen = ha[edge.succ]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[stateb]))
            #heuristic = max(heuristica, heuristicb)
            heuristic = heur(edge.succ, stateb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            #res, timen = ha[statea]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[edge.succ]))
            #heuristic = max(heuristica, heuristicb)
            heuristic = heur(statea, edge.succ)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        #contour = zerocontour
        collisions = {}
        heur = {}
        #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
        #state.heur = [(res, time) for res, time in contour.iteritems()]
        collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
        #heur[state] = [(res, time) for res, time in enumerate(contour)]
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
                #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour), collisions, None
    return createPath(statetuple)

def a_star_search_numpy_min_current(autA, autB, resources, collA, collB, heurA, heurB, numpy_array_map, puck_res):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    ha, hb = init()
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[autB.initial])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(len(resources))], numpy.int16)
    to_visit = {}
    to_visit[(maxval, maxvala)] = [(initial, zerocontour, None, 0, None)]
    heurvalue = {}
    infinity = float('inf')
    secondaryval = collections.defaultdict(lambda:(infinity, 0))
    k, j = maxval, maxvala
    secondaryval[maxval] = (maxvala, maxvala)
    def heur(sa, sb):
        res, timen = ha[sa]
        heuristica = newcontour[res] + timen
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb), heuristica
    while k <= maxval:
        if (k,j) not in to_visit or len(to_visit[(k,j)]) == 0:
            if (j >= secondaryval[k][1]):
                k += 1
                while k not in secondaryval and k <= maxval:
                    k += 1
                if k > maxval:
                    break
                j = secondaryval[k][0]
            else:
                j += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[(k,j)].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            #res, timen = ha[edge.succ]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[stateb]))
            #heuristic = max(heuristica, heuristicb)
            heuristic, heuristica = heur(edge.succ, stateb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if (heuristic, heuristica) not in to_visit:
                to_visit[(heuristic, heuristica)] = []
            minsec, maxsec = secondaryval[heuristic]
            minsec, maxsec = min(minsec, heuristica), max(maxsec, heuristica)
            secondaryval[heuristic] = (minsec, maxsec)
            to_visit[(heuristic, heuristica)].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            #res, timen = ha[statea]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[edge.succ]))
            #heuristic = max(heuristica, heuristicb)
            heuristic, heuristica = heur(statea, edge.succ)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if (heuristic, heuristica) not in to_visit:
                to_visit[(heuristic, heuristica)] = []
            minsec, maxsec = secondaryval[heuristic]
            minsec, maxsec = min(minsec, heuristica), max(maxsec, heuristica)
            secondaryval[heuristic] = (minsec, maxsec)
            to_visit[(heuristic, heuristica)].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        #contour = zerocontour
        collisions = {}
        heur = {}
        #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
        #state.heur = [(res, time) for res, time in contour.iteritems()]
        collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
        #heur[state] = [(res, time) for res, time in enumerate(contour)]
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
                #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour), collisions, None
    return createPath(statetuple)

def a_star_search_numpy_drop(autA, autB, resources, collA, collB, heurA, heurB, numpy_array_map, puck_res):
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    trace = []
    newcollb = {}
    newheurb = {}
    newcolla = {}
    for state in autA.get_states():
        collset = collA[state]
        assert len(collset) == 1
        newcolla[state] = next(iter(collset))
    collA = newcolla
    state = autB.initial
    newcollb[0] = collB[state]
    newheurb[0] = heurB[state]
    positions = collections.defaultdict(lambda: ([],[]))
    while not state.marked:
        edge = state.get_outgoing()[0]
        split = edge.label.name.split('-')
        trace.append(edge)
        prev, succ = int(split[1]), int(split[2])
        positions[prev][0].append(len(trace))
        positions[succ][1].append(len(trace))
        state = edge.succ
        newcollb[len(trace)] = collB[state]
        newheurb[len(trace)] = heurB[state]
    for key in positions:
        (arr1, arr2) = positions[key]
        positions[key] = (numpy.array(arr1), numpy.array(arr2))
    collB = newcollb
    heurB = newheurb
    ha, hb = init()
    initial = (autA.initial, 0)
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[0])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(len(resources))], numpy.int16)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    heurvalue = {}
    secondaryval = {}
    k, j = maxval, maxvala
    secondaryval[maxval] = (maxvala, maxvala)
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb == len(trace):
            break
        stateaposition = collA[statea]
        entercurrstate = positions[stateaposition][1]
        index = numpy.searchsorted(entercurrstate, stateb)
        executeupto = entercurrstate[index] if index < len(entercurrstate) else len(trace)
        stackcache = {}
        stackcache[stateb] = contour
        def findbstackcontour(stackto):
            for i in range(stateb, stackto):
                edge = trace[i]
                event = edge.label
                stackcache[i+1] = numpy_stack_drop(stackcache[i],numpy_array_map[event],edge.weight)
            return stackcache[stackto]
        def add_new_state(state, number, contour, edge = None, front = False):
            def heur(sa, sb):
                res, timen = ha[sa]
                heuristica = newcontour[res] + timen
                heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
                return max(heuristica, heuristicb)
            newtuple = (state, number)
            if (newtuple in look_back):
                return 0
            newcontour = findbstackcontour(number)
            if edge != None:
                newcontour = numpy_stack_drop(newcontour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(state, number)
            heurvalue[newtuple] = heuristic
            if heuristic not in to_visit or front:
                to_visit[heuristic] = []
            event, weight = (edge.label, edge.weight) if edge != None else (None, None)
            to_visit[heuristic].append((newtuple, newcontour, event, weight, statetuple))
            return heuristic
        if statea.marked and executeupto == len(trace):
            maxval = max(add_new_state(statea, executeupto, contour, front=True), maxval)
        else:
            for edge in statea.get_outgoing():
                posentered = collA[edge.succ]
                executeto = [ti for ti in positions[posentered][0] if ti > stateb and ti < executeupto]
                if posentered not in collB[stateb]:
                    executeto.append(stateb)
                for newstateb in executeto:
                    maxval = max(add_new_state(edge.succ, newstateb, contour, edge), maxval)
    if not statea.marked or not stateb == len(trace):
        #print 'k={}'.format(k)
        #    print '{}:{}'.format(key, len(to_visit[key]))
        return None, None, None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        #contour = zerocontour
        collisions = {}
        heur = {}
        #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
        #state.heur = [(res, time) for res, time in contour.iteritems()]
        collisions[state] = collB[statetuple[1]].union([collA[statetuple[0]]])
        #heur[state] = [(res, time) for res, time in enumerate(contour)]
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                if event != None:
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[statetuple[1]].union([collA[prevtuple[0]]])
                    state = prevstate
                for sb in range(statetuple[1]-1, prevtuple[1]-1, -1):
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, trace[sb].label, trace[sb].weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[sb].union([collA[prevtuple[0]]])
                    state = prevstate
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour), collisions, None
    return createPath(statetuple)

def a_star_search_numpy_drop_mincurrent(autA, autB, resources, collA, collB, heurA, heurB, numpy_array_map, puck_res):
    def numpy_drop_modify_orig(c, r, w):
        early = max([c[i] for i in r])
        for i in r:
            c[i] += w
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    trace = []
    def calculate_stacks(c, vals, start, end):
        contours = {}
        for i in range(start, end):
            edge = trace[i]
            #numpy_drop_modify_orig(c, event_res_map[edge.label], edge.weight)
            if i in vals:
                contour[i] = numpy.array(c)
        return contours
    newcollb = {}
    newheurb = {}
    newcolla = {}
    for state in autA.get_states():
        collset = collA[state]
        assert len(collset) == 1
        newcolla[state] = next(iter(collset))
    collA = newcolla
    state = autB.initial
    newcollb[0] = collB[state]
    newheurb[0] = heurB[state]
    positions = collections.defaultdict(lambda: ([],[]))
    while not state.marked:
        edge = state.get_outgoing()[0]
        split = edge.label.name.split('-')
        trace.append(edge)
        prev, succ = int(split[1]), int(split[2])
        positions[prev][0].append(len(trace))
        positions[succ][1].append(len(trace))
        state = edge.succ
        newcollb[len(trace)] = collB[state]
        newheurb[len(trace)] = heurB[state]
    for key in positions:
        (arr1, arr2) = positions[key]
        positions[key] = (numpy.array(arr1), numpy.array(arr2))
    collB = newcollb
    heurB = newheurb
    ha, hb = init()
    initial = (autA.initial, 0)
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[0])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(len(resources))], numpy.int16)
    to_visit = {}
    to_visit[(maxval, maxvala)] = [(initial, zerocontour, None, 0, None,0)]
    heurvalue = {}
    infinity = float('inf')
    secondaryval = collections.defaultdict(lambda:(infinity, 0))
    k, j = maxval, maxvala
    secondaryval[maxval] = (maxvala, maxvala)
    while k <= maxval:
        if (k,j) not in to_visit or len(to_visit[(k,j)]) == 0:
            if (j >= secondaryval[k][1]):
                k += 1
                while k not in secondaryval and k <= maxval:
                    k += 1
                if k > maxval:
                    break
                j = secondaryval[k][0]
            else:
                j += 1
            continue
        statetuple, contour, event, weight, previous,moves = to_visit[(k,j)].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb == len(trace):
            break
        stateaposition = collA[statea]
        entercurrstate = positions[stateaposition][1]
        index = numpy.searchsorted(entercurrstate, stateb)
        executeupto = entercurrstate[index] if index < len(entercurrstate) else len(trace)
        stackcache = {}
        stackcache[stateb] = contour
        stackedto = stateb
        def findbstackcontour(stackto):
            #print '{}-{}'.format(max(0,stackto-stackedto), stackto - stateb)
            #print '{}-{}-{}'.format(stateb,stackedto,stackto)
            for i in range(stackedto, stackto):
                edge = trace[i]
                event = edge.label
                stackcache[i+1] = numpy_stack_drop(stackcache[i],numpy_array_map[event],edge.weight)
            return stackcache[stackto]
        def add_new_state(state, number, edge = None, front = False):
            def heur(c, sa, sb):
                res, timen = ha[sa]
                heuristica = c[res] + timen
                heuristicb = numpy.amax(numpy.add(c, hb[sb]))
                return max(heuristica, heuristicb), heuristica #newmoves + timen
            newtuple = (state, number)
            if (newtuple in look_back):
                return -1
            newcontour = findbstackcontour(number)
            if edge != None:
                newcontour = numpy_stack_drop(newcontour, numpy_array_map[edge.label], edge.weight)
                newmoves = moves + 1
            else:
                newmoves = moves
            heuristic, heuristica = heur(c, state, number)
            heurvalue[newtuple] = heuristic
            if (heuristic, heuristica) not in to_visit or front:
                to_visit[(heuristic, heuristica)] = []
            event, weight = (edge.label, edge.weight) if edge != None else (None, None)
            to_visit[(heuristic, heuristica)].append((newtuple, newcontour, event, weight, statetuple, newmoves))
            minsec, maxsec = secondaryval[heuristic]
            oms = minsec
            minsec, maxsec = min(minsec, heuristica), max(maxsec, heuristica)
            secondaryval[heuristic] = (minsec, maxsec)
            assert(heuristic >= k)
            assert(heuristic > k or oms >= j)
            return heuristic
        if statea.marked and executeupto == len(trace):
            maxval = max(add_new_state(statea, executeupto, front=True), maxval)
        else:
            for edge in statea.get_outgoing():
                posentered = collA[edge.succ]
                executeto = [ti for ti in positions[posentered][0] if ti > stateb and ti < executeupto]
                if posentered not in collB[stateb]:
                    executeto.append(stateb)
                for newstateb in executeto:
                    heur = add_new_state(edge.succ, newstateb, edge)
                    maxval = max(heur, maxval)
                    if heur != -1:
                        stackedto = max(stackedto, newstateb)
    if not statea.marked or not stateb == len(trace):
        #print 'k={}'.format(k)
        #    print '{}:{}'.format(key, len(to_visit[key]))
        tot = 0
        for key in to_visit:
            #print '{},{}'.format(key, len(to_visit[key]))
            tot += len(to_visit[key])
        assert(tot == 0)
        return None, None, None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        #contour = zerocontour
        collisions = {}
        heur = {}
        #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
        #state.heur = [(res, time) for res, time in contour.iteritems()]
        collisions[state] = collB[statetuple[1]].union([collA[statetuple[0]]])
        #heur[state] = [(res, time) for res, time in enumerate(contour)]
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                if event != None:
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[statetuple[1]].union([collA[prevtuple[0]]])
                    state = prevstate
                for sb in range(statetuple[1]-1, prevtuple[1]-1, -1):
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, trace[sb].label, trace[sb].weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[sb].union([collA[prevtuple[0]]])
                    state = prevstate
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour), collisions, None
    return createPath(statetuple)

def a_star_search_numpy_drop_mincurrent_experiment(autA, autB, resources, collA, collB, heurA, heurB, numpy_array_map, puck_res):
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    trace = []
    newcollb = {}
    newheurb = {}
    newcolla = {}
    for state in autA.get_states():
        collset = collA[state]
        assert len(collset) == 1
        newcolla[state] = next(iter(collset))
    collA = newcolla
    state = autB.initial
    newcollb[0] = collB[state]
    newheurb[0] = heurB[state]
    positions = collections.defaultdict(lambda: ([],[]))
    while not state.marked:
        edge = state.get_outgoing()[0]
        split = edge.label.name.split('-')
        trace.append(edge)
        prev, succ = int(split[1]), int(split[2])
        positions[prev][0].append(len(trace))
        positions[succ][1].append(len(trace))
        state = edge.succ
        newcollb[len(trace)] = collB[state]
        newheurb[len(trace)] = heurB[state]
    for key in positions:
        (arr1, arr2) = positions[key]
        positions[key] = (numpy.array(arr1), numpy.array(arr2))
    collB = newcollb
    heurB = newheurb
    ha, hb = init()
    initial = (autA.initial, 0)
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[0])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(len(resources))], numpy.int16)
    to_visit = {}
    to_visit[(maxval, maxvala)] = [(initial, zerocontour, None, 0, None, 0, None)]
    heurvalue = {}
    infinity = float('inf')
    secondaryval = collections.defaultdict(lambda:(infinity, 0))
    k, j = maxval, maxvala
    secondaryval[maxval] = (maxvala, maxvala)
    while k <= maxval:
        if (k,j) not in to_visit or len(to_visit[(k,j)]) == 0:
            if (j >= secondaryval[k][1]):
                k += 1
                while k not in secondaryval and k <= maxval:
                    k += 1
                if k > maxval:
                    break
                j = secondaryval[k][0]
            else:
                j += 1
            continue
        statetuple, contour, event, weight, previous,moves,stackstuff = to_visit[(k,j)].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb == len(trace):
            break
        #for i in range(stateb+1, executeupto):
        #    if (statea, i) in look_back:
        #        executeupto = i+1
        #        break
        #if tried:
        #    continue
        if stackstuff != None:
            pushto, index, stack, orstatetuple = stackstuff
            atuple = None
            #if pushto[index] < executeupto:
            if index + 1 < len(pushto):
                atuple = pushto, index + 1
            heur, heura = add_new_state(statea, pushto[index], stack, orstatetuple, (event, weight), nextones=atuple)
            if (heur < k):
                print '{}-{}-{}-{}'.format(k,j, heur, heura)
                k = min(heur, k)
                j = min(heura, j)
            if (heur == k and heura < j):
                print '{}-{}-{}-{}'.format(k,j, heur, heura)
                j = min(heura, j)
            maxval = max(heur, maxval)
        stateaposition = collA[statea]
        entercurrstate = positions[stateaposition][1]
        index = numpy.searchsorted(entercurrstate, stateb)
        executeupto = entercurrstate[index] if index < len(entercurrstate) else len(trace)
        stack = [{}, stateb]
        stack[0][stateb] = contour
        #stackcache[stateb] = contour
        #stackedto = stateb
        def findbstackcontour(stackcache, stackto):
            #print '{}-{}'.format(max(0,stackto-stackedto), stackto - stateb)
            #print '{}-{}-{}'.format(stateb,stackedto,stackto)
            for i in range(stackcache[1], stackto):
                edge = trace[i]
                event = edge.label
                stackcache[0][i+1] = numpy_stack_drop(stackcache[0][i],numpy_array_map[event],edge.weight)
            stackcache[1] = max(stackto, stackcache[1])
            return stackcache[0][stackto]
        def add_new_state(state, number, stack, statetuple, edge = None, front = False, nextones = None):
            def heur(sa, sb):
                res, timen = ha[sa]
                heuristica = newcontour[res] + timen
                heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
                return max(heuristica, heuristicb), heuristica #newmoves + timen
            newtuple = (state, number)
            if (newtuple in look_back):
                return k,j
            newcontour = findbstackcontour(stack, number)
            if edge != None:
                event, weight = edge
                newcontour = numpy_stack_drop(newcontour, numpy_array_map[event], weight)
                newmoves = moves + 1
            else:
                event, weight = None, None
                newmoves = moves
            heuristic, heuristica = heur(state, number)
            heurvalue[newtuple] = heuristic
            if (heuristic, heuristica) not in to_visit or front:
                to_visit[(heuristic, heuristica)] = []
            newstackstuff = None
            if nextones != None:
                pushto, index = nextones
                newstackstuff = (pushto, index, stack, statetuple)
            to_visit[(heuristic, heuristica)].append((newtuple, newcontour, event, weight, statetuple, newmoves, newstackstuff))
            minsec, maxsec = secondaryval[heuristic]
#            oms = minsec
            minsec, maxsec = min(minsec, heuristica), max(maxsec, heuristica)
            secondaryval[heuristic] = (minsec, maxsec)
            return heuristic, heuristica
        if statea.marked and executeupto == len(trace):
            heur, heura = add_new_state(statea, executeupto, stack, statetuple, front=True)
            if (heur < k):
                print '{}-{}-{}-{}'.format(k,j, heur, heura)
                k = min(heur, k)
                j = min(heura, j)
            if (heur == k and heura < j):
                print '{}-{}-{}-{}'.format(k,j, heur, heura)
                j = min(heura, j)
            maxval = max(heur, maxval)
        else:
            for edge in statea.get_outgoing():
                posentered = collA[edge.succ]
                executeto = [ti for ti in positions[posentered][0] if ti > stateb and ti < executeupto]
                if posentered not in collB[stateb]:
                    executeto = [stateb] + executeto
                atuple = None
                if len(executeto) > 1:
                    atuple = executeto, 1
                elif len(executeto) == 0:
                    continue
                heur, heura = add_new_state(edge.succ, executeto[0], stack, statetuple, (edge.label, edge.weight), nextones=atuple)
                if (heur < k):
                    print '{}-{}-{}-{}'.format(k,j, heur, heura)
                    k = min(heur, k)
                    j = min(heura, j)
                if (heur == k and heura < j):
                    print '{}-{}-{}-{}'.format(k,j, heur, heura)
                    j = min(heura, j)
                #assert(heuristic > k or heuristica >= j)
                maxval = max(heur, maxval)
    if not statea.marked or not stateb == len(trace):
        #print 'k={}'.format(k)
        #    print '{}:{}'.format(key, len(to_visit[key]))
        tot = 0
        for key in to_visit:
            #print '{},{}'.format(key, len(to_visit[key]))
            tot += len(to_visit[key])
        #assert(tot == 0)
        return None, None, None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        #contour = zerocontour
        collisions = {}
        heur = {}
        #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
        #state.heur = [(res, time) for res, time in contour.iteritems()]
        collisions[state] = collB[statetuple[1]].union([collA[statetuple[0]]])
        #heur[state] = [(res, time) for res, time in enumerate(contour)]
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                if event != None:
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[statetuple[1]].union([collA[prevtuple[0]]])
                    state = prevstate
                for sb in range(statetuple[1]-1, prevtuple[1]-1, -1):
                    prevstate = path.add_new_state(False)
                    edge = weighted_structure.WeightedEdge(prevstate, state, trace[sb].label, trace[sb].weight)
                    path.add_edge(edge)
                    #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
                    #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
                    collisions[prevstate] = collB[sb].union([collA[prevtuple[0]]])
                    state = prevstate
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour), collisions, None
    return createPath(statetuple)

def a_star_search_default_wafer(autA, autB, resources, collA, collB, heurA, heurB, event_resource_map, puck_res):
    initial = (autA.initial, autB.initial)
    alphabet = autA.alphabet.union(autB.alphabet)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = collections.defaultdict(lambda: 0)
    to_visit = {}
    least_wafer = min([int(event.name.split('-')[0][1:]) for event in alphabet])
    to_visit[maxval] = [(initial, zerocontour, None, 0, None, least_wafer-1)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous, wafer_started = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            split = edge.label.name.split('-')
            if split[1] == 'start':
                wafer_number = int(split[0][1:])
                if new_wafer == None or new_wafer + 1 == wafer_number:
                    new_wafer = wafer_number
                else:
                    continue
            else:
                new_wafer = wafer_started
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, new_wafer))
        for edge in stateb.get_outgoing():
            split = edge.label.name.split('-')
            if split[1] == 'start':
                wafer_number = int(split[0][1:])
                if new_wafer == None or new_wafer + 1 == wafer_number:
                    new_wafer = wafer_number
                else:
                    continue
            else:
                new_wafer = wafer_started
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, new_wafer))
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(alphabet, autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = zerocontour
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
            heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
            collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def a_star_search_default_min_current(autA, autB, resources, collA, collB, heurA, heurB, event_resource_map, puck_res):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = collections.defaultdict(lambda: 0)
    to_visit = {}
    count = 1
    to_visit[maxval] = [(0, 0, initial, zerocontour, None, 0, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        asteps,_, statetuple, contour, event, weight, previous = heapq.heappop(to_visit[k])
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            heapq.heappush(to_visit[heuristic], (asteps + edge.weight, -count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            heapq.heappush(to_visit[heuristic], (heuristica, -count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = zerocontour
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    #heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            #contour = progressivetimeoptimalsynthesis.rev_res_plus_default(contour, edge, event_resource_map[edge.label])
            #heur[prevstate] = [(res, time) for res, time in contour.iteritems() if res in puck_res]
            #collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def greedy_search(autA, autB, resources, collA, collB, heurA, heurB, state_resources = []):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    count = 1
    zerocontour = {}
    for res in resources:
        zerocontour[res] = 0
    for res in state_resources:
        zerocontour[res] = 0
    to_visit = [(maxval,0,initial, zerocontour, None, 0, None)]
    while len(to_visit) != 0:
        _, _, statetuple, contour, event, weight, previous = heapq.heappop(to_visit)
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res]*.75 + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res]*.75 + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            heapq.heappush(to_visit, (heuristic, count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res]*.75 + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res]*.75 + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            heapq.heappush(to_visit, (heuristic, count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = zerocontour
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            if (state_resources == []):
                contour = progressivetimeoptimalsynthesis.rev_res_plus(contour, edge)
            else:
                contour = progressivetimeoptimalsynthesis.rev_res_plus_drop(contour, edge, state_resources)
            #prevstate.heur = [(res, time) for res, time in contour.iteritems()]
            #prevstate.collisions = prevtuple[0].collisions.union(prevtuple[1].collisions)
            heur[prevstate] = [(res, time) for res, time in contour.iteritems()]
            collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def a_star_search_min_current(autA, autB, resources, collA, collB, heurA, heurB, state_resources = []):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = {}
    for res in resources:
        zerocontour[res] = 0
    for res in state_resources:
        zerocontour[res] = 0
    to_visit = {}
    count = 1
    to_visit[maxval] = [(maxvala, 0, initial, zerocontour, None, 0, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    while k <= maxval:
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        _,_, statetuple, contour, event, weight, previous = heapq.heappop(to_visit[k])
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if len(collA[edge.succ].intersection(collB[stateb])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[edge.succ]] + [0])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[stateb]] + [0])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            #to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
            heapq.heappush(to_visit[heuristic], (heuristica, -count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if len(collB[edge.succ].intersection(collA[statea])) != 0:
                continue
            if (state_resources == []):
                newcontour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            else:
                newcontour = progressivetimeoptimalsynthesis.res_plus_drop(contour, edge, state_resources)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            heuristica = max([newcontour[res] + timeneeded for res, timeneeded in heurA[statea]])
            heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in heurB[edge.succ]])
            heuristic = max(heuristica, heuristicb)
            if heuristic >= heurvalue.get(newtuple, infinity):
                continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            #to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
            heapq.heappush(to_visit[heuristic], (heuristica, -count, newtuple, newcontour, edge.label, edge.weight, statetuple))
            count += 1
    if not statea.marked or not stateb.marked:
        return None, None, None, None
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    prevstate = None
    state = path.add_new_state(True)
    contour = zerocontour
    collisions = {}
    heur = {}
    #state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    #state.heur = [(res, time) for res, time in contour.iteritems()]
    collisions[state] = collA[statetuple[0]].union(collB[statetuple[1]])
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while statetuple != None:
        event, weight, prevtuple = look_back[statetuple]
        if (prevtuple != None):
            prevstate = path.add_new_state(False)
            edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
            path.add_edge(edge)
            if (state_resources == []):
                contour = progressivetimeoptimalsynthesis.rev_res_plus(contour, edge)
            else:
                contour = progressivetimeoptimalsynthesis.rev_res_plus_drop(contour, edge, state_resources)
            #prevstate.heur = [(res, time) for res, time in contour.iteritems()]
            #prevstate.collisions = prevtuple[0].collisions.union(prevtuple[1].collisions)
            heur[prevstate] = [(res, time) for res, time in contour.iteritems()]
            collisions[prevstate] = collA[prevtuple[0]].union(collB[prevtuple[1]])
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour), collisions, heur

def mark_aut_reverse_djikstra(aut):
    to_visit = {}
    to_visit[0] = list(filter(lambda state: state.marked, aut.get_states()))
    k = 0
    maxval = 0
    heur = {}
    while k <= maxval:
        if (k not in to_visit or len(to_visit[k]) == 0):
            k += 1
            continue
        state = to_visit[k].pop()
        #if hasattr(state, 'heur'):
        if state in heur:
            continue
        #state.heur = [(frozenset(aut.alphabet), k)]
        heur[state] = [(frozenset(aut.alphabet), k)]
        for edge in state.get_incoming():
            #if hasattr(edge.pred, 'heur'):
            if edge.pred in heur:
                continue
            dist = k + edge.weight
            if dist not in  to_visit:
                to_visit[dist] = []
                maxval = max(maxval, dist)
            to_visit[dist].append(edge.pred)
    return heur

def mark_aut_reverse_djikstra_default(aut, res):
    to_visit = {}
    to_visit[0] = list(filter(lambda state: state.marked, aut.get_states()))
    k = 0
    maxval = 0
    heur = {}
    while k <= maxval:
        if (k not in to_visit or len(to_visit[k]) == 0):
            k += 1
            continue
        state = to_visit[k].pop()
        #if hasattr(state, 'heur'):
        if state in heur:
            continue
        #state.heur = [(frozenset(aut.alphabet), k)]
        heur[state] = [(res, k)]
        for edge in state.get_incoming():
            #if hasattr(edge.pred, 'heur'):
            if edge.pred in heur:
                continue
            dist = k + edge.weight
            if dist not in to_visit:
                to_visit[dist] = []
                maxval = max(maxval, dist)
            to_visit[dist].append(edge.pred)
    #state = aut.initial
    #while not state.marked:
    #    assert len(state.get_outgoing()) == 1
    #    edge = state.get_outgoing()[0]
    #    nextstate = edge.succ
    #    print "{}-{}-{}".format(heur[state][0][1], edge.weight, heur[nextstate][0][1])
    #    state = nextstate
    return heur

def make_resources_varied_width(index, coll, width):
    not_used = set([])
    mod = (width * 2)-1
    intersections = []
    for i in range(width):
        intersections.extend(range(i*mod,i*mod+ width))
    places = [0,-width+1,1,width]
    resources = []
    for i in intersections:
        resource = set()
        for puck in range(1, index + 1):
            for j in places:
                if i + j in not_used or i + j <= 0 or i + j > 40:
                    continue
                if j == 0 and i % mod == 0 or j == 1 and i % mod == width-1:
                    continue
                for k in places:
                    if j == k or i + k in not_used or i + k <= 0 or i + k > 40:
                        continue
                    if k == 0 and i % mod == 0 or k == 1 and i % mod == width-1:
                        continue
                    resource.add(coll.events["P" + str(puck) + "-" + str(i + j).zfill(2) + "-" + str(i + k).zfill(2)])
        #resource = set(map(lambda x: coll.events[x], resource))
        resources.append(resource)
    return resources

def make_epuck(index, initial, marked, blocked = [], not_intersection = []):
    not_used = set([35,36,39,40])
    blockedintersection = set()
    for intersection in not_intersection:
        x, y = (intersection -1)%5, (intersection -1)/5
        neighbours = [y * 9 + x, y * 9 + x + 1, y * 9 + x + 5, y * 9 + x - 4]
        for neig1 in neighbours:
            for neig2 in neighbours:
                blockedintersection.add((neig1, neig2))
    not_used.update(blocked)
    maps_to = {}
    maps_to[37] = 35
    maps_to[38] = 36
    string = "[weighted-automaton]\n"
    string += "states = " + ",".join(map(lambda x: str(x).zfill(2), range(1,35) + [37,38])) + "\n"
    puck = "P" + str(index)
    state_resources = {}
    destinations1 = [-5,-4,-1,1,4,5]
    destinations2 = [-5,-4,-9,9,4,5]
    def destinations(index):
        dests = []
        if (index-1) % 9 < 4:
            if index % 9 != 1:
                dests.append(-1)
            if index % 9 != 4:
                dests.append(1)
            dests += [-5,-4,4,5]
        else:
            dests += [-9, 9]
            if index % 9 != 5:
                dests += [-5,4]
            if index % 9 != 0:
                dests += [-4,5]
        return dests
    alphabet = []
    for i in range(1, 41):
        if i in not_used:
            continue
        place = str(i).zfill(2)
        state_resources[place] = []
        out_going = [puck + "-" + place + "-" + str(i + val).zfill(2) for val in destinations(i) if
                     (i + val > 0) and (i + val <= 40) and ((i+val) not in not_used) and (place, i+val) not in blockedintersection]
        alphabet += out_going
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(event):
        split = event.split('-')
        state_resources[split[1]].append(event)
        state_resources[split[2]].append(event)
        return "(" + split[1] + "," + split[2] + "," + event + ",1)"
    string += "transitions = " + ','.join(map(transition, alphabet)) + "\n"
    string += "initial-state = " + str(initial).zfill(2) + "\n"
    string += "marker-states = " + str(marked).zfill(2) + "\n"
    #state_resources = map(frozenset, list(state_resources.values()))
    return string, state_resources

def make_resources_indexs(indexs, coll):
    not_used = set([35,36,39,40])
    intersections = range(5) + range(9,14) + range(18, 23) + range(27, 32) + range(36, 39)
    places = [0,-4,1,5]
    resources = []
    for i in intersections:
        resource = set()
        for puck in indexs:
            for j in places:
                if i + j in not_used or i + j <= 0 or i + j > 40:
                    continue
                if j == 0 and i % 9 == 0 or j == 1 and i % 9 == 4:
                    continue
                for k in places:
                    if j == k or i + k in not_used or i + k <= 0 or i + k > 40:
                        continue
                    if k == 0 and i % 9 == 0 or k == 1 and i % 9 == 4:
                        continue
                    resource.add("P" + str(puck) + "-" + str(i + j).zfill(2) + "-" + str(i + k).zfill(2))
        resource = set(map(lambda x: coll.events[x], resource))
        resources.append(resource)
    return resources

def make_resources(index, coll):
    not_used = set([35,36,39,40])
    intersections = range(5) + range(9,14) + range(18, 23) + range(27, 32) + range(36, 39)
    places = [0,-4,1,5]
    resources = []
    for i in intersections:
        resource = set()
        for puck in range(1, index + 1):
            for j in places:
                if i + j in not_used or i + j <= 0 or i + j > 40:
                    continue
                if j == 0 and i % 9 == 0 or j == 1 and i % 9 == 4:
                    continue
                for k in places:
                    if j == k or i + k in not_used or i + k <= 0 or i + k > 40:
                        continue
                    if k == 0 and i % 9 == 0 or k == 1 and i % 9 == 4:
                        continue
                    resource.add("P" + str(puck) + "-" + str(i + j).zfill(2) + "-" + str(i + k).zfill(2))
        resource = set(map(lambda x: coll.events[x], resource))
        resources.append(resource)
    return resources

def make_epucks_indexed(startstop, blocked = [], notintersection = []):
    startplaces = range(1, 35) + [37,38]
    endplaces = range(1, 35) + [37,38]
    names = []
    state_resources = []
    for (i, initial, marked) in startstop:
        handle = file("SimonEpuck" + str(i) + ".cfg", 'w')
        names.append("SimonEpuck" + str(i) + ".cfg")
        aut, resources = make_epuck(i, initial, marked, blocked, notintersection)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_resources

def make_epucks(number, startstop = None):
    startplaces = range(1, 35) + [37,38]
    endplaces = range(1, 35) + [37,38]
    names = []
    state_resources = []
    for i in range(1, number + 1):
        handle = file("SimonEpuck" + str(i) + ".cfg", 'w')
        names.append("SimonEpuck" + str(i) + ".cfg")
        if startstop == None:
            initial = startplaces.pop(random.randrange(len(startplaces)))
            marked =  endplaces.pop(random.randrange(len(endplaces)))
        else:
            initial, marked = startstop[i-1]
        aut, resources = make_epuck(i, initial, marked)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_resources

def make_epucks_width(number, startstop = None, width = 5):
    total = ((width * 2)-1) * (width-1) + width-1
    startplaces = range(1, total+1)
    endplaces = range(1, total+1)
    names = []
    state_resources = []
    for i in range(1, number + 1):
        handle = file("SimonEpuck" + str(i) + ".cfg", 'w')
        names.append("SimonEpuck" + str(i) + ".cfg")
        if startstop == None:
            initial = startplaces.pop(random.randrange(len(startplaces)))
            marked =  endplaces.pop(random.randrange(len(endplaces)))
        else:
            initial, marked = startstop[i-1]
        aut, resources = make_epuck_varied_width(i, initial, marked, width)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_resources


def incrementally_improve_greedy(trace, auts, resources):
    eou

def construct_resource_automaton(resource, eventweight, coll, tick):
    aut = data_structure.Automaton(resource.union([tick], coll))
    max_weight = max(map(lambda x: eventweight[x], resource))
    states = [aut.add_new_state(i == 0) for i in range(max_weight+1)]
    for i in range(max_weight):
        aut.add_edge_data(states[i+1], states[i], tick)
    for event in resource:
        aut.add_edge_data(states[0], states[eventweight[event]], event)
    return aut

def incrementally_improve_tick_unfinished(trace, auts, resources):
    eventweight = {}
    for aut in auts:
        for state in aut.get_states():
            for edge in state.get_outgoing():
                eventweight[edge.label] = edge.weight
    if 'tick' not in auts[0].collection.events:
        aut[0].collection.make_event('tick', False, True, False)
    tick = aut[0].collection.events['tick']
    resource_automata = {}
    for resource in resources:
        resource_automata[resource] = construct_resource_automaton(resource, eventweight, aut[0].collection, tick)

def compress_path(trace, resources, state_resources):
    zerocontour = {}
    for res in resources:
        zerocontour[res] = 0
    dependant_events = {}
    for edge in trace:
        if edge.label not in dependant_events:
            deps = set()
            for res in resources:
                if edge.label in res:
                    deps.update(res)
            for res in state_resources:
                if edge.label in res:
                    deps.update(res)
            dependant_events[edge.label] = deps
    contours = [zerocontour]
    for i in range(len(trace)):
        j = i -1
        event = trace[i].label
        dependants = dependant_events[trace[i].label]
        contours.append(progressivetimeoptimalsynthesis.res_plus(contours[i], trace[i]))
        swapwith = None
        while j >= 0:
            swapevent = trace[j].label
            if swapevent in dependants:
                break
            if progressivetimeoptimalsynthesis.earliest_fire(contours[j], event) \
                < progressivetimeoptimalsynthesis.earliest_fire(contours[j], swapevent):
                swapwith = j
            j -= 1
        if swapwith != None:
            insert = trace[i]
            for j in range(swapwith, i + 1):
                temp = trace[j]
                trace[j] = insert
                insert = temp
                contours[j+1] = progressivetimeoptimalsynthesis.res_plus(contours[j], trace[j])
    print "weight: " + str(progressivetimeoptimalsynthesis.ceil(contours[-1]))
    return trace, progressivetimeoptimalsynthesis.ceil(contours[-1])

def compress_path_default(trace, resources, state_resources, event_resource_map):
    zerocontour = {}
    for res in resources:
        zerocontour[res] = 0
    dependant_events = {}
    for edge in trace:
        if edge.label not in dependant_events:
            deps = set()
            for res in resources:
                if edge.label in res:
                    deps.update(res)
            for res in state_resources:
                if edge.label in res:
                    deps.update(res)
            dependant_events[edge.label] = deps
    contours = [collections.defaultdict(lambda : 0)]
    for i in range(len(trace)):
        j = i - 1
        event = trace[i].label
        dependants = dependant_events[trace[i].label]
        contours.append(progressivetimeoptimalsynthesis.res_plus_default(contours[i], trace[i], event_resource_map[event]))
        swapwith = None
        while j >= 0:
            swapevent = trace[j].label
            if swapevent in dependants:
                break
            if progressivetimeoptimalsynthesis.earliest_fire_default(contours[j], event, event_resource_map[event]) \
                < progressivetimeoptimalsynthesis.earliest_fire_default(contours[j], swapevent, event_resource_map[swapevent]):
                swapwith = j
            j -= 1
        if swapwith != None:
            insert = trace[i]
            for j in range(swapwith, i + 1):
                temp = trace[j]
                trace[j] = insert
                insert = temp
                contours[j+1] = progressivetimeoptimalsynthesis.res_plus_default(contours[j], trace[j],
                                                                                 event_resource_map[trace[j].label])
    #print "weight: " + str(progressivetimeoptimalsynthesis.ceil(contours[-1]))
    return trace, progressivetimeoptimalsynthesis.ceil(contours[-1])

def compress_path_better(trace, event_resource_map, event_state_resource_map, drop_resource_usage = collections.defaultdict(lambda : 0)):
    contour = drop_resource_usage.copy()
    buckets = collections.defaultdict(list)
    for edge in trace:
        #print '{}-{}'.format(edge.label.name, contour)
        #print '{}-{}'.format(edge.label.name, event_state_resource_map[edge.label])
        earliestfire = max([contour[index] for index in event_resource_map[edge.label]])
        earliestfire = max([earliestfire] + [contour[index] for index in event_state_resource_map[edge.label]])
        buckets[earliestfire].append(edge)
        for index in event_state_resource_map[edge.label]:
            contour[index] = earliestfire
        for index in event_resource_map[edge.label]:
            contour[index] = earliestfire + edge.weight
    newtrace = []
    keys = sorted(buckets.keys())
    for key in keys:
        for edge in buckets[key]:
            newtrace.append(edge)
    return newtrace, progressivetimeoptimalsynthesis.ceil(contour)

#def compress_path_better_numpy(trace, numpy_complex_map, num_resources):
#    contour = numpy.array([0 for i in range(num_resources)])
#    buckets = {}
#    for edge in trace:
#        n1, n2 = numpy_complex_map[edge.event]
#        earlyfire = numpy
#        earliestfire = max([contour[index] for index in event_resource_map[edge.label]])
#        earliestfire = max([earliestfire] + [contour[index] for index in event_state_resource_map[edge.label]])
#        if (earliestfire not in buckets):
#            buckets[earliestfire] = []
#        buckets[earliestfire].append(edge)
#        for index in event_state_resource_map[edge.label]:
#            contour[index] = earliestfire
#        for index in event_resource_map[edge.label]:
#            contour[index] = earliestfire + edge.weight
#    newtrace = []
#    keys = sorted(buckets.keys())
#    for key in keys:
#        for edge in buckets[key]:
#            newtrace.append(edge)
#    return newtrace, progressivetimeoptimalsynthesis.ceil(contour)

def make_cluster_wafer(index, numclusters):
    string = "[weighted-automaton]\n"
    clusters = [[str(i) + '1', str(i) + '3', str(i) + '2'] for i in range(1, numclusters+1)]
    state_resources = {}
    for cluster in clusters:
        for cl in cluster:
            state_resources[cl] = []
    state_resources[''] = []
    wafer = 'W' + str(index)
    state = 'start_'
    states = [state]
    transitions = []
    cluster = 0
    count = 1
    robot_resource = [[] for i in range(numclusters)]
    while cluster != -1:
        if len(clusters[cluster]) == 0:
            cluster -= 1
            if cluster == -1:
                continue
            chamber = str(cluster+1) + '3'
            newstate = str(count) + '_' + chamber
            states.append(newstate)
            transition = wafer + '-' + state + '-' + newstate
            transitions.append((transition, 2))
            robot_resource[cluster+1].append(transition)
            state = newstate
            count += 1
            continue
        chamber = clusters[cluster].pop(0)
        newstate = str(count) + '_' + chamber
        states.append(newstate)
        transition = wafer + '-' + state + '-' + newstate
        transitions.append((transition, 2))
        robot_resource[cluster].append(transition)
        state = newstate
        count += 1
        if (chamber.endswith('3') and cluster + 1 < numclusters):
            cluster += 1
        else:
            newstate = str(count) + '_' + chamber
            states.append(newstate)
            transition = wafer + '-' + state + '-' + newstate
            transitions.append((transition, 4))
            count += 1
            state = newstate
    newstate = 'end_'
    states.append(newstate)
    transition = wafer + '-' + state + '-' + newstate
    transitions.append((transition, 2))
    robot_resource[0].append(transition)
    #if index != 1:
    #    states.append('prestart_')
    #    transitions.append(('W' + str(index-1) + '-start_-1_11', 2))
    string += "states = " + ",".join(states) + "\n"
    alphabet = [tup[0] for tup in transitions]
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(tup):
        event = tup[0]
        weight = str(tup[1])
        split = event.split('-')
        print split[1]
        print split[1].split('_')[1]
        state_resources[split[1].split('_')[1]].append(event)
        state_resources[split[2].split('_')[1]].append(event)
        if split[0] == 'W' + str(index):
            return "(" + split[1] + "," + split[2] + "," + event + "," + weight + ")"
        else:
            return "(prestart_,start_," + event + ",2)"
    string += "transitions = " + ','.join(map(transition, transitions)) + "\n"
    if True:# index == 1:
        string += "initial-state = start_\n"
    else:
        string += "initial-state = prestart_\n"
    string += "marker-states = end_\n"
    state_resources.pop('')
    return string, robot_resource, state_resources

def make_cluster_wafers(number, clusters):
    names = []
    robot_resources = []
    state_resources = []
    for i in range(1, number + 1):
        handle = file("Wafer" + str(i) + ".cfg", 'w')
        names.append("Wafer" + str(i) + ".cfg")
        aut, robot_cluster, resources = make_cluster_wafer(i, clusters)
        robot_resources.append(robot_cluster)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_robot = [[] for i in range(clusters)]
    for robot_cluster in robot_resources:
        for i, robot in enumerate(robot_cluster):
            list_robot[i].extend(robot)
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_robot, list_resources

def create_run_wafer(index, clusters):
    names, robot_resources, state_resources = make_cluster_wafers(index, clusters)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts]
    robot_resources = map(lambda list: map(auts[0].collection.events.get, list), robot_resources)
    resources.extend(robot_resources)
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    resources = map(frozenset, resources)
    alphabet = set()
    for aut in auts:
        alphabet.update(aut.alphabet)
    resource_int_map = {}
    for i, res in enumerate(resources):
        resource_int_map[res] = i
    event_resource_map = {}
    for event in alphabet:
        event_resource_map[event] = [resource_int_map[res] for res in resources if event in res]
    epuck_res = [resource_int_map[frozenset(aut.alphabet)] for aut in auts]
    int_resources = set(resource_int_map.values())
    make_path_wafer_default(auts, resources, state_resources, event_resource_map, epuck_res,
                            int_resources, resource_int_map)


def reverse_stack_path(path, resources):
    contour = {}
    for res in resources:
        contour[res] = 0
    for state in path.get_states():
        if state.marked:
            break
    heur = {}
    heur[state] = [(res, time) for res, time in contour.iteritems()]
    while state != path.initial:
        edge = state.get_incoming()[0]
        state = edge.pred
        contour = progressivetimeoptimalsynthesis.rev_res_plus(contour, edge)
        heur[state] = [(res, time) for res, time in contour.iteritems()]
    return heur

def set_collision_states_wafer(aut):
    collisions = {}
    notfirst = False
    for state in aut.get_states():
        if state.marked or aut.initial == state:
            collisions[state] = set()
        for edge in state.get_incoming():
            if not edge.label.name.startswith('W1'):
                notfirst = True
            split = edge.label.name.split('-')
            statecol = split[2].split('_')[1]
            if statecol != '':
                collisions[state] = set([statecol])
    edge = aut.initial.get_outgoing()[0]
    #if notfirst:
    #    collisions[edge.succ] = set()
    return collisions

def make_path_wafer(auts, resources, state_resources):
    handle = file('resultsepuck', 'w')
    for arbitrary in [1]:
        autweights = []
        dur = -time.time()
        state_resources = set(state_resources)
        for aut in auts:
            collisions = set_collision_states_wafer(aut)
            heur = reverse_stack_path(aut, resources)
            #autweights.append((aut, aut.initial.heur[0][1]))
            autweights.append((aut, 0, collisions, heur))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
        path.initial = path.add_new_state(True)
        pathcoll = {}
        pathheur = {}
        pathcoll[path.initial] = []
        pathheur[path.initial] = []
        #path.initial.collisions = []
        #path.initial.heur = []
        for (i, (aut,_,collA,heurA)) in enumerate(autweights):
            path, weight, pathcoll, pathheur = a_star_search_min_current(aut, path, resources, collA, pathcoll, heurA, pathheur)
            if path == None:
                break
            #product = progressivetimeoptimalsynthesis.synchronousproduct_weighted_epucks([aut, path], 0)
            #product, weight = progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([product],
            #                                                                                        frozenset(product.alphabet), resources)
            #product, weight = progressivetimeoptimalsynthesis.make_greedy_prog_supervisor_all_controllable_epuck(product,
            #                                                                                               frozenset(product.alphabet), resources)
            #print "weight: " + str(weight)
            #product.save_as_dot("product.dot")
            #path = tau_abstraction.restrictpath(product)
            #print "restricted"
        dur += time.time()
        handle.write("took: " + str(dur) + "\n")
        print "took: " + str(dur)
        state = path.initial
        for _, weight,_,_ in autweights:
            handle.write("autweight: " + str(weight) + "\n")
            print "autweight: " + str(weight)
        events = []
        contour = progressivetimeoptimalsynthesis.frozendict()
        for r in resources:
            contour[r] = 0
        trace = []
        while not state.marked:
            edge = state.get_outgoing()[0]
            trace.append(state.get_outgoing()[0])
            contour = progressivetimeoptimalsynthesis.res_plus(contour, edge)
            split = edge.label.name.split("-")
            def replace3738(string):
                if string == '37':
                    return '35'
                if string == '38':
                    return '36'
                return string
            name = '-'.join(map(replace3738, split))
            print name
            handle.write(name + '\n')
            events.append(name)
            state = edge.succ
        handle.write("path weight:" + str(progressivetimeoptimalsynthesis.ceil(contour)) + "\n")
        print "path weight:" + str(progressivetimeoptimalsynthesis.ceil(contour))
        for aut in auts:
            for state in aut.get_states():
                if state.marked:
                    markedstate = state
                    continue
            print aut.state_names[aut.initial.number] + "->" + aut.state_names[markedstate.number]
            handle.write(aut.state_names[aut.initial.number] + "->" + aut.state_names[markedstate.number] + "\n")
        trace, weight = compress_path(trace, resources, state_resources)
        handle.write("compress weight:" + str(weight))
        events = map(lambda edge: edge.label.name, trace)
        print 'la la la'
    return events

def make_path_wafer_default(auts, resources, state_resources, event_resource_map, puck_res, int_resources, resource_to_int):
    handle = file('resultsepuck', 'w')
    for arbitrary in [1]:
        autweights = []
        dur = -time.clock()
        state_resources = set(state_resources)
        for aut in auts:
            collisions = set_collision_states_wafer(aut)
            heur = mark_aut_reverse_djikstra_default(aut, resource_to_int[frozenset(aut.alphabet)])
            #autweights.append((aut, aut.initial.heur[0][1]))
            autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        autweights.sort(key= lambda x: x[1])
        autweights.reverse()
        lbe = autweights[0][1]
        numepucks = len(autweights)
        size = auts[0].get_num_states()
        #path.initial.collisions = []
        #path.initial.heur = []
        bestorigweight = float('inf')
        bestcompressweight = float('inf')
        comptime = 0
        for trie in range(attempts):
            path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
            path.initial = path.add_new_state(True)
            pathcoll = {}
            pathheur = {}
            pathcoll[path.initial] = []
            pathheur[path.initial] = []
            if trie == 1:
                autweights.reverse()
            elif trie > 1:
                random.shuffle(autweights)
            for (i, (aut,aw,collA,heurA)) in enumerate(autweights):
                path, weight, pathcoll, pathheur = a_star_search_default_wafer(aut, path, int_resources, collA,
                                                                         pathcoll, heurA, pathheur,
                                                                         event_resource_map, puck_res)
                if path == None:
                    break
                for state in path.get_states():
                    if state.marked:
                        fin_state = state
                        break
                fin_coll = pathcoll[fin_state]
                trace = []
                state = path.initial
                while not state.marked:
                    edge = state.get_outgoing()[0]
                    trace.append(edge)
                    state = edge.succ
                comptime -= time.clock()
                trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
                comptime += time.clock()
                path, pathheur, pathcoll = trace_to_path_wafer(trace, path.alphabet, path.collection,
                                                         event_resource_map, fin_coll, puck_res)
                #product = progressivetimeoptimalsynthesis.synchronousproduct_weighted_epucks([aut, path], 0)
                #product, weight = progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([product],
                #                                                                                        frozenset(product.alphabet), resources)
                #product, weight = progressivetimeoptimalsynthesis.make_greedy_prog_supervisor_all_controllable_epuck(product,
                #                                                                                               frozenset(product.alphabet), resources)
                #print "weight: " + str(weight)
                #product.save_as_dot("product.dot")
                #path = tau_abstraction.restrictpath(product)
                #print "restricted"
            if path == None:
                origweight = float('inf')
                compressweight = float('inf')
            else:
                origweight = weight
                #trace = []
                #state = path.initial
                #while not state.marked:
                #    edge = state.get_outgoing()[0]
                #    trace.append(edge)
                #    state = edge.succ
                #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
            bestorigweight = min(bestorigweight, origweight)
            bestcompressweight = min(bestcompressweight, compressweight)
            print "weight:{}".format(bestcompressweight)
            tim = dur + time.clock()
            resultsfiles[trie].write('epucks:{},size:{},lbe:{},weight:{},cweight:{},bweight:{},bcweight{},time:{},tncomp:{}\n'.format(
                numepucks, size, lbe, origweight, compressweight, bestorigweight, bestcompressweight, tim, comptime
            ))
            resultsfiles[trie].flush()

def make_cluster_wafer_real(index):
    recipe = [['HHP1', 'HHP2'], ['LPAH1', 'LPAH2'],
              ['CP2', 'CP3'], ['SC1', 'SC2'],
              ['SC3'], ['HP5', 'HP6'],
              ['CP10', 'CP11'], ['SCANNER'],
              ['PEB1', 'PEB2'], ['CP8', 'CP9'],
              ['EE1', 'EE2'], ['SD1', 'SD2', 'SD3'],
              ['HP3', 'HP4'], ['CP4', 'CP5']]
    numclusters = 3
    string = "[weighted-automaton]\n"
    clusters = [set(['HHP1', 'HHP2', 'HP1', 'HP2', 'CP2', 'CP3', 'SC1', 'SC2', 'LPAH1', 'LPAH2']),
                set(['HP3', 'HP4', 'HP8', 'CP4', 'CP5', 'CP6', 'CP7','CP1','HP7','HP6','HP5','SC3']),
                set(['SD1', 'SD2', 'EE1', 'EE2', 'CP11', 'CP10', 'CP9', 'CP8', 'PEB1', 'PEB2', 'SD3']),
                set(['SCANNER'])]
    state_resources = {}
    for cluster in clusters:
        for cl in cluster:
            state_resources[cl] = []
    state_resources[''] = []
    wafer = 'W' + str(index)
    state = 'start_'
    states = [state]
    transitions = []
    cluster = 0
    count = 1
    robot_resource = [[] for i in range(numclusters)]
    while cluster != -1:
        if len(clusters[cluster]) == 0:
            cluster -= 1
            if cluster == -1:
                continue
            chamber = str(cluster+1) + '3'
            newstate = str(count) + '_' + chamber
            states.append(newstate)
            transition = wafer + '-' + state + '-' + newstate
            transitions.append((transition, 2))
            robot_resource[cluster+1].append(transition)
            state = newstate
            count += 1
            continue
        chamber = clusters[cluster].pop(0)
        newstate = str(count) + '_' + chamber
        states.append(newstate)
        transition = wafer + '-' + state + '-' + newstate
        transitions.append((transition, 2))
        robot_resource[cluster].append(transition)
        state = newstate
        count += 1
        if (chamber.endswith('3') and cluster + 1 < numclusters):
            cluster += 1
        else:
            newstate = str(count) + '_' + chamber
            states.append(newstate)
            transition = wafer + '-' + state + '-' + newstate
            transitions.append((transition, 4))
            count += 1
            state = newstate
    newstate = 'end_'
    states.append(newstate)
    transition = wafer + '-' + state + '-' + newstate
    transitions.append((transition, 2))
    robot_resource[0].append(transition)
    #if index != 1:
    #    states.append('prestart_')
    #    transitions.append(('W' + str(index-1) + '-start_-1_11', 2))
    string += "states = " + ",".join(states) + "\n"
    alphabet = [tup[0] for tup in transitions]
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(tup):
        event = tup[0]
        weight = str(tup[1])
        split = event.split('-')
        state_resources[split[1].split('_')[1]].append(event)
        state_resources[split[2].split('_')[1]].append(event)
        if split[0] == 'W' + str(index):
            return "(" + split[1] + "," + split[2] + "," + event + "," + weight + ")"
        else:
            return "(prestart_,start_," + event + ",2)"
    string += "transitions = " + ','.join(map(transition, transitions)) + "\n"
    if True:# index == 1:
        string += "initial-state = start_\n"
    else:
        string += "initial-state = prestart_\n"
    string += "marker-states = end_\n"
    state_resources.pop('');

def xytoi(x, y, width):
    return (y*width) + x

def create_close_coridor(index, layout, initial, marked):
    width = len(layout)
    height = len(layout[0])
    states = [str(xytoi(x, y, width)) for x in range(width) for y in range(height) if layout[x][y] != 'W']
    def outgoingtrans(x, y):
        out = []
        for dx, dy in [(0,1),(0,-1),(1,0),(-1,0)]:
            try:
                if x + dx < 0 or x + dx >= width or y + dy < 0 or y + dy >= height:
                    continue
                if (layout[x + dx][y + dy] != 'W'):
                    out.append('P{}-{}-{}'.format(str(index), str(xytoi(x,y,width)),
                                                  str(xytoi(x+dx, y+dy, width))))
            except IndexError:
                continue
        return out
    alphabet = []
    state_resources = {}
    for x in range(width):
        for y in range(height):
            if (layout[x][y] != 'W'):
                state_resources[str(xytoi(x,y,width))] = []
                alphabet.extend(outgoingtrans(x,y))
    string = "[weighted-automaton]\n"
    string += "states = " + ",".join(states) + "\n"
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(event):
        weight = str(1)
        split = event.split('-')
        state_resources[split[1]].append(event)
        state_resources[split[2]].append(event)
        return "(" + split[1] + "," + split[2] + "," + event + "," + weight + ")"
    string += "transitions = " + ','.join(map(transition, alphabet)) + "\n"
    string += "initial-state = {}\n".format(initial)
    string += "marker-states = {}\n".format(marked)
    return string, state_resources

def make_epucks_closed_corridor(number, layout, startstop = None, seed = None, restricted = False):
    width = len(layout)
    height = len(layout[0])
    if restricted:
        states = [str(xytoi(x, y, width)) for x in range(width) for y in range(height) if layout[x][y] != 'W' and (x <= 2 or x >= 5)]
    else:
        states = [str(xytoi(x, y, width)) for x in range(width) for y in range(height) if layout[x][y] != 'W']
    startplaces = list(states)
    endplaces = list(states)
    names = []
    state_resources = []
    random.seed(seed)
    for i in range(1, number + 1):
        handle = file("SimonEpuck" + str(i) + ".cfg", 'w')
        names.append("SimonEpuck" + str(i) + ".cfg")
        if startstop == None:
            initial = startplaces.pop(random.randrange(len(startplaces)))
            marked =  endplaces.pop(random.randrange(len(endplaces)))
        else:
            initial, marked = startstop[i-1]
        print '{},{}'.format(initial, marked)
        aut, resources = create_close_coridor(i, layout, initial, marked)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_resources

def create_run_closed_corridor(index, layout, startstop = None, seed = None, restricted = False):
    names, state_resources = make_epucks_closed_corridor(index, layout, startstop, seed, restricted)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts]
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    resources.extend(state_resources)
    resources = map(frozenset, resources)
    alphabet = set()
    for aut in auts:
        alphabet.update(aut.alphabet)
    resource_int_map = {}
    for i, res in enumerate(resources):
        resource_int_map[res] = i
    event_resource_map = {}
    numpy_array_map = {}
    for event in alphabet:
        event_resource_map[event] = [resource_int_map[res] for res in resources if event in res]
        indexs = set(event_resource_map[event])
        numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(len(resources))], numpy.int8)
    epuck_res = [resource_int_map[frozenset(aut.alphabet)] for aut in auts]
    int_resources = set(resource_int_map.values())
    epuck_res = int_resources
    #make_path(auts, resources, state_resources)
    make_path_default(auts, resources, state_resources, event_resource_map, epuck_res,
                      int_resources, resource_int_map, collections.defaultdict(list), numpy_array_map)

def create_open_coridor(index, rooms, initial, marked):
    width = rooms * 3 + 4
    height = 8
    total = width * height
    states = [str(xytoi(x, y, width)) for x in range(width) for y in range(height)]
    def outgoingtrans(x, y):
        out = []
        #exits = []
        if (y % 2 == 1 or x < 2 or x >= width - 2 or ((y == 2 or y == 6) and x % 3 == 0)) and y != 0:
            #exits.append('U')
            out.append('P{}-{}-{}'.format(str(index), str(xytoi(x,y,width)),
                                          str(xytoi(x, y-1, width))))
        if (y % 2 == 0 or x < 2 or x >= width - 2 or ((y == 1 or y == 5) and x % 3 == 0)) and y != height - 1:
            #exits.append('D')
            out.append('P{}-{}-{}'.format(str(index), str(xytoi(x,y,width)),
                                          str(xytoi(x, y+1, width))))
        if (y < 2 or y >= height - 2 or x % 3 != 2) and x != 0:
            #exits.append('W')
            out.append('P{}-{}-{}'.format(str(index), str(xytoi(x,y,width)),
                                          str(xytoi(x-1, y, width))))
        if (y < 2 or y >= height - 2 or x % 3 != 1) and x != width - 1:
            #exits.append('E')
            out.append('P{}-{}-{}'.format(str(index), str(xytoi(x,y,width)),
                                          str(xytoi(x+1, y, width))))
        return out#, exits
    alphabet = []
    state_resources = {}
    stringdesc = ['' for i in range(3*height)]
    simpledesc = ['' for i in range(height)]
    for x in range(width):
        for y in range(height):
            state_resources[str(xytoi(x,y,width))] = []
            events = outgoingtrans(x, y)#, exits = outgoingtrans(x,y)
            #top = [' ',' ',' ']
            #mid = [' ',' ',' ']
            #bot = [' ',' ',' ']
            #ex = 0
            #if 'U' in exits:
            #    bot[1] = '|'
            #    ex += 1
            #if 'D' in exits:
            #    top[1] = '|'
            #    ex += 4
            #if 'W' in exits:
            #    mid[0] = '-'
            #    ex += 8
            #if 'E' in exits:
            #    mid[2] = '-'
            #    ex += 2
            #stringdesc[y*3] = stringdesc[y*3] + ''.join(top)
            #stringdesc[y*3 + 1] = stringdesc[y*3] + ''.join(mid)
            #stringdesc[y*3 + 2] = stringdesc[y*3] + ''.join(bot)
            #simpledesc[y] += hex(ex)[2]
            alphabet.extend(events)
    string = "[weighted-automaton]\n"
    string += "states = " + ",".join(states) + "\n"
    string += "alphabet = " + ','.join(alphabet) + "\n"
    string += "controllable = " + ','.join(alphabet) + "\n"
    string += "observable = " + ','.join(alphabet) + "\n"
    def transition(event):
        weight = str(1)
        split = event.split('-')
        state_resources[split[1]].append(event)
        state_resources[split[2]].append(event)
        return "(" + split[1] + "," + split[2] + "," + event + "," + weight + ")"
    string += "transitions = " + ','.join(map(transition, alphabet)) + "\n"
    string += "initial-state = {}\n".format(initial)
    string += "marker-states = {}\n".format(marked)
    return string, state_resources

def make_epucks_open_corridor(number, rooms = 4, startstop = None):
    width = rooms * 3 + 4
    height = 8
    total = width * height
    states = [str(xytoi(x, y, width)) for x in range(width) for y in range(height)]
    startplaces = list(states)
    endplaces = list(states)
    names = []
    state_resources = []
    for i in range(1, number + 1):
        handle = file("SimonEpuck" + str(i) + ".cfg", 'w')
        names.append("SimonEpuck" + str(i) + ".cfg")
        if startstop == None:
            initial = startplaces.pop(random.randrange(len(startplaces)))
            marked =  endplaces.pop(random.randrange(len(endplaces)))
        else:
            initial, marked = startstop[i-1]
        aut, resources = create_open_coridor(i, rooms, initial, marked)
        state_resources.append(resources)
        handle.write(aut)
        handle.close()
    list_resources = []
    for state in state_resources[0]:
        resource = []
        for state_resource in state_resources:
            resource.extend(state_resource[state])
        list_resources.append(resource)
    return ','.join(names), list_resources

def create_run_open_corridor(index, rooms = 4):
    names, state_resources = make_epucks_open_corridor(index, rooms)
    auts = weighted_frontend.load_weighted_automata(collection.Collection(), names, False, True)
    resources = [set(aut.alphabet) for aut in auts]
    state_resources = map(lambda list: map(auts[0].collection.events.get, list), state_resources)
    state_resources = map(frozenset, state_resources)
    resources.extend(state_resources)
    resources = map(frozenset, resources)
    alphabet = set()
    for aut in auts:
        alphabet.update(aut.alphabet)
    resource_int_map = {}
    for i, res in enumerate(resources):
        resource_int_map[res] = i
    event_resource_map = {}
    numpy_array_map = {}
    for event in alphabet:
        event_resource_map[event] = [resource_int_map[res] for res in resources if event in res]
        indexs = set(event_resource_map[event])
        numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(len(resources))], numpy.int8)
    epuck_res = [resource_int_map[frozenset(aut.alphabet)] for aut in auts]
    int_resources = set(resource_int_map.values())
    epuck_res = int_resources
    make_path_default(auts, resources, state_resources, event_resource_map, epuck_res,
                      int_resources, resource_int_map, collections.defaultdict(list), numpy_array_map)

def make_wafer_real(index, path, coll, colltoevent, robotevents, reticle = None):
    alphabet = set()
    new_aut = weighted_structure.WeightedAutomaton(alphabet, coll)
    new_aut.initial = new_aut.add_new_state(len(path) == 0)
    colldict = {}
    state = new_aut.initial
    colldict[state] = []
    for i, (place, cost, robot) in enumerate(path):
        nextstate = new_aut.add_new_state(False)
        event = coll.make_event('{}-{}'.format(index, i*2), True, True, False)
        robotevents[robot].append(event)
        alphabet.add(event)
        new_aut.add_edge_data(state, nextstate, event, 3)
        if reticle != None and place == 'Scanner':
            colldict[nextstate] = [place, '!' + str(reticle)]
        else:
            colldict[nextstate] = [place]
        if i == 0:
            colltoevent[' '].append(event)
        colltoevent[place].append(event)
        if i != 0:
            colltoevent[path[i-1][0]].append(event)
        state = nextstate
        if cost != 0:
            nextstate = new_aut.add_new_state(False)
            event = coll.make_event('{}-{}'.format(index, i*2+1), True, True, False)
            alphabet.add(event)
            new_aut.add_edge_data(state, nextstate, event, cost)
            state = nextstate
            if reticle != None and place == 'Scanner':
                colldict[nextstate] = [place, '!' + str(reticle)]
                colltoevent[place].append(event)
            else:
                colldict[nextstate] = [place]
    nextstate = new_aut.add_new_state(True)
    event = coll.make_event('{}-{}'.format(index, i*2+2), True, True, False)
    robotevents[0].append(event)
    alphabet.add(event)
    new_aut.add_edge_data(state, nextstate, event, 3)
    if (colldict[state] != []):
        colltoevent[colldict[state][0]].append(event)
    state = nextstate
    colldict[state] = []
    return new_aut, colldict

def make_real_clusters(numberwafers, path, reticle = None, setup = None):
    if setup == None:
        coll = collection.Collection()
        colltoevent = collections.defaultdict(list)
        robot_events = collections.defaultdict(list)
        start = 0
    else:
        coll, colltoevent, robot_events, start = setup
    auttuples = []
    for i in range(start, start + numberwafers):
        auttuples.append(make_wafer_real(i, path, coll, colltoevent, robot_events, reticle))
    return auttuples, colltoevent, robot_events

def make_real_clusters_mult(tups):
    coll = collection.Collection()
    colltoevent = collections.defaultdict(list)
    robot_events = collections.defaultdict(list)
    auttuples = []
    val = 0
    for numberwafers, path in tups:
        for i in range(numberwafers):
            auttuples.append(make_wafer_real(i+val, path, coll, colltoevent, robot_events))
        val += numberwafers
    return auttuples, colltoevent, robot_events

def create_path_real_clusters(numwafers1, numwafers2, numwafers3):
    path1 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('B1', 0, 0), ('SC3', 50, 1),
            ('HP58', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path2 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('HP12', 90, 0), ('B1', 0, 0),
            ('CP67', 60, 1), ('SC3', 50, 1),
            ('B2', 0, 1), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path3 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('B1', 0, 0),
            ('SC3', 50, 1), ('HP58', 90, 1),
            ('CP67', 60, 1), ('B1', 0, 1),
            ('SC12', 65, 0), ('B1', 0, 0),
            ('HP67', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    places = dict([('HHP', 2), ('LPAH', 2),
            ('CP23', 2), ('SC12', 2),
            ('B1', 1), ('SC3', 1),
            ('HP58', 2), ('B2', 1),
            ('CP1011', 2), ('STK', 15), ('STK2', 1),
            ('Scanner', 1), ('PEB12', 2),
            ('CP89', 2), ('EE12', 2),
            ('SD123', 3), ('HP34', 2), ('HP67', 2),
            ('CP45', 2), ('HP12', 2), ('CP67', 2)])
    #auttuples, colltoevent, robot_events  = make_real_clusters(numwafers, path)
    auttuples, colltoevent, robot_events  = make_real_clusters_mult([(numwafers1, path1), (numwafers2, path2), (numwafers3, path3)])
    event_resource_map = collections.defaultdict(list)
    resource_to_int = {}
    for key,events in robot_events.iteritems():
        for event in events:
            event_resource_map[event].append(key)
    for i, (aut, _) in enumerate(auttuples):
        resource_to_int[frozenset(aut.alphabet)] = 4 + i
        for event in aut.alphabet:
            event_resource_map[event].append(4 + i)
    event_state_resource_map = collections.defaultdict(list)
    for i, (key, events) in enumerate(colltoevent.iteritems()):
        for event in events:
            event_state_resource_map[event].append(4 + len(auttuples) + i)
    num_resources = 4 + len(auttuples)
    num_resources_coll = 4 + len(auttuples) + len(colltoevent)
    alphabet = []
    numpy_array_map = {}
    for aut, _ in auttuples:
        print aut
        alphabet.extend(aut.alphabet)
    for event in alphabet:
        indexs = set(event_resource_map[event])
        numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(num_resources)], numpy.int32)
    make_path_multi_recipe(auttuples, event_resource_map, resource_to_int, event_state_resource_map,
                           numpy_array_map, places, num_resources, num_resources_coll)

def create_path_real_clusters_reticle_alignment(lots):
    path1 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('B1', 0, 0), ('SC3', 50, 1),
            ('HP58', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path2 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('HP12', 90, 0), ('B1', 0, 0),
            ('CP67', 60, 1), ('SC3', 50, 1),
            ('B2', 0, 1), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path3 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('B1', 0, 0),
            ('SC3', 50, 1), ('HP58', 90, 1),
            ('CP67', 60, 1), ('B1', 0, 1),
            ('SC12', 65, 0), ('B1', 0, 0),
            ('HP67', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    paths = [path1, path2, path3]
    places = dict([('HHP', 2), ('LPAH', 2),
            ('CP23', 2), ('SC12', 2),
            ('B1', 1), ('SC3', 1),
            ('HP58', 2), ('B2', 1),
            ('CP1011', 2), ('STK', 15), ('STK2', 1),
            ('Scanner', 1), ('PEB12', 2),
            ('CP89', 2), ('EE12', 2),
            ('SD123', 3), ('HP34', 2), ('HP67', 2),
            ('CP45', 2), ('HP12', 2), ('CP67', 2)])
    if len(lots) == 0:
        lots = []
        for i in range(1440):
            lots.append(str(random.randint(0,2)))
    coll = collection.Collection()
    colltoevent = collections.defaultdict(list)
    robot_events = collections.defaultdict(list)
    trace = []
    ret_aut = weighted_structure.WeightedAutomaton(set(), coll)
    ret_aut.initial = ret_aut.add_new_state(True)
    ret_colls = {}
    ret_colls[ret_aut.initial] = []
    auttuples = [(ret_aut, ret_colls)]
    #auttuples = []
    for lotnum, lot in enumerate(lots):
        reticle_event = coll.make_event('ret{}'.format(lotnum), True, True, False)
        ret_edge = append_reticle(ret_aut, ret_colls, reticle_event, str(lotnum))
        #trace.append(ret_edge)
        newtuples, colltoevent, robot_events = make_real_clusters(24, paths[int(lot)], lotnum, (coll, colltoevent, robot_events, lotnum * 24))
        auttuples.extend(newtuples)
        colltoevent['Scanner'].extend(ret_aut.alphabet)
        set_events = set(colltoevent['Scanner'])
        places[str(lotnum)] = 1
        event_resource_map = collections.defaultdict(list)
        resource_to_int = {}
        for key,events in robot_events.iteritems():
            for event in events:
                event_resource_map[event].append(key)
        for i, (aut, _) in enumerate(auttuples):
            resource_to_int[frozenset(aut.alphabet)] = 4 + i
            for event in aut.alphabet:
                event_resource_map[event].append(4 + i)
        event_state_resource_map = collections.defaultdict(list)
        for i, (key, events) in enumerate(colltoevent.iteritems()):
            if key != 'Scanner':
                for event in events:
                    event_state_resource_map[event].append(4 + len(auttuples) + i+1)
            else:
                for event in events:
                    event_resource_map[event].append(4 + len(auttuples))
        num_resources = 4 + len(auttuples) + 1
        num_resources_coll = 4 + len(auttuples) + len(colltoevent)
        alphabet = []
        numpy_array_map = {}
        for aut, _ in auttuples:
            alphabet.extend(aut.alphabet)
        for event in alphabet:
            indexs = set(event_resource_map[event])
            numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(num_resources)], numpy.int32)
        alphabet = set(alphabet)
        init_path = lotnum*24 + 1 , trace, alphabet, coll
        print 'numauts:{}'.format(len(auttuples))
        #contours = [numpy.array([0 for i in range(num_resources)], numpy.int32)]
        #for i in range(len(trace)):
        #    contours.append(numpy_stack(contours[i], numpy_array_map[trace[i].label], trace[i].weight))
        #insertedpos = len(trace)
        #retedgearray = numpy_array_map[ret_edge.label]
        #for i in range(len(trace)-1, -1,-1):
        #    earlyret = numpy.amax(numpy.multiply(contours[i], retedgearray))
        #    earlyorig = numpy.amax(numpy.multiply(contours[i], numpy_array_map[trace[i].label]))
        #    if earlyret < earlyorig:
        #        insertedpos = i
        #    if i == 0 or trace[i-1].label in set_events:
        #        break
        trace.append(ret_edge)
        trace = make_path_multi_recipe(auttuples, event_resource_map, resource_to_int, event_state_resource_map,
                                       numpy_array_map, places, num_resources, num_resources_coll, init_path)

def create_path_real_clusters_reticle_alignment_window(lots):
    path1 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('B1', 0, 0), ('SC3', 50, 1),
            ('HP58', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path2 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('HP12', 90, 0), ('B1', 0, 0),
            ('CP67', 60, 1), ('SC3', 50, 1),
            ('B2', 0, 1), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path3 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('B1', 0, 0),
            ('SC3', 50, 1), ('HP58', 90, 1),
            ('CP67', 60, 1), ('B1', 0, 1),
            ('SC12', 65, 0), ('B1', 0, 0),
            ('HP67', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    paths = [path1, path2, path3]
    places = dict([('HHP', 2), ('LPAH', 2),
            ('CP23', 2), ('SC12', 2),
            ('B1', 1), ('SC3', 1),
            ('HP58', 2), ('B2', 1),
            ('CP1011', 2), ('STK', 15), ('STK2', 1),
            ('Scanner', 1), ('PEB12', 2),
            ('CP89', 2), ('EE12', 2),
            ('SD123', 3), ('HP34', 2), ('HP67', 2),
            ('CP45', 2), ('HP12', 2), ('CP67', 2)])
    if len(lots) == 0:
        lots = []
        for i in range(999999):
            lots.append(str(random.randint(0,2)))
    coll = collection.Collection()
    colltoevent = collections.defaultdict(list)
    robot_events = collections.defaultdict(list)
    trace = []
    ret_aut = weighted_structure.WeightedAutomaton(set(), coll)
    ret_aut.initial = ret_aut.add_new_state(True)
    ret_colls = {}
    ret_colls[ret_aut.initial] = []
    auttuples = [(ret_aut, ret_colls)]
    robot_start = [0, 0, 0, 0]
    scanner_start = 0
    aut_start = collections.defaultdict(lambda:0)
    init_state_floor = collections.defaultdict(lambda:0)
    STK = ()
    handle = file('tracelen', 'w')
    handle.write('start')
    #auttuples = []
    for lotnum, lot in enumerate(lots):
        reticle_event = coll.make_event('ret{}'.format(lotnum), True, True, False)
        ret_edge = append_reticle(ret_aut, ret_colls, reticle_event, str(lotnum))
        #trace.append(ret_edge)
        newtuples, colltoevent, robot_events = make_real_clusters(24, paths[int(lot)], lotnum, (coll, colltoevent, robot_events, lotnum * 24))
        auttuples.extend(newtuples)
        colltoevent['Scanner'].extend(ret_aut.alphabet)
        set_events = set(colltoevent['Scanner'])
        places[str(lotnum)] = 1
        event_resource_map = collections.defaultdict(list)
        resource_to_int = {}
        num_resources = 4 + len(auttuples) + 1
        num_resources_coll = 4 + len(auttuples) + len(colltoevent)
        initial_resource_usage = numpy.array([0 for i in range(num_resources)], numpy.int32)
        initial_resource_usage[-1] = scanner_start
        drop_resource_usage = collections.defaultdict(lambda: 0)
        drop_resource_usage[len(initial_resource_usage)-1] = scanner_start
        for i in range(4):
            initial_resource_usage[i] = robot_start[i]
            drop_resource_usage[i] = robot_start[i]
        for key,events in robot_events.iteritems():
            for event in events:
                event_resource_map[event].append(key)
        for i, (aut, _) in enumerate(auttuples):
            resource_to_int[frozenset(aut.alphabet)] = 4 + i
            for event in aut.alphabet:
                event_resource_map[event].append(4 + i)
            initial_resource_usage[4+i] = aut_start[aut]
            drop_resource_usage[4+i] = aut_start[aut]
        event_state_resource_map = collections.defaultdict(list)
        place_to_int = {}
        for i, (key, events) in enumerate(colltoevent.iteritems()):
            if key != 'Scanner':
                for event in events:
                    event_state_resource_map[event].append(4 + len(auttuples) + i+1)
                place_to_int[frozenset(events)] = 4 + len(auttuples) + i + 1
                drop_resource_usage[4+len(auttuples)+i+1] = init_state_floor[key]
            else:
                for event in events:
                    event_resource_map[event].append(4 + len(auttuples))
        alphabet = []
        numpy_array_map = {}
        for aut, _ in auttuples:
            alphabet.extend(aut.alphabet)
        for event in alphabet:
            indexs = set(event_resource_map[event])
            numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(num_resources)], numpy.int32)
        alphabet = set(alphabet)
        init_path = len(auttuples)-24, trace, alphabet, coll
        print 'numauts:{}'.format(len(auttuples))
        #contours = [numpy.array([0 for i in range(num_resources)], numpy.int32)]
        #for i in range(len(trace)):
        #    contours.append(numpy_stack(contours[i], numpy_array_map[trace[i].label], trace[i].weight))
        #insertedpos = len(trace)
        #retedgearray = numpy_array_map[ret_edge.label]
        #for i in range(len(trace)-1, -1,-1):
        #    earlyret = numpy.amax(numpy.multiply(contours[i], retedgearray))
        #    earlyorig = numpy.amax(numpy.multiply(contours[i], numpy_array_map[trace[i].label]))
        #    if earlyret < earlyorig:
        #        insertedpos = i
        #    if i == 0 or trace[i-1].label in set_events:
        #        break
        trace.append(ret_edge)
        print 'numpyarraymap-{}, num_resources-{}, event_resource_map-{}'.format(len(numpy_array_map), num_resources, len(event_resource_map))
        print 'event_state_resource_map-{}, resource_to_int-{}'.format(len(event_state_resource_map), len(resource_to_int))
        trace = make_path_multi_recipe(auttuples, event_resource_map, resource_to_int, event_state_resource_map,
                                       numpy_array_map, places, num_resources, num_resources_coll, init_path, initial_resource_usage,
                                       STK, drop_resource_usage)
        upto, contour, events, init_state_floor = calculate_needed_trace(trace, initial_resource_usage, numpy_array_map,
                                                                         init_state_floor, event_state_resource_map)
        print upto
        handle.write('afttrace')
        scanner_start = initial_resource_usage[-1]
        for i in range(4):
            robot_start[i] = contour[i]
        for i in range(4, len(contour)-1):
            aut_start[auttuples[i-4][0]] = contour[i]
        traceto = trace[:upto]
        to_keep = []
        put_events = set()
        pop_events = set()
        events_to_remove = set()
        for (aut, collissions) in auttuples:
            if aut != ret_aut and events.isdisjoint(aut.alphabet):
                events_to_remove.update(aut.alphabet)
                continue
            to_keep.append((aut, collissions))
            update_initial(aut, traceto)
            for state in aut.get_states():
                if state.marked:
                    continue
                edge = state.get_outgoing()[0]
                if "STK" in collissions[edge.succ]:
                    put_events.add(edge.label)
                elif "STK" in collissions[edge.pred]:
                    pop_events.add(edge.label)
        handle.write('aftkeep')
        for k, events in colltoevent.iteritems():
            ne = []
            for e in events:
                if e not in events_to_remove:
                    ne.append(e)
            colltoevent[k] = ne
        for k, events in robot_events.iteritems():
            ne = []
            for e in events:
                if e not in events_to_remove:
                    ne.append(e)
            robot_events[k] = ne
        auttuples = to_keep
        trace = trace[upto:]
        print(len(trace))
        handle.write('Tracelen={}\n'.format(len(trace)))
        #handle.flush()
        STK = []
        handle = file('STK', 'w')
        for edge in reversed(trace):
            if edge.label in pop_events:
                split = edge.label.name.split('-')
                STK.append(split[0])
                handle.write('pop-{}-{}\n'.format(split,STK))
            if edge.label in put_events:
                split = edge.label.name.split('-')
                STK.pop()
                handle.write('put-{}-{}\n'.format(split,STK))
        STK = tuple(STK)

def create_path_real_clusters_reticle_alignment_window_poisson(lots):
    path1 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('B1', 0, 0), ('SC3', 50, 1),
            ('HP58', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path2 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('HP12', 90, 0), ('B1', 0, 0),
            ('CP67', 60, 1), ('SC3', 50, 1),
            ('B2', 0, 1), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path3 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('B1', 0, 0),
            ('SC3', 50, 1), ('HP58', 90, 1),
            ('CP67', 60, 1), ('B1', 0, 1),
            ('SC12', 65, 0), ('B1', 0, 0),
            ('HP67', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    paths = [path1, path2, path3]
    places = dict([('HHP', 2), ('LPAH', 2),
            ('CP23', 2), ('SC12', 2),
            ('B1', 1), ('SC3', 1),
            ('HP58', 2), ('B2', 1),
            ('CP1011', 2), ('STK', 15), ('STK2', 1),
            ('Scanner', 1), ('PEB12', 2),
            ('CP89', 2), ('EE12', 2),
            ('SD123', 3), ('HP34', 2), ('HP67', 2),
            ('CP45', 2), ('HP12', 2), ('CP67', 2)])
    if len(lots) == 0:
        lots = []
        for i in range(999999):
            lots.append((str(random.randint(0,2)), int(random.expovariate(1.196) * 3600)))
    coll = collection.Collection()
    colltoevent = collections.defaultdict(list)
    robot_events = collections.defaultdict(list)
    trace = []
    track_alignment = weighted_structure.WeightedAutomaton(set(), coll)
    track_alignment.initial = track_alignment.add_new_state(True)
    ret_aut = weighted_structure.WeightedAutomaton(set(), coll)
    ret_aut.initial = ret_aut.add_new_state(True)
    ret_colls = {}
    ret_colls[ret_aut.initial] = []
    auttuples = [(ret_aut, ret_colls)]
    robot_start = [0, 0, 0, 0]
    scanner_start = 0
    arrivetime = 0
    aut_start = collections.defaultdict(lambda:arrivetime)
    init_state_floor = collections.defaultdict(lambda:arrivetime)
    STK = ()
    handle = file('tracelen', 'w')
    handle.write('start')
    #auttuples = []
    for lotnum, (lot, time) in enumerate(lots):
        reticle_event = coll.make_event('ret{}'.format(lotnum), True, True, False)
        arrivetime += time
        ret_edge = append_reticle(ret_aut, ret_colls, reticle_event, str(lotnum))
        #trace.append(ret_edge)
        newtuples, colltoevent, robot_events = make_real_clusters(24, paths[int(lot)], lotnum, (coll, colltoevent, robot_events, lotnum * 24))
        auttuples.extend(newtuples)
        colltoevent['Scanner'].extend(ret_aut.alphabet)
        set_events = set(colltoevent['Scanner'])
        places[str(lotnum)] = 1
        event_resource_map = collections.defaultdict(list)
        resource_to_int = {}
        num_resources = 4 + len(auttuples) + 1
        num_resources_coll = 4 + len(auttuples) + len(colltoevent)
        initial_resource_usage = numpy.array([0 for i in range(num_resources)], numpy.int32)
        initial_resource_usage[-1] = scanner_start
        drop_resource_usage = collections.defaultdict(lambda: 0)
        drop_resource_usage[len(initial_resource_usage)-1] = scanner_start
        for i in range(4):
            initial_resource_usage[i] = robot_start[i]
            drop_resource_usage[i] = robot_start[i]
        for key,events in robot_events.iteritems():
            for event in events:
                event_resource_map[event].append(key)
        for i, (aut, _) in enumerate(auttuples):
            resource_to_int[frozenset(aut.alphabet)] = 4 + i
            for event in aut.alphabet:
                event_resource_map[event].append(4 + i)
            initial_resource_usage[4+i] = aut_start[aut]
            drop_resource_usage[4+i] = aut_start[aut]
        event_state_resource_map = collections.defaultdict(list)
        place_to_int = {}
        for i, (key, events) in enumerate(colltoevent.iteritems()):
            if key != 'Scanner':
                for event in events:
                    event_state_resource_map[event].append(4 + len(auttuples) + i+1)
                place_to_int[frozenset(events)] = 4 + len(auttuples) + i + 1
                drop_resource_usage[4+len(auttuples)+i+1] = init_state_floor[key]
            else:
                for event in events:
                    event_resource_map[event].append(4 + len(auttuples))
        alphabet = []
        numpy_array_map = {}
        for aut, _ in auttuples:
            alphabet.extend(aut.alphabet)
        for event in alphabet:
            indexs = set(event_resource_map[event])
            numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(num_resources)], numpy.int32)
        alphabet = set(alphabet)
        init_path = len(auttuples)-24, trace, alphabet, coll
        print 'numauts:{}'.format(len(auttuples))
        #contours = [numpy.array([0 for i in range(num_resources)], numpy.int32)]
        #for i in range(len(trace)):
        #    contours.append(numpy_stack(contours[i], numpy_array_map[trace[i].label], trace[i].weight))
        #insertedpos = len(trace)
        #retedgearray = numpy_array_map[ret_edge.label]
        #for i in range(len(trace)-1, -1,-1):
        #    earlyret = numpy.amax(numpy.multiply(contours[i], retedgearray))
        #    earlyorig = numpy.amax(numpy.multiply(contours[i], numpy_array_map[trace[i].label]))
        #    if earlyret < earlyorig:
        #        insertedpos = i
        #    if i == 0 or trace[i-1].label in set_events:
        #        break
        trace.append(ret_edge)
        print 'numpyarraymap-{}, num_resources-{}, event_resource_map-{}'.format(len(numpy_array_map), num_resources, len(event_resource_map))
        print 'event_state_resource_map-{}, resource_to_int-{}'.format(len(event_state_resource_map), len(resource_to_int))
        trace = make_path_multi_recipe(auttuples, event_resource_map, resource_to_int, event_state_resource_map,
                                       numpy_array_map, places, num_resources, num_resources_coll, init_path, initial_resource_usage,
                                       STK, drop_resource_usage)
        upto, contour, events, init_state_floor = calculate_needed_trace(trace, initial_resource_usage, numpy_array_map,
                                                                         init_state_floor, event_state_resource_map)
        print upto
        handle.write('afttrace')
        scanner_start = initial_resource_usage[-1]
        for i in range(4):
            robot_start[i] = contour[i]
        for i in range(4, len(contour)-1):
            aut_start[auttuples[i-4][0]] = contour[i]
        traceto = trace[:upto]
        to_keep = []
        put_events = set()
        pop_events = set()
        events_to_remove = set()
        for (aut, collissions) in auttuples:
            if aut != ret_aut and events.isdisjoint(aut.alphabet):
                events_to_remove.update(aut.alphabet)
                continue
            to_keep.append((aut, collissions))
            update_initial(aut, traceto)
            for state in aut.get_states():
                if state.marked:
                    continue
                edge = state.get_outgoing()[0]
                if "STK" in collissions[edge.succ]:
                    put_events.add(edge.label)
                elif "STK" in collissions[edge.pred]:
                    pop_events.add(edge.label)
        handle.write('aftkeep')
        for k, events in colltoevent.iteritems():
            ne = []
            for e in events:
                if e not in events_to_remove:
                    ne.append(e)
            colltoevent[k] = ne
        for k, events in robot_events.iteritems():
            ne = []
            for e in events:
                if e not in events_to_remove:
                    ne.append(e)
            robot_events[k] = ne
        auttuples = to_keep
        trace = trace[upto:]
        print(len(trace))
        handle.write('Tracelen={}\n'.format(len(trace)))
        #handle.flush()
        STK = []
        handle = file('STK', 'w')
        for edge in reversed(trace):
            if edge.label in pop_events:
                split = edge.label.name.split('-')
                STK.append(split[0])
                handle.write('pop-{}-{}\n'.format(split,STK))
            if edge.label in put_events:
                split = edge.label.name.split('-')
                STK.pop()
                handle.write('put-{}-{}\n'.format(split,STK))
        STK = tuple(STK)

def create_path_real_clusters_reticle_alignment_reverse(lots):
    path1 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('B1', 0, 0), ('SC3', 50, 1),
            ('HP58', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path2 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('SC12', 65, 0),
            ('HP12', 90, 0), ('B1', 0, 0),
            ('CP67', 60, 1), ('SC3', 50, 1),
            ('B2', 0, 1), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    path3 = [('HHP', 80, 0), ('LPAH', 90, 0),
            ('CP23', 60, 0), ('B1', 0, 0),
            ('SC3', 50, 1), ('HP58', 90, 1),
            ('CP67', 60, 1), ('B1', 0, 1),
            ('SC12', 65, 0), ('B1', 0, 0),
            ('HP67', 90, 1), ('B2', 0, 1),
            ('CP1011', 60, 2), ('STK', 0, 2),
            ('Scanner', 100, 3), ('STK2', 0, 3),
            ('PEB12', 90, 2), ('CP89', 60, 2),
            ('EE12', 90, 2), ('SD123', 130, 2),
            ('B2', 0, 2), ('HP34', 90, 1),
            ('CP45', 60, 1), ('B1', 0, 1)]
    paths = [path1, path2, path3]
    places = dict([('HHP', 2), ('LPAH', 2),
            ('CP23', 2), ('SC12', 2),
            ('B1', 1), ('SC3', 1),
            ('HP58', 2), ('B2', 1),
            ('CP1011', 2), ('STK', 16), ('STK2', 1),
            ('Scanner', 1), ('PEB12', 2),
            ('CP89', 2), ('EE12', 2),
            ('SD123', 3), ('HP34', 2), ('HP67', 2),
            ('CP45', 2), ('HP12', 2), ('CP67', 2)])
    coll = collection.Collection()
    colltoevent = collections.defaultdict(list)
    robot_events = collections.defaultdict(list)
    trace = []
    ret_aut = weighted_structure.WeightedAutomaton(set(), coll)
    ret_aut.initial = ret_aut.add_new_state(True)
    ret_colls = {}
    ret_colls[ret_aut.initial] = []
    auttuples = []
    for lotnum, lot in enumerate(lots):
        reticle_event = coll.make_event('ret{}'.format(lotnum), True, True, False)
        ret_edge = append_reticle(ret_aut, ret_colls, reticle_event, str(lotnum))
        trace.append(ret_edge)
        newtuples, colltoevent, robot_events = make_real_clusters(24, paths[int(lot)], lotnum, (coll, colltoevent, robot_events, lotnum * 24))
        auttuples.extend(newtuples)
        colltoevent['Scanner'].append(reticle_event)
        places[str(lotnum)] = 1
    auttuples.insert(0, (ret_aut, ret_colls))
    #auttuples.reverse()
    event_resource_map = collections.defaultdict(list)
    resource_to_int = {}
    for key,events in robot_events.iteritems():
        for event in events:
            event_resource_map[event].append(key)
    for i, (aut, _) in enumerate(auttuples):
        resource_to_int[frozenset(aut.alphabet)] = 4 + i
        for event in aut.alphabet:
            event_resource_map[event].append(4 + i)
    event_state_resource_map = collections.defaultdict(list)
    for i, (key, events) in enumerate(colltoevent.iteritems()):
        if key != 'Scanner':
            for event in events:
                event_state_resource_map[event].append(4 + len(auttuples) + i+1)
        else:
            for event in events:
                event_resource_map[event].append(4 + len(auttuples))
    num_resources = 4 + len(auttuples) + 1
    num_resources_coll = 4 + len(auttuples) + len(colltoevent)
    alphabet = []
    numpy_array_map = {}
    for aut, _ in auttuples:
        alphabet.extend(aut.alphabet)
    for event in alphabet:
        indexs = set(event_resource_map[event])
        numpy_array_map[event] = numpy.array([True if i in indexs else False for i in range(num_resources)], numpy.int32)
    alphabet = set(alphabet)
    init_path = 1 , trace, alphabet, coll
    print 'numauts:{}'.format(len(auttuples))
    trace = make_path_multi_recipe_proj(auttuples, event_resource_map, resource_to_int, event_state_resource_map,
                                   numpy_array_map, places, num_resources, num_resources_coll, init_path)

def make_path_multi_recipe(auts, event_resource_map, resource_to_int,
                           event_state_resource_map, numpy_array_map, coll_capacity, num_resources,
                           num_resources_coll, init_path = None, init_resource_usage = None,
                           init_STK = (), drop_resource_usage = collections.defaultdict(lambda: 0)):
    autweights = []
    dur = -time.clock()
    for aut,collisions in auts:
        heur = mark_aut_reverse_djikstra_default(aut, resource_to_int[frozenset(aut.alphabet)])
        #autweights.append((aut, aut.initial.heur[0][1]))
        autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
        #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
    lbe = autweights[0][1]
    numepucks = len(autweights)
    size = auts[0][0].get_num_states()
    #path.initial.collisions = []
    #path.initial.heur = []
    bestorigweight = float('inf')
    bestcompressweight = float('inf')
    comptime = 0
    astar_time = 0
    #p1 = cp.Profile()
    #p2 = cp.Profile()
    handle = file('trace','w')
    start = 0
    if init_path == None:
        path = weighted_structure.WeightedAutomaton(set(), auts[0][0].collection)
        path.initial = path.add_new_state(True)
        pathcoll = {}
        pathheur = {}
        pathcoll[path.initial] = []
        pathheur[path.initial] = numpy.array([0 for _ in range(num_resources)], numpy.int8)
    else:
        start, trace, alphabet, collection = init_path
        #print 'start:{}'.format(start)
        #print 'here kitty'
        trace, compressweight = compress_path_better(trace, event_resource_map,
                                                     event_state_resource_map, drop_resource_usage)
        path, pathheur, pathcoll = trace_to_path_numpy_multi(trace, alphabet, collection, numpy_array_map,
                                                             num_resources, autweights[0:start], coll_capacity)
    for (i, (aut,aw,collA,heurA)) in enumerate(autweights[start:]):
        #print i
        #print aut.initial.get_outgoing()[0].label.name
        tup = a_star_search_numpy_multi_STK(aut, path, collA, pathcoll, heurA, pathheur, numpy_array_map,
                                            coll_capacity, num_resources, init_resource_usage, init_STK)
        path, weight = tup
        #print 'w:{}'.format(weight)
        if path == None:
            for edge in trace:
                handle.write(edge.label.name +'\n')
            handle.close()
            stdi = ad
            break
        trace = []
        state = path.initial
        while not state.marked:
            edge = state.get_outgoing()[0]
            trace.append(edge)
            state = edge.succ
        #comptime -= time.clock()
        compressweight = weight
        #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
        trace, compressweight = compress_path_better(trace, event_resource_map,
                                                     event_state_resource_map, drop_resource_usage)
        #print compressweight
        path, pathheur, pathcoll = trace_to_path_numpy_multi(trace, path.alphabet, path.collection, numpy_array_map,
                                                             num_resources, autweights[0:i+start+1], coll_capacity)
    if path == None:
        origweight = float('inf')
        compressweight = float('inf')
    else:
        origweight = weight
        #trace = []
        #state = path.initial
        #while not state.marked:
        #    edge = state.get_outgoing()[0]
        #    trace.append(edge)
        #    state = edge.succ
        #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
    bestorigweight = min(bestorigweight, origweight)
    bestcompressweight = min(bestcompressweight, compressweight)
    #bestcompressweight = comp
    #compressweight = origweight
    tim = dur + time.clock()
    resultsfiles[0].write('epucks:{},size:{},lbe:{},weight:{},cweight:{},bweight:{},bcweight{},time:{},tncomp:{}\n'.format(
        numepucks, size, lbe, origweight, compressweight, bestorigweight, bestcompressweight, tim, comptime
    ))
    resultsfiles[0].flush()
    contour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    for edge in trace:
        contour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
        #print '{}-{}'.format(edge.label.name, contour)
    return trace
    #print 'default'
    #s = StringIO.StringIO()
    #sortby = 'cumulative'
    #ps = pstats.Stats(p1, stream=s).sort_stats(sortby)
    #ps.print_stats()

def make_path_multi_recipe_proj(auts, event_resource_map, resource_to_int,
                                event_state_resource_map, numpy_array_map, coll_capacity, num_resources,
                                num_resources_coll, init_path = None):
    autweights = []
    dur = -time.clock()
    for aut,collisions in auts:
        heur = mark_aut_reverse_djikstra_default(aut, resource_to_int[frozenset(aut.alphabet)])
        autweights.append((aut, heur[aut.initial][0][1], collisions, heur))
    lbe = autweights[0][1]
    numepucks = len(autweights)
    size = auts[0][0].get_num_states()
    bestorigweight = float('inf')
    bestcompressweight = float('inf')
    comptime = 0
    start = 0
    if init_path == None:
        path = weighted_structure.WeightedAutomaton(set(), auts[0][0].collection)
        path.initial = path.add_new_state(True)
        pathcoll = {}
        pathheur = {}
        pathcoll[path.initial] = []
        pathheur[path.initial] = numpy.array([0 for _ in range(num_resources)], numpy.int8)
    else:
        start, trace, alphabet, collection = init_path
        print 'start:{}'.format(start)
        trace, compressweight = compress_path_better(trace, event_resource_map,
                                                     event_state_resource_map)
        path, pathheur, pathcoll = trace_to_path_numpy_multi(trace, alphabet, collection, numpy_array_map,
                                                             num_resources, autweights[0:start], coll_capacity)
    for (i, (aut,aw,collA,heurA)) in enumerate(autweights[start:]):
        print i
        print aut.initial.get_outgoing()[0].label.name
        #auts = [autweights[j][0] for j in range(i, i + 3)]
        #colls = [autweights[j][2] for j in range(i, i + 3)]
        #heurs = [autweights[j][3] for j in range(i, i + 3)]
        #tup = a_star_search_numpy_multi_lots(auts, path, colls, pathcoll,
        #                                         heurs, pathheur, numpy_array_map,
        #                                         coll_capacity, num_resources, i)
        if i == 0:
            h = file('check', 'w')
            state = autweights[start][0].initial
            while not state.marked:
                edge = state.get_outgoing()[0]
                state = edge.succ
                h.write(edge.label.name + '\n')
        tup = a_star_search_numpy_multi_STK_PROJ(aut, path, autweights[0][0], collA, pathcoll, autweights[0][2],
                                                 heurA, pathheur, numpy_array_map, coll_capacity, num_resources,i)
        path, weight = tup
        if i == 0:
            h.write('next\n')
            state = path.initial
            while not state.marked:
                edge = state.get_outgoing()[0]
                state = edge.succ
                h.write(edge.label.name + '\n')
            h.close()
        print 'w:{}'.format(weight)
        #astar_time += time.clock()
        #p2.disable()
        if path == None:
            break
        trace = []
        state = path.initial
        while not state.marked:
            edge = state.get_outgoing()[0]
            trace.append(edge)
            state = edge.succ
        #comptime -= time.clock()
        compressweight = weight
        #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
        #trace, compressweight = compress_path_better(trace, event_resource_map,
        #                                             event_state_resource_map)
        ntrace = []
        for edge in trace:
            if edge.label not in autweights[0][0].alphabet:
                ntrace.append(edge)
        trace = ntrace
        print compressweight
        #print "{}-{}".format(compressweight, compressweight2)
        #comptime += time.clock()
        #path, pathheur, pathcoll = trace_to_path(trace, path.alphabet, path.collection,
        #                                         event_resource_map, fin_coll, puck_res)
        path, pathheur, pathcoll = trace_to_path_numpy_multi(trace, path.alphabet, path.collection, numpy_array_map,
                                                             num_resources, autweights[1:i+start+1], coll_capacity)
        #path, pathheur, pathcoll = trace_to_path_numpy_drop(trace, path.alphabet, path.collection, numpy_array_map,
        #                                               fin_coll, puck_res, len(resources))
        #product = progressivetimeoptimalsynthesis.synchronousproduct_weighted_epucks([aut, path], 0)
        #product, weight = progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([product],
        #                                                                                        frozenset(product.alphabet), resources)
        #product, weight = progressivetimeoptimalsynthesis.make_greedy_prog_supervisor_all_controllable_epuck(product,
        #                                                                                               frozenset(product.alphabet), resources)
        #print "weight: " + str(weight)
        #product.save_as_dot("product.dot")
        #path = tau_abstraction.restrictpath(product)
        #print "restricted"
    if path == None:
        origweight = float('inf')
        compressweight = float('inf')
    else:
        origweight = weight
        #trace = []
        #state = path.initial
        #while not state.marked:
        #    edge = state.get_outgoing()[0]
        #    trace.append(edge)
        #    state = edge.succ
        #trace, compressweight = compress_path_default(trace, resources, state_resources, event_resource_map)
    bestorigweight = min(bestorigweight, origweight)
    bestcompressweight = min(bestcompressweight, compressweight)
    #bestcompressweight = comp
    #compressweight = origweight
    tim = dur + time.clock()
    resultsfiles[0].write('epucks:{},size:{},lbe:{},weight:{},cweight:{},bweight:{},bcweight{},time:{},tncomp:{}\n'.format(
        numepucks, size, lbe, origweight, compressweight, bestorigweight, bestcompressweight, tim, comptime
    ))
    resultsfiles[0].flush()
    contour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    for edge in trace:
        contour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
        #print '{}-{}'.format(edge.label.name, contour)
    return trace

def a_star_search_numpy_multi(autA, autB, collA, collB, heurA, heurB, numpy_array_map, max_slot,
                              num_resources,number):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    ha, hb = init()
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[autB.initial])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    #heurvalue = {}
    k = maxval
    infinity = float('inf')
    def heur(sa, sb):
        res, timen = ha[sa]
        heuristica = newcontour[res] + timen
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb)
    while k <= maxval:
        def collision(slots):
            needs = set()
            slotsnums = collections.defaultdict(lambda: 0)
            for slot in slots:
                if (slot.startswith('!')):
                    needs.add(slot[1:])
                else:
                    num = slotsnums[slot]
                    num += 1
                    slotsnums[slot] = num
                    if num > max_slot[slot]:
                        return True
            for need in needs:
                if need not in slotsnums:
                    return True
            return False
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if 'STK' in collA[edge.succ] and 'STK2' in collB[stateb]:
                continue
            if collision(collA[edge.succ] + collB[stateb]):
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(edge.succ, stateb)
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            if (newtuple in look_back):
                continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            STKc1 = 0
            STKc2 = 0
            for p in collB[stateb]:
                if p == 'STK':
                    STKc1 += 1
            for p in collB[edge.succ]:
                if p == 'STK':
                    STKc2 += 1
            if 'STK2' in collA[statea] and STKc2 > STKc1:
                continue
            if collision(collA[statea] + collB[edge.succ]):
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(statea, edge.succ)
            #if heuristic >= heurvalue.get(newtuple, infinity):
            #    continue
            #heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not statea.marked or not stateb.marked:
        for k in to_visit:
            if (len(to_visit[k]) != 0):
                print "{}:{}".format(k, len(to_visit[k]))
        return None, None
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != None):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour)
    return createPath(statetuple)

def a_star_search_numpy_multi_STK(autA, autB, collA, collB, heurA, heurB, numpy_array_map, max_slot,
                                  num_resources, initial_resource_usage = None, init_STK = ()):
    def heur(sa, sb, contour):
        res, timen = ha[sa]
        heuristica = contour[res] + timen
        heuristicb = numpy.amax(numpy.add(contour, hb[sb]))
        return max(heuristica, heuristicb)
    initial = (autA.initial, autB.initial)
    look_back = {}
    wafer = 0
    if not autB.initial.get_outgoing()[0].label.name.startswith("ret"):
        wafer = int(autB.initial.get_outgoing()[0].label.name.split('-')[0])
    #print(wafer)
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        return ha, hb
    ha, hb = init()
    if initial_resource_usage == None:
        initial_resource_usage = numpy.array([0 for i in range(num_resources)], numpy.int32)
    #handle = file('astar', 'w')
    #maxvala = ha[autA.initial][1]
    #maxvalb = numpy.amax(hb[autB.initial])
    maxval = heur(autA.initial, autB.initial, initial_resource_usage)#max(maxvala, maxvalb)
    to_visit = {}
    to_visit[maxval] = [(initial, initial_resource_usage, None, 0, None, init_STK, None, wafer)]
    ks = []
    k = maxval
    #while k <= maxval:
    while True:
        def collision(slots):
            needs = set()
            slotsnums = collections.defaultdict(lambda: 0)
            for slot in slots:
                if (slot.startswith('!')):
                    needs.add(slot[1:])
                else:
                    num = slotsnums[slot]
                    num += 1
                    slotsnums[slot] = num
                    if num > max_slot[slot]:
                        return True
            for need in needs:
                if need not in slotsnums:
                    return True
            return False
        if k not in to_visit or len(to_visit[k]) == 0:
            #k += 1
            if (len(ks) == 0):
                break
            k = heapq.heappop(ks)
            continue
        statetuple, contour, event, weight, previous, STK, PSTK, wafer = to_visit[k].pop()
        if (statetuple, STK) in look_back:
            continue
        look_back[(statetuple, STK)] = (event, weight, (previous, PSTK))
        statea, stateb = statetuple
        #handle.write('c{}-{}-{}-{}\n'.format(collA[statea], collB[stateb], statea.number, stateb.number))
        if statea.marked and stateb.marked:
            #print 'marked'
            break
        for edge in statea.get_outgoing():
            nwafer = wafer
            if not edge.label.name.startswith('ret'):
                nwafer = int(edge.label.name.split('-')[0])
                if nwafer > wafer:
                    continue
                nwafer = max(wafer, nwafer+1)
            newtuple = (edge.succ, stateb)
            #handle.write('a{}-{}-{}-{}\n'.format(collA[edge.succ], collB[stateb], edge.succ.number, stateb.number))
            NSTK = STK
            if 'STK' in collA[edge.succ] or 'STK2' in collA[edge.succ]:
                if (len(STK) >= 16):
                    continue
                #print 'add to stack'
                split = edge.label.name.split('-')
                NSTK = tuple(list(STK) + [split[0]])
            elif 'STK' in collA[statea] or 'STK2' in collA[statea]:
                split = edge.label.name.split('-')
                if split[0] != STK[-1]:
                    continue
                NSTK = tuple(STK[:len(STK)-1])
            if ((newtuple, NSTK) in look_back):
                #handle.write('already\n')
                continue
            if collision(collA[edge.succ] + collB[stateb]):
                #print collA[edge.succ] + collB[stateb]
                #handle.write('coll\n')
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(edge.succ, stateb, newcontour)
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
                heapq.heappush(ks, heuristic)
            #handle.write('append\n')
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, NSTK, STK, nwafer))
        for edge in stateb.get_outgoing():
            nwafer = wafer
            if not edge.label.name.startswith('ret'):
                nwafer = int(edge.label.name.split('-')[0])
                if nwafer > wafer:
                    continue
                nwafer = max(wafer, nwafer+1)
            newtuple = (statea, edge.succ)
            #handle.write('b{}-{}-{}-{}\n'.format(collA[statea], collB[edge.succ], statea.number, edge.succ.number))
            #handle.write('{}\n'.format(edge.label.name))
            #handle.write('{}\n'.format(STK))
            NSTK = STK
            stkbef = 0
            stkaft = 0
            for place in collB[edge.succ]:
                if place in ['STK', 'STK2']:
                    stkaft += 1
            for place in collB[stateb]:
                if place in ['STK', 'STK2']:
                    stkbef += 1
            if stkbef < stkaft:
                if (len(STK) >= 16):
                    continue
                split = edge.label.name.split('-')
                NSTK = tuple(list(STK) + [split[0]])
            elif stkbef > stkaft:
                split = edge.label.name.split('-')
                if split[0] != STK[-1]:
                    continue
                NSTK = tuple(STK[:len(STK)-1])
            #handle.write('bleftstack\n')
            if ((newtuple, NSTK) in look_back):
                #handle.write('already\n')
                continue
            if collision(collA[statea] + collB[edge.succ]):
                #handle.write('coll\n')
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(statea, edge.succ, newcontour)
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
                heapq.heappush(ks, heuristic)
            #handle.write('append\n')
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, NSTK, STK, nwafer))
    if not statea.marked or not stateb.marked:
        for k in to_visit:
            if (len(to_visit[k]) != 0):
                print "{}:{}".format(k, len(to_visit[k]))
        return None, None
    statetuple = (statetuple, STK)
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        while statetuple != (None, None):
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != (None, None)):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour)
    return createPath(statetuple)

def a_star_search_numpy_multi_STK_PROJ(autA, autB, autC, collA, collB, collC, heurA, heurB, numpy_array_map, max_slot,
                                       num_resources, number):
    initial = (autA.initial, autB.initial, autC.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    handle = file('astarfile', 'w')
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    ha, hb = init()
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[autB.initial])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None, (), None)]
    #heurvalue = {}
    k = maxval
    infinity = float('inf')
    def heur(sa, sb):
        res, timen = ha[sa]
        heuristica = newcontour[res] + timen
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb)
    while k <= maxval:
        def collision(slots):
            needs = set()
            slotsnums = collections.defaultdict(lambda: 0)
            for slot in slots:
                if (slot.startswith('!')):
                    needs.add(slot[1:])
                else:
                    num = slotsnums[slot]
                    num += 1
                    slotsnums[slot] = num
                    if num > max_slot[slot]:
                        handle.write('s{}-{}\n'.format(slotsnums, slot))
                        return True
            for need in needs:
                if need not in slotsnums:
                    handle.write('n{}-{}\n'.format(slotsnums, need))
                    return True
            return False
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous, STK, PSTK = to_visit[k].pop()
        if (statetuple, STK) in look_back:
            continue
        look_back[(statetuple, STK)] = (event, weight, (previous, PSTK))
        handle.write('cstate-{}-{}\n'.format(collA[statetuple[0]],collB[statetuple[1]]))
        statea, stateb, statec = statetuple
        #print statetuple
        if statea.marked and stateb.marked:
            print 'marked'
            break
        for edge in statea.get_outgoing():
            #if (len(stateb.get_outgoing()) != 0 and not stateb.get_outgoing()[0].label.name.startswith('ret')):
             #   True
                #break
            newtuple = (edge.succ, stateb, statec)
            handle.write('nstatea-{}-{}\n'.format(collA[newtuple[0]],collB[newtuple[1]]))
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            NSTK = STK
            if 'STK' in collA[edge.succ] or 'STK2' in collA[edge.succ]:
                if (len(STK) >= 16):
                    continue
                #print 'add to stack'
                split = edge.label.name.split('-')
                NSTK = tuple(list(STK) + [split[0]])
            elif 'STK' in collA[statea] or 'STK2' in collA[statea]:
                split = edge.label.name.split('-')
                if split[0] != STK[-1]:
                    continue
                NSTK = tuple(STK[:len(STK)-1])
            handle.write('passed stack\n')
            if ((newtuple, NSTK) in look_back):
                handle.write('already\n')
                continue
            if collision(collA[edge.succ] + collB[stateb] + collC[statec]):
                #print collA[edge.succ] + collB[stateb]
                handle.write('coll\n')
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(edge.succ, stateb)
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            handle.write('append\n')
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, NSTK, STK))
            #k = min(heuristic, k)
        for edge in stateb.get_outgoing():
            if edge.label.name.startswith('ret'):
                print edge.label.name
            newtuple = (statea, edge.succ, statec)
            handle.write('nstateb-{}-{}\n'.format(collA[newtuple[0]],collB[newtuple[1]]))
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            NSTK = STK
            stkbef = 0
            stkaft = 0
            for place in collB[edge.succ]:
                if place in ['STK', 'STK2']:
                    stkaft += 1
            for place in collB[stateb]:
                if place in ['STK', 'STK2']:
                    stkbef += 1
            if stkbef < stkaft:
                if (len(STK) >= 16):
                    continue
                split = edge.label.name.split('-')
                NSTK = tuple(list(STK) + [split[0]])
            elif stkbef > stkaft:
                split = edge.label.name.split('-')
                if split[0] != STK[-1]:
                    continue
                NSTK = tuple(STK[:len(STK)-1])
            handle.write('passed stack\n')
            if ((newtuple, NSTK) in look_back):
                handle.write('already\n')
                continue
            if collision(collA[statea] + collB[edge.succ] + collC[statec]):
                handle.write('coll\n')
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(statea, edge.succ)
            #if heuristic >= heurvalue.get(newtuple, infinity):
            #    continue
            #heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            handle.write('appended\n')
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, NSTK, STK))
            #k = min(heuristic, k)
        for edge in statec.get_outgoing():
            newtuple = (statea, stateb, edge.succ)
            handle.write('nstatec-{}-{}\n'.format(collA[newtuple[0]],collB[newtuple[1]]))
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            NSTK = STK
            if ((newtuple, NSTK) in look_back):
                handle.write('already\n')
                continue
            if collision(collA[statea] + collB[stateb] + collC[edge.succ]):
                handle.write('coll\n')
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(statea, stateb)
            #if heuristic >= heurvalue.get(newtuple, infinity):
            #    continue
            #heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            handle.write('appended\n')
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, NSTK, STK))
            #k = min(heuristic, k)
    if not statea.marked or not stateb.marked:
        for k in to_visit:
            if (len(to_visit[k]) != 0):
                print "{}:{}".format(k, len(to_visit[k]))
        return None, None
    statetuple = (statetuple, STK)
    def createPath(statetuple):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        while statetuple != (None, None):
            event, weight, prevtuple = look_back[statetuple]
            if (prevtuple != (None, None)):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
            else:
                path.initial = state
            statetuple, state = prevtuple, prevstate
        return path, numpy.amax(contour)
    return createPath(statetuple)

def a_star_search_numpy_multi_optimal(autA, autB, collA, collB, heurA, heurB, numpy_array_map, max_slot,
                              num_resources):
    initial = (autA.initial, autB.initial)
    look_back = {}
    #maxvala = max([time for _, time in autA.initial.heur] + [0])
    #maxvalb = max([time for _, time in autB.initial.heur] + [0])
    def init():
        ha = {}
        for x in heurA:
            ha[x] = heurA[x][0]
        hb = heurB
        #hb = {}
        #for x in heurB:
        #    arr = [0 for i in range(len(resources))]
        #    for res, timeneeded in heurB[x]:
        #        arr[res] = timeneeded
        #    hb[x] = numpy.array(arr, numpy.int16)
        return ha, hb
    ha, hb = init()
    maxvala = ha[autA.initial][1]
    maxvalb = numpy.amax(hb[autB.initial])
    #maxvala = max([time for _, time in heurA[autA.initial]] + [0])
    #maxvalb = max([time for _, time in heurB[autB.initial]] + [0])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None, None)]
    heurvalue = {}
    k = maxval
    infinity = float('inf')
    def heur(sa, sb):
        res, timen = ha[sa]
        heuristica = newcontour[res] + timen
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb)
    while k <= maxval:
        def collision(slots):
            slotsnums = collections.defaultdict(lambda: 0)
            for slot in slots:
                num = slotsnums[slot]
                num += 1
                if num > max_slot[slot]:
                    return True
                slotsnums[slot] = num
            return False
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous, prevground = to_visit[k].pop()
        ground = tuple(numpy.subtract(contour, numpy.amin(contour)))
        if (statetuple, ground) in look_back:
            continue
        look_back[(statetuple, ground)] = (event, weight, previous, prevground)
        statea, stateb = statetuple
        if statea.marked and stateb.marked:
            break
        for edge in statea.get_outgoing():
            newtuple = (edge.succ, stateb)
            #if (newtuple in look_back):
            #    continue
            #if len(edge.succ.collisions.intersection(stateb.collisions)) != 0:
            if collision(collA[edge.succ] + collB[stateb]):
                continue
            #newcontour = progressivetimeoptimalsynthesis.res_plus_default(contour, edge, event_resource_map[edge.label])
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur] + [0])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in stateb.heur] + [0])
            #res, timen = ha[edge.succ]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[stateb]))
            #heuristic = max(heuristica, heuristicb)
            heuristic = heur(edge.succ, stateb)
            #if heuristic >= heurvalue.get(newtuple, infinity):
            #    continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, ground))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            #if (newtuple in look_back):
            #    continue
            #if len(edge.succ.collisions.intersection(statea.collisions)) != 0:
            if collision(collA[statea] + collB[edge.succ]):
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            #heuristica = max([newcontour[res] + timeneeded for res, timeneeded in statea.heur])
            #heuristicb = max([newcontour[res] + timeneeded for res, timeneeded in edge.succ.heur])
            #res, timen = ha[statea]
            #heuristica = newcontour[res] + timen
            #heuristicb = numpy.amax(numpy.add(newcontour, hb[edge.succ]))
            #heuristic = max(heuristica, heuristicb)
            heuristic = heur(statea, edge.succ)
            #if heuristic >= heurvalue.get(newtuple, infinity):
            #    continue
            heurvalue[newtuple] = heuristic
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple, ground))
    if not statea.marked or not stateb.marked:
        for k in to_visit:
            print "{}:{}".format(k, len(to_visit[k]))
        return None, None
    def createPath(statetuple, ground):
        path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
        prevstate = None
        state = path.add_new_state(True)
        while statetuple != None:
            event, weight, prevtuple, prevground = look_back[statetuple, ground]
            if (prevtuple != None):
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
            else:
                path.initial = state
            statetuple, state, ground = prevtuple, prevstate, prevground
        return path, numpy.amax(contour)
    return createPath(statetuple, ground)

def a_star_search_numpy_multi_lots(auts, autB, colls, collB, heurs, heurB, numpy_array_map, max_slot,
                                   num_resources, number):
    initial = (tuple([aut.initial for aut in auts]), autB.initial)
    autheur = [(auts[i], heurs[i]) for i in range(len(auts))]
    allowed = set()
    look_back = {}
    def init():
        m = 0
        ha = []
        hb = heurB
        for i in range(len(autheur)):
            aut, heur = autheur[i]
            h = {}
            for x in heur:
                h[x] = heur[x][0]
            autheur[i] = (aut, h)
            ha.append(h)
            m = max(m, h[aut.initial][1])
        return ha, hb, m
    ha, hb, maxvala = init()
    maxvalb = numpy.amax(hb[autB.initial])
    maxval = max(maxvala, maxvalb)
    zerocontour = numpy.array([0 for i in range(num_resources)], numpy.int32)
    to_visit = {}
    to_visit[maxval] = [(initial, zerocontour, None, 0, None)]
    k = maxval
    infinity = float('inf')
    def allmarked(stupl):
        for s in stupl:
            if not s.marked:
                return False
        return True
    def heur(sa, sb):
        heuristica = 0
        for i in range(len(sa)):
            res, timen = ha[i][sa[i]]
            heuristica = max(newcontour[res] + timen, heuristica)
        heuristicb = numpy.amax(numpy.add(newcontour, hb[sb]))
        return max(heuristica, heuristicb)
    while k <= maxval:
        def collision(slots):
            slotsnums = collections.defaultdict(lambda: 0)
            for slot in slots:
                num = slotsnums[slot]
                num += 1
                slotsnums[slot] = num
                if num > max_slot[slot]:
                    return True
            return False
        if k not in to_visit or len(to_visit[k]) == 0:
            k += 1
            continue
        statetuple, contour, event, weight, previous = to_visit[k].pop()
        if statetuple in look_back:
            continue
        look_back[statetuple] = (event, weight, previous)
        statea, stateb = statetuple
        if allmarked(statea) and stateb.marked:
            break
        for i in range(len(autheur)):
            for edge in statea[i].get_outgoing():
                if len(allowed) - i < number:
                    print 'continue'
                    continue
                allowed.add(edge.label.name.split('-')[0])
                nstatea = list(statea)
                nstatea[i] = edge.succ
                nstatea = tuple(nstatea)
                newtuple = (nstatea, stateb)
                if (newtuple in look_back):
                    continue
                colllist = []
                for i,s in enumerate(nstatea):
                    colllist.extend(colls[i][s])
                if collision(colllist + collB[stateb]):
                    continue
                newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
                heuristic = heur(nstatea, stateb)
                maxval = max(heuristic, maxval)
                if heuristic not in to_visit:
                    to_visit[heuristic] = []
                to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
        for edge in stateb.get_outgoing():
            newtuple = (statea, edge.succ)
            allowed.add(edge.label.name.split('-')[0])
            if (newtuple in look_back):
                continue
            colllist = []
            for i,s in enumerate(statea):
                colllist.extend(colls[i][s])
            if collision(colllist + collB[edge.succ]):
                continue
            newcontour = numpy_stack(contour, numpy_array_map[edge.label], edge.weight)
            heuristic = heur(statea, edge.succ)
            maxval = max(heuristic, maxval)
            if heuristic not in to_visit:
                to_visit[heuristic] = []
            to_visit[heuristic].append((newtuple, newcontour, edge.label, edge.weight, statetuple))
    if not allmarked(statea) or not stateb.marked:
        for k in to_visit:
            if (len(to_visit[k]) != 0):
                print "{}:{}".format(k, len(to_visit[k]))
        return None, None
    def createPath(statetuple):
        alph = auts[0].alphabet.union(autB.alphabet)
        path = weighted_structure.WeightedAutomaton(alph, autB.collection)
        state = path.add_new_state(True)
        while statetuple != None:
            event, weight, prevtuple = look_back[statetuple]
            if event in alph:
                #if event in autB.alphabet:
                #    print 'path:{}->{}'.format(collB[prevtuple[1]], collB[statetuple[1]])
                #else:
                #    print 'aut[0]:{}->{}'.format(colls[0][prevtuple[0][0]], colls[0][statetuple[0][0]])
                #print event
                prevstate = path.add_new_state(False)
                edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
                path.add_edge(edge)
                state = prevstate
            statetuple = prevtuple
        path.initial = state
        return path, numpy.amax(contour)
    return createPath(statetuple)

def trace_to_path_numpy_multi(trace, alphabet, coll, numpy_resource_map, num_resources, prev_auts, max_slot):
    path = weighted_structure.WeightedAutomaton(alphabet, coll)
    state = path.add_new_state(True)
    contour = numpy.array([0 for i in range(num_resources)], numpy.int8)
    heur = {}
    heur[state] = contour
    for edge in reversed(trace):
        event, weight = edge.label, edge.weight
        prevstate = path.add_new_state(False)
        edge = weighted_structure.WeightedEdge(prevstate, state, event, weight)
        path.add_edge(edge)
        contour = numpy_rev_stack(contour, numpy_resource_map[event], weight)
        heur[prevstate] = contour
        state = prevstate
    path.initial = state
    collisions = find_collisions(path, prev_auts, max_slot)
    return path, heur, collisions

def calculate_needed_trace(trace, initial_resources, numpy_array_map, init_state_floor, event_state_resource_map):
    events = set()
    wafer = 0
    first_event = 0
    contour = initial_resources
    contourupto = contour
    state_to_floor = init_state_floor
    floor_to_keep = state_to_floor.copy()
    for i, edge in enumerate(trace):
        if not edge.label.name.startswith('ret'):
            nwafer = int(edge.label.name.split('-')[0])
            if (nwafer >= wafer):
                wafer = nwafer+1
                first_event = i
                events.clear()
                contourupto = contour
                floor_to_keep = state_to_floor.copy()
        contour, early = numpy_stack_keep_early(contour, numpy_array_map[edge.label], edge.weight)
        for place in event_state_resource_map:
            state_to_floor[place] = early
        events.add(edge.label)
    return first_event, contourupto, events, floor_to_keep

def update_initial(aut, trace):
    state = aut.initial
    for edge in trace:
        if edge.label in aut.alphabet:
            autedge = state.get_outgoing()[0]
            assert (autedge.label == edge.label)
            state = autedge.succ
    aut.initial = state

def find_collisions(path, prev_auts, max_slot):
    collisions = collections.defaultdict(list)
    #retevents = set()
    #events = set()
    #state = path.initial
    #wafer = 0
    #while not state.marked:
    #    edge = state.get_outgoing()[0]
    #    if not edge.label.name.startswith('ret'):
    #        nwafer = int(edge.label.name.split('-')[0])
    #        if (nwafer >= wafer):
    #            wafer = nwafer+1
    #            events.clear()
    #    else:
    #        retevents.add(edge.label)
    #    events.add(edge.label)
    #    state = edge.succ
    #events.update(retevents)
    for aut, _, autcoll, _ in prev_auts:
        #if (events.isdisjoint(aut.alphabet)):
        #    continue
        path_state = path.initial
        aut_state = aut.initial
        while not path_state.marked:
            collisions[path_state].extend(autcoll[aut_state])
            #if (collision(collisions[path_state])):
                #print collisions[path_state]
            edge = path_state.get_outgoing()[0]
            path_state = edge.succ
            #print edge.label.name
            if edge.label in aut.alphabet:
                edge2 = None
                for edge2 in aut_state.get_outgoing():
                    if edge.label == edge2.label:
                        break
                assert edge2.label == edge.label
                aut_state = edge2.succ
        collisions[path_state].extend(autcoll[aut_state])
        assert aut_state.marked
    return collisions

def append_track_alignment(track_path, colls, track_event, track_places):
    track_path.alphabet.add(reticle_event)
    mstate = None
    for state in ret_path.get_states():
        if state.marked:
            mstate = state
    mstate.marked = True
    nstate = ret_path.add_new_state(True)
    edge = weighted_structure.WeightedEdge(mstate, nstate, reticle_event, 235)
    ret_path.add_edge(edge)
    colls[nstate] = [scanner_place]
    return edge

def append_reticle(ret_path, colls, reticle_event, scanner_place):
    ret_path.alphabet.add(reticle_event)
    mstate = None
    for state in ret_path.get_states():
        if state.marked:
            mstate = state
    mstate.marked = True
    nstate = ret_path.add_new_state(True)
    edge = weighted_structure.WeightedEdge(mstate, nstate, reticle_event, 235)
    ret_path.add_edge(edge)
    colls[nstate] = [scanner_place]
    return edge