Add an ltl2tgba option to read Kripke structure.

Also offers two ways to output Kripke structures.

* src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
: Simplify includes.
* src/kripke/kripkeprint.hh (kripke_save_reachable,
kripke_save_reachable_renumbered): New declarations.
(KripkePrinter): Move and rename...
* src/kripke/kripkeprint.cc (kripke_printer): ... here.
(kripke_printer_renumbered): New class.
(kripke_save_reachable, kripke_save_reachable_renumbered): New
function.
* src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
structures.
* iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
* iface/dve2/defs.in (run2): Remove.
* iface/dve2/kripke.test: Adjust tests.

ChangeLog

@@ -1,3 +1,24 @@
+2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Add an ltl2tgba option to read Kripke structure.
+
+	Also offers two ways to output Kripke structures.
+
+	* src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
+	: Simplify includes.
+	* src/kripke/kripkeprint.hh (kripke_save_reachable,
+	kripke_save_reachable_renumbered): New declarations.
+	(KripkePrinter): Move and rename...
+	* src/kripke/kripkeprint.cc (kripke_printer): ... here.
+	(kripke_printer_renumbered): New class.
+	(kripke_save_reachable, kripke_save_reachable_renumbered): New
+	function.
+	* src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
+	structures.
+	* iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
+	* iface/dve2/defs.in (run2): Remove.
+	* iface/dve2/kripke.test: Adjust tests.
+
 2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* AUTHORS: Add Thomas Badie.

iface/dve2/defs.in

@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -88,40 +88,4 @@ run()
   test $exitcode = $expected_exitcode || exit 1
 }
 
-
-run2()
-{
-  expected_exitcode=$1
-  shift
-  exitcode=0
-  if test -n "$VALGRIND"; then
-    exec 6>valgrind.err
-    GLIBCPP_FORCE_NEW=1 \
-    ../../../libtool --mode=execute \
-    $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" | grep -v + > log ||
-      exitcode=$?
-    cat valgrind.err 1>&2
-    test -z "`sed 1q valgrind.err`" || exit 50
-    rm -f valgrind.err
-  else
-    "$@" || exitcode=$?
-  fi
-  test $exitcode = $expected_exitcode || exit 1
-
-  exec 6>valgrind.err
-  ../../../libtool --mode=execute \
-      $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q $1 log \
-      | grep -v + > log2 ||
-  exitcode=$?
-    cat valgrind.err 1>&2
-    test -z "`sed 1q valgrind.err`" || exit 50
-    rm -f valgrind.err
-  test $exitcode = $expected_exitcode || exit 1
-
-  diff log log2 || exit 42
-  rm -f log log2
-
-}
-
-
 set -x

iface/dve2/dve2check.cc

@@ -252,8 +252,7 @@ main(int argc, char **argv)
       if (output == Kripke)
       {
         tm.start("kripke output");
-        spot::KripkePrinter p (model, std::cout);
+	spot::kripke_save_reachable_renumbered(std::cout, model);
-        p.run();
         tm.stop("kripke output");
         goto safe_exit;
       }

iface/dve2/kripke.test

@@ -33,10 +33,12 @@ else
   exit 77
 fi
 
-
 set -e
 
-run 0 ${top_builddir}/iface/dve2/dve2check -gK \
+run 0 ../dve2check -gK ${srcdir}/finite.dve 'F("P.a > 5")' > output
-${srcdir}/finite.dve 'F("P.a > 5")' | grep -v + > parse
+run 0 ${top_builddir}/src/kripketest/parse_print output | tr -d '"' > output2
-run2 0 ${top_builddir}/src/kripketest/parse_print parse
+tr -d '"' < output >outputF
-rm -f parse
+cmp outputF output2
+
+../dve2check -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP
+${top_builddir}/src/tgbatest/ltl2tgba -e -KPoutputP '!G("pos[1] < 3")'

src/kripke/kripkeexplicit.cc

@@ -20,10 +20,9 @@
 
 
 #include "kripkeexplicit.hh"
-#include "../tgba/bddprint.hh"
+#include "tgba/bddprint.hh"
 #include "tgba/formula2bdd.hh"
 #include <iostream>
