new: OnTheFlyProductAutomaton

to incrementally build the automaton from a TS and a BA.
It has methods to add the successors of a specific state to the state space and to iteratively repeat this until the state space does not increase any more.

find_prod_succ has been adapted to recognize whether it is given a product BA or a product TS, and annotate it accordingly.
This allows using it in both OnTheFlyAutomaton.add_successors and ts_ba_sync_prod.
Ideally the latter should be implemented by creating a generic OnTheFly class and calling its "add_all_states" method.
bugfix: do not use next_sqs twice
housekeeping
reduce type checking in ts_ba_sync_prod