* src/tgbatest/emptinesscheckexplicit.test (acc): New file.

* src/tgbatest/emptinesscheckexplicit.cc (main): New file.

* src/tgbatest/emptinesscheck.test: New file.

* src/tgbatest/emptinesscheck.cc (main): New file.

* src/tgbaalgos/emptinesscheck.cc (spot): New method.

* src/tgbaalgos/emptinesscheck.hh: New interface.

ChangeLog

+2003-09-25  Rachid REBIHA  <rebiha@nyx>
+
+	* src/tgbatest/emptinesscheckexplicit.test (acc): New file.
+
+	* src/tgbatest/emptinesscheckexplicit.cc (main): New file.
+
+	* src/tgbatest/emptinesscheck.test: New file.
+
+	* src/tgbatest/emptinesscheck.cc (main): New file.
+
+	* src/tgbaalgos/emptinesscheck.cc (spot): New method.
+
+	* src/tgbaalgos/emptinesscheck.hh: New interface.
+
 2003-09-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ...

src/tgbaalgos/Makefile.am

@@ -10,6 +10,7 @@ tgbaalgos_HEADERS = \
   ltl2tgba_fm.hh \
   ltl2tgba_lacim.hh \
   magic.hh \
+  emptinesscheck.hh \
   save.hh
 
 noinst_LTLIBRARIES = libtgbaalgos.la
@@ -20,4 +21,5 @@ libtgbaalgos_la_SOURCES = \
   ltl2tgba_fm.cc \
   ltl2tgba_lacim.cc \
   magic.cc \
+  emptinesscheck.cc \
   save.cc

src/tgbaalgos/emptinesscheck.hh

+#ifndef SPOT_EMPTINESS_CHECK_HH
+# define SPOT_EMPTINESS_CHECK_HH
+//#include "tgba/bddfactory.hh"
+#include "tgba/tgba.hh"
+#include "tgba/statebdd.hh"
+#include "tgba/tgbabddfactory.hh"
+#include "tgba/succiterconcrete.hh"
+#include "tgba/tgbabddconcrete.hh"
+#include <map>
+#include <stack>
+#include <list>
+#include <vector>
+#include <set>
+
+namespace spot
+{
+  /// \brief Emptiness check on spot::tgba
+
+  class connected_component
+  {
+  /// During the Depth path we keep the connected component that we met.
+  public:
+    connected_component();
+    connected_component(int i, bdd a);
+    virtual
+    ~connected_component();
+    std::string
+    to_string_component();
+    bool
+    isAccepted(tgba* aut);
+
+  public:
+    int index;
+    /// The bdd condition is the union of all accepting condition of
+    /// transitions which connect the states of the connected component.
+    bdd condition;
+    typedef std::set<const spot::state*, spot::state_ptr_less_than> set_of_state;
+    /// for the counter example we need to know all the states of the
+    ///component
+    set_of_state state_set;
+    int transition_acc;
+    int nb_transition;
+    int nb_state;
+    bool not_null;
+  };
+
+  class emptiness_check
+  {
+
+    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
+    typedef std::pair<pair_state_iter, bdd> triplet;
+    typedef std::map <const spot::state*, int, spot::state_ptr_less_than> seen;
+    typedef std::list<const state*> state_sequence;
+    typedef std::pair<const spot::state*, bdd> state_proposition;
+    typedef std::list<state_proposition> cycle_path;
+
+  public:
+
+virtual
+    ~emptiness_check();
+
+    emptiness_check();
+
+    /// this function remove all accessible state from a given
+    /// state. In other words, it removes the strongly connected
+    /// component that contents this state.
+    void
+    remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete);
+
+ /// \brief Emptiness check on spot::tgba
+  /// This is based on the following papers.
+  /// \verbatim
+  /// @InProceedings{   couvreur.00.lacim,
+  ///   author        = {Jean-Michel Couvreur},
+  ///   title         = {Un point de vue symbolique sur la logique temporelle
+  ///                   lin{\'e}aire},
+  ///   booktitle     = {Actes du Colloque LaCIM 2000},
+  ///   month         = {August},
+  ///   year          = {2000},
+  ///   pages         = {131--140},
+  ///   volume        = {27},
+  ///   series        = {Publications du LaCIM},
+  ///   publisher     = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al},
+  ///   editor        = {Pierre Leroux}
+  /// }
+  /// \endverbatim
+  /// and
+  /// \verbatim
+  /// @InProceedings{couvreur.99.fm,
+  ///   author	  = {Jean-Michel Couvreur},
+  ///   title     = {On-the-fly Verification of Temporal Logic},
+  ///   pages     = {253--271},
+  ///   editor	  = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
+  ///   booktitle = {Proceedings of the World Congress on Formal Methods in the
+  /// 		     Development of Computing Systems (FM'99)},
+  ///   publisher = {Springer-Verlag},
+  ///   series	  = {Lecture Notes in Computer Science},
+  ///   volume	  = {1708},
+  ///   year      = {1999},
+  ///   address	  = {Toulouse, France},
+  ///   month	  = {September},
+  ///   isbn      = {3-540-66587-0}
+  /// }
+  /// \endverbatim
+  /// This function return true if the automata is empty and build a stack of SCC.
+    bool
+    tgba_emptiness_check(const spot::tgba* aut_check);
+
+    /// counter_example check if the automata is empty. If it is not,
+    ///then this function return an accepted word (a trace) and an accepted sequence.
+
+    void
+ counter_example(const spot::tgba* aut_counter);
+
+    std::stack <bdd> arc_accepting;
+    std::stack <connected_component> root_component;
+    seen seen_state_num;
+    state_sequence seq_counter;
+    cycle_path periode;
+  private:
+    std::stack <pair_state_iter> todo;
+    std::vector<state_sequence> vec_sequence;
+
+    /// This function is called by counter_example to find a path
+    /// which contents all accepting conditions in the accepted SCC (get all the
+    /// accepting conditions).
+
+    void
+    accepting_path (const spot::tgba* aut_counter, const connected_component& comp_path, const spot::state* start_path, bdd to_accept);
+
+
+    /// This function is called by counter_example (after
+    //accepting_path) to complete the cycle that caraterise the periode
+    //of the counter example.  Append a sequence to the path given by  accepting_path.
+    void
+    complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state);
+  };
+}
+#endif // SPOT_EMPTINESS_CHECK_HH