-#include "../tgba/state.hh"
 
 namespace spot
 {

src/kripke/kripkeprint.cc

@@ -21,33 +21,32 @@
 
 #include "kripkeprint.hh"
 #include "kripkeexplicit.hh"
-#include "../tgba/bddprint.hh"
+#include "tgba/bddprint.hh"
 #include "misc/escape.hh"
+#include "tgbaalgos/reachiter.hh"
 #include <iostream>
+#include <sstream>
 
 namespace spot
 {
-  KripkePrinter::KripkePrinter(const kripke* automata,
+  namespace
-                               std::ostream& os)
+  {
-    : tgba_reachable_iterator_breadth_first(automata), os_(os)
+
+    class kripke_printer : public tgba_reachable_iterator_breadth_first
+    {
+    public:
+      kripke_printer(const kripke* a, std::ostream& os)
+	: tgba_reachable_iterator_breadth_first(a), os_(os)
       {
       }
 
-  void KripkePrinter::start()
+      void process_state(const state* s, int, tgba_succ_iterator* si)
-  {
-  }
-
-  void KripkePrinter::process_state(const state* s,
-                                    int,
-                                    tgba_succ_iterator* si)
       {
 	const bdd_dict* d = automata_->get_dict();
-    std::string cur = automata_->format_state(s);
 	os_ << "\"";
 	escape_str(os_, automata_->format_state(s));
 	os_ << "\", \"";
-    const kripke* automata = down_cast<const kripke*>
+	const kripke* automata = down_cast<const kripke*> (automata_);
-      (automata_);
 	assert(automata);
 	escape_str(os_, bdd_format_formula(d,
 					   automata->state_condition(s)));
@@ -60,7 +59,82 @@ namespace spot
 	    escape_str(os_, automata_->format_state(dest));
 	    os_ << "\"";
 	}
-    os_ << ";" << std::endl;
+	os_ << ";\n";
       }
 
+    private:
+      std::ostream& os_;
+    };
+
+    class kripke_printer_renumbered :
+      public tgba_reachable_iterator_breadth_first
+    {
+    public:
+      kripke_printer_renumbered(const kripke* a, std::ostream& os)
+	: tgba_reachable_iterator_breadth_first(a), os_(os),
+	  notfirst(false)
+      {
+      }
+
+      void finish_state()
+      {
+	os_ << lastsuccs.str() << ";\n";
+	lastsuccs.str("");
+      }
+
+      void process_state(const state* s, int in_s, tgba_succ_iterator*)
+      {
+	if (notfirst)
+	  finish_state();
+	else
+	  notfirst = true;
+
+	const bdd_dict* d = automata_->get_dict();
+	std::string cur = automata_->format_state(s);
+	os_ << "S" << in_s << ", \"";
+	const kripke* automata = down_cast<const kripke*>(automata_);
+	assert(automata);
+	escape_str(os_, bdd_format_formula(d,
+					   automata->state_condition(s)));
+	os_ << "\",";
+      }
+
+      void
+      process_link(const state*, int, const state*, int d,
+		   const tgba_succ_iterator*)
+      {
+	lastsuccs << " S" << d;
+      }
+
+      void
+      end()
+      {
+	finish_state();
+      }
+
+    private:
+      std::ostream& os_;
+      std::ostringstream lastsuccs;
+      bool notfirst;
+    };
+
+  }
+
+  std::ostream&
+  kripke_save_reachable(std::ostream& os, const kripke* k)
+  {
+    kripke_printer p(k, os);
+    p.run();
+    return os;
+  }
+
+  std::ostream&
+  kripke_save_reachable_renumbered(std::ostream& os, const kripke* k)
+  {
+    kripke_printer_renumbered p(k, os);
+    p.run();
+    return os;
+  }
+
+
 } // End namespace Spot

src/kripke/kripkeprint.hh

@@ -23,30 +23,32 @@
 # define SPOT_KRIPKE_KRIPKEPRINT_HH
 
 # include <iosfwd>
-# include "tgbaalgos/reachiter.hh"
 namespace spot
 {
 
-  class kripke_explicit;
-  class state_kripke;
-  class kripke_succ_iterator;
   class kripke;
 
-  /// \brief Iterate over all reachable states of a spot::kripke
+  /// \brief Save the reachable part of Kripke structure in text format.
-  /// Override start and process_state methods from
+  ///
-  /// tgba_reachable_iterator_breadth_first.
+  /// The states will be named with the value returned by the
-  class KripkePrinter : public tgba_reachable_iterator_breadth_first
+  /// kripke::format_state() method.  Such a string can be large, so
-  {
+  /// the output will not be I/O efficient.  We recommend using this
-    public:
+  /// function only for debugging.  Use
-      KripkePrinter(const kripke* state, std::ostream& os);
+  /// kripke_save_reachable_renumbered() for large output.
+  ///
+  /// \ingroup tgba_io
+  std::ostream& kripke_save_reachable(std::ostream& os, const kripke* k);
 
-      void start();
+  /// \brief Save the reachable part of Kripke structure in text format.
-
+  ///
-      void process_state(const state*, int, tgba_succ_iterator* si);
+  /// States will be renumbered with sequential number.  This is much
-
+  /// more I/O efficient when dumping large Kripke structures with big
-    private:
+  /// state names.  The drawback is that any information carried by
-      std::ostream& os_;
+  /// the state name is lost.
-  };
+  ///
+  /// \ingroup tgba_io
+  std::ostream& kripke_save_reachable_renumbered(std::ostream& os,
+						 const kripke* k);
 
 } // End namespace spot
 

