Hi Alexandre,
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:
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.
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...
You are right of course, I hadn't thought it through properly.
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.)
OK, thanks. Many thanks for the answers too, they are very helpful in understanding Spot!
Nikos