24 Oct
2011
24 Oct
'11
7:20 p.m.
Hi Nikos,
On Mon, Oct 24, 2011 at 5:52 PM, Nikos Gorogiannis
<nikos.gorogiannis(a)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