diff --git a/ChangeLog b/ChangeLog index ac38e6319..21d40e7f2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2004-01-06 Alexandre Duret-Lutz + * iface/gspn/ltleesrg.cc: Emptinesscheck the full product, not + the control automaton. + * iface/gspn/eesrg.cc (tgba_gspn_eesrg::project_state): New method. * iface/gspn/eesrg.hh: Likewise. diff --git a/iface/gspn/ltleesrg.cc b/iface/gspn/ltleesrg.cc index 734aafbeb..91618593f 100644 --- a/iface/gspn/ltleesrg.cc +++ b/iface/gspn/ltleesrg.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -69,12 +69,12 @@ main(int argc, char **argv) { spot::tgba_gspn_eesrg a(dict, env, prod); - spot::emptiness_check ec(prod); + spot::emptiness_check ec(&a); bool res = ec.check(); if (!res) { ec.counter_example(); - ec.print_result(std::cout, prod); + ec.print_result(std::cout, &a); exit(1); } else