From 4ccdcb4a5bb64021833db0e9aab2c0d9083299a2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 12 Sep 2024 17:28:17 +0200
Subject: [PATCH] tests: rewrite the syntimpl test

* tests/core/syntimpl.cc: Rewrite to test multiple formulas at once,
and test them with three different implication checks.
* tests/core/syntimpl.test: Adjust the test to execute syntimpl only
once.
---
 tests/core/syntimpl.cc   | 113 ++++++++++++++++------------------
 tests/core/syntimpl.test | 127 ++++++++++++++++++---------------------
 2 files changed, 109 insertions(+), 131 deletions(-)

diff --git a/tests/core/syntimpl.cc b/tests/core/syntimpl.cc
index 65995898a..329c3e01d 100644
--- a/tests/core/syntimpl.cc
+++ b/tests/core/syntimpl.cc
@@ -18,85 +18,74 @@
 
 #include "config.h"
 #include <iostream>
+#include <fstream>
+#include <sstream>
 #include <cassert>
 #include <cstdlib>
+#include <cstring>
 #include <spot/tl/parse.hh>
-#include <spot/tl/print.hh>
-#include <spot/tl/simplify.hh>
 #include <spot/tl/nenoform.hh>
+#include <spot/tl/simplify.hh>
+#include <spot/tl/print.hh>
 
 static void
 syntax(char* prog)
 {
-  std::cerr << prog << " formula1 formula2?\n";
+  std::cerr << prog << " file\n";
   exit(2);
 }
 
 int
 main(int argc, char** argv)
 {
-  if (argc < 4)
+  if (argc != 2)
     syntax(argv[0]);
-
-  int opt = atoi(argv[1]);
-  int exit_return = 0;
-
-  {
-    auto ftmp1 = spot::parse_infix_psl(argv[2]);
-
-    if (ftmp1.format_errors(std::cerr))
+  std::ifstream input(argv[1]);
+  if (!input)
+    {
+      std::cerr << "failed to open " << argv[1] << '\n';
       return 2;
+    }
 
-    auto ftmp2 = spot::parse_infix_psl(argv[3]);
+  spot::tl_simplifier* c = new spot::tl_simplifier;
+  std::string s;
+  unsigned line = 0;
+  while (std::getline(input, s))
+    {
+      ++line;
+      std::cerr << line << ": " << s << '\n';
+      if (s[0] == '#')                // Skip comments
+        continue;
 
-    if (ftmp2.format_errors(std::cerr))
-      return 2;
-
-    spot::formula f1 = spot::negative_normal_form(ftmp1.f);
-    spot::formula f2 = spot::negative_normal_form(ftmp2.f);
-
-    std::string f1s = spot::str_psl(f1);
-    std::string f2s = spot::str_psl(f2);
-
-    spot::tl_simplifier* c = new spot::tl_simplifier;
-
-    switch (opt)
-      {
-      case 0:
-        std::cout << "Test f1 < f2" << std::endl;
-        if (c->syntactic_implication(f1, f2))
-          {
-            std::cout << f1s << " < " << f2s << '\n';
-            exit_return = 1;
-          }
-        break;
-
-      case 1:
-        std::cout << "Test !f1 < f2" << std::endl;
-        if (c->syntactic_implication_neg(f1, f2, false))
-          {
-            std::cout << "!(" << f1s << ") < " << f2s << '\n';
-            exit_return = 1;
-          }
-        break;
-
-      case 2:
-        std::cout << "Test f1 < !f2" << std::endl;
-        if (c->syntactic_implication_neg(f1, f2, true))
-          {
-            std::cout << f1s << " < !(" << f2s << ")\n";
-            exit_return = 1;
-          }
-        break;
-      default:
-        break;
-      }
-
-    f1.dump(std::cout) << '\n';
-    f2.dump(std::cout) << '\n';
-
-    delete c;
-  }
+      spot::formula f[2];
+      std::istringstream ss(s);
+      for (unsigned i = 0; i < 2; ++i)
+        {
+          std::string form;
+          if (!std::getline(ss, form, ','))
+            {
+              std::cerr << "missing first formula\n";
+              exit(2);
+            }
+          std::string tmp;
+          while (form.size() > 0 && form.back() == '\\'
+                 && std::getline(ss, tmp, ','))
+            {
+              form.back() = ',';
+              form += tmp;
+            }
+          auto pf = spot::parse_infix_psl(form);
+          if (pf.format_errors(std::cerr))
+            return 2;
+          f[i] = spot::negative_normal_form(pf.f);
+        }
+      // ignore the rest of the line
+      std::cout << spot::str_psl(f[0]) << ',' << spot::str_psl(f[1]) << ','
+                << c->syntactic_implication(f[0], f[1]) << ','
+                << c->syntactic_implication_neg(f[0], f[1], false) << ','
+                << c->syntactic_implication_neg(f[0], f[1], true) << '\n';
+    }
+  delete c;
   assert(spot::fnode::instances_check());
-  return exit_return;
+  return 0;
 }
diff --git a/tests/core/syntimpl.test b/tests/core/syntimpl.test
index 663672c4c..413b01802 100755
--- a/tests/core/syntimpl.test
+++ b/tests/core/syntimpl.test
@@ -22,74 +22,63 @@
 
 . ./defs || exit 1
 
