25 Oct
2011
25 Oct
'11
12:35 p.m.
Hi Alexandre,
OK, I should have checked the source. The text on what to implement when
interfacing with Spot suggests that this may be necessary but does not
provide any details so I assumed I had to implement the method.
You are right of course, I hadn't thought it through properly.
OK, thanks. Many thanks for the answers too, they are very helpful in
understanding Spot!
Nikos
Where aut is
the product and proj is automaton A. I have also written (what
I think are reasonable) project_state methods for A and B.
I believe you should not have to write anything. There is a default
implementation in the
TGBA class: This method
is
never called on B (perhaps because the complementation algorithm intercepts
that?).
I don't think it would make sense to have project_state() traverse the
complementation: if a run is accepted by !B we don't expect it to map
to a run of B... I think the projection only projects the states, but
it does nothing
for the labels and acceptance sets of the transitions, so those might
not match actual transition of the original automaton. Hence
replayrun() will fail.
In practice, replayrun() was mainly a tool for us to debug the
emptiness checks, so I have never tried to run it on a projection. I
can see how it would make sense, though.
It's not clear to me how to fix the project_run to use only the
transition from the considered automaton. Actually I believe there
are cases where you cannot decide which transition to use in the
considered automaton if you do not know the other automata involved in
the product... Maybe it is easier to project such a run with some
additional hypotheses on the automaton you project onto (e.g. it has
no acceptance sets and has no more than one transition between two
given states) but then it become a projection specialized to a
subclass of automata.
It makes sense that the transitions of the product may not be
projectable back onto the original automaton. In any case I can do
without them, as my automaton is very deterministic and by looking at
the states I can deduce the transitions as you say.
The reason I used replayrun instead of print_tgba_run is the hint in the
documentation that print_tgba_run may print something which is not an
actual accepting run. I assume that this only applies to bit-hashing
emptiness checks, but couldn't know for sure.
PS this is
with the patch to the safra complementation algorithm.
FWIW, that patch was incomplete. I have made further tests yesterday
with Martin's test case, a discovered that
the all_acceptance_conditions() method of Safra automata was still
incorrect. Also there where some collisions
in the names of states output by format_state() (this only matters
when trying to output Safra automata as text files for debugging, not
when using them in a product), and a few other minor nits. The set of
three patches I have finally applied is different from the small patch
I sent, you can find them here:
http://git.lrde.epita.fr/?p=spot.git;a=patch;h=a4d1e18b;hp=101b18b2
(I'll probably have a snapshot ready in a couple of days.)