From 61824f9b87cc3bc86e349a0552451f0e58033364 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 12 May 2019 15:49:23 +0200
Subject: [PATCH] state if a non SSI formula can be simplified to an SSI
 formula

---
 client/src/LtlApp.js |  2 ++
 server/spotapi.py    | 15 +++++++++++++--
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/client/src/LtlApp.js b/client/src/LtlApp.js
index 7b4a582..9260296 100644
--- a/client/src/LtlApp.js
+++ b/client/src/LtlApp.js
@@ -1005,6 +1005,8 @@ class LtlStudy extends React.Component {
             <Typography>
               This formula is <b>stutter-invariant</b> even if it might not look
               so syntactically.
+              {"stutter_invariant_eq" in res &&
+               (<><br/>Furthermore, it can be simplified to the following <i>syntactically sutter-invariant</i> formula:<br/><Ltl f={res["stutter_invariant_eq"]}/></>)}
             </Typography>
           )}
           {res["stutter_invariant"] === false && (
diff --git a/server/spotapi.py b/server/spotapi.py
index 0bae0b9..8459ff7 100755
--- a/server/spotapi.py
+++ b/server/spotapi.py
@@ -216,13 +216,19 @@ mp_class_to_english = {
 #
 # on success:
 # { mp_class: 'name',
-#   pathological: True,   (absent if not pathological)
+#   pathological: true,   (absent if not pathological)
 #   mp_hierarchy_svg: '<svg...'
 #   acc_word: 'word',     (an example of accepting word, or null)
 #   rej_word: 'word',     (an example of rejecting word, or null)
-#   stutter_invariant: False,   (or True, or 'no X')
+#   stutter_invariant: false,   (or true, or 'no X')
+#   stutter_invariant_eq: formula,  (* see below)
 #   safety_liveness: 'safety'  (or 'liveness', or 'both', or 'none')
 # }
+#
+# stutter_invariant_eq is only given if stutter_invariant=true (not 'no X'),
+# and simplifying the input ltlformula gives a syntactically stutter-invariant
+# formula.
+
 @app.route('/api/study/<path:ltlformula>')
 @cachecontrol()
 def study(ltlformula, method='GET'):
@@ -259,6 +265,11 @@ def study(ltlformula, method='GET'):
     ssi = f.is_syntactic_stutter_invariant()
 
     pos = spot.translate(f, 'med')
+
+    # f was simplified by translate.
+    if (ssi is False and f.is_syntactic_stutter_invariant()):
+        result['stutter_invariant_eq'] = str(f)
+
     neg = spot.translate(spot.formula_Not(f), 'med')
 
     if ssi:
-- 
GitLab