22 Apr
2022
22 Apr
'22
5:32 a.m.
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
22 Apr
22 Apr
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.
1020
days inactive
1020
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Edmond Irani Liu