From 8d2d9be39cf1b2254206f481e2bdc868522a327a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 15 Jul 2012 18:30:45 +0200
Subject: [PATCH] ltl2tgba.html: Add a warning.

* wrap/python/ajax/spot.in: Warn about formulae that don't look
stuttering insensitive.
---
 wrap/python/ajax/spot.in | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 6588f2aa1..b78365307 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -480,6 +480,9 @@ cannot be translated using this algorithm.  Please use Couveur/FM.'''
 
 dict = spot.bdd_dict()
 
+if output_type == 't' and not (f.is_ltl_formula() and f.is_X_free()):
+    unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
+
 # Should the automaton be displayed as a SBA?
 issba = False