Re: [Spot] Questions regarding handling of Kripke structures in Spot - Spot

5 Mar 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 &lt;patrick.halder(a)tum.de&gt; 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