Preliminary implementation of a tool to generate some interesting

families of LTL formulae.

* src/ltltest/genltl.cc: New file.  Based on five classes of
formulae defined in a paper by Cichón, Czubak, and Jasiński.
* src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl.

ChangeLog

+2010-12-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Preliminary implementation of a tool to generate some interesting
+	families of LTL formulae.
+
+	* src/ltltest/genltl.cc: New file.  Based on five classes of
+	formulae defined in a paper by Cichón, Czubak, and Jasiński.
+	* src/ltltest/Makefile.am (noinst_PROGRAMS): Build genltl.
+
 2010-12-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Add full_parent support to to_spin_string().
@@ -587,7 +596,7 @@
 	Optimize tgba_tba_proxy and tgba_sba_proxy for states that share
 	an acceptance condition on all outgoing transitions.
 
-	This was motivated by experiments from Rdiger Ehlers, showing
+	This was motivated by experiments from Rüdiger Ehlers, showing
 	that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
 	U (b U c)'".  With this change and the previous one, it is no
 	longer the case.
@@ -610,7 +619,7 @@
 	* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
 	degeneralization, because it might remove useless acceptance
 	conditions.  I realized this while looking at experiments from
-	Rdiger Ehlers.
+	Rüdiger Ehlers.
 
 2010-02-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
@@ -620,7 +629,7 @@
 
 	Work around a spurious style.test error.
 
-	* src/saba/sabacomplementtgba.hh (spot): Rewrite Bchi as B\"uchi
+	* src/saba/sabacomplementtgba.hh (spot): Rewrite Büchi as B\"uchi
 	is the BibTex entry used as comment, because some version of sed
 	will choke on non-ascii character and cause sanity/style.test to
 	fail.
@@ -1242,12 +1251,12 @@
 
 2009-11-30  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 
-	Add a new type of automata: State-labeled Alternating Bchi
+	Add a new type of automata: State-labeled Alternating Büchi
 	Automata (SABA).
 
 	* src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh,
 	src/saba/sabasucciter.hh: New.  Interface for
-	SABA (State-labeled Alternating Bchi Automata).
+	SABA (State-labeled Alternating Büchi Automata).
 	* src/saba/explicitstateconjunction.cc,
 	src/saba/explicitstateconjunction.hh: New.  Default
 	implementation for a conjunction of states.
@@ -1843,7 +1852,7 @@
 
 2009-10-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
-	* AUTHORS: Add Damien Lefortier, Guillaume Sadegh, and Flix
+	* AUTHORS: Add Damien Lefortier, Guillaume Sadegh, and Félix
 	Abecassis.
 
 2009-10-01  Guillaume Sadegh  <sadegh@lrde.epita.fr>
@@ -2043,7 +2052,7 @@
 
 	* src/tgba/tgbacomplement.cc: Stay on 80 columns.
 
-2009-07-08  Flix Abecassis <abecassis@lrde.epita.fr>
+2009-07-08  Félix Abecassis <abecassis@lrde.epita.fr>
 
 	Add 2 benchmarks directories.
 	Add an algorithm to split an automaton in several automata.
@@ -2095,7 +2104,7 @@
 	automaton into a TGBA instead of a TBA.
 
 	* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc:
-	Adjust the transformation from Streett to Bchi to support
+	Adjust the transformation from Streett to Büchi to support
 	generalized acceptance conditions.
 	* src/tgbatest/complementation.cc: Improve output messages.
 	* src/tgbatest/complementation.test: New tests.
@@ -2125,7 +2134,7 @@
 
 2009-06-05  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 
-	Add an algorithm to complement Bchi automata.
+	Add an algorithm to complement Büchi automata.
 
 	* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New
 	files. The complementation algorithm.
@@ -4944,10 +4953,10 @@
 	* src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do
 	not parenthesize the type after the new operator (g++ 3.4 complains).
 	* src/tgbaalgos/dupexp.cc (dupexp_iter::process_state,
-	dupexp_iter::declare_state): Use this->automata_instead of
+	dupexp_iter::declare_state): Use this->automata_ instead of
 	automata_.  Local protected member automata_ inherited from
 	template base class must be prefixed or g++ 3.4 will not look it
-	up (conforming to 14.6.2.3).
+	up (conforming to §14.6.2.3).
 
 2004-07-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
@@ -8208,7 +8217,7 @@
 	not a bdd.
 	* src/tgba/tgbabddconcrete.cc: Likewise.
 
-	Initial code for TGBA (Transition Generalized Bchi Automata).
+	Initial code for TGBA (Transition Generalized Büchi Automata).
 	Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
 	a LTL-to-TGBA translator using Couvreur's algorithm.
 

src/ltltest/.gitignore

@@ -21,3 +21,4 @@ randltl
 *.dot
 reductau
 reductaustr
+genltl

src/ltltest/Makefile.am

-## Copyright (C) 2009 Laboratoire de Recherche et Développement
+## Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
@@ -43,6 +43,7 @@ check_PROGRAMS = \
   tunenoform
 
 noinst_PROGRAMS = \
+  genltl \
   randltl
 
 equals_SOURCES = equals.cc

src/ltltest/genltl.cc

+// Copyright (C) 2010 Laboratoire de Recherche et Dveloppement 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.
+
+#include <cassert>
+#include <iostream>
+#include <sstream>
+#include <set>
+#include <string>
+#include <cstdlib>
+#include <cstring>
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/tostring.hh"
+#include "ltlenv/defaultenv.hh"
+
+using namespace spot;
+using namespace spot::ltl;
+
+environment& env(default_environment::instance());
+
+
+
+// The five first classes defined here come from the following paper:
+//
+// @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},
+// }
+
+void
+syntax(char* prog)
+{
+  std::cerr << "Usage: "<< prog << " [-s] F N" << std::endl
+	    << std::endl
+	    << "-s output using Spin's syntax" << std::endl
+	    << "F  specifies the familly of LTL formula to build" << std::endl
+	    << "N  is the size parameter of the familly" << std::endl
+	    << std::endl
+	    << "Classes available (F):" << std::endl
+	    << "  1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))"
+	    << std::endl
+	    << "  2: p&X(p&X(p&...X(p)))) & X(q&F(q&F(q&...F(q))))"
+	    << std::endl
+	    << "  3: p&(Xp)&(XXp)&...(X...X(p)) & p&(Xq)&(XXq)&...(X...X(q))"
+	    << std::endl
+	    << "  4: GF(p1)&GF(p2)&...&GF(pn)"
+	    << std::endl
+	    << "  5: FG(p1)|GF(p2)|...|GF(pn)"
+	    << std::endl;
+  exit(2);
+}
+
+int
+to_int(const char* s)
+{
+  char* endptr;
+  int res = strtol(s, &endptr, 10);
+  if (*endptr)
+    {
+      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
+      exit(1);
+    }
+  return res;
+}
+
+
+// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
+formula* E_n(std::string name, int n)
+{
+  if (n <= 0)
+    return constant::true_instance();
+
+  formula* result = 0;
+
+  for (; n > 0; --n)
+    {
+      std::ostringstream p;
+      p << name << n;
+      formula* f = env.require(p.str());
+      if (result)
+	result = multop::instance(multop::And, f, result);
+      else
+	result = f;
+      result = unop::instance(unop::F, result);
+    }
+  return result;
+}
+
+// p & X(p & X(p & ... X(p)))
+formula* phi_n(std::string name, int n)
+{
+  if (n <= 0)
+    return constant::true_instance();
+
+  formula* result = 0;
+  formula* p = env.require(name);
+  for (; n > 0; --n)
+    {
+      if (result)
+	result =
+	  multop::instance(multop::And, p->clone(),
+			   unop::instance(unop::X, result));
+      else
+	result = p;
+    }
+  return result;
+}
+
+formula* N_n(std::string name, int n)
+{
+  return unop::instance(unop::F, phi_n(name, n));
+}
+
+// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
+formula* phi_prime_n(std::string name, int n)
+{
+  if (n <= 0)
+    return constant::true_instance();
+
+  formula* result = 0;
+  formula* p = env.require(name);
+  for (; n > 0; --n)
+    {
+      if (result)
+	{
+	  p = unop::instance(unop::X, p->clone());
+	  result = multop::instance(multop::And, result, p);
+	}
+      else
+	{
+	  result = p;
+	}
+    }
+  return result;
+}
+
+formula* N_prime_n(std::string name, int n)
+{
+  return unop::instance(unop::F, phi_prime_n(name, n));
+}
+
+
+// GF(p_1) | GF(p_2) | ... | GF(p_n)
+formula* FG_n(std::string name, int n)
+{
+  if (n <= 0)
+    return constant::true_instance();
+
+  formula* result = 0;
+
+  for (int i = 1; i <= n; ++i)
+    {
+      std::ostringstream p;
+      p << name << i;
+      formula* f = unop::instance(unop::G,
+				  unop::instance(unop::F,
+						 env.require(p.str())));
+
+      if (result)
+	result = multop::instance(multop::And, f, result);
+      else
+	result = f;
+    }
+  return result;
+}
+
+// FG(p_1) | FG(p_2) | ... | FG(p_n)
+formula* GF_n(std::string name, int n)
+{
+  if (n <= 0)
+    return constant::false_instance();
+
+  formula* result = 0;
+
+  for (int i = 1; i <= n; ++i)
+    {
+      std::ostringstream p;
+      p << name << i;
+      formula* f = unop::instance(unop::F,
+				  unop::instance(unop::G,
+						 env.require(p.str())));
+
+      if (result)
+	result = multop::instance(multop::Or, f, result);
+      else
+	result = f;
+    }
+  return result;
+}
+
+int
+main(int argc, char** argv)
+{
+  bool spin_syntax = false;
+  if (argc >= 2 && !strcmp(argv[1], "-s"))
+    {
+      spin_syntax = true;
+      --argc;
+      ++argv;
+    }
+
+  if (argc != 3)
+    syntax(argv[0]);
+
+  int f = to_int(argv[1]);
+  int n = to_int(argv[2]);
+
+  formula* res = 0;
+
+  switch (f)
+    {
+    case 1:
+      res = multop::instance(multop::And, E_n("p", n), E_n("q", n));
+      break;
+    case 2:
+      res = multop::instance(multop::And, N_n("p", n), N_n("q", n));
+      break;
+    case 3:
+      res = multop::instance(multop::And, N_prime_n("p", n), N_prime_n("q", n));
+      break;
+    case 4:
+      res = FG_n("p", n);
+      break;
+    case 5:
+      res = GF_n("p", n);
+      break;
+    default:
+      std::cerr << "Unknown familly " << f << std::endl;
+      break;
+    }
+
+  if (spin_syntax)
+    to_spin_string(res, std::cout, true) << std::endl;
+  else
+    to_string(res, std::cout, true) << std::endl;
+
+  res->destroy();
+
+  return 0;
+}