move function _ts_ba_sync_prod from automata to transys
fix imports and calls related to _ts_ba_sync_prod

When BuchiAutomaton.sync_prod calls _ba_ts_sync_prod, the 1st argument is self, so certainly a BuchiAutomaton. The 2nd argument is not checked in automata._ba_ts_sync_prod, to avoid a circular dependency. Function _ba_ts_sync_prod needs to initialize a BuchiAutomaton, so it must know about the class BuchiAutomaton (i.e., it needs it for more than type checking).

So the 2nd argument is type-checked in transys.transys._ts_ba_sync_prod. The function _ts_ba_sync_prod is now in transys, so it knows about the class FiniteTransitionSystem and can use it for type checking. The real reason _ts_ba_sync_prod needs to be in transys is because it initializes a FiniteTransitionSystem object.

The above ensure that both arguments to BA * TS eventually get type checked.

The other way, when using TS * BA, the TS is self, so a FiniteTransitionSystem, but BA cannote be type checked within tulip.transys.transys w/o introducing a circular dependency on tulip.transys.automata. Instead, it is checked whether the buchi_automaton argument has an 'alphabet' attribute.

Note that usage of isinstance (so type checking) is not so pythonic in the first place, so it may be relaxed in the future. Nonetheless, it aided debugging during initial development.