From 436e5a2d7f25dd5e29690649f7207ecb4ee509c9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 Aug 2024 11:18:14 +0200
Subject: [PATCH] ltlgrind: improve error message when formulas are missing

The error message, inherited from ltl2tgba, used to say "No formula to
translate", but "translate" isn't appropriate here.

* bin/common_finput.cc, bin/common_finput.hh (check_no_formula): Allow
"translate" to be changed.
* bin/ltlgrind.cc: Change it.
* tests/core/ltlgrind.test: Test it.
---
 bin/common_finput.cc     | 6 +++---
 bin/common_finput.hh     | 2 +-
 bin/ltlgrind.cc          | 2 +-
 tests/core/ltlgrind.test | 8 ++++++++
 4 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/bin/common_finput.cc b/bin/common_finput.cc
index df0343dd1..14cd06b36 100644
--- a/bin/common_finput.cc
+++ b/bin/common_finput.cc
@@ -388,14 +388,14 @@ job_processor::run()
   return error;
 }
 
-void check_no_formula()
+void check_no_formula(const char* action)
 {
   if (!jobs.empty())
     return;
   if (isatty(STDIN_FILENO))
-    error(2, 0, "No formula to translate?  Run '%s --help' for help.\n"
+    error(2, 0, "No formula to %s?  Run '%s --help' for help.\n"
           "Use '%s -' to force reading formulas from the standard "
-          "input.", program_name, program_name);
+          "input.", action, program_name, program_name);
   jobs.emplace_back("-", job_type::LTL_FILENAME);
 }
 
diff --git a/bin/common_finput.hh b/bin/common_finput.hh
index 30b7f333c..491364d19 100644
--- a/bin/common_finput.hh
+++ b/bin/common_finput.hh
@@ -93,5 +93,5 @@ public:
 
 // Report and error message or add a default job depending on whether
 // the input is a tty.
-void check_no_formula();
+void check_no_formula(const char* action = "translate");
 void check_no_automaton();
diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc
index 626211adc..61ffc3cd5 100644
--- a/bin/ltlgrind.cc
+++ b/bin/ltlgrind.cc
@@ -199,7 +199,7 @@ main(int argc, char* argv[])
 
       mut_opts |= opt_all;
 
-      check_no_formula();
+      check_no_formula("mutate");
 
       mutate_processor processor;
       if (processor.run())
diff --git a/tests/core/ltlgrind.test b/tests/core/ltlgrind.test
index f508c4826..bfceef88a 100755
--- a/tests/core/ltlgrind.test
+++ b/tests/core/ltlgrind.test
@@ -200,3 +200,11 @@ EOF
 
 ltlgrind -f 'a U b' -m 999999999999999999999999999 2>err && exit 1
 grep 'too large' err
+
+# The following message appears only if run from a tty.
+if (: > /dev/tty) >/dev/null 2>&1 ; then
+   ltlgrind </dev/tty 2>err && exit 1
+   grep 'No formula to mutate' err
+fi
+
+: