Add support for printing LTL formulas using Wring's syntax.

* src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc
(to_wring_string): New option.
* src/bin/common_output.hh, src/bin/common_output.cc:
Add support for a --wring option.
* src/bin/ltlcheck.cc: Add %w and %W format specifiers.

src/bin/common_output.cc

@@ -26,6 +26,7 @@
 #include "error.h"
 
 #define OPT_SPOT 1
+#define OPT_WRING 2
 
 output_format_t output_format = spot_output;
 bool full_parenth = false;
@@ -37,6 +38,7 @@ static const argp_option options[] =
     { "spin", 's', 0, 0, "output in Spin's syntax", -20 },
     { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", -20 },
     { "lbt", 'l', 0, 0, "output in LBT's syntax", -20 },
+    { "wring", OPT_WRING, 0, 0, "output in Wring's syntax", -20 },
     { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 },
     { 0, 0, 0, 0, 0, 0 }
   };
@@ -64,6 +66,9 @@ parse_opt_output(int key, char*, struct argp_state*)
     case OPT_SPOT:
       output_format = spot_output;
       break;
+    case OPT_WRING:
+      output_format = wring_output;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }
@@ -105,6 +110,12 @@ output_formula(const spot::ltl::formula* f, const char* filename, int linenum)
       else
 	report_not_ltl(f, filename, linenum, "Spin");
       break;
+    case wring_output:
+      if (f->is_ltl_formula())
+	spot::ltl::to_wring_string(f, std::cout);
+      else
+	report_not_ltl(f, filename, linenum, "Wring");
+      break;
     case utf8_output:
       spot::ltl::to_utf8_string(f, std::cout, full_parenth);
       break;

src/bin/common_output.hh

@@ -25,7 +25,8 @@
 #include <argp.h>
 #include "ltlast/formula.hh"
 
-enum output_format_t { spot_output, spin_output, utf8_output, lbt_output };
+enum output_format_t { spot_output, spin_output, utf8_output,
+		       lbt_output, wring_output };
 extern output_format_t output_format;
 extern bool full_parenth;
 

src/bin/ltlcheck.cc

@@ -92,10 +92,11 @@ static const argp_option options[] =
     { 0, 0, 0, 0,
       "COMMANDFMT should specify input and output arguments using the "
       "following character sequences:", 3 },
-    { "%f,%s,%l", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+    { "%f,%s,%l,%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
-      "the formula as a (quoted) string in Spot, Spin, or LBT's syntax", 0 },
+      "the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax",
-    { "%F,%S,%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+      0 },
-      "the formula as a file in Spot, Spin, or LBT's syntax", 0 },
+    { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+      "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
     { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "the output automaton as a Never claim, or in LBTT's format", 0 },
     { 0, 0, 0, 0,
@@ -458,9 +459,11 @@ namespace
     quoted_string string_ltl_spot;
     quoted_string string_ltl_spin;
     quoted_string string_ltl_lbt;
+    quoted_string string_ltl_wring;
     quoted_string filename_ltl_spot;
     quoted_string filename_ltl_spin;
     quoted_string filename_ltl_lbt;
+    quoted_string filename_ltl_wring;
     // Run-specific variables
     printable_result_filename output;
   public:
@@ -472,9 +475,11 @@ namespace
       declare('f', &string_ltl_spot);
       declare('s', &string_ltl_spin);
       declare('l', &string_ltl_lbt);
+      declare('w', &string_ltl_wring);
       declare('F', &filename_ltl_spot);
       declare('S', &filename_ltl_spin);
       declare('L', &filename_ltl_lbt);
+      declare('W', &filename_ltl_wring);
       declare('N', &output);
       declare('T', &output);
 
@@ -503,6 +508,8 @@ namespace
 	return string_ltl_spot;
       if (!string_ltl_spin.val().empty())
 	return string_ltl_spin;
+      if (!string_ltl_wring.val().empty())
+	return string_ltl_wring;
       if (!string_ltl_lbt.val().empty())
 	return string_ltl_lbt;
       error(2, 0, "None of the translators need the input formula?");
@@ -518,12 +525,16 @@ namespace
 	string_ltl_spin = spot::ltl::to_spin_string(f, true);
       if (has('l') || has('L'))
 	string_ltl_lbt = spot::ltl::to_lbt_string(f);
+      if (has('w') || has('W'))
+	string_ltl_wring = spot::ltl::to_wring_string(f);
       if (has('F'))
 	string_to_tmp(string_ltl_spot, serial, filename_ltl_spot);
       if (has('S'))
 	string_to_tmp(string_ltl_spin, serial, filename_ltl_spin);
       if (has('L'))
 	string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt);
+      if (has('W'))
+	string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
     }
 
     const spot::tgba*

src/ltlvisit/tostring.cc

@@ -128,6 +128,36 @@ namespace spot
 	":",			// not supported
       };
 