-#
-#GFa && GFb && FG(!a && !b)
-run 1 ../syntimpl 0 'a' 'a | b'
-run 1 ../syntimpl 0 'F(a)' 'F(a | b)'
-run 1 ../syntimpl 0 'G(a)' 'G(a | b)'
-run 1 ../syntimpl 0 'GF(a)' 'GF(a | b)'
-run 1 ../syntimpl 0 'GF(a)' '!FG(!a && !b)'
 
-run 1 ../syntimpl 0 'Xa' 'X(b U a)'
-run 1 ../syntimpl 0 'XXa' 'XX(b U a)'
+cat >input <<EOF
+a,a | b,1,0,0
+Fa,F(a | b),1,0,0
+Ga,G(a | b),1,0,0
+GFa,GF(a | b),1,0,0
+GFa,GF(a | b),1,0,0
+Xa,X(b U a),1,0,0
+XXa,XX(b U a),1,0,0
+e R f,g U f,1,0,0
+X(a | b),X(a | b | c | d),1,0,0
+X(a | b) U (e R f),X(a | b | c | d) U (g U f),1,0,0
+1,1,1,1,0
+0,0,1,0,1
+a,1,1,1,0
+a,a,1,0,0
+a,!a,0,1,1
+!a,1,1,1,0
+a,a,1,0,0
+a & b,b,1,0,0
+a & b,a,1,0,0
+!a,a & b,0,0,1
+a,a & b,0,0,0
+a,!a | !b,0,1,0
+a,a | b,1,0,0
+b,a | b,1,0,0
+a | b,1,1,1,0
+a,b U a,1,0,0
+a,1,1,1,0
+a U b,1,1,1,0
+a,a,1,0,0
+a,1,1,1,0
+a R b,b,1,0,0
+a R b,1,1,1,0
+Xa,X(b U a),1,0,0
+X(a R b),Xb,1,0,0
+a U b,1 U b,1,0,0
+a R b,b,1,0,0
+b & (a U b),a U b,1,0,0
+a U b,c | (a U b),1,0,0
+Xa,XX(b U a),0,0,0
+XXa,X(b U a),0,0,0
+X(a | b),X(c | d | X(a | b)),0,0,0
+X(a | b) U (e R f),X(c | d | X(a | b)) U (g U f),0,0,0
+a,b,0,0,0
+a,b | c,0,0,0
+a | b,a,0,0,0
+a,a & c,0,0,0
+a & b,c,0,0,0
+a,a U b,0,0,0
+a,a R b,0,0,0
+a R b,a,0,0,0
+p2,p3 | G(p2 & p5),0,0,0
+!p3 & F(!p2 | !p5),!p2,0,0,0
+Xc W 0,Xc R b,0,0,0
+(b & c) W (a & b),a R b,1,0,0
+EOF
 
-run 1 ../syntimpl 0 '(e R f)' '(g U f)'
-run 1 ../syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
-run 1 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
-
-run 1 ../syntimpl 0 '1' '1'
-run 1 ../syntimpl 0 '0' '0'
-
-run 1 ../syntimpl 0 'a' '1'
-run 1 ../syntimpl 0 'a' 'a'
-
-run 1 ../syntimpl 0 'a' 'a & 1'
-
-run 1 ../syntimpl 0 'a & b' 'b'
-run 1 ../syntimpl 0 'a & b' 'a'
-
-run 1 ../syntimpl 0 'a' 'a + b'
-run 1 ../syntimpl 0 'b' 'a + b'
-
-run 1 ../syntimpl 0 'a + b' '1'
-
-run 1 ../syntimpl 0 'a' 'b U a'
-run 1 ../syntimpl 0 'a' 'b U 1'
-run 1 ../syntimpl 0 'a U b' '1'
-
-run 1 ../syntimpl 0 'a' '1 R a'
-run 1 ../syntimpl 0 'a' 'a R 1'
-run 1 ../syntimpl 0 'a R b' 'b'
-run 1 ../syntimpl 0 'a R b' '1'
-
-run 1 ../syntimpl 0 'Xa' 'X(b U a)'
-run 1 ../syntimpl 0 'X(a R b)' 'Xb'
-
-run 1 ../syntimpl 0 'a U b' '1 U b'
-run 1 ../syntimpl 0 'a R b' '1 R b'
-
-run 1 ../syntimpl 0 'b & (a U b)' 'a U b'
-run 1 ../syntimpl 0 'a U b' 'c + (a U b)'
-
-run 0 ../syntimpl 0 'Xa' 'XX(b U a)'
-run 0 ../syntimpl 0 'XXa' 'X(b U a)'
-
-run 0 ../syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
-run 0 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
-
-run 0 ../syntimpl 0 'a' 'b'
-run 0 ../syntimpl 0 'a' 'b + c'
-run 0 ../syntimpl 0 'a + b' 'a'
-run 0 ../syntimpl 0 'a' 'a & c'
-run 0 ../syntimpl 0 'a & b' 'c'
-run 0 ../syntimpl 0 'a' 'a U b'
-run 0 ../syntimpl 0 'a' 'a R b'
-run 0 ../syntimpl 0 'a R b' 'a'
-
-run 0 ../syntimpl 0 'p2' 'p3 || G(p2 && p5)'
-run 0 ../syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
-
-run 0 ../syntimpl 0 'Xc W 0' 'Xc R b'
-run 1 ../syntimpl 0 '(c&b) W (b&a)' 'a R b'
-
-exit 0
\ No newline at end of file
+run 0 ../syntimpl input > output
+diff input output