Commit 85beeec2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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/ Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.
parent d9d9837e
......@@ -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
......@@ -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 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 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
......@@ -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
......@@ -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':
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>')
unbufprint('<div class="formula lbt-format">' + spot.to_lbt_string(f) + '</div>')
elif formula_format == 'g':
elif formula_format == 'p':
......@@ -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;
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment