From a9f4b01d9b8cac042ebecd96883250f873c8d469 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 20 Jun 2015 20:37:05 +0200
Subject: [PATCH] ajax: relabel formula and automata around ltl3ba

Fixes #53.

* wrap/python/ajax/spotcgi.in: Do that.
* wrap/python/ajax/trans.html: Fixup jquery code to
avoid looping over tabs.
* wrap/python/spot_impl.i: Wrap the automaton relabeling code.
* NEWS: Update.
---
 NEWS                        |  4 ++++
 wrap/python/ajax/spotcgi.in | 36 ++++++++++++------------------------
 wrap/python/ajax/trans.html |  6 ++++--
 wrap/python/spot_impl.i     |  2 ++
 4 files changed, 22 insertions(+), 26 deletions(-)

diff --git a/NEWS b/NEWS
index a1a15bf3f..6f3281b85 100644
--- a/NEWS
+++ b/NEWS
@@ -266,6 +266,10 @@ New in spot 1.99b (not yet released)
     - The on-line interface at http://spot.lrde.epita.fr/trans.html
       can be used to check stutter-invariance of any LTL/PSL formula.
 
+    - The on-line interface will work around atomic propositions not
+      supported by ltl3ba.  (E.g. you can now translate F(A) or
+      G("foo < bar").)
+
   * Noteworthy code changes
 
     - Boost is not used anymore.
diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in
index ccb484ca7..90a1b7893 100755
--- a/wrap/python/ajax/spotcgi.in
+++ b/wrap/python/ajax/spotcgi.in
@@ -136,7 +136,7 @@ os.dup2(fd, sys.stdout.fileno())
 # allowed to send strings to sys.stdout.  Always use the following
 # method instead.
 def unbufprint(s):
-    if sys.getdefaultencoding() != 'ascii':
+    if sys.getdefaultencoding() != 'ascii' and type(s) != bytes:
         sys.stdout.write(s.encode("utf-8"))
     else:
         sys.stdout.write(s)
@@ -378,7 +378,7 @@ if output_type == 'v3':
     if err != 0:
         unbufprint('not available')
     else:
-        unbufprint(ver.replace("\n", "<br>"))
+        unbufprint(ver.replace(b"\n", b"<br>"))
     finish()
 
 spot.unblock_signal(signal.SIGALRM)
@@ -580,29 +580,17 @@ elif translator == 'l3':
             l3opt.remove('-p')
     args = ["@LTL3BA@", l3out]
     args.extend(l3opt)
-    args.extend(['-f', spot.str_spin_ltl(f)])
-    import subprocess
-    l3file = tmpdir + "/aut"
-    with open(l3file, "w+") as l3aut:
-        try:
-            l3proc = subprocess.Popen(args, stdout=l3aut)
-            ret = l3proc.wait()
-        except:
-            unbufprint('<div class="error">Failed to run ltl3ba. Is it installed?</div>')
-            finish()
-        if ret != 0:
-            unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret)
-            finish()
-    tpel = spot.empty_parse_aut_error_list()
-    automaton = spot.parse_aut(l3file, tpel, dict, env)
-    if tpel:
-        unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
-        unbufprint('<div class="parse-error">')
-        err = spot.format_parse_aut_errors(spot.get_cout(), "output", tpel)
-        unbufprint('</div>')
-        automaton = 0
+    # Relabel the formula in case it contains unsupported atomic
+    # propositions (e.g., starting with _ or double-quoted).
+    m = spot.relabeling_map()
+    g = spot.relabel(f, spot.Pnn, m)
+    args.extend(['-f', "'" + spot.str_spin_ltl(g) + "' |"])
+    try:
+        automaton = spot.automaton(" ".join(args))
+    except RuntimeError as e:
+        unbufprint('<div class="error">{}</div>'.format(e))
         finish()
-    automaton = automaton.aut
+    spot.relabel_here(automaton, m)
 elif translator == 'cs':
     donot_inject = False
     cs_nowdba = True
diff --git a/wrap/python/ajax/trans.html b/wrap/python/ajax/trans.html
index 343185469..36266aae9 100644
--- a/wrap/python/ajax/trans.html
+++ b/wrap/python/ajax/trans.html
@@ -165,9 +165,11 @@
             $.spotvars.internalchange = false;
 	    var o = $('input[name="o"]').val();
 	    hideOrShowPanels(o, duration);
-	    $("#output-tabs").tabs('option', 'active', $("#tabs-o" + o).index());
+            $("#output-tabs").tabs('option', 'active',
+			           $('#output-tabs a[href="#tabs-o' + o + '"]').parent().index() - 1);
             var t = $('input[name="t"]').val();
-	    $("#translator-tabs").tabs('option', 'active', $('#tabs-t' + t).index());
+            $("#translator-tabs").tabs('option', 'active',
+				       $('#translator-tabs a[href="#tabs-t' + t + '"]').parent().index() - 1);
 	    updateResults();
 	}
 
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index bcd3f3402..59e7054fd 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -142,6 +142,7 @@ namespace std {
 #include "twaalgos/translate.hh"
 #include "twaalgos/hoa.hh"
 #include "twaalgos/dtgbasat.hh"
+#include "twaalgos/relabel.hh"
 
 #include "parseaut/public.hh"
 
@@ -307,6 +308,7 @@ namespace std {
 %include "twaalgos/translate.hh"
 %include "twaalgos/hoa.hh"
 %include "twaalgos/dtgbasat.hh"
+%include "twaalgos/relabel.hh"
 
 %include "parseaut/public.hh"