22 Apr
2022
22 Apr
'22
2:16 p.m.
Hi Edmond,
Edmond Irani Liu <edmond.irani(a)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.