From 85beeec2e4348cef6440d0670677c61975c7315c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 21 Aug 2014 15:18:43 +0200
Subject: [PATCH] ltl2tgba.html: Add option to output LBT format.

Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: New option.
* wrap/python/ajax/protocol.txt, NEWS: Document it.
* wrap/python/ajax/spot.in: Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.
---
 NEWS                           | 3 ++-
 wrap/python/ajax/ltl2tgba.html | 4 ++++
 wrap/python/ajax/protocol.txt  | 1 +
 wrap/python/ajax/spot.in       | 7 ++++++-
 wrap/python/spot.i             | 2 ++
 5 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index e6b10c458..66922d6c7 100644
--- a/NEWS
+++ b/NEWS
@@ -4,7 +4,8 @@ New in spot 1.2.4a (not yet released)
 
     - The online ltl2tgba translator will automatically attempt to
       parse a formula using LBT's syntax if it cannot parse it using
-      the normal infix syntax.
+      the normal infix syntax.  It also has an option to display
+      formulas using LBT's syntax.
 
     - ltl2tgba and dstar2tgba have a new experimental option --hoaf to
       output automata in the Hanoï Omega Automaton Format whose
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 949cfad06..231e612ec 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -489,6 +489,10 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  <INPUT type="radio" name="ff" value="i">
 		  text in Spin's syntax
 		</label><br>
+		<label class="rtip" title="This output can be given to LBT, LBTT, ltl2dstar, scheck, or any other tool using a similar syntax.  Spot can also read it back.  The original syntax only support atomic propositions named <span class='formula'>p0</span>, <span class='formula'>p1</span>, etc.   As an extension, also supported by ltl2dstar, other atomic proposition are enclosed in double quotes.  PSL formulas are not supported.">
+		  <INPUT type="radio" name="ff" value="l">
+		  text in LBT's syntax
+		</label><br>
 		<label class="rtip" title="A graphical representation of Spot's internal representation.  Actually this is not a tree but an acyclic graph, because equal subformulas are shared.">
 		  <INPUT type="radio" name="ff" value="g">
 		  a syntactic tree
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 374ffb283..bb1588711 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -27,6 +27,7 @@ Type of formula output if o=f (pick one)
 
   ff=o    Spot syntax
   ff=i    Spin syntax
+  ff=l    LBT syntax
   ff=g    graphviz output of the AST
   ff=p    property dump
 
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index c396baa5a..3fc19fd16 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -447,7 +447,7 @@ if dored:
 # Formula manipulation only.
 if output_type == 'f':
     formula_format = form.getfirst('ff', 'o')
-    # o = Spot, i = Spin, g = GraphViz, p = properties
+    # o = Spot, i = Spin, l = LBT, g = GraphViz, p = properties
     if formula_format == 'o':
         unbufprint(format_formula(f))
     elif formula_format == 'i':
@@ -458,6 +458,11 @@ if output_type == 'f':
             if simpopt.reduce_size_strictly:
                 s = '<br><b>Try enabling larger formula rewritings.</b>'
             unbufprint('<div class="error">The above formula contains PSL operators that Spin will not understand.%s</div>' % s)
+    elif formula_format == 'l':
+        if not f.is_ltl_formula():
+            unbufprint('<div class="error">PSL formulas cannot be expressed in this format.</div>')
+        else:
+            unbufprint('<div class="formula lbt-format">' + spot.to_lbt_string(f) + '</div>')
     elif formula_format == 'g':
         render_formula(f)
     elif formula_format == 'p':
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index ac11bcf1c..3b175b6e7 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -70,6 +70,7 @@ namespace std {
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/tunabbrev.hh"
 #include "ltlvisit/apcollect.hh"
+#include "ltlvisit/lbt.hh"
 
 #include "tgba/bdddict.hh"
 #include "tgba/bddprint.hh"
@@ -182,6 +183,7 @@ using namespace spot;
 %include "ltlvisit/tostring.hh"
 %include "ltlvisit/tunabbrev.hh"
 %include "ltlvisit/apcollect.hh"
+%include "ltlvisit/lbt.hh"
 
 %feature("new") spot::emptiness_check::check;
 %feature("new") spot::emptiness_check_instantiator::construct;