def get_pins(line):
    """ Extract the pin names from the vector line """
    line = line.replace('{','')
    line = line.replace(')','')
    line = line.replace('(','')
    bits = line.split(',')
    return [s.strip() for s in bits[1:]]