lbtt: improve the LBTT output

Provide a way to output automata with state-based acceptance.  Also
print the guards using to_lbt_string() for consistency: as a
consequence, atomic proposition that do not match p[0-9]+ are now
double-quoted.

* src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
* src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
* src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
* src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
Add an option --lbtt=t to get the old behavior.
* src/bin/man/ltl2tgba.x: Document the LBTT format we use with
some links and examples.
* src/tgbatest/lbttparse.test: More tests.
* src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
* NEWS: Update.

NEWS

@@ -1,6 +1,30 @@
 New in spot 1.1a (not yet released):
 
-  Bug fixes:
+  * New features:
+
+    - lbtt_reachable(), the function that outputs a TGBA in LBTT's
+      format, has a new option to indicate that the TGBA being printed
+      is in fact a Büchi automaton.  In this case it outputs an LBTT
+      automaton with state-based acceptance.
+
+      The output of the guards has also been changed in two ways:
+      1. atomic propositions that do not match p[0-9]+ are always
+         double-quoted.  This avoids issues where t or f were used as
+         atomic propositions in the formula, output as-is in the
+         automaton, and read back as true or false.  Other names that
+         correspond to LBT operators would cause problem as well.
+      2. formulas that label transitions are now output as
+         irredundant-sums-of-products.
+
+    - 'ltl2tgba --ba --lbtt' will now output automata with state-based
+      acceptance.  You can use 'ltl2tgba --ba --lbtt=t' to force the
+      output of transition-based acceptance like in the previous
+      versions.
+
+      Some illustrations of this point and the previous one can be
+      found in the man page for ltl2tgba(1).
+
+  * Bug fixes:
 
     - genltl --gh-r generated the wrong formulas due to a typo.
 

src/bin/ltl2tgba.cc

