From a67e2d0b237d0fac3b7037f567330d858b7d2b51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Nov 2004 12:28:47 +0000 Subject: [PATCH] * iface/gspn/ltlgspn.cc (main): Adjust to recent changes to src/tgbaalgos/magic.cc, call explicit_magic_search() instead of building a spot::magic_search. * iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run(). --- ChangeLog | 7 +++++++ iface/gspn/ltlgspn.cc | 5 +++-- iface/gspn/udcseltl.test | 4 ++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0b5ed78d6..0517916c2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2004-11-10 Alexandre Duret-Lutz + + * iface/gspn/ltlgspn.cc (main): Adjust to recent changes to + src/tgbaalgos/magic.cc, call explicit_magic_search() instead of + building a spot::magic_search. + * iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run(). + 2004-11-09 Alexandre Duret-Lutz * src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index ccd67ec24..382f051cf 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -302,9 +302,9 @@ main(int argc, char **argv) case Magic: { spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); - spot::magic_search ms(d); + spot::emptiness_check* ec = spot::explicit_magic_search(d); - spot::emptiness_check_result* res = ms.check(); + spot::emptiness_check_result* res = ec->check(); if (res) { if (compute_counter_example) @@ -331,6 +331,7 @@ main(int argc, char **argv) { std::cout << "empty" << std::endl; } + delete ec; delete d; } } diff --git a/iface/gspn/udcseltl.test b/iface/gspn/udcseltl.test index 351306aa9..606fbd7c0 100755 --- a/iface/gspn/udcseltl.test +++ b/iface/gspn/udcseltl.test @@ -22,6 +22,6 @@ chmod +w udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 ../ltlgspn-srg -d dead -c -l -e2 udcs/udcs \ '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -grep 'dead:0' output -grep 'dead:1' output && exit 1 +grep ' !dead' output +grep ' dead' output && exit 1 :