[Spot] Question regarding Spot operations on automata

Dear Spot team, greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool! I have been using Spot lately, and have a few questions regarding automata manipulation in Spot. I attach a Jupyter notebook explaining my use case: we are using spot to compute the product automata of some LTLf formulas and our system described in Kripke structure. If I understand this (https://spot.lrde.epita.fr/tut12.html) page correctly, we need to append a new state at the end of the system that holds a proposition which becomes inactive at the end of our system. Could you give us a quick feedback if our formulation in the notebook is correct? There states z1-z8 are system states, and z9 is the extra state for Spot to correctly handle LTLf formulas. As we are trying to obtain the product automaton of a relatively large formula with our system, we assume that breaking down the formula and paralellizing the computation will observe a speed up in the computation. We would like to inquire if there exist operations like taking the union or intersection of the accepting runs of the automata? The concrete example is illustrated in the note book. Is there a documentation available somewhere explaining the functions of objects in the Python wrapper? I tried looking around but couldn't find one explaining those. An example is also attached. Thank you for your attention. Looking forward to hearing from you. Kind Regards, Edmond