genltl: move all formula generation code to spot/gen/

Fixes #254.

* spot/gen/formulas.cc, spot/gen/formulas.hh: New files.
* spot/gen/Makefile.am: Add them.
* spot/Makefile.am: Fix build order.
* bin/genltl.cc: Move most code to the above files and adjust.
* bin/Makefile.am: Link genltl with libspotgen.
* doc/org/arch.tex: Adjust picture to show that genltl uses
libspotgen.
* python/spot/gen.i: Include formulas.hh.
* tests/python/gen.py: Make sure genltl() and ltl_pattern_name()
can be called.

bin/Makefile.am

@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2012, 2013, 2014, 2015, 2016-2017 Laboratoire de Recherche
+## Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
-## et Développement de l'Epita (LRDE).
+## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -79,6 +79,7 @@ ltlfilt_SOURCES = ltlfilt.cc
 genaut_SOURCES = genaut.cc
 genaut_LDADD = $(top_builddir)/spot/gen/libspotgen.la $(LDADD)
 genltl_SOURCES = genltl.cc
+genltl_LDADD = $(top_builddir)/spot/gen/libspotgen.la $(LDADD)
 randaut_SOURCES = randaut.cc
 randltl_SOURCES = randltl.cc
 ltl2tgba_SOURCES = ltl2tgba.cc

doc/org/arch.tex

@@ -20,7 +20,6 @@
   \node[cppbox=14.12cm] (libspot) {\texttt{libspot\strut}};
   \node[shbox=3cm,above right=2mm and 0mm of libspot.north west,align=center] (shcmd) {
     \texttt{randltl}\\
-    \texttt{genltl}\\
     \texttt{ltlfilt}\\
     \texttt{randaut}\\
     \texttt{autfilt}\\
@@ -36,7 +35,10 @@
   \node[pybox=2.5cm,above right=0mm and 2mm of buddy.south east,double height] (pyspot) {\texttt{import spot}};
   \node[cppbox=4cm,above right=0mm and 2mm of pyspot.south east] (libltsmin) {\texttt{libspotltsmin\strut}};
 
-  \node[shbox=1.5cm,above right=2mm and 0mm of libgen.north west,align=center] (genaut) {\texttt{genaut}};
+  \node[shbox=1.5cm,above right=2mm and 0mm of libgen.north west,align=center] (genaut) {
+    \texttt{genaut\strut}\\
+    \texttt{genltl}
+  };
 
   \node[pybox=3cm,above left=2mm and 0mm of libgen.north east] (pygen) {\texttt{import spot.gen\strut}};
   \node[pybox=2.5cm,above=of buddy] (pybuddy) {\texttt{import bdd\strut}};

python/spot/gen.i

@@ -33,6 +33,7 @@
 
 %{
 #include <spot/gen/automata.hh>
+#include <spot/gen/formulas.hh>
 using namespace spot;
 %}
 
@@ -51,3 +52,4 @@ using namespace spot;
 }
 
 %include <spot/gen/automata.hh>
+%include <spot/gen/formulas.hh>

spot/Makefile.am

@@ -25,8 +25,8 @@ AUTOMAKE_OPTIONS = subdir-objects
 # List directories in the order they must be built.  Keep tests at the
 # end, after building '.' (since the current directory contains
 # libspot.la needed by the tests)
-SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke	gen \
+SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \
-          parseaut parsetl . ltsmin
+          parseaut parsetl . ltsmin gen
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =

spot/gen/Makefile.am

@@ -21,10 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 spotgendir = $(pkgincludedir)/gen
-spotgen_HEADERS = automata.hh
+spotgen_HEADERS = automata.hh formulas.hh
 
 lib_LTLIBRARIES = libspotgen.la
-libspotgen_la_SOURCES = \
+libspotgen_la_SOURCES = automata.cc formulas.cc
-  automata.cc
+libspotgen_la_LDFLAGS = ../libspot.la -no-undefined $(SYMBOLIC_LDFLAGS)
-#libspotgen_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined $(SYMBOLIC_LDFLAGS)
-

spot/gen/formulas.hh

