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", "
"))
+ unbufprint(ver.replace(b"\n", b"
"))
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('
Failed to run ltl3ba. Is it installed?
')
- finish()
- if ret != 0:
- unbufprint('ltl3ba exited with error %s
' % ret)
- finish()
- tpel = spot.empty_parse_aut_error_list()
- automaton = spot.parse_aut(l3file, tpel, dict, env)
- if tpel:
- unbufprint('''failed to read ltl3ba's output
''')
- unbufprint('')
- err = spot.format_parse_aut_errors(spot.get_cout(), "output", tpel)
- unbufprint('
')
- 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('{}
'.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"