From 98790f5345ecceb76dbeb0ea7f9b1afc1a2eeeb8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 3 Jun 2015 09:03:50 +0200
Subject: [PATCH] ltlparse: rename the main functions

parse         -> parse_infix_psl
parse_lbt     -> parse_prefix_ltl
parse_sere    -> parse_infix_sere
parse_boolean -> parse_infix_boolean

Fixes #87.

* src/ltlparse/ltlparse.yy, src/ltlparse/public.hh:
Do the above changes.
* doc/mainpage.dox, doc/org/tut01.org, iface/ltsmin/modelcheck.cc,
src/bin/common_finput.cc, src/hoaparse/hoaparse.yy,
src/kripkeparse/kripkeparse.yy, src/tests/checkpsl.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/consterm.cc, src/tests/emptchk.cc, src/tests/equalsf.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltl2tgba.cc,
src/tests/ltlprod.cc, src/tests/ltlrel.cc, src/tests/randtgba.cc,
src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
src/tests/tostring.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py: Adjust.
---
 doc/mainpage.dox               |  8 ++---
 doc/org/tut01.org              | 21 ++++++++------
 iface/ltsmin/modelcheck.cc     |  2 +-
 src/bin/common_finput.cc       |  7 ++---
 src/hoaparse/hoaparse.yy       |  6 ++--
 src/kripkeparse/kripkeparse.yy |  5 ++--
 src/ltlparse/ltlparse.yy       | 40 ++++++++++++-------------
 src/ltlparse/public.hh         | 53 ++++++++++++++++++----------------
 src/tests/checkpsl.cc          |  2 +-
 src/tests/checkta.cc           |  6 ++--
 src/tests/complementation.cc   |  6 ++--
 src/tests/consterm.cc          |  2 +-
 src/tests/emptchk.cc           |  2 +-
 src/tests/equalsf.cc           |  6 ++--
 src/tests/kind.cc              |  2 +-
 src/tests/length.cc            |  4 +--
 src/tests/ltl2tgba.cc          |  2 +-
 src/tests/ltlprod.cc           |  4 +--
 src/tests/ltlrel.cc            |  4 +--
 src/tests/randtgba.cc          |  2 +-
 src/tests/readltl.cc           |  5 ++--
 src/tests/reduc.cc             |  6 ++--
 src/tests/syntimpl.cc          |  6 ++--
 src/tests/tostring.cc          |  6 ++--
 wrap/python/ajax/spot.in       |  4 +--
 wrap/python/tests/alarm.py     |  4 +--
 wrap/python/tests/interdep.py  |  6 ++--
 wrap/python/tests/ltl2tgba.py  |  4 +--
 wrap/python/tests/ltlparse.py  |  6 ++--
 29 files changed, 118 insertions(+), 113 deletions(-)

diff --git a/doc/mainpage.dox b/doc/mainpage.dox
index 280948c32..3ee6a4499 100644
--- a/doc/mainpage.dox
+++ b/doc/mainpage.dox
@@ -20,13 +20,13 @@
 /// \section pointers Handy starting points
 ///
 /// \li spot::ltl::formula    Base class for an LTL or PSL formula.
-/// \li spot::ltl::parse      Parsing a text string into a
+/// \li spot::ltl::parse_infix_psl Parsing a text string into a
 ///                           spot::ltl::formula.
-/// \li spot::tgba            Base class for Transition-based
-///                           Generalized Büchi Automaton.
+/// \li spot::twa             Base class for Transition-based
+///                           ω-Automata.
 /// \li spot::translator      Convert a spot::ltl::formula into a
 ///                           spot::tgba.
 /// \li spot::kripke          Base class for Kripke structures.
-/// \li spot::tgba_product    On-the-fly product of two spot::tgba.
+/// \li spot::twa_product     On-the-fly product of two spot::twa.
 /// \li spot::emptiness_check Base class for all emptiness-check algorithms
 ///                           (see also module \ref emptiness_check)