src/tgbatest/Makefile.am

@@ -6,6 +6,8 @@ check_SCRIPTS = defs
 check_PROGRAMS = \
   bddprod \
   explicit \
+  emptinesscheck \
+emptinesscheckexplicit \
   explprod \
   ltl2tgba \
   ltlmagic \
@@ -18,6 +20,8 @@ check_PROGRAMS = \
 # 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
@@ -42,6 +46,8 @@ TESTS = \
   explpro3.test \
   tripprod.test \
   mixprod.test \
+  emptinesscheck.test \
+  emptinesscheckexplicit.test \
   ltlmagic.test \
   spotlbtt.test
 

src/tgbatest/emptinesscheck.cc

+
+#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:
+	  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

+#!/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))'
\ No newline at end of file

src/tgbatest/emptinesscheckexplicit.cc

+#include <iostream>
+#include "tgbaparse/public.hh"
+#include "tgba/tgbaexplicit.hh"
+#include "tgbaalgos/dotty.hh"
+#include "tgbaalgos/emptinesscheck.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " [-d] filename" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+
+  if (argc < 2)
+    syntax(argv[0]);
+
+  bool debug = false;
+  int filename_index = 1;
+  bool emptiness = false;
+
+  if (!strcmp(argv[1], "-d"))
+    {
+      debug = true;
+      if (argc < 3)
+	syntax(argv[0]);
+      filename_index = 2;
+    }
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+  spot::tgba_parse_error_list pel;
+  spot::bdd_dict* dict = new spot::bdd_dict();
+  spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
+					    pel, dict, env, debug);
+  spot::emptiness_check empty_check;
+
+  if (spot::format_tgba_parse_errors(std::cerr, pel))
+    return 2;
+  empty_check.counter_example(a);
+  delete a;
+  return 0;
+}

src/tgbatest/emptinesscheckexplicit.test

+#!/bin/sh
+
+. ./defs
+
+set -e
+
+cat >input <<'EOF'
+acc = c d;
+s1, "s2", a!b, c d;
+"s2", "state 3", a, c;
+"state 3", s1,,;
+EOF
+
+./emptinesscheckexplicit input > stdout