From dfd080e005fc1afa934b389474d801ad7161eff3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 14 Apr 2015 20:28:37 +0200
Subject: [PATCH] acc: add a parser for string -> acc_code

* src/tgba/acc.cc, src/tgba/acc.hh (parse_acc_code): New function.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
---
 src/tgba/acc.cc       | 133 ++++++++++++++++++++++++++++++++++++++++++
 src/tgba/acc.hh       |  19 ++++++
 src/tgbatest/acc.cc   |  14 +++++
 src/tgbatest/acc.test |   8 +++
 4 files changed, 174 insertions(+)

diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc
index 9828541c0..6c3777295 100644
--- a/src/tgba/acc.cc
+++ b/src/tgba/acc.cc
@@ -19,7 +19,10 @@
 
 
 #include <iostream>
+#include <sstream>
 #include <set>
+#include <cctype>
+#include <cstring>
 #include "acc.hh"
 #include "priv/bddalloc.hh"
 #include "misc/minato.hh"
@@ -879,4 +882,134 @@ namespace spot
   {
     return code.to_text(os);
   }
+
+
+
+  namespace
+  {
+
+    /// acc ::= term | term "|" acc
+    /// term := "t" | "f" | "Inf" "(" num ")"
+    ///       | "Fin" "(" num ") " | "(" acc ")
+    ///       | term "&" term
+
+    static void skip_space(const char*& input)
+    {
+      while (std::isspace(*input))
+	++input;
+    }
+
+    // Eat c and remove the following spaces.
+    // Complain if there is no c.
+    void expect(const char*& input, char c)
+    {
+      if (*input != c)
+	{
+	  std::ostringstream s;
+	  s << "syntax error at '" << input << "', was expecting " << c << '.';
+	  throw parse_error(s.str());
+	}
+      ++input;
+      skip_space(input);
+    }
+
+    static acc_cond::acc_code parse_term(const char*& input);
+
+    static acc_cond::acc_code parse_acc(const char*& input)
+    {
+      auto t = parse_term(input);
+      skip_space(input);
+      while (*input == '|')
+	{
+	  ++input;
+	  skip_space(input);
+	  t.append_or(parse_term(input));
+	}
+      return t;
+    }
+
+    static unsigned parse_num(const char*& input)
+    {
+      skip_space(input);
+      expect(input, '(');
+
+      errno = 0;
+      char* end;
+      unsigned long n = strtoul(input, &end, 10);
+      unsigned num = n;
+      if (errno || num != n)
+	{
+	  std::ostringstream s;
+	  s << "syntax error at '" << input << "': value too large.";
+	  throw parse_error(s.str());
+	}
+      input = end;
+
+      skip_space(input);
+      expect(input, ')');
+      return num;
+    }
+
+    static acc_cond::acc_code parse_term(const char*& input)
+    {
+      acc_cond::acc_code res;
+      if (*input == 't')
+	{
+	  ++input;
+	  res = acc_cond::acc_code::t();
+	}
+      else if (*input == 'f')
+	{
+	  ++input;
+	  res = acc_cond::acc_code::f();
+	}
+      else if (*input == '(')
+	{
+	  ++input;
+	  skip_space(input);
+	  res = parse_acc(input);
+	  skip_space(input);
+	  expect(input, ')');
+	}
+      else if (!strncmp(input, "Inf", 3))
+	{
+	  input += 3;
+	  res = acc_cond::acc_code::inf({parse_num(input)});
+	}
+      else if (!strncmp(input, "Fin", 3))
+	{
+	  input += 3;
+	  res = acc_cond::acc_code::fin({parse_num(input)});
+	}
+      else
+	{
+	  std::ostringstream s;
+	  s << "syntax error at '" << input << "', unexpected character.";
+	  throw parse_error(s.str());
+	}
+
+      skip_space(input);
+      while (*input == '&')
+	{
+	  ++input;
+	  skip_space(input);
+	  res.append_and(parse_term(input));
+	}
+      return res;
+    }
+
+  }
+
+  acc_cond::acc_code parse_acc_code(const char* input)
+  {
+    skip_space(input);
+    acc_cond::acc_code c = parse_acc(input);
+    if (*input)
+      {
+	std::ostringstream s;
+	s << "syntax error at '" << input << "', unexpected character.";
+	throw parse_error(s.str());
+      }
+    return c;
+  }
 }
diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh
index b2b7ecee2..879e03e94 100644
--- a/src/tgba/acc.hh
+++ b/src/tgba/acc.hh
@@ -968,6 +968,25 @@ namespace spot
     bool uses_fin_acceptance_ = false;
   };
 
+  /// \brief Parse a string into an acc_code
+  ///
+  /// The string should follow the following grammar:
+  ///
+  /// <pre>
+  ///   acc ::= "t"
+  ///         | "f"
+  ///         | "Inf" "(" num ")"
+  ///         | "Fin" "(" num ")"
+  ///         | "(" acc ")"
+  ///         | acc "&" acc
+  ///         | acc "|" acc
+  /// </pre>
+  ///
+  /// Where num is an integer and "&" has priority over "|".  Note that
+  /// "Fin(!x)" and "Inf(!x)" are not supported by this parser.
+  ///
+  /// A spot::parse_error is thrown on syntax error.
+  SPOT_API acc_cond::acc_code parse_acc_code(const char* input);
 }
 
 namespace std
diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc
index 253fe2fd1..9344c7dce 100644
--- a/src/tgbatest/acc.cc
+++ b/src/tgbatest/acc.cc
@@ -127,4 +127,18 @@ int main()
   auto code3 = ac.inf({0, 1});
   code3.append_and(ac.fin({2, 3}));
   std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n';
+
+
+  std::cout << spot::parse_acc_code("t") << '\n';
+  std::cout << spot::parse_acc_code("f") << '\n';
+  std::cout << spot::parse_acc_code("Fin(2)") << '\n';
+  std::cout << spot::parse_acc_code("Inf(2)") << '\n';
+  std::cout << spot::parse_acc_code("Fin(2) | Inf(2)") << '\n';
+  std::cout << spot::parse_acc_code("Inf(2) & Fin(2)") << '\n';
+  auto c1 = spot::parse_acc_code("Fin(0)|Inf(1)&Fin(2)|Fin(3)");
+  auto c2 = spot::parse_acc_code
+    ("(  Fin  (  0 ))  | (Inf   (   1) &  Fin(2 ))| Fin (3)   ");
+  std::cout << c1 << '\n';
+  std::cout << c2 << '\n';
+  assert(c1 == c2);
 }
diff --git a/src/tgbatest/acc.test b/src/tgbatest/acc.test
index 8168a5148..d0b1a766e 100755
--- a/src/tgbatest/acc.test
+++ b/src/tgbatest/acc.test
@@ -68,6 +68,14 @@ stripping
 2 f 1
 9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
 5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
+t
+f
+Fin(2)
+Inf(2)
+Inf(2) | Fin(2)
+Fin(2) & Inf(2)
+Fin(3) | (Fin(2) & Inf(1)) | Fin(0)
+Fin(3) | (Fin(2) & Inf(1)) | Fin(0)
 EOF
 
 run 0 ../acc | tee stdout