From 3dfde9e85f5af4aa101ce71150d2c0f92f9c8339 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 5 Dec 2011 17:29:39 +0100
Subject: [PATCH] Make sure PSL formulae are translated with the FM
 translation.

* src/tgbatest/ltl2tgba.cc: Diagnose attempt to use -l and -taa
on PSL formulae.  Switch back to -f for these formulae.
---
 src/tgbatest/ltl2tgba.cc | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 6ab6934ff..884d1976e 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -826,6 +826,15 @@ main(int argc, char** argv)
 		std::cout << spot::ltl::to_string(f) << std::endl;
 	    }
 
+	  if (f->is_psl_formula()
+	      && !f->is_ltl_formula()
+	      && translation != TransFM)
+	    {
+	      std::cerr << "Only the FM algorithm can translate PSL formulae;"
+			<< " I'm using it for this formula." << std::endl;
+	      translation = TransFM;
+	    }
+
 	  tm.start("translating formula");
 	  switch (translation)
 	    {