Merge emptiness-checks tests into ltl2tgba.

* src/tgbatest/Makefile (check_PRORGRAMS): Remove
emptinesscheck and ltlmagic.
(emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove.
(TESTS): Replace emptinesscheck.test and ltlmagic.test by
emptchk.test.
* src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test:
Delete.
* src/tgbatest/emptchk.test: New file.
* src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc:
Delete.
* src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n.

ChangeLog

@@ -1,5 +1,18 @@
 2003-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	Merge emptiness-checks tests into ltl2tgba.
+	* src/tgbatest/Makefile (check_PRORGRAMS): Remove
+	emptinesscheck and ltlmagic.
+	(emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove.
+	(TESTS): Replace emptinesscheck.test and ltlmagic.test by
+	emptchk.test.
+	* src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test:
+	Delete.
+	* src/tgbatest/emptchk.test: New file.
+	* src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc:
+	Delete.
+	* src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n.
+
 	* src/tgbaalgos/emptinesscheck.cc
 	(emptiness_check::tgba_emptiness_check): Do not print anything.
 	(emptiness_check::counter_example): Assume that tgba_emptiness_check

src/tgbatest/Makefile.am

@@ -6,11 +6,9 @@ check_SCRIPTS = defs
 check_PROGRAMS = \
   bddprod \
   explicit \
-  emptinesscheck \
+  emptinesscheckexplicit \
-emptinesscheckexplicit \
   explprod \
   ltl2tgba \
-  ltlmagic \
   ltlprod \
   mixprod \
   readsave \
@@ -20,12 +18,10 @@ emptinesscheckexplicit \
 # Keep this sorted alphabetically.
 bddprod_SOURCES  = ltlprod.cc
 bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
-emptinesscheck_SOURCES = emptinesscheck.cc
 emptinesscheckexplicit_SOURCES = emptinesscheckexplicit.cc
 explicit_SOURCES = explicit.cc
 explprod_SOURCES = explprod.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
-ltlmagic_SOURCES = ltlmagic.cc
 ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
 readsave_SOURCES = readsave.cc
@@ -46,9 +42,8 @@ TESTS = \
   explpro3.test \
   tripprod.test \
   mixprod.test \
-  emptinesscheck.test \
+  emptchk.test \
   emptinesscheckexplicit.test \
-  ltlmagic.test \
   spotlbtt.test
 
 EXTRA_DIST = $(TESTS)

src/tgbatest/emptchk.test

@@ -0,0 +1,42 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+expect_ce()
+{
+  ./ltl2tgba -e "$1"
+  ./ltl2tgba -e -D "$1"
+  ./ltl2tgba -e -f "$1"
+  ./ltl2tgba -e -f -D "$1"
+  ./ltl2tgba -m "$1"
+  ./ltl2tgba -m -f "$1"
+}
+
+expect_no()
+{
+  ./ltl2tgba -E "$1"
+  ./ltl2tgba -E -D "$1"
+  ./ltl2tgba -E -f "$1"
+  ./ltl2tgba -E -f -D "$1"
+  ./ltl2tgba -M "$1"
+  ./ltl2tgba -M -f "$1"
+}
+
+expect_ce 'a'
+expect_ce 'a U b'
+expect_ce 'X a'
+expect_ce 'a & b & c'
+expect_ce 'a | b | (c U (d & (g U (h ^ i))))'
+expect_ce 'Xa & (b U !a) & (b U !a)'
+expect_ce 'Fa & Xb & GFc & Gd'
+expect_ce 'Fa & Xa & GFc & Gc'
+expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+expect_ce '!((FF a) <=> (F x))'
+expect_no '!((FF a) <=> (F a))'
+expect_no 'Xa && (!a U b) && !b && X!b'
+expect_no '(a U !b) && Gb'
+
+# Expect four counter-examples..
+test `./ltl2tgba -n 'FFx <=> Fx' | grep Prefix: | wc -l` = 4

src/tgbatest/emptinesscheck.cc

@@ -1,146 +0,0 @@
-
-#include <iostream>
-#include <cassert>
-#include "ltlvisit/destroy.hh"
-#include "ltlast/allnodes.hh"
-#include "ltlparse/public.hh"
-#include "tgbaalgos/ltl2tgba_fm.hh"
-#include "tgbaalgos/emptinesscheck.hh"
-#include "tgba/bddprint.hh"
-//#include "tgba/tgbabddtranslatefactory.hh"
-#include "tgbaalgos/dotty.hh"
-
-void
-syntax(char* prog)
-{ std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
-	    << std::endl
-	    << "Options:" << std::endl
-	    << "  -a   display the accepting_conditions BDD, not the reachability graph"
-	    << std::endl
-	    << "  -A   same as -a, but as a set" << std::endl
-	    << "  -d   turn on traces during parsing" << std::endl
-            << "  -c   emptinesschecking + counter example" << std::endl
-            << "  -e   emptinesschecking for the automaton" << std::endl
-	    << "  -o   re-order BDD variables in the automata" << std::endl
-	    << std::endl
-	    << "  -r   display the relation BDD, not the reachability graph"
-	    << std::endl
-	    << "  -R   same as -r, but as a set" << std::endl
-	    << "  -v   display the BDD variables used by the automaton"
-	    << std::endl;
-  exit(2);
-}
-
-std::string
-print_emptiness_check_ans (bool ans)
-{
-    if (ans)
-      {
-	return "EMPTY-LANGAGE";
-      }
-    else
-      {
-	return "CONSISTENT-AUTOMATA";
-      }
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-
-  bool debug_opt = false;
-  bool defrag_opt = false;
-  spot::emptiness_check* empty_check = new spot::emptiness_check();
-  bool emptiness = true;
-  int output = 0;
-  int formula_index = 0;
-
-  for (;;)
-    {
-      if (argc < formula_index + 2)
-	syntax(argv[0]);
-
-      ++formula_index;
-
-      if (!strcmp(argv[formula_index], "-a"))
-	{
-	  output = 2;
-	}
-      else if (!strcmp(argv[formula_index], "-A"))
-	{
-	  output = 4;
-	}
-      else if (!strcmp(argv[formula_index], "-d"))
-	{
-	  debug_opt = true;
-	}
-      else if (!strcmp(argv[formula_index], "-e"))
-	{
-	  output = 6;
-	}
-      else if (!strcmp(argv[formula_index], "-c"))
-	{
-	  output = 7;
-	}
-      else if (!strcmp(argv[formula_index], "-o"))
-	{
-	  defrag_opt = true;
-	}
-      else if (!strcmp(argv[formula_index], "-r"))
-	{
-	  output = 1;
-	}
-      else if (!strcmp(argv[formula_index], "-R"))
-	{
-	  output = 3;
-	}
-      else if (!strcmp(argv[formula_index], "-v"))
-	{
-	  output = 5;
-	}
-      else
-	{
-	  break;
-	}
-    }
-
-
-  spot::ltl::environment& env(spot::ltl::default_environment::instance());
-  spot::ltl::parse_error_list pel;
-  spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
-					   pel, env, debug_opt);
-
-  exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
-      spot::bdd_dict* dict = new spot::bdd_dict();
-  if (f)
-    {
-      spot::tgba_explicit* a = spot::ltl_to_tgba_fm(f, dict);
-      spot::ltl::destroy(f);
-      switch (output)
-	{
-	case 6:
-	  emptiness = empty_check->tgba_emptiness_check(a);
-	  std::cout << print_emptiness_check_ans(emptiness) << std::endl;
-	  break;
-	case 7:
-	  emptiness = empty_check->tgba_emptiness_check(a);
-	  empty_check->counter_example(a);
-     	  break;
-	default:
-	  assert(!"unknown output option");
-	}
-      delete a;
-      delete empty_check;
-    }
-  else
-    {
-      exit_code = 1;
-    }
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  delete dict;
-  return exit_code;
-}

src/tgbatest/emptinesscheck.test

@@ -1,20 +0,0 @@
-#!/bin/sh
-
-. ./defs
-
-set -e
-
-# We don't check the output, but just running these might be enough to
-# trigger assertions.
-
-./emptinesscheck -e 'a'
-./emptinesscheck -e 'a U b'
-./emptinesscheck -e 'X a'
-./emptinesscheck -e 'a & b & c'
-./emptinesscheck -e 'a | b | (c U (d & (g U (h ^ i))))'
-./emptinesscheck -e 'Xa & (b U !a) & (b U !a)'
-./emptinesscheck -e 'Fa & Xb & GFc & Gd'
-./emptinesscheck -e 'Fa & Xa & GFc & Gc'
-./emptinesscheck -e 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
-./emptinesscheck -e '!((FF a) <=> (F x))'
-./emptinesscheck -e '!((FF a) <=> (F a))'

src/tgbatest/ltl2tgba.cc

@@ -11,6 +11,8 @@
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbatba.hh"
+#include "tgbaalgos/magic.hh"
+#include "tgbaalgos/emptinesscheck.hh"
 
 void
 syntax(char* prog)
@@ -19,14 +21,25 @@ syntax(char* prog)
             << "       "<< prog << " -F [OPTIONS...] file" << std::endl
 	    << std::endl
 	    << "Options:" << std::endl
-	    << "  -a   display the accepting_conditions BDD, not the reachability graph"
+	    << "  -a   display the accepting_conditions BDD, not the "
+	    << "reachability graph"
 	    << std::endl
 	    << "  -A   same as -a, but as a set" << std::endl
 	    << "  -d   turn on traces during parsing" << std::endl
 	    << "  -D   degeneralize the automaton" << std::endl
+	    << "  -e   emptiness-check (Couvreur), expect and compute "
+	    << "a counter-example" << std::endl
+	    << "  -E   emptiness-check (Couvreur), expect no counter-example "
+	    << std::endl
             << "  -f   use Couvreur's FM algorithm for translation"
 	    << std::endl
             << "  -F   read the formula from the file" << std::endl
+	    << "  -m   magic-search (implies -D), expect a counter-example"
+	    << std::endl
+	    << "  -M   magic-search (implies -D), expect no counter-example"
+	    << std::endl
+	    << "  -n   same as -m, but display more counter-examples"
+	    << std::endl
 	    << "  -r   display the relation BDD, not the reachability graph"
 	    << std::endl
 	    << "  -R   same as -r, but as a set" << std::endl
@@ -47,6 +60,9 @@ main(int argc, char** argv)
   bool file_opt = false;
   int output = 0;
   int formula_index = 0;
+  enum { None, Couvreur, MagicSearch } echeck = None;
+  bool magic_many = false;
+  bool expect_counter_example = false;
 
   for (;;)
     {
@@ -71,6 +87,18 @@ main(int argc, char** argv)
 	{
 	  degeneralize_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-e"))
+	{
+	  echeck = Couvreur;
+	  expect_counter_example = true;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-E"))
+	{
+	  echeck = Couvreur;
+	  expect_counter_example = false;
+	  output = -1;
+	}
       else if (!strcmp(argv[formula_index], "-f"))
 	{
 	  fm_opt = true;
@@ -79,6 +107,28 @@ main(int argc, char** argv)
 	{
 	  file_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-m"))
+	{
+	  echeck = MagicSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-M"))
+	{
+	  echeck = MagicSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = false;
+	  output = -1;
+	}
+      else if (!strcmp(argv[formula_index], "-n"))
+	{
+	  echeck = MagicSearch;
+	  degeneralize_opt = true;
+	  expect_counter_example = true;
+	  output = -1;
+	  magic_many = true;
+	}
       else if (!strcmp(argv[formula_index], "-r"))
 	{
 	  output = 1;
@@ -143,12 +193,15 @@ main(int argc, char** argv)
 
       spot::ltl::destroy(f);
 
-      spot::tgba* degeneralized = 0;
+      spot::tgba_tba_proxy* degeneralized = 0;
       if (degeneralize_opt)
 	a = degeneralized = new spot::tgba_tba_proxy(a);
 
       switch (output)
 	{
+	case -1:
+	  /* No output.  */
+	  break;
 	case 0:
 	  spot::dotty_reachable(std::cout, a);
 	  break;
@@ -184,6 +237,53 @@ main(int argc, char** argv)
 	  assert(!"unknown output option");
 	}
 
+      switch (echeck)
+	{
+	case None:
+	  break;
+	case Couvreur:
+	  {
+	    spot::emptiness_check ec = spot::emptiness_check();
+	    bool res = ec.tgba_emptiness_check(a);
+	    if (expect_counter_example)
+	      {
+		if (res)
+		  {
+		    exit_code = 1;
+		    break;
+		  }
+		ec.counter_example(a);
+		ec.print_result(std::cout, a);
+	      }
+	    else
+	      {
+		exit_code = !res;
+	      }
+	  }
+	  break;
+	case MagicSearch:
+	  {
+	    spot::magic_search ms(degeneralized);
+	    bool res = ms.check();
+	    if (expect_counter_example)
+	      {
+		if (!res)
+		  {
+		    exit_code = 1;
+		    break;
+		  }
+		do
+		  ms.print_result(std::cout);
+		while (magic_many && ms.check());
+	      }
+	    else
+	      {
+		exit_code = res;
+	      }
+	  }
+	  break;
+	}
+
       if (degeneralize_opt)
 	delete degeneralized;
 

src/tgbatest/ltlmagic.cc

@@ -1,77 +0,0 @@
-#include <iostream>
-#include <cassert>
-#include "ltlvisit/destroy.hh"
-#include "ltlast/allnodes.hh"
-#include "ltlparse/public.hh"
-#include "tgbaalgos/ltl2tgba_lacim.hh"
-#include "tgbaalgos/magic.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " formula" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-  int formula_index = 0;
-  bool all_opt = false;
-
-  for (;;)
-    {
-      if (argc < formula_index + 1)
-	syntax(argv[0]);
-
-      ++formula_index;
-
-      if (!strcmp(argv[formula_index], "-a"))
-	{
-	  all_opt = true;
-	}
-      else
-	{
-	  break;
-	}
-    }
-
-  spot::ltl::environment& env(spot::ltl::default_environment::instance());
-
-  spot::ltl::parse_error_list pel1;
-  spot::ltl::formula* f1 = spot::ltl::parse(argv[formula_index], pel1, env);
-
-  if (spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel1))
-    return 2;
-
-  spot::bdd_dict* dict = new spot::bdd_dict();
-  {
-    spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict);
-    spot::tgba_tba_proxy* a2 = new spot::tgba_tba_proxy(a1);
-    spot::ltl::destroy(f1);
-
-    spot::magic_search ms(a2);
-
-    if (ms.check())
-      {
-	do
-	  ms.print_result (std::cout);
-	while (all_opt && ms.check());
-      }
-    else
-      {
-	exit_code = 1;
-      }
-
-    delete a2;
-    delete a1;
-  }
-
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  delete dict;
-  return exit_code;
-}

src/tgbatest/ltlmagic.test

@@ -1,15 +0,0 @@
-#!/bin/sh
-
-. ./defs
-
-set -e
-
-./ltlmagic a
-./ltlmagic 0 || test $? = 1
-./ltlmagic 'a & !a' || test $? = 1
-./ltlmagic 'a U b'
-./ltlmagic '!(a U b)'
-./ltlmagic '!(a U b) & !(!a R !b)' || test $? = 1
-# Expect four satisfactions
-test `./ltlmagic -a 'FFx <=> Fx' | grep Prefix: | wc -l` = 4
-./ltlmagic '!(FFx <=> Fx)'  || test $? = 1