[Spot] Questions regarding handling of Kripke structures in Spot

Alexandre Duret-Lutz adl at lrde.epita.fr
Tue Mar 5 10:49:47 CET 2019


Dear Patrick,

(Please keep the mailing list in copy so that these explanations get
archived and then indexed by search engines.)

On Tue, Mar 5, 2019 at 8:58 AM Halder, Patrick <patrick.halder at tum.de> wrote:
> When I have the twa_product automaton with its respective acceptance states,
> how can I find out, to which states of my original Kripke structure they correspond to.
> I read somewhere in the spot examples that the labeling of the twa_product states
> (of the form <*,*>) has just cosmetic reasons and does therefor not give any help.

Let's say you have built the product between two automata autx and auty:

prod = spot.product(autx, auty)

then

pairs = prod.get_product_states()

will return an array of pairs of the form [(x0,y0),(x1,y1),....].
State i in the product corresponds to states pairs[i][0] in autx, and
pairs[i][1] in auty.

See https://spot.lrde.epita.fr/ipynb/product.html around cell 10 for a
concrete example, and a tip about using show("1") in this context.


> Is it even possible to do this, meaning getting directly from the acc states of the product automaton to the acc states/runs of the Kripke structure?

You should probably look for the accepting SCCs of the product, not
only its accepting states.

You could list all states that belong to acceptings SCCs of the
product with something like

si = spot.scc_info(prod)
n = si.scc_count()
for i in range(n):
    if si.is_accepting_scc(i):
        for s in si.states_of(i):
            print(s)

Unfortunately, we do not yet have any online example of use of
scc_info in Python.  You can find some in the test suite, or simply
look at the C++ documentation for this class
https://spot.lrde.epita.fr/doxygen/classspot_1_1scc__info.html

> Or do I have to get the accepting runs of the product automaton, e.g., with the x.intersecting_run(y) method and reason with it about the accepting runs in the Kripke structure?

This will only return one accepting run.

-- 
Alexandre Duret-Lutz


More information about the Spot mailing list