Hi Edmond, Edmond Irani Liu <edmond.irani@tum.de> writes:
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.
1. If I understand this page correctly, we need to append a new
(Beware that we recently found out that the example on https://spot.lrde.epita.fr/tut12.html was incorrectly using remove_ap() to remove "alive" propositions. The current development version as a to_finite() method to fix the automaton when one want to remove the "alive" see https://spot-dev.lrde.epita.fr/tut12.html instead. Furtunately, you seem to keep those dead propositions, so you should be fine.)
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.
This looks fine to me.
2. 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.
You already know how to build the intersection with product(). You can take the union with product_or(). Finally you can remove all those states that cannot reach an accepting cycle by using scc_filter(). p1 = spot.scc_filter(spot.product(ts, ltlf1)) p2 = spot.scc_filter(spot.product(ts, ltlf2)) p = spot.scc_filter(spot.product_or(p1, p2)) (Also be very wary of paralellizing code using Spot. These automata are labeled by BDDs and most BDD operations are not thread safe. It is safer to do these products in separate processes.)
3. 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.
Unfortunately the Python documentation is a bit lacking. We only have code examples. The rest of the documentation is the Doxygen documentation for the C++ classes at https://spot.lrde.epita.fr/doxygen/ but almost all of the Python bindings are generated automatically from the C++ interface.