@@ -67,7 +67,9 @@ static const argp_option options[] =
     /**************************************************/
     { 0, 0, 0, 0, "Output format:", 3 },
     { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
-    { "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 },
+    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
+      "LBTT's format (add =t to force transition-based acceptance even"
+      " on Büchi automata)", 0 },
     { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
     { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
     { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
@@ -106,7 +108,7 @@ const struct argp_child children[] =
     { 0, 0, 0, 0 }
   };
 
-enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot;
+enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot;
 bool utf8 = false;
 const char* stats = "";
 spot::option_map extra_options;
@@ -142,7 +144,17 @@ parse_opt(int key, char* arg, struct argp_state*)
       format = Dot;
       break;
     case OPT_LBTT:
-      format = Lbtt;
+      if (arg)
+	{
+	  if (arg[0] == 't' && arg[1] == 0)
+	    format = Lbtt_t;
+	  else
+	    error(2, 0, "unknown argument for --lbtt: '%s'", arg);
+	}
+      else
+	{
+	  format = Lbtt;
+	}
       break;
     case OPT_SPOT:
       format = Spot;
@@ -220,7 +232,10 @@ namespace
 				|| (type == spot::postprocessor::Monitor));
 	  break;
 	case Lbtt:
-	  spot::lbtt_reachable(std::cout, aut);
+	  spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
+	  break;
+	case Lbtt_t:
+	  spot::lbtt_reachable(std::cout, aut, false);
 	  break;
 	case Spot:
 	  spot::tgba_save_reachable(std::cout, aut);

src/bin/man/ltl2tgba.x

@@ -1,6 +1,84 @@
 [NAME]
 ltl2tgba \- translate LTL/PSL formulas into Büchi automata
-[DESCRIPTION]
+[NOTE ON LBTT'S FORMAT]
-.\" Add any additional description here
+The format, described at
+http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html,
+has support for both transition-based and state based generalized acceptance.
+
+Because Spot uses transition-based generalized Büchi automata
+internally, it will normally use the transition-based flavor of that
+format, indicated with a 't' flag after the number of acceptance sets.
+For instance:
+
+  % bin/ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2'
+  2 2t                   // 2 states, 2 transition-based acceptance sets
+  0 1                    // state 0: initial
+  0 -1 t                 //   trans. to state 0, no acc., label: true
+  1 -1 | & p0 p2 & p1 p2 //   trans. to state 1, no acc., label: (p0&p2)|(p1&p2)
+  -1                     // end of state 0
+  1 0                    // state 1: not initial
+  1 0 1 -1 & & p0 p1 p2  //   trans. to state 1, acc. 0 and 1, label: p0&p1&p2
+  1 0 -1 & & p1 p2 ! p0  //   trans. to state 1, acc. 0, label: !p0&p1&p2
+  1 1 -1 & & p0 p2 ! p1  //   trans. to state 1, acc. 1, label: p0&!p1&p2
+  1 -1 & & p2 ! p0 ! p1  //   trans. to state 1, no acc., label: !p0&!p1&p2
+  -1                     // end if state 1
+
+Here, the two acceptance sets are represented by the numbers 0 and 1,
+and they each contain two transitions (the first transition of state 1
+belongs to both sets).
+
+When both --ba and --lbtt options are used, the state-based flavor of
+the format is used instead.  Note that the LBTT format supports
+generalized acceptance conditions on states, but Spot only use this
+format for Büchi automata, where there is always only one acceptance
+set.  Unlike in the LBTT documentation, we do not use the
+optional 's' flag to indicate the state-based acceptance, this way our
+output is also compatible with that of LBT (see
+http://www.tcs.hut.fi/Software/maria/tools/lbt/).
+
+  % ltl2tgba --ba --lbtt FGp0
+  2 1                 // 2 states, 1 (state-based) accepance set
+  0 1 -1              // state 0: initial, non-accepting
+  0 t                 //   trans. to state 0, label: true
+  1 p0                //   trans. to state 1, label: p0
+  -1                  // end of state 0
+  1 0 0 -1            // state 1: not initial, in acceptance set 0
+  1 p0                //   trans. to state 0, label: p0
+  -1                  // end if state 1
+
+You can force ltl2tgba to use the transition-based flavor of the
+format even for Büchi automaton using --lbtt=t.
+
+  % ltl2tgba --ba --lbtt=t FGp0
+  2 1t                // 2 states, 1 transition-based accepance set.
+  0 1                 // state 0: initial
+  0 -1 t              //   trans. to state 0, no acc., label: true
+  1 -1 p0             //   trans. to state 1, no acc., label: p0
+  -1                  // end of state 0
+  1 0                 // state 1: not initial
+  1 0 -1 p0           //   trans. to state 1, acc. 0, label: p0
+  -1                  // end if state 1
+
+When representing a Büchi automaton using transition-based acceptance,
+all transitions leaving accepting states are put into the acceptance set.
+
+A final note concerns the name of the atomic propositions.  The
+original LBTT and LBT formats require these atomic propositions to
+have names such as 'p0', 'p32', ...  We extend the format to accept
+atomic proposition with arbitrary names that do not conflict with
+LBT's operators (e.g. 'i' is the symbol of the implication operator so
+it may not be used as an atomic proposition), or as double-quoted
+strings.  Spot will always output atomic-proposition that do not match
+p[0-9]+ as double-quoted strings.
+
+  % bin/ltl2tgba --lbtt 'GFa & GFb'
+  1 2t
+  0 1
+  0 0 1 -1 & "a" "b"
+  0 0 -1 & "b" ! "a"
+  0 1 -1 & "a" ! "b"
+  0 -1 & ! "b" ! "a"
+  -1
+
 [SEE ALSO]
 .BR spot-x (7)

src/ltlvisit/lbt.cc

@@ -33,10 +33,11 @@ namespace spot
   {
     namespace
     {
+      // Does str match p[0-9]+ ?
       static bool
       is_pnum(const char* str)
       {
-	if (str[0] != 'p')
+	if (str[0] != 'p' || str[1] == 0)
 	  return false;
 	while (*++str)
 	  if (*str < '0' || *str > '9')

src/tgbaalgos/lbtt.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -25,10 +25,10 @@
 #include <string>
 #include <ostream>
 #include <sstream>
-#include "tgba/bddprint.hh"
 #include "tgba/tgbaexplicit.hh"
 #include "reachiter.hh"
 #include "misc/bddlt.hh"
+#include "ltlvisit/lbt.hh"
 #include "ltlparse/public.hh"
 
 namespace spot
@@ -70,54 +70,64 @@ namespace spot
       split_map sm;
     };
 
-    // Convert a BDD formula to the syntax used by LBTT's transition guards.
-    // Conjunctions are printed by bdd_format_sat, so we just have
-    // to handle the other cases.
-    static std::string
-    bdd_to_lbtt(bdd b, const bdd_dict* d)
-    {
-      if (b == bddfalse)
-	return "f";
-      else if (b == bddtrue)
-	return "t";
-      else
-	{
-	  bdd cube = bdd_satone(b);
-	  b -= cube;
-	  if (b != bddfalse)
-	    {
-	      return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d);
-	    }
-	  else
-	    {
-	      std::string res = "";
-	      for (int count = bdd_nodecount(cube); count > 1; --count)
-		res += "& ";
-	      return res + bdd_format_sat(d, cube);
-	    }
-	}
-
-    }
-
     class lbtt_bfs : public tgba_reachable_iterator_breadth_first
     {
     public:
-      lbtt_bfs(const tgba* a, std::ostream& os)
+      lbtt_bfs(const tgba* a, std::ostream& os, bool sba_format)
 	: tgba_reachable_iterator_breadth_first(a),
 	  os_(os),
-	  acc_count_(a->number_of_acceptance_conditions()),
+	  all_acc_conds_(a->all_acceptance_conditions()),
-	  acs_(a->all_acceptance_conditions())
+	  acs_(all_acc_conds_),
+	  sba_format_(sba_format),
+	  // If outputting with state-based acceptance, check if the
+	  // automaton can be converted into an sba. This makes the
+	  // state_is_accepting() function more efficient.
+	  sba_(sba_format ? dynamic_cast<const sba*>(a) : 0)
       {
       }
 
+      bool
+      state_is_accepting(const state *s) const
+      {
+	// If the automaton has a SBA type, it's easier to just query the
+	// state_is_accepting() method.
+	if (sba_)
+	  return sba_->state_is_accepting(s);
+
+	// Otherwise, since we are dealing with a degeneralized
+	// automaton nonetheless, the transitions leaving an accepting
+	// state are either all accepting, or all non-accepting.  So
+	// we just check the acceptance of the first transition.  This
+	// is not terribly efficient since we have to create the
+	// iterator.
+	tgba_succ_iterator* it = aut_->succ_iter(s);
+	it->first();
+	bool accepting =
+	  !it->done() && it->current_acceptance_conditions() == all_acc_conds_;
+	delete it;
+	return accepting;
+      }
+
+
       void
-      process_state(const state*, int n, tgba_succ_iterator*)
+      process_state(const state* s, int n, tgba_succ_iterator*)
       {
 	--n;
 	if (n == 0)
-	  body_ << "0 1" << std::endl;
+	  body_ << "0 1";
 	else
-	  body_ << "-1" << std::endl << n << " 0" << std::endl;
+	  body_ << "-1\n" << n << " 0";
+	// Do we have state-based acceptance?
+	if (sba_format_)
+	  {
+	    // We support only one acceptance condition in the
+	    // state-based format.
+	    if (state_is_accepting(s))
+	      body_ << " 0 -1";
+	    else
+	      body_ << " -1";
+	  }
+	body_ << "\n";
       }
 
       void
@@ -125,31 +135,44 @@ namespace spot
 		   const state*, int out, const tgba_succ_iterator* si)
       {
 	body_ << out - 1 << " ";
-	acs_.split(body_, si->current_acceptance_conditions());
+	if (!sba_format_)
-	body_ << "-1 " << bdd_to_lbtt(si->current_condition(),
+	  {
-				      aut_->get_dict()) << std::endl;
+	    acs_.split(body_, si->current_acceptance_conditions());
+	    body_ << "-1 ";
+	  }
+	const ltl::formula* f = bdd_to_formula(si->current_condition(),
+					       aut_->get_dict());
+	to_lbt_string(f, body_);
+	f->destroy();
+	body_ << "\n";
       }
 
       void
       end()
       {
-	os_ << seen.size() << " " << acc_count_ << "t" << std::endl
+	os_ << seen.size() << " ";
-	    << body_.str() << "-1" << std::endl;
+	if (sba_format_)
+	  os_ << "1";
+	else
+	  os_ << aut_->number_of_acceptance_conditions() << "t";
+	os_ << "\n" << body_.str() << "-1" << std::endl;
       }
 
     private:
       std::ostream& os_;
       std::ostringstream body_;
-      unsigned acc_count_;
+      bdd all_acc_conds_;
       acceptance_cond_splitter acs_;
+      bool sba_format_;
+      const sba* sba_;
     };
 
   } // anonymous
 
   std::ostream&
-  lbtt_reachable(std::ostream& os, const tgba* g)
+  lbtt_reachable(std::ostream& os, const tgba* g, bool sba)
   {
-    lbtt_bfs b(g, os);
+    lbtt_bfs b(g, os, sba);
     b.run();
     return os;
   }

src/tgbaalgos/lbtt.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -29,13 +29,15 @@
 
 namespace spot
 {
-  /// \brief Print reachable states in LBTT format.
+  /// \brief Print reachable states in LBTT's format.
   /// \ingroup tgba_io
   ///
   /// \param g The automata to print.
   /// \param os Where to print.
-  std::ostream& lbtt_reachable(std::ostream& os, const tgba* g);
+  /// \param sba Assume \a g is an SBA and use LBTT's state-based
-
+  /// acceptance format (similar to LBT's format).
+  std::ostream& lbtt_reachable(std::ostream& os, const tgba* g,
+			       bool sba = false);
 
   /// \brief Read an automaton in LBTT's format
   /// \ingroup tgba_io

src/tgbatest/lbttparse.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -38,8 +38,29 @@ do
   tr=`cat size | sed -n 's/transitions: //p'`
   l=`expr $st \* 2 + $tr + 1`
   test "$s" -eq "$l"
-done
 
+  # Do the same with bin/ltl2tgba
+  run 0 ../../bin/ltl2tgba --low --any --lbtt "$f" >out3
+  cmp out out3
+  head -n 1 out3 | grep t
+  # Make sure we output the state-based format
+  # for BA...
+  run 0 ../../bin/ltl2tgba --ba --lbtt --low --any "$f" >out4
+  head -n 1 out4 | grep t && exit 1
+  s4=`wc -l < out4`
+  test "$s" -eq "$s4"
+  run 0 ../ltl2tgba -t -XL out4 > out5
+  s5=`wc -l < out5`
+  test "$s" -eq "$s5"
+  # ... unless --lbtt=t is used.
+  run 0 ../../bin/ltl2tgba --ba --lbtt=t --low --any "$f" >out6
+  head -n 1 out6 | grep t
+  s6=`wc -l < out6`
+  test "$s" -eq "$s6"
+  run 0 ../ltl2tgba -t -XL out6 > out7
+  s7=`wc -l < out7`
+  test "$s" -eq "$s7"
+done
 
 # This is the output of 'lbt' on the formula 'U p0 p1'.
 cat >Up0p1 <<EOF

src/tgbatest/ltlcross2.test

@@ -37,4 +37,5 @@ ltl2tgba=../../bin/ltl2tgba
 "$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \
 "$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
 "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
+"$ltl2tgba --lbtt --ba --high %f > %T" \
 --json=output.json --csv=output.csv