[Spot] spot-beginner questions

Hi,

I'm trying to learn spot, and I want to run an emptiness check on a product of two automata which I will be creating by subclassing tgba.

The two automata have overlapping, but different, signatures i.e. atomic propositions. If I understand correctly, I cannot achieve this by using two different bdd_dicts, as the two automata passed to the product object must share the same bdd_dict.

How does one deal with this problem in spot?

Thanks Nikos