* src/tgba/bddprint.cc (dict): Make this variable static.

(want_prom): New global static variable.
(print_handle): Honor want_prom.
(print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
(bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
* src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
save.cc and save.hh.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
(readsave_SOURCES): New variable.
(TESTS): Add readsave.test.

ChangeLog

 2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/bddprint.cc (dict): Make this variable static.
+	(want_prom): New global static variable.
+	(print_handle): Honor want_prom.
+	(print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
+	(bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
+	* src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
+	* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
+	src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
+	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
+	save.cc and save.hh.
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
+	(readsave_SOURCES): New variable.
+	(TESTS): Add readsave.test.
+
 	* configure.ac: Output src/tgbaparse/Makefile.
 	* src/Makefile.am (SUBDIRS): Add tgbaparse.
 	(libspot_la_LDADD): Add tgbaparse/libtgbaparse.la.

src/tgba/bddprint.cc

@@ -5,7 +5,10 @@
 namespace spot
 {
   /// Global dictionary used by print_handler() to lookup variables.
-  const tgba_bdd_dict* dict;
+  static const tgba_bdd_dict* dict;
+  
+  /// Global flag to enable Prom[x] output (instead of `x').
+  static bool want_prom;
 
   /// Stream handler used by Buddy to display BDD variables.
   static void
@@ -20,7 +23,11 @@ namespace spot
 	isi = dict->prom_formula_map.find(var);
 	if (isi != dict->prom_formula_map.end())
 	  {
-	    o << "Prom["; to_string(isi->second, o) << "]";
+	    if (want_prom)
+	      o << "Prom["; 
+	    to_string(isi->second, o);
+	    if (want_prom)
+	      o << "]";
 	  }
 	else
 	  {
@@ -46,10 +53,49 @@ namespace spot
   }
 
 
+  static std::ostream* where;
+  static void
+  print_sat_handler(char* varset, int size)
+  {
+    bool not_first = false;
+    for (int v = 0; v < size; ++v)
+      {
+	if (varset[v] < 0)
+	  continue;
+	if (not_first)
+	  *where << " ";
+	else
+	  not_first = true;
+	if (varset[v] == 0)
+	  *where << "!";
+	print_handler(*where, v);
+      }
+  }
+
+  std::ostream&
+  bdd_print_sat(std::ostream& os, const tgba_bdd_dict& d, bdd b)
+  {
+    dict = &d;
+    where = &os;
+    want_prom = false;
+    assert (bdd_satone(b) == b);
+    bdd_allsat (b, print_sat_handler);
+    return os;
+  }
+
+  std::string
+  bdd_format_sat(const tgba_bdd_dict& d, bdd b)
+  {
+    std::ostringstream os;
+    bdd_print_sat(os, d, b);
+    return os.str();
+  }
+
   std::ostream&
   bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
   {
     dict = &d;
+    want_prom = true;
     bdd_strm_hook(print_handler);
     os << bddset << b;
     bdd_strm_hook(0);
@@ -68,6 +114,7 @@ namespace spot
   bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
   {
     dict = &d;
+    want_prom = true;
     bdd_strm_hook(print_handler);
     os << bdddot << b;
     bdd_strm_hook(0);
@@ -78,6 +125,7 @@ namespace spot
   bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
   {
     dict = &d;
+    want_prom = true;
     bdd_strm_hook(print_handler);
     os << bddtable << b;
     bdd_strm_hook(0);

src/tgba/bddprint.hh

@@ -9,29 +9,46 @@
 namespace spot
 {
 
+  /// \brief Print a BDD as a list of literals.
+  ///
+  /// This assumes that \a b is a conjunction of literals.
+  /// \param os The output stream.
+  /// \param dict The dictionary to use, to lookup variables.
+  /// \param b The BDD to print.
+  std::ostream& bdd_print_sat(std::ostream& os,
+			      const tgba_bdd_dict& dict, bdd b);
+
+  /// \brief Format a BDD as a list of literals.
+  ///
+  /// This assumes that \a b is a conjunction of literals.
+  /// \param dict The dictionary to use, to lookup variables.
+  /// \param b The BDD to print.
+  /// \return The BDD formated as a string.
+  std::string bdd_format_sat(const tgba_bdd_dict& dict, bdd b);
+
   /// \brief Print a BDD as a set.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
-  /// \param b The BDD to print. 
+  /// \param b The BDD to print.
   std::ostream& bdd_print_set(std::ostream& os,
 			      const tgba_bdd_dict& dict, bdd b);
   /// \brief Format a BDD as a set.
   /// \param dict The dictionary to use, to lookup variables.
-  /// \param b The BDD to print. 
+  /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b);
 
   /// \brief Print a BDD as a diagram in dotty format.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
-  /// \param b The BDD to print. 
+  /// \param b The BDD to print.
   std::ostream& bdd_print_dot(std::ostream& os,
 			      const tgba_bdd_dict& dict, bdd b);
 
   /// \brief Print a BDD as a table.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
-  /// \param b The BDD to print. 
+  /// \param b The BDD to print.
   std::ostream& bdd_print_table(std::ostream& os,
 				const tgba_bdd_dict& dict, bdd b);
 

src/tgbaalgos/Makefile.am

@@ -4,4 +4,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 noinst_LTLIBRARIES = libtgbaalgos.la
 libtgbaalgos_la_SOURCES = \
   dotty.cc \
-  dotty.hh
+  dotty.hh \
+  save.cc \
+  save.hh
+

src/tgbaalgos/save.cc

+#include <set>
+#include "tgba/tgba.hh"
+#include "save.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  typedef std::set<state*, state_ptr_less_than> seen_set;
+
+  /// Process successors.
+  static void
+  save_rec(std::ostream& os, const tgba& g, state* st, seen_set& m)
+  {
+    m.insert(st);
+    std::string cur = g.format_state(st);
+    tgba_succ_iterator* si = g.succ_iter(st);
+    for (si->first(); !si->done(); si->next())
+      {
+	state* s = si->current_state();
+	os << "\"" << cur << "\", \"" << g.format_state(s) << "\", ";
+
+	bdd_print_sat(os, g.get_dict(), si->current_condition()) << ", ";
+	bdd_print_sat(os, g.get_dict(), si->current_promise()) << ";"
+							       << std::endl;
+
+	// Destination already explored?
+	seen_set::iterator i = m.find(s);
+	if (i != m.end())
+	  {
+	    delete s;
+	  }
+	else
+	  {
+	    save_rec(os, g, s, m);
+	    // Do not delete S, it is used as key in M.
+	  }
+      }
+    delete si;
+  }
+
+  std::ostream&
+  tgba_save_reachable(std::ostream& os, const tgba& g)
+  {
+    seen_set m;
+    state* state = g.get_init_state();
+    save_rec(os, g, state, m);
+    // Finally delete all states used as keys in m:
+    for (seen_set::iterator i = m.begin(); i != m.end(); ++i)
+      delete *i;
+    return os;
+  }
+}

src/tgbaalgos/save.hh

+#ifndef SPOT_TGBAALGOS_SAVE_HH
+# define SPOT_TGBAALGOS_SAVE_HH
+
+#include "tgba/tgba.hh"
+#include <iostream>
+
+namespace spot
+{
+  /// \brief Save reachable states in text format.
+  std::ostream& tgba_save_reachable(std::ostream& os, const tgba& g);
+}
+
+#endif // SPOT_TGBAALGOS_SAVE_HH

src/tgbatest/.cvsignore

@@ -5,3 +5,4 @@ defs
 explicit
 .libs
 tgbaread
+readsave

src/tgbatest/Makefile.am

@@ -5,14 +5,18 @@ check_SCRIPTS = defs
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
   explicit \
+  readsave \
   tgbaread
 
+
 explicit_SOURCES = explicit.cc
+readsave_SOURCES = readsave.cc
 tgbaread_SOURCES = tgbaread.cc
 
 TESTS = \
   explicit.test \
-  tgbaread.test
+  tgbaread.test \
+  readsave.test
 
 EXTRA_DIST = $(TESTS)
 

src/tgbatest/readsave.cc

+#include <iostream>
+#include "tgbaparse/public.hh"
+#include "tgba/tgbaexplicit.hh"
+#include "tgbaalgos/save.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;
+
+  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::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
+					    pel, env, debug);
+  
+  exit_code =
+    spot::format_tgba_parse_errors(std::cerr, pel);
+
+  if (a)
+    {
+      spot::tgba_save_reachable(std::cout, *a);
+      delete a;
+    }
+  else
+    {
+      exit_code = 1;
+    }
+  return exit_code;
+}

src/tgbatest/readsave.test

+#!/bin/sh
+
+. ./defs
+
+set -e
+
+cat >input <<EOF
+s1, "s2", a!b, c d;
+"s2", "state 3", a, !c;
+"state 3", s1,,;
+EOF
+
+./readsave input > stdout
+
+cat >expected <<EOF
+"s1", "s2", a !b, c d;
+"s2", "state 3", a, !c;
+"state 3", "s1", , ;
+EOF
+
+diff stdout expected
+
+mv stdout input
+./readsave input > stdout
+diff input stdout
+
+rm input stdout expected