tostring: add LaTeX output

* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh
(to_latex_string): New function.
* src/bin/common_output.cc, src/bin/common_output.hh:
Add a --latex option.
* doc/tl/spotltl.sty: New file.
* doc/tl/Makefile.am: Distribute it.
* src/ltltest/latex.test: New test.
* src/ltltest/Makefile.am: Add it.
* NEWS: Mention it.

NEWS

@@ -69,6 +69,10 @@ New in spot 1.1.4a (not relased)
       default.  See the spot-x(7) man page for documentation about the
       related options: sat-minimize, sat-states, sat-acc, state-based.
 
+    - ltlfilt, genltl, and randltl now have a --latex option to output
+      formulas in a way that its easier to embed in a LaTeX document.
+      Each operator is output as a command such as \U, \F, etc.
+      doc/tl/spotltl.sty gives one possible definition for each macro.
 
   * New functions and classes in the library:
 
@@ -131,6 +135,8 @@ New in spot 1.1.4a (not relased)
       a couple of specializations for classes where is can be know
       without exploration.
 
+    - to_latex_string(): Output a formula using LaTeX syntax.
+
   * Noteworthy internal changes:
 
     - When minimize_obligation() is not given the formula associated

doc/tl/Makefile.am

@@ -28,7 +28,7 @@ LATEXMK = BIBINPUTS='$(srcdir)' latexmk -pdf -ps- -dvi- -pvc- \
   -e '$$pdflatex="pdflatex %O \"\\def\\SpotVersion{$(VERSION)}\\input{%S}\""'
 
 dist_pdf_DATA = $(srcdir)/tl.pdf
-EXTRA_DIST = tl.tex tl.bib
+EXTRA_DIST = tl.tex tl.bib spotltl.sty
 
 # latexmk produces its output in the current directory, and may not
 # update its timestamp when no rebuild was necessary.  This can cause

doc/tl/spotltl.sty

