Add documentation for temporal logic operators.

* doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files.
* doc/Makefile.am (SUBDIRS): Recurse into tl/.
* configure.ac: Output doc/tl/Makefile
* README: Describe doc/tl/.

README

@@ -143,7 +143,8 @@ src/              Sources for libspot.
    neverparse/    Parser for SPIN never claims.
    sanity/        Sanity tests for the whole project.
 doc/              Documentation for libspot.
-   spot.html/     HTML reference manual.
+   tl/            Documentation of the Temporal Logic operators.
+   spot.html/     HTML reference manual for the library.
 bench/            Benchmarks for ...
    emptchk/       ... emptiness-check algorithms,
    gspn-ssp/      ... various symmetry-based methods with GreatSPN,

configure.ac

@@ -118,6 +118,7 @@ AC_CONFIG_FILES([
   bench/wdba/defs
   doc/Doxyfile
   doc/Makefile
+  doc/tl/Makefile
   iface/dve2/defs
   iface/dve2/Makefile
   iface/gspn/defs

doc/Makefile.am

@@ -23,6 +23,8 @@
 
 DOXYGEN = doxygen
 
+SUBDIRS = tl
+
 .PHONY: doc fast-doc
 
 all-local: $(srcdir)/stamp

doc/tl/.gitignore

@@ -0,0 +1,6 @@
+*.bbl
+*.blg
+*.idx
+*.log
+*.out
+tmp.t2d

doc/tl/Makefile.am

@@ -0,0 +1,33 @@
+## Copyright (C) 2011 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+
+all: $(srcdir)/tl.pdf
+TEXI2PDF = texi2dvi --pdf
+TEXI2PDF_FLAGS =  --tidy --build-dir=tmp.t2d --batch
+
+dist_pdf_DATA = $(srcdir)/tl.pdf
+
+$(srcdir)/tl.pdf: $(srcdir)/tl.tex $(srcdir)/tl.bib
+	$(TEXI2PDF) $(TEXI2PDF_FLAGS) -o $@ $<
+
+.PHONY: mostlyclean-local
+mostlyclean-local:
+	rm -rf tmp.t2d

doc/tl/tl.bib

@@ -0,0 +1,101 @@
+@InProceedings{	  somenzi.00.cav,
+  author	= {Fabio Somenzi and Roderick Bloem},
+  title		= {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
+  booktitle	= {Proceedings of the 12th International Conference on
+		  Computer Aided Verification (CAV'00)},
+  pages		= {247--263},
+  year		= {2000},
+  volume	= {1855},
+  series	= {Lecture Notes in Computer Science},
+  address	= {Chicago, Illinois, USA},
+  publisher	= {Springer-Verlag}
+}
+
+@InProceedings{	  etessami.00.concur,
+  author	= {Kousha Etessami and Gerard J. Holzmann},
+  title		= {Optimizing {B\"u}chi Automata},
+  booktitle	= {Proceedings of the 11th International Conference on
+		  Concurrency Theory (Concur'00)},
+  pages		= {153--167},
+  year		= {2000},
+  editor	= {C. Palamidessi},
+  volume	= {1877},
+  series	= {Lecture Notes in Computer Science},
+  address	= {Pennsylvania, USA},
+  publisher	= {Springer-Verlag},
+  note          = {Beware of a typo in the version from the
+                  proceedings: $f \U g$ is purely eventual if both
+                  operands are purely eventual.  The revision of the
+                  paper available at
+                  \url{http://www.bell-labs.com/project/TMP/} is
+                  fixed.  We fixed the bug in Spot in 2005, thanks to
+                  LBTT.  See also \url{http://arxiv.org/abs/1011.4214v2}
+                  for a discussion about this problem.}
+}
+
+@InProceedings{manna.87.podc,
+ author = {Zohar Manna and Amir Pnueli},
+ title = {A hierarchy of temporal properties},
+ booktitle = {Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC'90)},
+ year = {1990},
+ location = {Quebec City, Canada},
+ pages = {377--410},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@InProceedings{	  chang.92.icalp,
+  author	= {Edward Y. Chang and Zohar Manna and Amir Pnueli},
+  title		= {Characterization of Temporal Property Classes},
+  booktitle	= {Proceedings of the 19th International Colloquium on
+		  Automata, Languages and Programming (ICALP'92)},
+  year		= {1992},
+  pages		= {474--486},
+  publisher	= {Springer-Verlag},
+  address	= {London, UK}
+}
+
+@InProceedings{	  cerna.03.mfcs,
+  author	= {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
+  title		= {Relating Hierarchy of Temporal Properties to Model
+		  Checking},
+  booktitle	= {Proceedings of the 28th International Symposium on
+		  Mathematical Foundations of Computer Science (MFCS'03)},
+  pages		= {318--327},
+  year		= {2003},
+  editor	= {Branislav Rovan and Peter Vojt{\'a}{\v{a}}},
+  volume	= {2747},
+  series	= {Lecture Notes in Computer Science},
+  address	= {Bratislava, Slovak Republic},
+  month		= aug,
+  publisher	= {Springer-Verlag}
+}
+
+@InProceedings{	  schneider.01.lpar,
+  author	= {Klaus Schneider},
+  title		= {Improving Automata Generation for Linear Temporal Logic by
+		  Considering the Automaton Hierarchy},
+  booktitle	= {Proceedings of the 8th International Conference on Logic
+		  for Programming, Artificial Intelligence and Reasoning},
+  pages		= {39--54},
+  year		= {2001},
+  volume	= {2250},
+  series	= {Lecture Notes in Artificial Intelligence},
+  address	= {Havana, Cuba},
+  publisher	= {Springer-Verlag}
+}
+
+@TechReport{	  tauriainen.03.a83,
+  author	= {Heikki Tauriainen},
+  title		= {On Translating Linear Temporal Logic into Alternating and
+		  Nondeterministic Automata},
+  institution	= {Helsinki University of Technology, Laboratory for
+		  Theoretical Computer Science},
+  address	= {Espoo, Finland},
+  month		= dec,
+  number	= {A83},
+  pages		= {132},
+  type		= {Research Report},
+  year		= {2003},
+  note		= {Reprint of Licentiate's thesis}
+}