From 01838a2456580963fa4ceb3a4a06dbc023f52a3e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 13 Jan 2017 21:26:53 +0100
Subject: [PATCH] ltlcross, ltldo: Add support for ltl3hoa.

* bin/common_trans.cc: Add shorthand for ltl3hoa.
* NEWS, doc/org/ltlcross.org, doc/org/ltldo.org: Mention it.
---
 NEWS                 | 3 +++
 bin/common_trans.cc  | 1 +
 doc/org/ltlcross.org | 6 ++++--
 doc/org/ltldo.org    | 7 ++++---
 4 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 4c5217c48..afe01ad22 100644
--- a/NEWS
+++ b/NEWS
@@ -56,6 +56,9 @@ New in spot 2.2.2.dev (Not yet released)
     atomic propositions it supports, and the output automaton will
     then be fixed to use the original atomic propositions.
 
+  * ltldo and ltlcross have learned how to call ltl3hoa, so
+    'ltl3hoa -f %f>%O' can be abbreviated to just 'ltl3hoa'.
+
   Library:
 
   * A twa is required to have at least one state, the initial state.
diff --git a/bin/common_trans.cc b/bin/common_trans.cc
index 6b9363c0a..e351ef3ce 100644
--- a/bin/common_trans.cc
+++ b/bin/common_trans.cc
@@ -47,6 +47,7 @@ static struct shorthands_t
     { "ltl2tgba", " -H %f>%O" },
     { "ltl3ba", " -f %s>%O" },
     { "ltl3dra", " -f %s>%O" },
+    { "ltl3hoa", " -f %f>%O" },
     { "modella", " %[MWei^]L %O" },
     { "spin", " -f %s>%O" },
   };
diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org
index fd282244c..66628a841 100644
--- a/doc/org/ltlcross.org
+++ b/doc/org/ltlcross.org
@@ -163,9 +163,10 @@ tools:
   - '=java -jar Rabinizer.jar -ltl2dstar %[MW]F %O; mv %O.dst %O=' (Rabinizer
     uses the last =%O= argument as a prefix to which it always append =.dst=,
     so we have to rename =%O.dst= as =%O= so that =ltlcross= can find the file)
-  - '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %[MWR]f >%O~'
+  - '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %[MWRei^]f >%O~'
     (rabinizer 3.1 can output automata in the HOA format)
-  - '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl2dra=.)
+  - '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl3dra=.)
+  - '=ltl3hoa -f %s >%O=' (The HOA format is the default for =ltl3hoa=.)
 
 To simplify the use of some of the above tools, a set of predefined
 shorthands are available.  Those can be listed with the
@@ -185,6 +186,7 @@ the following words, then the string on the right is appended.
   ltl2tgba     -H %f>%O
   ltl3ba       -f %s>%O
   ltl3dra      -f %s>%O
+  ltl3hoa      -f %f>%O
   modella      %[MWei^]L %O
   spin         -f %s>%O
 
diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org
index ca50be734..99b8a31b2 100644
--- a/doc/org/ltldo.org
+++ b/doc/org/ltldo.org
@@ -304,18 +304,19 @@ the following words, then the string on the right is appended.
 
   lbt          <%L>%O
   ltl2ba       -f %s>%O
-  ltl2dstar    --output-format=hoa %L %O
+  ltl2dstar    --output-format=hoa %[MW]L %O
   ltl2tgba     -H %f>%O
   ltl3ba       -f %s>%O
   ltl3dra      -f %s>%O
-  modella      %L %O
+  ltl3hoa      -f %f>%O
+  modella      %[MWei^]L %O
   spin         -f %s>%O
 
 Any {name} and directory component is skipped for the purpose of
 matching those prefixes.  So for instance
   '{DRA} ~/mytools/ltl2dstar-0.5.2'
 will changed into
-  '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O'
+  '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'
 #+end_example
 
 Therefore you can type just