diff --git a/ChangeLog b/ChangeLog index be83b3bd7..cc6546f1b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2003-10-08 Alexandre Duret-Lutz + * iface/gspn/ltlgspn.cc: Use command-line options to + select algorithms, not #defines. + * iface/gspn/Makefile.am (check_PROGRAMS): Remove eltlgspn-srg, + efmgspn-srg, fmgspn-rg, and fmgspn-srg and their associated + source variables. These are all replaced by + ltlgspn-rg and ltlgspn-srg. + * iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test, + iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test, + iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, + iface/gspn/udcsltl.test: Adjust calls to ltlgspn-srg. + * iface/gspn/Makefile.am (XFAIL_TESTS): Remove. 2003-10-06 Rachid REBIHA @@ -1691,7 +1702,7 @@ now that CVS Bison is fixed. * src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning. -2003-04-24 Rachid REBIHA +2003-04-24 Rachid REBIHA * src/ltltest/tostring.test: New file. * src/ltltest/tostring.cc: New files. diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index d445b188c..22b2ad947 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -15,11 +15,7 @@ check_PROGRAMS = \ dottygspn-rg \ dottygspn-srg \ ltlgspn-rg \ - ltlgspn-srg \ - eltlgspn-srg \ - efmgspn-srg \ - fmgspn-rg \ - fmgspn-srg + ltlgspn-srg dottygspn_rg_SOURCES = dottygspn.cc dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) @@ -33,22 +29,6 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) ltlgspn_srg_SOURCES = ltlgspn.cc ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -eltlgspn_srg_SOURCES = ltlgspn.cc -eltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -eltlgspn_srg_CPPFLAGS = -DCEC $(AM_CPPFLAGS) - -efmgspn_srg_SOURCES = ltlgspn.cc -efmgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -efmgspn_srg_CPPFLAGS = -DCEC -DFM $(AM_CPPFLAGS) - -fmgspn_rg_SOURCES = ltlgspn.cc -fmgspn_rg_CPPFLAGS = -DFM $(AM_CPPFLAGS) -fmgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) - -fmgspn_srg_SOURCES = ltlgspn.cc -fmgspn_srg_CPPFLAGS = -DFM $(AM_CPPFLAGS) -fmgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) - EXTRA_DIST = \ examples/DCSwave/DCSWave.def \ examples/DCSwave/DCSWave.net \ diff --git a/iface/gspn/dcswaveeltl.test b/iface/gspn/dcswaveeltl.test index 25533fa7f..f19a87a68 100755 --- a/iface/gspn/dcswaveeltl.test +++ b/iface/gspn/dcswaveeltl.test @@ -6,8 +6,8 @@ cp -R $srcdir/examples/DCSwave . chmod +w DCSwave # G(ATTiIDLj => F(!SCj U SCi)) is true -../eltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 +../ltlgspn-srg -c -l -e DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 # G(F(!SCj U SCi)) is false -../eltlgspn-srg DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output +../ltlgspn-srg -c -l -e DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output test $? = 1 || exit 1 diff --git a/iface/gspn/dcswavefm.test b/iface/gspn/dcswavefm.test index 989a46cfb..4ccdc5749 100755 --- a/iface/gspn/dcswavefm.test +++ b/iface/gspn/dcswavefm.test @@ -6,8 +6,8 @@ cp -R $srcdir/examples/DCSwave . chmod +w DCSwave # G(ATTiIDLj => F(!SCj U SCi)) is true -../fmgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 +../ltlgspn-srg -c -f -m DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 # G(F(!SCj U SCi)) is false -../fmgspn-srg DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output +../ltlgspn-srg -c -f -m DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output test $? = 1 || exit 1 diff --git a/iface/gspn/dcswaveltl.test b/iface/gspn/dcswaveltl.test index 8690396dd..8dd7fc2ed 100755 --- a/iface/gspn/dcswaveltl.test +++ b/iface/gspn/dcswaveltl.test @@ -6,8 +6,8 @@ cp -R $srcdir/examples/DCSwave . chmod +w DCSwave # G(ATTiIDLj => F(!SCj U SCi)) is true -../ltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 +../ltlgspn-srg -c -l -m DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output || exit 1 # G(F(!SCj U SCi)) is false -../ltlgspn-srg DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output +../ltlgspn-srg -c -l -m DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output test $? = 1 || exit 1 diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index f8dd3724a..1f66fdc46 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -8,75 +8,146 @@ #include "tgbaalgos/magic.hh" #include "tgbaalgos/emptinesscheck.hh" +void +syntax(char* prog) +{ + std::cerr << "Usage: "<< prog + << " [OPTIONS...] model formula props..." << std::endl + << std::endl + << " -c compute a counter example" << std::endl + << " (instead of just checking for emptiness)" << std::endl + << std::endl + << " -e use Couvreur's emptiness-check (default)" << std::endl + << " -m degeneralize and perform a magic-search" << std::endl + << std::endl + << " -l use Couvreur's LaCIM algorithm for translation (default)" + << std::endl + << " -f use Couvreur's FM algorithm for translation" + << std::endl; + exit(2); +} + int main(int argc, char **argv) try { + int formula_index = 1; + enum { Couvreur, Magic } check = Couvreur; + enum { Lacim, Fm } trans = Lacim; + bool compute_counter_example = false; + spot::gspn_environment env; - if (argc <= 3) + while (formula_index < argc && *argv[formula_index] == '-') { - std::cerr << "usage: " << argv[0] - << " model formula props..." << std::endl; - exit(1); + if (!strcmp(argv[formula_index], "-c")) + { + compute_counter_example = true; + } + else if (!strcmp(argv[formula_index], "-e")) + { + check = Couvreur; + } + else if (!strcmp(argv[formula_index], "-m")) + { + check = Magic; + } + else if (!strcmp(argv[formula_index], "-l")) + { + trans = Lacim; + } + else if (!strcmp(argv[formula_index], "-f")) + { + trans = Fm; + } + else + { + syntax(argv[0]); + } + ++formula_index; } + if (argc < formula_index + 4) + syntax(argv[0]); - while (argc > 3) + + while (argc > formula_index + 2) { env.declare(argv[argc - 1]); --argc; } spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[2], pel, env); + spot::ltl::formula* f = spot::ltl::parse(argv[formula_index + 1], + pel, env); - if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel)) - exit(1); + if (spot::ltl::format_parse_errors(std::cerr, + argv[formula_index + 1], pel)) + exit(2); + argv[1] = argv[formula_index]; spot::gspn_interface gspn(2, argv); spot::bdd_dict* dict = new spot::bdd_dict(); -#if FM - spot::tgba* a_f = spot::ltl_to_tgba_fm(f, dict); -#else - spot::tgba* a_f = spot::ltl_to_tgba_lacim(f, dict); -#endif + spot::tgba* a_f = 0; + switch (trans) + { + case Fm: + a_f = spot::ltl_to_tgba_fm(f, dict); + break; + case Lacim: + a_f = spot::ltl_to_tgba_lacim(f, dict); + break; + } spot::ltl::destroy(f); spot::tgba* model = new spot::tgba_gspn(dict, env); spot::tgba_product* prod = new spot::tgba_product(model, a_f); -#if CEC - { - spot::emptiness_check empty_check; - bool res = empty_check.tgba_emptiness_check(prod); - if (!res) - { - empty_check.counter_example(prod); -std::cout << empty_check.print_result(std::cout, prod, model); - exit(1); - } - else - { - std::cout << "not found"; - } - } -#else - spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); - { - spot::magic_search ms(d); - if (ms.check()) + switch (check) + { + case Couvreur: { - ms.print_result (std::cout, model); - exit(1); + spot::emptiness_check ec; + bool res = ec.tgba_emptiness_check(prod); + if (!res) + { + if (compute_counter_example) + { + ec.counter_example(prod); + ec.print_result(std::cout, prod, model); + } + else + { + std::cout << "non empty" << std::endl; + } + exit(1); + } + else + { + std::cout << "empty" << std::endl; + } } - else + break; + case Magic: { - std::cout << "not found"; + spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); + spot::magic_search ms(d); + + if (ms.check()) + { + if (compute_counter_example) + ms.print_result (std::cout, model); + else + std::cout << "non-empty" << std::endl; + exit(1); + } + else + { + std::cout << "empty" << std::endl; + } + delete d; } - } - delete d; -#endif + } delete prod; delete model; delete a_f; diff --git a/iface/gspn/udcsefm.test b/iface/gspn/udcsefm.test index ed909e1ec..988eae037 100755 --- a/iface/gspn/udcsefm.test +++ b/iface/gspn/udcsefm.test @@ -6,12 +6,12 @@ cp -R $srcdir/examples/udcs . chmod +w udcs # F(ReP1 => F(gsP1)) is false -../efmgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -f -e udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 # !F(ReP1 => F(gsP1)) is true -../efmgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 +../ltlgspn-srg -c -f -e udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 # !G(ReP1 => F(gsP1)) is false -../efmgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -f -e udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 diff --git a/iface/gspn/udcseltl.test b/iface/gspn/udcseltl.test index 61c210eaa..f7899bfdb 100755 --- a/iface/gspn/udcseltl.test +++ b/iface/gspn/udcseltl.test @@ -6,12 +6,12 @@ cp -R $srcdir/examples/udcs . chmod +w udcs # F(ReP1 => F(gsP1)) is false -../eltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -l -e udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 # !F(ReP1 => F(gsP1)) is true -../eltlgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 +../ltlgspn-srg -c -l -e udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 # !G(ReP1 => F(gsP1)) is false -../eltlgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -l -e udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 diff --git a/iface/gspn/udcsfm.test b/iface/gspn/udcsfm.test index 4de91e2e0..e1c979f0c 100755 --- a/iface/gspn/udcsfm.test +++ b/iface/gspn/udcsfm.test @@ -6,12 +6,12 @@ cp -R $srcdir/examples/udcs . chmod +w udcs # F(ReP1 => F(gsP1)) is false -../fmgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -f -m udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 # !F(ReP1 => F(gsP1)) is true -../fmgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 +../ltlgspn-srg -c -f -m udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 # !G(ReP1 => F(gsP1)) is false -../fmgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -f -m udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 diff --git a/iface/gspn/udcsltl.test b/iface/gspn/udcsltl.test index 7b0d861b2..e57af8ff4 100755 --- a/iface/gspn/udcsltl.test +++ b/iface/gspn/udcsltl.test @@ -6,12 +6,12 @@ cp -R $srcdir/examples/udcs . chmod +w udcs # F(ReP1 => F(gsP1)) is false -../ltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -l -m udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1 # !F(ReP1 => F(gsP1)) is true -../ltlgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 +../ltlgspn-srg -c -l -m udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1 # !G(ReP1 => F(gsP1)) is false -../ltlgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output +../ltlgspn-srg -c -l -m udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output test $? = 1 || exit 1