From 35fea2f5d125d1c766727ad2264ca07a45dad6e4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 16 Jun 2015 18:56:49 +0200
Subject: [PATCH] cgi: test formulas for stutter invariance

* wrap/python/ajax/spotcgi.in: Here.
---
 wrap/python/ajax/spotcgi.in | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in
index b5753027c..819356bed 100755
--- a/wrap/python/ajax/spotcgi.in
+++ b/wrap/python/ajax/spotcgi.in
@@ -500,6 +500,11 @@ if output_type == 'f':
                 unbufprint('<li>not an obligation</li>')
             minimized = 0
             automaton = 0
+        if not f.is_syntactic_stutter_invariant():
+            if spot.is_stutter_invariant(f):
+                unbufprint('<li>stutter invariant</li>')
+            else:
+                unbufprint('<li>stutter sensitive</li>')
         unbufprint('</ul>\n')
     finish()
 
@@ -514,8 +519,9 @@ cannot be translated using this algorithm.  Please use Couveur/FM.'''
 
 dict = spot.make_bdd_dict()
 
-if output_type == 't' and not f.is_syntactic_stutter_invariant():
-    unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
+if output_type == 't' and not spot.is_stutter_invariant(f):
+    unbufprint('<b>Warning:</b> Testing automata are only valid '
+               + 'for stutter-insensitive formulas, but the input is not.</br>')
 
 # Should the automaton be displayed as a SBA?
 issba = False