diff --git a/doc/org/tut01.org b/doc/org/tut01.org
index 24c0b0a85..71857cf15 100644
--- a/doc/org/tut01.org
+++ b/doc/org/tut01.org
@@ -102,7 +102,7 @@ parser.  Additionally, this give you control over how to print errors.
   {
     std::string input = "[]<>p0 || <>[]p1";
     spot::ltl::parse_error_list pel;
-    const spot::ltl::formula* f = spot::ltl::parse(input, pel);
+    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
     if (spot::ltl::format_parse_errors(std::cerr, input, pel))
       {
         if (f)
@@ -119,10 +119,13 @@ parser.  Additionally, this give you control over how to print errors.
 : | G F p0 F G p1
 : ([](<>(p0))) || (<>([](p1)))
 
-So =parse()= process the =input=, and stores any diagnostic in =pel=,
-which is a list of pairs associating each error to a location.  You could
-iterate over that list to print it by yourself as you wish, or you can
-call =format_parse_errors()= to do that for you.
+So =parse_infix_psl()= processes =input=, and stores any diagnostic in
+=pel=, which is a list of pairs associating each error to a location.
+You could iterate over that list to print it by yourself as you wish,
+or you can call =format_parse_errors()= to do that for you.  Note that
+as its name implies, this parser can read more than LTL formulas (the
+fragment of PSL we support is basically LTL extended with regular
+expressions).
 
 If =pel= is empty, =format_parse_errors()= will do nothing and return
 false.
@@ -147,7 +150,7 @@ with the "fixed" formula if you wish.  Here is an example:
   {
     std::string input = "(a U b))";
     spot::ltl::parse_error_list pel;
-    const spot::ltl::formula* f = spot::ltl::parse(input, pel);
+    const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
     // Use std::cout instead of std::cerr because we can only
     // show the output of std::cout in this documentation.
     (void) spot::ltl::format_parse_errors(std::cout, input, pel);
@@ -186,8 +189,8 @@ currently this is done manually by calling =f->clone()= and
 
 ** Calling the prefix parser explicitly
 
-The only difference here is the call to =parse_lbt()= instead of
-=parse()=.
+The only difference here is the call to =parse_prefix_ltl()= instead of
+=parse_infix_psl()=.
 
 #+BEGIN_SRC C++ :results verbatim :exports both
   #include <string>
@@ -199,7 +202,7 @@ The only difference here is the call to =parse_lbt()= instead of
   {
     std::string input = "& & G p0 p1 p2";
     spot::ltl::parse_error_list pel;
-    const spot::ltl::formula* f = spot::ltl::parse_lbt(input, pel);
+    const spot::ltl::formula* f = spot::ltl::parse_prefix_ltl(input, pel);
     if (spot::ltl::format_parse_errors(std::cerr, input, pel))
       {
         if (f)
diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc
index a6777f867..8cbd42550 100644
--- a/iface/ltsmin/modelcheck.cc
+++ b/iface/ltsmin/modelcheck.cc
@@ -195,7 +195,7 @@ checked_main(int argc, char **argv)
   tm.start("parsing formula");
   {
     spot::ltl::parse_error_list pel;
-    f = spot::ltl::parse(argv[2], pel, env, false);
+    f = spot::ltl::parse_infix_psl(argv[2], pel, env, false);
     exit_code = spot::ltl::format_parse_errors(std::cerr, argv[2], pel);
   }
   tm.stop("parsing formula");
diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc
index c834c6f01..292fdff97 100644
--- a/src/bin/common_finput.cc
+++ b/src/bin/common_finput.cc
@@ -79,11 +79,10 @@ const spot::ltl::formula*
 parse_formula(const std::string& s, spot::ltl::parse_error_list& pel)
 {
   if (lbt_input)
-    return spot::ltl::parse_lbt(s, pel);
+    return spot::ltl::parse_prefix_ltl(s, pel);
   else
-    return spot::ltl::parse(s, pel,
-			    spot::ltl::default_environment::instance(),
-			    false, lenient);
+    return spot::ltl::parse_infix_psl
+      (s, pel, spot::ltl::default_environment::instance(), false, lenient);
 }
 
 job_processor::job_processor()
diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index cb43a9015..f1e8f185f 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -1212,8 +1212,8 @@ nc-formula: nc-formula-or-ident
        if (i == res.fcache.end())
 	 {
 	   spot::ltl::parse_error_list pel;
-	   auto f = spot::ltl::parse_boolean(*$1, pel, *res.env,
-					     debug_level(), true);
+	   auto f = spot::ltl::parse_infix_boolean(*$1, pel, *res.env,
+						   debug_level(), true);
 	   for (auto& j: pel)
 	     {
 	       // Adjust the diagnostic to the current position.
@@ -1391,7 +1391,7 @@ lbtt-acc:               { $$ = 0U; }
 lbtt-guard: STRING
           {
 	    spot::ltl::parse_error_list pel;
-	    auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env);
+	    auto* f = spot::ltl::parse_prefix_ltl(*$1, pel, *res.env);
 	    if (!f || !pel.empty())
 	      {
 		std::string s = "failed to parse guard: ";
diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy
index a2b8bdd1e..6dd85891d 100644
--- a/src/kripkeparse/kripkeparse.yy
+++ b/src/kripkeparse/kripkeparse.yy
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -110,7 +110,8 @@ strident "," condition "," follow_list ";"
     if (i == fcache.end())
     {
       parse_error_list pel;
-      const formula* f = spot::ltl::parse(*$3, pel, parse_environment);
+      const formula* f = spot::ltl::parse_infix_boolean(*$3, pel,
+							parse_environment);
       for (parse_error_list::iterator i = pel.begin();
            i != pel.end(); ++i)
       {
diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 5e9dbff58..517e22044 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -91,7 +91,7 @@ using namespace spot::ltl;
 
   enum parser_type { parser_ltl, parser_bool, parser_sere };
 
-  const formula*
+  static const formula*
   try_recursive_parse(const std::string& str,
 		      const spot::location& location,
 		      spot::ltl::environment& env,
@@ -125,13 +125,13 @@ using namespace spot::ltl;
       switch (type)
 	{
 	case parser_sere:
-	  f = spot::ltl::parse_sere(str, suberror, env, debug, true);
+	  f = spot::ltl::parse_infix_sere(str, suberror, env, debug, true);
 	  break;
 	case parser_bool:
-	  f = spot::ltl::parse_boolean(str, suberror, env, debug, true);
+	  f = spot::ltl::parse_infix_boolean(str, suberror, env, debug, true);
 	  break;
 	case parser_ltl:
-	  f = spot::ltl::parse(str, suberror, env, debug, true);
+	  f = spot::ltl::parse_infix_psl(str, suberror, env, debug, true);
 	  break;
 	}
 
@@ -996,10 +996,10 @@ namespace spot
   namespace ltl
   {
     const formula*
-    parse(const std::string& ltl_string,
-	  parse_error_list& error_list,
-	  environment& env,
-	  bool debug, bool lenient)
+    parse_infix_psl(const std::string& ltl_string,
+		    parse_error_list& error_list,
+		    environment& env,
+		    bool debug, bool lenient)
     {
       const formula* result = 0;
       flex_set_buffer(ltl_string,
@@ -1013,10 +1013,10 @@ namespace spot
     }
 
     const formula*
-    parse_boolean(const std::string& ltl_string,
-		  parse_error_list& error_list,
-		  environment& env,
-		  bool debug, bool lenient)
+    parse_infix_boolean(const std::string& ltl_string,
+			parse_error_list& error_list,
+			environment& env,
+			bool debug, bool lenient)
     {
       const formula* result = 0;
       flex_set_buffer(ltl_string,
@@ -1030,7 +1030,7 @@ namespace spot
     }
 
     const formula*
-    parse_lbt(const std::string& ltl_string,
+    parse_prefix_ltl(const std::string& ltl_string,
 	  parse_error_list& error_list,
 	  environment& env,
 	  bool debug)
@@ -1047,11 +1047,11 @@ namespace spot
     }
 
     const formula*
-    parse_sere(const std::string& sere_string,
-	       parse_error_list& error_list,
-	       environment& env,
-	       bool debug,
-	       bool lenient)
+    parse_infix_sere(const std::string& sere_string,
+		     parse_error_list& error_list,
+		     environment& env,
+		     bool debug,
+		     bool lenient)
     {
       const formula* result = 0;
       flex_set_buffer(sere_string,
@@ -1068,12 +1068,12 @@ namespace spot
     parse_formula(const std::string& ltl_string, environment& env)
     {
       parse_error_list pel;
-      const formula* f = parse(ltl_string, pel, env);
+      const formula* f = parse_infix_psl(ltl_string, pel, env);
       std::ostringstream s;
       if (format_parse_errors(s, ltl_string, pel))
 	{
 	  parse_error_list pel2;
-	  const formula* g = parse_lbt(ltl_string, pel2, env);
+	  const formula* g = parse_prefix_ltl(ltl_string, pel2, env);
 	  if (pel2.empty())
 	    return g;
 	  else
diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh
index 69c6d7aab..9e14dd374 100644
--- a/src/ltlparse/public.hh
+++ b/src/ltlparse/public.hh
@@ -66,11 +66,12 @@ namespace spot
     ///
     /// \warning This function is not reentrant.
     SPOT_API
-    const formula* parse(const std::string& ltl_string,
-			 parse_error_list& error_list,
-			 environment& env = default_environment::instance(),
-			 bool debug = false,
-			 bool lenient = false);
+    const formula* parse_infix_psl(const std::string& ltl_string,
+				   parse_error_list& error_list,
+				   environment& env =
+				   default_environment::instance(),
+				   bool debug = false,
+				   bool lenient = false);
 
     /// \brief Build a Boolean formula from a string.
     /// \param ltl_string The string to parse.
@@ -91,12 +92,12 @@ namespace spot
     ///
     /// \warning This function is not reentrant.
     SPOT_API
-    const formula* parse_boolean(const std::string& ltl_string,
-				 parse_error_list& error_list,
-				 environment& env =
-				 default_environment::instance(),
-				 bool debug = false,
-				 bool lenient = false);
+    const formula* parse_infix_boolean(const std::string& ltl_string,
+				       parse_error_list& error_list,
+				       environment& env =
+				       default_environment::instance(),
+				       bool debug = false,
+				       bool lenient = false);
 
     /// \brief Build a formula from an LTL string in LBT's format.
     /// \param ltl_string The string to parse.
@@ -118,16 +119,18 @@ namespace spot
     ///
     /// \warning This function is not reentrant.
     SPOT_API
-    const formula* parse_lbt(const std::string& ltl_string,
-			     parse_error_list& error_list,
-			     environment& env = default_environment::instance(),
-			     bool debug = false);
+    const formula* parse_prefix_ltl(const std::string& ltl_string,
+				    parse_error_list& error_list,
+				    environment& env =
+				    default_environment::instance(),
+				    bool debug = false);
 
-    /// \brief A simple wrapper to parse() and parse_lbt().
+    /// \brief A simple wrapper to parse_infix_psl() and parse_prefix_ltl().
     ///
-    /// This is mostly meant for interactive use.  It first tries parse(); if
-    /// this fails it tries parse_lbt(); and if both fails it returns the errors
-    /// of the first call to parse() as a parse_error exception.
+    /// This is mostly meant for interactive use.  It first tries
+    /// parse_infix_psl(); if this fails it tries parse_prefix_ltl();
+    /// and if both fails it returns the errors of the first call to
+    /// parse_infix_psl() as a parse_error exception.
     SPOT_API const formula*
     parse_formula(const std::string& ltl_string,
 		  environment& env = default_environment::instance());
@@ -151,12 +154,12 @@ namespace spot
     ///
     /// \warning This function is not reentrant.
     SPOT_API
-    const formula* parse_sere(const std::string& sere_string,
-			      parse_error_list& error_list,
-			      environment& env =
-			      default_environment::instance(),
-			      bool debug = false,
-			      bool lenient = false);
+    const formula* parse_infix_sere(const std::string& sere_string,
+				    parse_error_list& error_list,
+				    environment& env =
+				    default_environment::instance(),
+				    bool debug = false,
+				    bool lenient = false);
 
     /// \brief Format diagnostics produced by spot::ltl::parse
     ///        or spot::ltl::ratexp
diff --git a/src/tests/checkpsl.cc b/src/tests/checkpsl.cc
index 5502a16a6..4d7bf916e 100644
--- a/src/tests/checkpsl.cc
+++ b/src/tests/checkpsl.cc
@@ -62,7 +62,7 @@ main(int argc, char** argv)
 	continue;
 
       spot::ltl::parse_error_list pe;
-      auto fpos = spot::ltl::parse(s, pe);
+      auto fpos = spot::ltl::parse_infix_psl(s, pe);
 
       if (spot::ltl::format_parse_errors(std::cerr, s, pe))
 	return 2;
diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc
index 511125556..d499ea5d9 100644
--- a/src/tests/checkta.cc
+++ b/src/tests/checkta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -85,7 +85,7 @@ main(int argc, char** argv)
 	continue;
 
       spot::ltl::parse_error_list pe;
-      auto f = spot::ltl::parse(s, pe);
+      auto f = spot::ltl::parse_infix_psl(s, pe);
 
       if (spot::ltl::format_parse_errors(std::cerr, s, pe))
 	return 2;
diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc
index e7da51a8d..e25a7ab84 100644
--- a/src/tests/complementation.cc
+++ b/src/tests/complementation.cc
@@ -149,7 +149,7 @@ int main(int argc, char* argv[])
   else if (print_formula)
   {
     spot::ltl::parse_error_list p1;
-    const spot::ltl::formula* f1 = spot::ltl::parse(file, p1);
+    auto* f1 = spot::ltl::parse_infix_psl(file, p1);
 
     if (spot::ltl::format_parse_errors(std::cerr, file, p1))
       return 2;
@@ -169,7 +169,7 @@ int main(int argc, char* argv[])
     if (formula)
     {
       spot::ltl::parse_error_list p1;
-      f1 = spot::ltl::parse(file, p1);
+      f1 = spot::ltl::parse_infix_psl(file, p1);
 
       if (spot::ltl::format_parse_errors(std::cerr, file, p1))
         return 2;
@@ -227,7 +227,7 @@ int main(int argc, char* argv[])
   else
   {
     spot::ltl::parse_error_list p1;
-    const spot::ltl::formula* f1 = spot::ltl::parse(file, p1);
+    auto* f1 = spot::ltl::parse_infix_psl(file, p1);
 
     if (spot::ltl::format_parse_errors(std::cerr, file, p1))
       return 2;
diff --git a/src/tests/consterm.cc b/src/tests/consterm.cc
index de49de882..a9ff2516a 100644
--- a/src/tests/consterm.cc
+++ b/src/tests/consterm.cc
@@ -60,7 +60,7 @@ main(int argc, char **argv)
       ss >> expected;
 
       spot::ltl::parse_error_list p1;
-      const spot::ltl::formula* f1 = spot::ltl::parse_sere(form, p1);
+      auto* f1 = spot::ltl::parse_infix_sere(form, p1);
       if (spot::ltl::format_parse_errors(std::cerr, form, p1))
 	return 2;
 
diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc
index f704f2f45..9a9bf9fca 100644
--- a/src/tests/emptchk.cc
+++ b/src/tests/emptchk.cc
@@ -91,7 +91,7 @@ main(int argc, char** argv)
       int runs = atoi(tokens[0].c_str());
 
       spot::ltl::parse_error_list pe;
-      auto f = spot::ltl::parse(tokens[1], pe);
+      auto f = spot::ltl::parse_infix_psl(tokens[1], pe);
       if (spot::ltl::format_parse_errors(std::cerr, tokens[1], pe))
 	return 2;
 
diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc
index b33a8c7dd..471d16234 100644
--- a/src/tests/equalsf.cc
+++ b/src/tests/equalsf.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -100,7 +100,7 @@ main(int argc, char** argv)
 	}
 
       spot::ltl::parse_error_list p2;
-      const spot::ltl::formula* f2 = spot::ltl::parse(formulas[size - 1], p2);
+      auto* f2 = spot::ltl::parse_infix_psl(formulas[size - 1], p2);
 
       if (spot::ltl::format_parse_errors(std::cerr, formulas[size - 1], p2))
 	return 2;
@@ -109,7 +109,7 @@ main(int argc, char** argv)
 	{
 
 	  spot::ltl::parse_error_list p1;
-	  const spot::ltl::formula* f1 = spot::ltl::parse(formulas[n], p1);
+	  auto* f1 = spot::ltl::parse_infix_psl(formulas[n], p1);
 
 	  if (check_first &&
 	      spot::ltl::format_parse_errors(std::cerr, formulas[n], p1))
diff --git a/src/tests/kind.cc b/src/tests/kind.cc
index da45b7157..906d98c23 100644
--- a/src/tests/kind.cc
+++ b/src/tests/kind.cc
@@ -60,7 +60,7 @@ main(int argc, char **argv)
       std::getline(ss, expected);
 
       spot::ltl::parse_error_list p1;
-      const spot::ltl::formula* f1 = spot::ltl::parse(form, p1);
+      auto* f1 = spot::ltl::parse_infix_psl(form, p1);
       if (spot::ltl::format_parse_errors(std::cerr, form, p1))
 	return 2;
 
diff --git a/src/tests/length.cc b/src/tests/length.cc
index 60cf67523..8542608b9 100644
--- a/src/tests/length.cc
+++ b/src/tests/length.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Developement de
+// Copyright (C) 2012, 2015 Laboratoire de Recherche et Developement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -46,7 +46,7 @@ main(int argc, char **argv)
     }
 
   spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  auto* f1 = spot::ltl::parse_infix_psl(argv[1], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
     return 2;
diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc
index 77dcd73de..7399ec625 100644
--- a/src/tests/ltl2tgba.cc
+++ b/src/tests/ltl2tgba.cc
@@ -958,7 +958,7 @@ checked_main(int argc, char** argv)
 	  {
 	    spot::ltl::parse_error_list pel;
 	    tm.start("parsing formula");
-	    f = spot::ltl::parse(input, pel, env, debug_opt);
+	    f = spot::ltl::parse_infix_psl(input, pel, env, debug_opt);
 	    tm.stop("parsing formula");
 	    exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
 	  }
diff --git a/src/tests/ltlprod.cc b/src/tests/ltlprod.cc
index ffb2c4464..152accc02 100644
--- a/src/tests/ltlprod.cc
+++ b/src/tests/ltlprod.cc
@@ -48,13 +48,13 @@ main(int argc, char** argv)
     spot::ltl::environment& env(spot::ltl::default_environment::instance());
 
     spot::ltl::parse_error_list pel1;
-    const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env);
+    auto* f1 = spot::ltl::parse_infix_psl(argv[1], pel1, env);
 
     if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1))
       return 2;
 
     spot::ltl::parse_error_list pel2;
-    const spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env);
+    auto* f2 = spot::ltl::parse_infix_psl(argv[2], pel2, env);
 
     if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2))
       return 2;
diff --git a/src/tests/ltlrel.cc b/src/tests/ltlrel.cc
index a8d9d55e6..c977e39a1 100644
--- a/src/tests/ltlrel.cc
+++ b/src/tests/ltlrel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developement
+// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Developement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -39,7 +39,7 @@ main(int argc, char **argv)
     syntax(argv[0]);
 
   spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  auto* f1 = spot::ltl::parse_infix_psl(argv[1], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
     return 2;
diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc
index 9bd59c56c..d4d57372d 100644
--- a/src/tests/randtgba.cc
+++ b/src/tests/randtgba.cc
@@ -872,7 +872,7 @@ main(int argc, char** argv)
 	      else if (input == "")
 		break;
               spot::ltl::parse_error_list pel;
-              const spot::ltl::formula* f = spot::ltl::parse(input, pel, env);
+              auto* f = spot::ltl::parse_infix_psl(input, pel, env);
               if (spot::ltl::format_parse_errors(std::cerr, input, pel))
 		{
 		  exit_code = 1;
diff --git a/src/tests/readltl.cc b/src/tests/readltl.cc
index 185192504..6ba27277b 100644
--- a/src/tests/readltl.cc
+++ b/src/tests/readltl.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
+// Copyright (C) 2008, 2009, 2012, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -75,8 +75,7 @@ main(int argc, char** argv)
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::parse_error_list pel;
-  const spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
-						 pel, env, debug);
+  auto* f = spot::ltl::parse_infix_psl(argv[formula_index], pel, env, debug);
 
   exit_code =
     spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc
index 4ed52fc44..0355854ac 100644
--- a/src/tests/reduc.cc
+++ b/src/tests/reduc.cc
@@ -180,14 +180,14 @@ main(int argc, char** argv)
       while (input == "");
 
       spot::ltl::parse_error_list p1;
-      f1 = spot::ltl::parse(input, p1);
+      f1 = spot::ltl::parse_infix_psl(input, p1);
       if (spot::ltl::format_parse_errors(std::cerr, input, p1))
 	return 2;
     }
   else
     {
       spot::ltl::parse_error_list p1;
-      f1 = spot::ltl::parse(argv[2], p1);
+      f1 = spot::ltl::parse_infix_psl(argv[2], p1);
       if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
 	return 2;
     }
@@ -201,7 +201,7 @@ main(int argc, char** argv)
 	}
 
       spot::ltl::parse_error_list p2;
-      f2 = spot::ltl::parse(argv[3], p2);
+      f2 = spot::ltl::parse_infix_psl(argv[3], p2);
       if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
 	return 2;
     }
diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc
index dea1035e2..f5ac31837 100644
--- a/src/tests/syntimpl.cc
+++ b/src/tests/syntimpl.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -48,13 +48,13 @@ main(int argc, char** argv)
   int opt = atoi(argv[1]);
 
   spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1);
+  auto* ftmp1 = spot::ltl::parse_infix_psl(argv[2], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
     return 2;
 
   spot::ltl::parse_error_list p2;
-  const spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2);
+  auto* ftmp2 = spot::ltl::parse_infix_psl(argv[3], p2);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
     return 2;
diff --git a/src/tests/tostring.cc b/src/tests/tostring.cc
index 815c4558d..d798ecc32 100644
--- a/src/tests/tostring.cc
+++ b/src/tests/tostring.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
+// Copyright (C) 2008, 2009, 2012, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -41,7 +41,7 @@ main(int argc, char **argv)
     syntax(argv[0]);
 
   spot::ltl::parse_error_list p1;
-  const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  auto* f1 = spot::ltl::parse_infix_psl(argv[1], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
     return 2;
@@ -52,7 +52,7 @@ main(int argc, char **argv)
   std::string f1s = spot::ltl::to_string(f1);
   std::cout << f1s << std::endl;
 
-  const spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1);
+  auto* f2 = spot::ltl::parse_infix_psl(f1s, p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, f1s, p1))
     return 2;
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index ca64c379f..3e2236370 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -410,12 +410,12 @@ formula = form.getfirst('f', '')
 
 env = spot.default_environment.instance()
 pel = spot.empty_parse_error_list()
-f = spot.parse(formula, pel, env)
+f = spot.parse_infix_psl(formula, pel, env)
 
 if pel:
     # Try the LBT parser in case someone is throwing LBT formulas at us.
     pel2 = spot.empty_parse_error_list()
-    g = spot.parse_lbt(formula, pel2, env)
+    g = spot.parse_prefix_ltl(formula, pel2, env)
     if pel2:
         unbufprint('<div class="parse-error">')
         err = spot.format_parse_errors(spot.get_cout(), formula, pel)
diff --git a/wrap/python/tests/alarm.py b/wrap/python/tests/alarm.py
index ee8cc85ea..563396a0b 100755
--- a/wrap/python/tests/alarm.py
+++ b/wrap/python/tests/alarm.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012, 2014  Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2014, 2015  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -44,7 +44,7 @@ P_Rbt2.moins || P_Rbt2.stop))-> G((F "map[0]==1") && (F "map[1]==1")
 
 e = spot.default_environment.instance()
 p = spot.empty_parse_error_list()
-f = spot.parse(f, p, e)
+f = spot.parse_infix_psl(f, p, e)
 d = spot.make_bdd_dict()
 
 spot.unblock_signal(signal.SIGALRM)
diff --git a/wrap/python/tests/interdep.py b/wrap/python/tests/interdep.py
index 6c4e89643..853ff5d19 100755
--- a/wrap/python/tests/interdep.py
+++ b/wrap/python/tests/interdep.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2012, 2014 Laboratoire de Recherche et
+# Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'EPITA.
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -30,10 +30,10 @@ simp = spot.ltl_simplifier()
 
 e = spot.default_environment.instance()
 p = spot.empty_parse_error_list()
-f = spot.parse('GFa', p, e)
+f = spot.parse_infix_psl('GFa', p, e)
 d = simp.get_dict()
 a = spot.ltl_to_tgba_fm(f, d)
-g = spot.parse('b&c', p, e)
+g = spot.parse_infix_boolean('b&c', p, e)
 b = simp.as_bdd(g)
 buddy.bdd_printset(b); spot.nl_cout()
 del g
diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py
index 615db9cc7..5bafa7d0e 100755
--- a/wrap/python/tests/ltl2tgba.py
+++ b/wrap/python/tests/ltl2tgba.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -84,7 +84,7 @@ cerr = spot.get_cerr()
 e = spot.default_environment.instance()
 p = spot.empty_parse_error_list()
 
-f = spot.parse(args[0], p, e, debug_opt)
+f = spot.parse_infix_psl(args[0], p, e, debug_opt)
 if spot.format_parse_errors(cerr, args[0], p):
     exit_code = 1
 
diff --git a/wrap/python/tests/ltlparse.py b/wrap/python/tests/ltlparse.py
index a97c74b81..31ce218a1 100755
--- a/wrap/python/tests/ltlparse.py
+++ b/wrap/python/tests/ltlparse.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -29,14 +29,14 @@ p = spot.empty_parse_error_list()
 l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \/ a \/ b \/ a \/ a'];
 
 for str1 in l:
-    f = spot.parse(str1, p, e, False)
+    f = spot.parse_infix_psl(str1, p, e, False)
     if spot.format_parse_errors(spot.get_cout(), str1, p):
         sys.exit(1)
     str2 = str(f)
     f.destroy()
     sys.stdout.write(str2 + "\n")
     # Try to reparse the stringified formula
-    f = spot.parse(str2, p, e)
+    f = spot.parse_infix_psl(str2, p, e)
     if spot.format_parse_errors(spot.get_cout(), str2, p):
         sys.exit(1)
     sys.stdout.write(str(f) + "\n")