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

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):
    states_to_remove = []
    for state in aut.get_states():
        dict = {}
        states = set()
        for edge in state.get_incoming():
            split = edge.label.name.split('-')
            state.collisions = set([int(split[2])])

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_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.time()
        state_resources = set(state_resources)
        for aut in auts:
            set_collision_states(aut)
            mark_aut_reverse_djikstra(aut)
            autweights.append((aut, aut.initial.heur[0][1]))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        autweights.sort(key= lambda x: x[1])
        autweights.reverse()
        print(len(autweights))
        path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
        path.initial = path.add_new_state(True)
        path.initial.collisions = []
        path.initial.heur = []
        for (i, (aut,_)) in enumerate(autweights):
            if arbitrary == 1:
                path, weight = a_star_search(aut, path, resources)
            else:
                path, weight = a_star_search(aut, path, resources, state_resources)
            path.save_as_dot("path" + str(i) + ".dot")
            print "weight: " + str(weight)
            handle.write("weight: " + str(weight) + "\n")
            #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
            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_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, 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])
    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:
                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])
            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:
                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])
            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 k, values in to_visit.iteritems():
        print str(k) + ":" + str(len(values))
    assert(statea.marked and stateb.marked)
    path = weighted_structure.WeightedAutomaton(autA.alphabet.union(autB.alphabet), autA.collection)
    state = path.add_new_state(True)
    contour = zerocontour
    state.collisions = statetuple[0].collisions.union(statetuple[1].collisions)
    state.heur = [(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)
        else:
            path.initial = state
        statetuple, state = prevtuple, prevstate
    return path, progressivetimeoptimalsynthesis.ceil(contour)

def mark_aut_reverse_djikstra(aut):
    to_visit = {}
    to_visit[0] = list(filter(lambda state: state.marked, aut.get_states()))
    k = 0
    maxval = 0
    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'):
            continue
        state.heur = [(frozenset(aut.alphabet), k)]
        for edge in state.get_incoming():
            if hasattr(edge.pred, '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)

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):
    not_used = set([35,36,39,40])
    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)]
        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(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(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 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
            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)
    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].split('_')[1]
        state_resources[split[1].split('_')[1]].append(event)
        state_resources[split[2].split('_')[1]].append(event)
        return "(" + split[1] + "," + split[2] + "," + event + "," + weight + ")"
    string += "transitions = " + ','.join(map(transition, transitions)) + "\n"
    string += "initial-state = start_\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)
    return make_path_wafer(auts, resources, state_resources)

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

def set_collision_states_wafer(aut):
    for state in aut.get_states():
        for edge in state.get_incoming():
            split = edge.label.name.split('-')
            statecol = split[2].split('_')[1]
            if state != '':
                state.collisions = set([statecol])

def make_path_wafer(auts, resources, state_resources):
    handle = file('resultswafer', 'w')
    for arbitrary in [1]:
        autweights = []
        dur = -time.time()
        state_resources = set(state_resources)
        for aut in auts:
            set_collision_states_wafer(aut)
            mark_aut_reverse_djikstra(aut)
            autweights.append((aut, aut.initial.heur[0][1]))
            #autweights.append((aut, progressivetimeoptimalsynthesis.make_prog_supervisor_all_controllable([aut], frozenset(aut.alphabet), resources)[1]))
        autweights.sort(key= lambda x: x[1])
        autweights.reverse()
        print(len(autweights))
        path = weighted_structure.WeightedAutomaton(set(), auts[0].collection)
        path.initial = path.add_new_state(True)
        path.initial.collisions = []
        path.initial.heur = []
        for (i, (aut,_)) in enumerate(autweights):
            if arbitrary == 1:
                path, weight = a_star_search(aut, path, resources)
            else:
                path, weight = a_star_search(aut, path, resources, state_resources)
            path.save_as_dot("path" + str(i) + ".dot")
            print "weight: " + str(weight)
            handle.write("weight: " + str(weight) + "\n")
            #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
            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
