#!/usr/bin/env python3
import spot
from sys import argv
spot.setup()

def complement(f):
    detf = spot.tgba_determinize(f)
    notf = spot.dtwa_complement(detf)
    return notf
    # f.acc().set_acceptance(f.acc().get_acceptance().complement())

auts = []
notauts = []
for i in range(1,len(argv)):
    auts.append(spot.automaton(argv[i]))
    notauts.append(complement(spot.automaton(argv[i])))

#sanity check
for i in range(len(auts)):
    posneg = auts[i].intersecting_word(notauts[i])
    negpos = notauts[i].intersecting_word(auts[i])
    if (not posneg is None) or (not negpos is None):
        print('weird: product of', argv[i+1],'with own complement not empty!')
        exit(1)

for i in range(len(auts)):
    for j in range(i+1,len(auts)):
        print(argv[1+i],'intersect',argv[1+j])
        print(auts[i].intersecting_word(auts[j]))
        print(argv[1+j],'intersect',argv[1+i])
        print(auts[j].intersecting_word(auts[i]))

        print(argv[1+i],'\\',argv[1+j])
        print(auts[i].intersecting_word(notauts[j]))
        print(argv[1+j],'\\',argv[1+i])
        print(auts[j].intersecting_word(notauts[i]))