@@ -0,0 +1,49 @@
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{spotltl}[2013/08/28 Temporal Logic Operators for LTL and PSL]
+% NOTE: if you use amsmath.sty, make sure you include it before spotltl.sty
+% otherwise it will try to redefine some symbols from txfonts.
+\RequirePackage{txfonts}
+
+\newcommand{\ttrue}{\top}
+\newcommand{\ffalse}{\bot}
+\newcommand{\eword}{\varepsilon}  % empty word, denoted by [*0] in PSL
+
+% These three are not declared as operator 
+\newcommand{\F}{\mathsf{F}} % eventually
+\newcommand{\G}{\mathsf{G}} % always
+\newcommand{\X}{\mathsf{X}} % next
+% The \mathbin tell TeX to adjust spacing for binary operators
+\newcommand{\M}{\mathbin{\mathsf{M}}} % strong release
+\newcommand{\R}{\mathbin{\mathsf{R}}} % release
+\newcommand{\U}{\mathbin{\mathsf{U}}} % until
+\newcommand{\W}{\mathbin{\mathsf{W}}} % weak until
+
+% additional logical operators to complete \land, \lor, and \lnot.
+\newcommand{\limplies}{\rightarrow}
+\newcommand{\liff}{\leftrightarrow}
+\newcommand{\lxor}{\oplus}
+
+% Star-like PSL operators
+\newcommand{\SereStar}[1]{^{\star#1}}
+\newcommand{\SereEqual}[1]{^{=#1}}
+\newcommand{\SereGoto}[1]{^{\to#1}}
+\newcommand{\SerePlus}{^+}
+\newcommand{\SereFusion}{\mathbin{\mathsf{:}}}
+\newcommand{\SereConcat}{\mathbin{\mathsf{;}}}
+\newcommand{\SereOr}{\cup}
+\newcommand{\SereAnd}{\cap}
+\newcommand{\SereAndNLM}{\mathbin{\mathsf{\&}}}
+
+% Triggers and Seq operators, with their variant.  The *M variants of
+% these ope are internal "Marked" operators for Spot that should
+% normally not be output unless the formula is used to label a state
+% in an automaton (but we do not use LaTeX there).
+
+\newcommand{\seq}{\Diamondright}
+%\newcommand{\seqM}{\seq}
+\newcommand{\seqX}{\DiamondRight}
+%\newcommand{\seqXM}{\seqX}
+\newcommand{\triggers}{\boxright}
+\newcommand{\triggersX}{\boxRight}
+
+

src/bin/common_output.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -27,6 +27,7 @@
 
 #define OPT_SPOT 1
 #define OPT_WRING 2
+#define OPT_LATEX 3
 
 output_format_t output_format = spot_output;
 bool full_parenth = false;
@@ -40,6 +41,7 @@ static const argp_option options[] =
     { "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 },
+    { "latex", OPT_LATEX, 0, 0, "output using LaTeX macros", -20 },
     { 0, 0, 0, 0, 0, 0 }
   };
 
@@ -63,6 +65,9 @@ parse_opt_output(int key, char*, struct argp_state*)
     case 's':
       output_format = spin_output;
       break;
+    case OPT_LATEX:
+      output_format = latex_output;
+      break;
     case OPT_SPOT:
       output_format = spot_output;
       break;
@@ -119,6 +124,9 @@ output_formula(const spot::ltl::formula* f, const char* filename, int linenum)
     case utf8_output:
       spot::ltl::to_utf8_string(f, std::cout, full_parenth);
       break;
+    case latex_output:
+      spot::ltl::to_latex_string(f, std::cout, full_parenth);
+      break;
     }
   // Make sure we abort if we can't write to std::cout anymore
   // (like disk full or broken pipe with SIGPIPE ignored).

src/bin/common_output.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -26,7 +26,7 @@
 #include "ltlast/formula.hh"
 
 enum output_format_t { spot_output, spin_output, utf8_output,
-		       lbt_output, wring_output };
+		       lbt_output, wring_output, latex_output };
 extern output_format_t output_format;
 extern bool full_parenth;
 

src/ltltest/Makefile.am

@@ -95,6 +95,7 @@ TESTS = \
   kind.test \
   remove_x.test \
   ltlfilt.test \
+  latex.test \
   lbt.test \
   lenient.test \
   isop.test \

src/ltltest/latex.test

@@ -0,0 +1,62 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+set -e
+
+# Skip this test if we don't find a sufficiently complete LaTeX
+# installation
+
+(latexmk --version) || exit 77
+(pdflatex --version) || exit 77
+(kpsewhich txfonts.sty) || exit 77
+(kpsewhich amsmath.sty) || exit 77
+
+cat >input <<EOF
+XGFa <-> FGX(!b & !c) | (b ^ a)
+a U b W c R (d & e) M f
+{a;b[=2];((c:d*) && f*);e[*2..]}<>-> {((a | [*0])*;b[+]) & (c1[->2])}[]-> h
+{a;b;c} []=> {d*;e} <>=> !f
+!{a;b*;c}! -> d
+G(uglyname->Fuglierlongname42)
+EOF
+
+(
+cat <<\EOF
+\documentclass{article}
+\usepackage{amsmath}
+\usepackage{spotltl}
+\begin{document}
+\begin{align}
+EOF
+( ../../bin/ltlfilt --latex input;
+  ../../bin/genltl --go-theta=1..3 --latex ) | sed 's/$/\\\\/'
+cat <<\EOF
+\text{done}
+\end{align}
+\end{document}
+EOF
+) > output.tex
+
+TEXINPUTS=$srcdir/../../../doc/tl: latexmk -f -silent --pdf output.tex
+
+# latexmk will have a non-zero exit status on failure, so we will
+# detect that.  However the file output.pdf really ought to be
+# controled by eye...

src/ltlvisit/tostring.cc

@@ -49,12 +49,12 @@ namespace spot
 	KR,
 	KW,
 	KM,
-	KEConcat,
+	KSeq,
-	KEConcatNext,
+	KSeqNext,
-	KEConcatMarked,
+	KSeqMarked,
-	KEConcatMarkedNext,
+	KSeqMarkedNext,
-	KUConcat,
+	KTriggers,
-	KUConcatNext,
+	KTriggersNext,
 	KNot,
 	KX,
 	KF,
@@ -66,6 +66,13 @@ namespace spot
 	KAndNLM,
 	KConcat,
 	KFusion,
+	KOpenSERE,
+	KCloseSERE,
+	KCloseBunop,
+	KStarBunop,
+	KPlusBunop,
+	KEqualBunop,
+	KGotoBunop,
       };
 
       const char* spot_kw[] = {
@@ -96,6 +103,13 @@ namespace spot
 	" & ",
 	";",
 	":",
+	"{",
+	"}",
+	"]",
+	"[*",
+	"[+]",
+	"[=",
+	"[->",
       };
 
       const char* spin_kw[] = {
@@ -126,6 +140,13 @@ namespace spot
 	" & ",			// not supported
 	";",			// not supported
 	":",			// not supported
+	"{",			// not supported
+	"}",			// not supported
+	"]",			// not supported
+	"[*",			// not supported
+	"[+]",			// not supported
+	"[=",			// not supported
+	"[->",			// not supported
       };
 
       const char* wring_kw[] = {
@@ -156,6 +177,13 @@ namespace spot
 	" & ",			// not supported
 	";",			// not supported
 	":",			// not supported
+	"{",			// not supported
+	"}",			// not supported
+	"]",			// not supported
+	"[*",			// not supported
+	"[+]",			// not supported
+	"[=",			// not supported
+	"[->",			// not supported
       };
 
       const char* utf8_kw[] = {
@@ -186,6 +214,50 @@ namespace spot
 	" & ",
 	";",
 	":",
+	"{",
+	"}",
+	"]",
+	"[*",
+	"[+]",
+	"[=",
+	"[->",
+      };
+
+      const char* latex_kw[] = {
+	"\\ffalse",
+	"\\ttrue",
+	"\\eword",
+	" \\lxor ",
+	" \\limplies ",
+	" \\liff ",
+	" \\U ",
+	" \\R ",
+	" \\W ",
+	" \\M ",
+	"\\seq ",
+	"\\seqX ",
+	"\\seqM ",
+	"\\seqXM ",
+	"\\triggers ",
+	"\\triggersX ",
+	"\\lnot ",
+	"\\X ",
+	"\\F ",
+	"\\G ",
+	" \\lor ",
+	" \\SereOr ",
+	" \\land ",
+	" \\SereAnd ",
+	" \\SereAndNLM ",
+	" \\SereConcat ",
+	" \\SereFusion ",
+	"\\{",
+	"\\}",
+	"}",
+	"\\SereStar{",
+	"\\SerePlus{}",
+	"\\SereEqual{",
+	"\\SereGoto{",
       };
 
       static bool
@@ -258,17 +330,23 @@ namespace spot
 	void
 	openp() const
 	{
-	  os_ << (in_ratexp_ ? "{" : "(");
+	  if (in_ratexp_)
+	    emit(KOpenSERE);
+	  else
+	    os_ << "(";
 	}
 
 	void
 	closep() const
 	{
-	  os_ << (in_ratexp_ ? "}" : ")");
+	  if (in_ratexp_)
+	    emit(KCloseSERE);
+	  else
+	    os_ << ")";
 	}
 
 	std::ostream&
-	emit(int symbol)
+	emit(int symbol) const
 	{
 	  return os_ << kw_[symbol];
 	}
@@ -292,7 +370,28 @@ namespace spot
 	    }
 	  else
 	    {
-	      os_ << str;
+	      if (kw_ == latex_kw)
+		{
+		  size_t s = str.size();
+		  while (str[s - 1] >= '0' && str[s - 1] <= '9')
+		    {
+		      --s;
+		      assert(s != 0); // bare words cannot start with letters
+		    }
+		  if (s > 1)
+		    os_ << "\\mathit{";
+		  os_ << str.substr(0, s);
+		  if (s > 1)
+		    os_ << "}";
+		  if (s != str.size())
+		    os_ << "_{"
+			<< str.substr(s)
+			<< "}";
+		}
+	      else
+		{
+		  os_ << str;
+		}
 	    }
 	  if (kw_ == wring_kw)
 	    os_ << "=1";
@@ -336,8 +435,8 @@ namespace spot
 	    case binop::UConcat:
 	    case binop::EConcat:
 	    case binop::EConcatMarked:
-	      os_ << "{";
 	      in_ratexp_ = true;
+	      openp();
 	      top_level_ = true;
 	      {
 		const multop* m = is_multop(bo->first(), multop::Concat);
@@ -384,26 +483,26 @@ namespace spot
 	      emit(KM);
 	      break;
 	    case binop::UConcat:
-	      os_ << "}";
+	      closep();
-	      emit(onelast ? KUConcatNext : KUConcat);
+	      emit(onelast ? KTriggersNext : KTriggers);
 	      in_ratexp_ = false;
-	      top_level_ = top_level;
+	      top_level_ = false;
 	      break;
 	    case binop::EConcat:
+	      emit(KCloseSERE);
 	      if (bo->second() == constant::true_instance())
 		{
-		  os_ << "}!";
+		  os_ << "!";
 		  in_ratexp_ = false;
 		  goto second_done;
 		}
-	      os_ << "}";
+	      emit(onelast ? KSeqNext : KSeq);
-	      emit(onelast ? KEConcatNext : KEConcat);
 	      in_ratexp_ = false;
 	      top_level_ = false;
 	      break;
 	    case binop::EConcatMarked:
 	      os_ << "}";
-	      emit(onelast ? KEConcatMarkedNext : KEConcatMarked);
+	      emit(onelast ? KSeqMarkedNext : KSeqMarked);
 	      in_ratexp_ = false;
 	      top_level_ = false;
 	      break;
@@ -471,16 +570,16 @@ namespace spot
 	    case Star:
 	      if (min == 1 && max == bunop::unbounded)
 		{
-		  os_ << "[+]";
+		  emit(KPlusBunop);
 		  return;
 		}
-	      os_ << "[*";
+	      emit(KStarBunop);
 	      break;
 	    case Equal:
-	      os_ << "[=";
+	      emit(KEqualBunop);
 	      break;
 	    case Goto:
-	      os_ << "[->";
+	      emit(KGotoBunop);
 	      default_min = 1;
 	      default_max = 1;
 	      break;
@@ -517,7 +616,7 @@ namespace spot
 		    os_ << max;
 		}
 	    }
-	  os_ << "]";
+	  emit(KCloseBunop);
 	}
 
 	void