@@ -0,0 +1,219 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 Laboratoire de Recherche et Developpement 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/>.
+
+#pragma once
+
+#include <spot/tl/formula.hh>
+
+
+// Families defined here come from the following papers:
+//
+// @InProceedings{cichon.09.depcos,
+//   author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski},
+//   title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas},
+//   booktitle = {Proceedings of the Fourth International Conference on
+//                Dependability of Computer Systems},
+//   pages = {17--24},
+//   year = 2009,
+//   publisher = {IEEE Computer Society},
+// }
+//
+// @InProceedings{geldenhuys.06.spin,
+//   author = {Jaco Geldenhuys and Henri Hansen},
+//   title = {Larger Automata and Less Work for LTL Model Checking},
+//   booktitle = {Proceedings of the 13th International SPIN Workshop},
+//   year = {2006},
+//   pages = {53--70},
+//   series = {Lecture Notes in Computer Science},
+//   volume = {3925},
+//   publisher = {Springer}
+// }
+//
+// @InProceedings{gastin.01.cav,
+//   author = {Paul Gastin and Denis Oddoux},
+//   title = {Fast {LTL} to {B\"u}chi Automata Translation},
+//   booktitle        = {Proceedings of the 13th International Conference on
+//                   Computer Aided Verification (CAV'01)},
+//   pages = {53--65},
+//   year = 2001,
+//   editor = {G. Berry and H. Comon and A. Finkel},
+//   volume = {2102},
+//   series = {Lecture Notes in Computer Science},
+//   address = {Paris, France},
+//   publisher = {Springer-Verlag}
+// }
+//
+// @InProceedings{rozier.07.spin,
+//   author = {Kristin Y. Rozier and Moshe Y. Vardi},
+//   title = {LTL Satisfiability Checking},
+//   booktitle = {Proceedings of the 12th International SPIN Workshop on
+//                   Model Checking of Software (SPIN'07)},
+//   pages = {149--167},
+//   year = {2007},
+//   volume = {4595},
+//   series = {Lecture Notes in Computer Science},
+//   publisher = {Springer-Verlag}
+// }
+//
+// @InProceedings{dwyer.98.fmsp,
+//   author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett},
+//   title         = {Property Specification Patterns for Finite-state
+//                   Verification},
+//   booktitle     = {Proceedings of the 2nd Workshop on Formal Methods in
+//                   Software Practice (FMSP'98)},
+//   publisher     = {ACM Press},
+//   address       = {New York},
+//   editor        = {Mark Ardis},
+//   month         = mar,
+//   year          = {1998},
+//   pages         = {7--15}
+// }
+//
+// @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}
+// }
+//
+// @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{tabakov.10.rv,
+//   author = {Deian Tabakov and Moshe Y. Vardi},
+//   title = {Optimized Temporal Monitors for {SystemC}},
+//   booktitle = {Proceedings of the 1st International Conference on Runtime
+//		  Verification (RV'10)},
+//   pages = {436--451},
+//   year = 2010,
+//   volume = {6418},
+//   series = {Lecture Notes in Computer Science},
+//   month = nov,
+//   publisher = {Springer}
+// }
+//
+// @InProceedings{kupferman.10.mochart,
+//   author = {Orna Kupferman and And Rosenberg},
+//   title = {The Blow-Up in Translating LTL do Deterministic Automata},
+//   booktitle = {Proceedings of the 6th International Workshop on Model
+//                Checking and Artificial Intelligence (MoChArt 2010)},
+//   pages = {85--94},
+//   year = 2011,
+//   volume = {6572},
+//   series = {Lecture Notes in Artificial Intelligence},
+//   month = nov,
+//   publisher = {Springer}
+// }
+//
+// @techreport{holevek.04.tr,
+//    title = {Verification Results in {Liberouter} Project},
+//    author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak
+//              and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek},
+//    month = {September},
+//    year = 2004,
+//    number = 03,
+//    institution = {CESNET}
+// }
+//
+// @InProceedings{pelanek.07.spin,
+//   author = {Radek Pel\'{a}nek},
+//   title = {{BEEM}: benchmarks for explicit model checkers},
+//   booktitle = {Proceedings of the 14th international SPIN conference on
+//     Model checking software},
+//   year = 2007,
+//   pages = {263--267},
+//   numpages = {5},
+//   volume = {4595},
+//   series = {Lecture Notes in Computer Science},
+//   publisher = {Springer-Verlag}
+// }
+
+namespace spot
+{
+  namespace gen
+  {
+    enum ltl_pattern {
+      FIRST_CLASS = 256,
+      AND_F = FIRST_CLASS,
+      AND_FG,
+      AND_GF,
+      CCJ_ALPHA,
+      CCJ_BETA,
+      CCJ_BETA_PRIME,
+      DAC_PATTERNS,
+      EH_PATTERNS,
+      GH_Q,
+      GH_R,
+      GO_THETA,
+      HKRSS_PATTERNS,
+      KR_N,
+      KR_NLOGN,
+      KV_PSI,
+      OR_FG,
+      OR_G,
+      OR_GF,
+      P_PATTERNS,
+      R_LEFT,
+      R_RIGHT,
+      RV_COUNTER,
+      RV_COUNTER_CARRY,
+      RV_COUNTER_CARRY_LINEAR,
+      RV_COUNTER_LINEAR,
+      SB_PATTERNS,
+      TV_F1,
+      TV_F2,
+      TV_G1,
+      TV_G2,
+      TV_UU,
+      U_LEFT,
+      U_RIGHT,
+      LAST_CLASS,
+    };
+
+    /// \brief generate an LTL from a known pattern
+    ///
+    /// The pattern is specified using one value from the ltl_pattern
+    /// enum.  See the man page of the `genltl` binary for a
+    /// description of those pattern, and bibliographic references.
+    SPOT_API formula genltl(ltl_pattern pattern, int n);
+
+    /// \brief convert an ltl_pattern value into a name
+    ///
+    /// The returned name is suitable to be used as an option
+    /// key for the genltl binary.
+    SPOT_API const char* ltl_pattern_name(ltl_pattern pattern);
+  }
+}

tests/python/gen.py

@@ -37,3 +37,22 @@ except RuntimeError as e:
     assert 'positive argument' in str(e)
 else:
     exit(2)
+
+f = gen.genltl(gen.AND_F, 3)
+assert f.size() == 3
+assert gen.ltl_pattern_name(gen.AND_F) == "and-f"
+
+try:
+    gen.genltl(1000, 3)
+except RuntimeError as e:
+    assert 'unsupported pattern' in str(e)
+else:
+    exit(2)
+
+try:
+    gen.genltl(gen.OR_G, -10)
+except RuntimeError as e:
+     assert 'or-g' in str(e)
+     assert 'positive' in str(e)
+else:
+    exit(2)