ltlcross, ltldo: add a --relabel option

* bin/common_trans.cc, bin/common_trans.hh: Add the --relabel option.
* bin/ltlcross.cc, bin/ltldo.cc: Implement it.
* doc/org/ltldo.org, NEWS: Document it.
* tests/core/ltl3ba.test: Test it.

NEWS

@@ -50,6 +50,12 @@ New in spot 2.2.2.dev (Not yet released)
     print the class of a formula in the temporal hierarchy of Manna &
     Pnueli using %h.  See https://www.lrde.epita.fr/hierarchy.html
 
+  * ltldo and ltlcross learned a --relabel option to force the
+    relabeling of atomic propositions to p0, p1, etc.  This is more
+    useful with ltldo, as it allows calling a tool that restricts the
+    atomic propositions it supports, and the output automaton will
+    then be fixed to use the original atomic propositions.
+
   Library:
 
   * A twa is required to have at least one state, the initial state.

bin/common_trans.cc

@@ -622,6 +622,7 @@ exec_with_timeout(const char* cmd)
 
 enum {
   OPT_LIST = 1,
+  OPT_RELABEL = 2,
 };
 static const argp_option options[] =
 {
@@ -632,6 +633,8 @@ static const argp_option options[] =
     { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 },
     { "list-shorthands", OPT_LIST, nullptr, 0,
       "list availabled shorthands to use in COMMANDFMT", 0},
+    { "relabel", OPT_RELABEL, nullptr, 0,
+      "always relabel atomic propositions before calling any translator", 0 },
     /**************************************************/
     { nullptr, 0, nullptr, 0,
       "COMMANDFMT should specify input and output arguments using the "
@@ -649,7 +652,8 @@ static const argp_option options[] =
       "If either %l, %L, or %T are used, any input formula that does "
       "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "
       "relabeled automatically.  Likewise if %s or %S are used with "
-      "atomic proposition that compatible with Spin's syntax.\n"
+      "atomic proposition that compatible with Spin's syntax.  You can "
+      "force this relabeling to always occur with option --relabel.\n"
       "The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\""
       " by a bracketed sequence of operators to unabbreviate before outputing"
       " the formula.  For instance %[MW]f will rewrite operators M and W"
@@ -660,6 +664,8 @@ static const argp_option options[] =
     { nullptr, 0, nullptr, 0, nullptr, 0 }
 };
 
+bool opt_relabel = false;
+
 static int parse_opt_trans(int key, char* arg, struct argp_state*)
 {
   switch (key)
@@ -677,6 +683,9 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*)
     case OPT_LIST:
       show_shorthands();
       exit(0);
+    case OPT_RELABEL:
+      opt_relabel = true;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }

bin/common_trans.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -29,6 +29,7 @@
 
 
 extern const struct argp trans_argp;
+extern bool opt_relabel;
 
 struct translator_spec
 {

bin/ltlcross.cc

@@ -992,10 +992,12 @@ namespace
     {
       static unsigned round = 0;
 
+      if (opt_relabel
           // If we need LBT atomic proposition in any of the input or
           // output, relabel the formula.
-      if ((!f.has_lbt_atomic_props() &&
+          ||  (!f.has_lbt_atomic_props() &&
                (runner.has('l') || runner.has('L') || runner.has('T')))
+          // Likewise for Spin
           || (!f.has_spin_atomic_props() &&
               (runner.has('s') || runner.has('S'))))
         f = spot::relabel(f, spot::Pnn);

bin/ltldo.cc

@@ -299,7 +299,8 @@ namespace
 
       // If atomic propositions are incompatible with one of the
       // output, relabel the formula.
-      if ((!f.has_lbt_atomic_props() &&
+      if (opt_relabel
+          || (!f.has_lbt_atomic_props() &&
               (runner.has('l') || runner.has('L') || runner.has('T')))
           || (!f.has_spin_atomic_props() &&
               (runner.has('s') || runner.has('S'))))

doc/org/ltldo.org

@@ -359,7 +359,6 @@ ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges'
 : ltl3ba, 2 states, 4 edges
 : ltl3ba -H2, 1 states, 2 edges
 
-
 * Transparent renaming
 
 If you have ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate
@@ -407,6 +406,10 @@ formula has atomic propositions incompatible with Spin's conventions;
 or when some command uses =%l= or =%L=, and the formula has
 atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]].
 
+For =%f=, =%w=, =%F=, and =%W=, no relabeling is automatically
+performed, but you can pass option =--relabel= if you need to force it
+for some reason (e.g., if you have a tool that uses almost Spot's
+syntax, but cannot cope with double-quoted atomic propositions).
 
 There are some cases where the renaming is not completely transparent.
 For instance if a translator tool outputs some HOA file named after

tests/core/ltl3ba.test

@@ -47,3 +47,19 @@ sed 's/[^,]//g' <output.csv |
 while read l; do
   test "x$first" = "x$l" || exit 1
 done)
+
+# The name of the HOA is preserved
+case `ltldo 'ltl3ba -H' -f xxx --stats=%m` in
+    *xxx*);;
+    *) exit 1;;
+esac
+# The relabeling of atomic proposition can be forced.  This
+# will impact the name of the automaton set by ltldo...
+case `ltldo --relabel 'ltl3ba -H' -f xxx --stats=%m` in
+    *xxx*) exit 1;;
+    *p0*);;
+    *) exit 1;;
+esac
+# ... but the atomic propositions are still using xxx
+# because ltldo should relabel them back.
+ltldo --relabel 'ltl3ba -H' -f xxx | grep 'AP:.*"xxx"'