* 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.

ChangeLog

+2004-04-17  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* 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  <Souheib.Baarir@lip6.fr>
 	    Alexandre Duret-Lutz  <adl@src.lip6.fr>
 

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
+		    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);