diff --git a/ChangeLog b/ChangeLog index eb3cf7780..481c14d5e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2004-04-17 Alexandre Duret-Lutz + + * iface/gspn/ltlgspn.cc (main) [!SSP]: Do not accept -e3, -e4, or -e5. + (main) [SSP]: Use the standard counter-example computation + for -e and -e1. + 2004-04-15 Soheib Baarir Alexandre Duret-Lutz diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 860c19a3b..2bf5523cf 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -98,6 +98,7 @@ main(int argc, char **argv) { check = Couvreur2; } +#ifdef SSP else if (!strcmp(argv[formula_index], "-e3")) { check = Couvreur3; @@ -110,6 +111,7 @@ main(int argc, char **argv) { check = Couvreur5; } +#endif else if (!strcmp(argv[formula_index], "-m")) { check = Magic; @@ -230,7 +232,15 @@ main(int argc, char **argv) #ifndef SSP ce = new spot::counter_example(ecs); #else - ce = spot::counter_example_ssp(ecs); + switch (check) + { + case Couvreur: + case Couvreur2: + ce = new spot::counter_example(ecs); + break; + default: + ce = spot::counter_example_ssp(ecs); + } #endif ce->print_result(std::cout, proj ? model : 0); ce->print_stats(std::cout);