src/kripketest/parse_print_test.cc

@@ -19,10 +19,8 @@
 // 02111-1307, USA.
 
 
-#include "../kripkeparse/public.hh"
+#include "kripkeparse/public.hh"
-#include "../kripkeparse/parsedecl.hh"
+#include "kripke/kripkeprint.hh"
-#include "../kripke/kripkeprint.hh"
-#include "../tgba/bddprint.hh"
 #include "ltlast/allnodes.hh"
 
 
@@ -30,7 +28,7 @@ using namespace spot;
 
 int main(int argc, char** argv)
 {
-  int returnValue = 0;
+  int return_value = 0;
   kripke_parse_error_list pel;
   bdd_dict* dict = new bdd_dict;
 
@@ -38,15 +36,11 @@ int main(int argc, char** argv)
   if (!pel.empty())
   {
     format_kripke_parse_errors(std::cerr, argv[1], pel);
-    returnValue = 1;
+    return_value = 1;
   }
 
-  if (!returnValue)
+  if (!return_value)
-  {
+    kripke_save_reachable(std::cout, k);
-    KripkePrinter* kp = new KripkePrinter(k, std::cout);
-    kp->run();
-    delete kp;
-  }
 
   delete k;
   delete dict;
@@ -54,5 +48,5 @@ int main(int argc, char** argv)
   assert(ltl::unop::instance_count() == 0);
   assert(ltl::binop::instance_count() == 0);
   assert(ltl::multop::instance_count() == 0);
-  return returnValue;
+  return return_value;
 }

src/tgbatest/ltl2tgba.cc

@@ -58,10 +58,11 @@
 #include "tgbaalgos/gtec/gtec.hh"
 #include "eltlparse/public.hh"
 #include "misc/timer.hh"
-
 #include "tgbaalgos/stats.hh"
 #include "tgbaalgos/scc.hh"
 #include "tgbaalgos/emptiness_stats.hh"
+#include "tgbaalgos/scc.hh"
+#include "kripkeparse/public.hh"
 
 std::string
 ltl_defs()
@@ -111,9 +112,10 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -XN   do not compute an automaton, read it from a"
 	    << " neverclaim file" << std::endl
-	    << "  -Pfile  multiply the formula automaton with the automaton"
+	    << "  -Pfile  multiply the formula automaton with the TGBA read"
-	    << " from `file'"
+	    << " from `file'\n"
-	    << std::endl
+	    << "  -KPfile multiply the formula automaton with the Kripke"
+	    << " structure from `file'\n"
 	    << std::endl
 
 	    << "Translation algorithm:" << std::endl
@@ -330,7 +332,7 @@ main(int argc, char** argv)
   bool spin_comments = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
-  spot::tgba_explicit_string* system = 0;
+  spot::tgba* system = 0;
   const spot::tgba* product = 0;
   const spot::tgba* product_to_free = 0;
   spot::bdd_dict* dict = new spot::bdd_dict();
@@ -498,6 +500,18 @@ main(int argc, char** argv)
 	{
 	  output = 10;
 	}
+      else if (!strncmp(argv[formula_index], "-KP", 3))
+	{
+	  tm.start("reading -KP's argument");
+
+	  spot::kripke_parse_error_list pel;
+	  system = spot::kripke_parse(argv[formula_index] + 3,
+				      pel, dict, env, debug_opt);
+	  if (spot::format_kripke_parse_errors(std::cerr,
+					       argv[formula_index] + 2, pel))
+	    return 2;
+	  tm.stop("reading -KP's argument");
+	}
       else if (!strcmp(argv[formula_index], "-KV"))
 	{
 	  output = 11;
@@ -555,14 +569,15 @@ main(int argc, char** argv)
 	  tm.start("reading -P's argument");
 
 	  spot::tgba_parse_error_list pel;
-	  system = spot::tgba_parse(argv[formula_index] + 2,
+	  spot::tgba_explicit_string* s;
+	  s = spot::tgba_parse(argv[formula_index] + 2,
 			       pel, dict, env, env, debug_opt);
 	  if (spot::format_tgba_parse_errors(std::cerr,
 					     argv[formula_index] + 2, pel))
 	    return 2;
-	  system->merge_transitions();
+	  s->merge_transitions();
-
 	  tm.stop("reading -P's argument");
+	  system = s;
 	}
       else if (!strcmp(argv[formula_index], "-r"))
 	{