@@ -667,12 +766,15 @@ namespace spot
 		      // in which case it's b[=1].
 		      if (i + 2 < max && mo->nth(i) == mo->nth(i + 2))
 			{
-			  os_ << "[=1]";
+			  emit(KEqualBunop);
+			  os_ << "1";
+			  emit(KCloseBunop);
 			  i += 2;
 			}
 		      else
 			{
-			  os_ << "[->]";
+			  emit(KGotoBunop);
+			  emit(KCloseBunop);
 			  ++i;
 			}
 		      continue;
@@ -685,7 +787,7 @@ namespace spot
 			  if (b1 == b2)
 			    {
 			      emit_bunop_child(b1);
-			      os_ << "[=";
+			      emit(KEqualBunop);
 			      unsigned min = s->min();
 			      os_ << min;
 			      unsigned max = s->max();
@@ -695,7 +797,7 @@ namespace spot
 				  if (max != bunop::unbounded)
 				    os_ << max;
 				}
-			      os_ << "]";
+			      emit(KCloseBunop);
 			      ++i;
 			      continue;
 			    }
@@ -847,5 +949,24 @@ namespace spot
       return os.str();
     }
 
+    std::ostream&
+    to_latex_string(const formula* f, std::ostream& os,
+		    bool full_parent, bool ratexp)
+    {
+      to_string_visitor v(os, full_parent, ratexp, latex_kw);
+      f->accept(v);
+      return os;
+    }
+
+    std::string
+    to_latex_string(const formula* f,
+		    bool full_parent, bool ratexp)
+    {
+      std::ostringstream os;
+      to_latex_string(f, os, full_parent, ratexp);
+      return os.str();
+    }
+
+
   }
 }

src/ltlvisit/tostring.hh

@@ -101,6 +101,27 @@ namespace spot
     SPOT_API std::string
     to_wring_string(const formula* f);
 
+    /// \brief Output a formula as an LaTeX string which is parsable unless
+    /// the formula contains automaton operators (used in ELTL formulae).
+    /// \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
+    ///			   parenthesized.
+    /// \param ratexp Whether we are printing a SERE.
+    SPOT_API std::ostream&
+    to_latex_string(const formula* f, std::ostream& os,
+		    bool full_parent = false, bool ratexp = false);
+
+    /// \brief Output a formula as a LaTeX string which is parsable
+    /// unless the formula contains automaton operators (used in ELTL formulae).
+    /// \param f The formula to translate.
+    /// \param full_parent Whether or not the string should by fully
+    ///			   parenthesized.
+    /// \param ratexp Whether we are printing a SERE.
+    SPOT_API std::string
+    to_latex_string(const formula* f,
+		    bool full_parent = false, bool ratexp = false);
+
     /// @}
   }
 }