From 57f712fcbd7d82e7cd04cf77d303485c673eb1a4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 19 Aug 2013 16:23:44 +0200
Subject: [PATCH] ltlcross: Allow %D, %N, or %T to be used multiple time

For example to interface with Rabinizer, we can now use
'java -jar /pathto/Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D'
because Rabinizer always append a suffix to its last argument, we
rename the file...

* src/bin/ltlcross.cc (printable_result_filename): Adjust.
---
 src/bin/ltlcross.cc | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 7a0945047..dee18c300 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -562,6 +562,7 @@ namespace
     void
     print(std::ostream& os, const char* pos) const
     {
+      output_format old_format = format;
       if (*pos == 'N')
 	format = Spin;
       else if (*pos == 'T')
@@ -572,12 +573,20 @@ namespace
 	assert(!"BUG");
 
       if (val_)
-	error(2, 0, "you may have only one %%D, %%N, or %%T specifier: %s",
-	      translators[translator_num]);
-      char prefix[30];
-      snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
-      const_cast<printable_result_filename*>(this)->val_
-	= spot::create_tmpfile(prefix);
+	{
+	  // It's OK to use a specified multiple time, but it's not OK
+	  // to mix the formats.
+	  if (format != old_format)
+	    error(2, 0, "you may not mix %%D, %%N, and %%T specifiers: %s",
+		  translators[translator_num]);
+	}
+      else
+	{
+	  char prefix[30];
+	  snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
+	  const_cast<printable_result_filename*>(this)->val_
+	    = spot::create_tmpfile(prefix);
+	}
       os << '\'' << val_ << '\'';
     }
   };