+      const char* wring_kw[] = {
+	"FALSE",
+	"TRUE",
+	"[*0]",			// not supported
+	" ^ ",
+	" -> ",
+	" <-> ",
+	" U ",
+	" R ",
+	" W ",			// rewritten
+	" M ",			// rewritten
+	"<>-> ",		// not supported
+	"<>=> ",		// not supported
+	"<>+> ",		// not supported
+	"<>=+> ",		// not supported
+	"[]-> ",		// not supported
+	"[]=> ",		// not supported
+	"!",
+	"X",
+	"F",
+	"G",
+	" + ",
+	" | ",			// not supported
+	" * ",
+	" && ",			// not supported
+	" & ",			// not supported
+	";",			// not supported
+	":",			// not supported
+      };
+
       const char* utf8_kw[] = {
 	"0",
 	"1",
@@ -262,6 +292,8 @@ namespace spot
 	    {
 	      os_ << str;
 	    }
+	  if (kw_ == wring_kw)
+	    os_ << "=1";
 	  if (full_parent_)
 	    os_ << ")";
 	}
@@ -518,6 +550,15 @@ namespace spot
 		      overline = true;
 		      break;
 		    }
+	      // If we negate an atomic proposition for Wring,
+	      // output prop=0.
+	      if (kw_ == wring_kw)
+		if (const ltl::atomic_prop* ap = is_atomic_prop(uo->child()))
+		  if (is_bare_word(ap->name().c_str()))
+		    {
+		      os_ << ap->name() << "=0";
+		      goto skiprec;
+		    }
 	      emit(KNot);
 	      break;
 	    case unop::X:
@@ -570,6 +611,8 @@ namespace spot
 	      break;
 	    }
 
+	skiprec:
+
 	  if (full_parent_ && !top_level)
 	    closep();
 	  else if (overline)
@@ -782,5 +825,25 @@ namespace spot
       to_spin_string(f, os, full_parent);
       return os.str();
     }
+
+    std::ostream&
+    to_wring_string(const formula* f, std::ostream& os)
+    {
+      // Remove W and M.
+      f = unabbreviate_wm(f);
+      to_string_visitor v(os, true, false, wring_kw);
+      f->accept(v);
+      f->destroy();
+      return os;
+    }
+
+    std::string
+    to_wring_string(const formula* f)
+    {
+      std::ostringstream os;
+      to_wring_string(f, os);
+      return os.str();
+    }
+
   }
 }

src/ltlvisit/tostring.hh

@@ -74,7 +74,7 @@ namespace spot
     to_utf8_string(const formula* f, bool full_parent = false,
 		   bool ratexp = false);
 
-    /// \brief Output a formula as a (parsable by Spin) string.
+    /// \brief Output a formula as a string parsable by Spin.
     /// \param f The formula to translate.
     /// \param os The stream where it should be output.
     /// \param full_parent Whether or not the string should by fully
@@ -82,12 +82,21 @@ namespace spot
     std::ostream& to_spin_string(const formula* f, std::ostream& os,
 				 bool full_parent = false);
 
-    /// \brief Convert a formula into a (parsable by Spin) string.
+    /// \brief Convert a formula into a string parsable by Spin.
     /// \param f The formula to translate.
     /// \param full_parent Whether or not the string should by fully
     ///			   parenthesized.
     std::string to_spin_string(const formula* f, bool full_parent = false);
 
+    /// \brief Output a formula as a string parsable by Wring.
+    /// \param f The formula to translate.
+    /// \param os The stream where it should be output.
+    std::ostream& to_wring_string(const formula* f, std::ostream& os);
+
+    /// \brief Convert a formula into a string parsable by Wring
+    /// \param f The formula to translate.
+    std::string to_wring_string(const formula* f);
+
     /// @}
   }
 }