Hi Nikos, On Mon, Oct 24, 2011 at 5:52 PM, Nikos Gorogiannis <nikos.gorogiannis@eecs.qmul.ac.uk> wrote:
Hi,
I am checking emptiness of a product of an automaton A with the complement of another automaton B, as usual. I would like to project a run of the product to a run on A. I am trying to do this as follows.
spot::emptiness_check * ec = new spot::couvreur99_check(aut); spot::emptiness_check_result * res = ec->check(); spot::tgba_run* run = res->accepting_run(); spot::tgba_run * projrun = spot::project_tgba_run(aut, proj, run);
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: state* tgba::project_state(const state* s, const tgba* t) const { if (t == this) return s->clone(); return 0; }
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...
However, if I try to use replay_run of the projected run, I get the message below, when setting debug=true. With debug=false, I get a segfault.
state 1 in prefix: transition with label=p_0 & !p_1 & !p_2 and acc= state 2 in cycle: S1 t_1,t_2 ERROR: no transition with label=p_0 & p_1 & !p_2 and acc={Acc["1$1"]} leaving state 2 for state S3 t_1,t_2 The following transitions leave state 2: * S2 label=p_1 & !p_0 & !p_2 and acc= going to S2 t_2 * S3 label=p_0 & p_1 & !p_2 and acc= going to S3 t_1,t_2
Am I doing something obviously wrong here?
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.
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.) -- Alexandre Duret-Lutz