alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition):

Browse source 
Make sure to create the source state before the destination state.
This commit is contained in:
Alexandre Duret-Lutz 2004-12-09 08:20:12 +00:00
parent d645e0ac54
commit d4b9ebaaff
2 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,8 @@
2004-12-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition):
Make sure to create the source state before the destination state.
2004-12-08 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr> 2004-12-08 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbaalgos/emptiness.cc: Suppress a horrible space before a ')'. * src/tgbaalgos/emptiness.cc: Suppress a horrible space before a ')'.
@ -7,9 +12,9 @@
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(set_init_state): Return a pointer to the initial state. (set_init_state): Return a pointer to the initial state.
* src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc
(tgba_run_to_tgba): New function. (tgba_run_to_tgba): New function.
* src/tgbatest/ltl2tgba.cc: Add option -G. * src/tgbatest/ltl2tgba.cc: Add option -G.
2004-12-08 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-12-08 Alexandre Duret-Lutz <adl@src.lip6.fr>

6
src/tgba/tgbaexplicit.cc
View file

@ -175,7 +175,11 @@ namespace spot
tgba_explicit::create_transition(const std::string& source, tgba_explicit::create_transition(const std::string& source,
const std::string& dest) const std::string& dest)
{ {
return create_transition(add_state(source), add_state(dest)); // It's important that the source be created before the
// destination, so the first encountered source becomes the
// default initial state.
state* s = add_state(source);
return create_transition(s, add_state(dest));
} }
void void