alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Support LBT formula in ltl2tgba.html.

Browse source 
Suggested by Joachim Klein.

* wrap/python/ajax/spot.in: Try parse_lbt() when parse() fails.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-20 21:40:51 +02:00
parent e78548ebae
commit e997676c3e
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -1,6 +1,12 @@
New in spot 1.2.4a (not yet released) New in spot 1.2.4a (not yet released)
* Documentation * New feature:
- 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.
* Documentation:
- The man page for ltl2tgba has some new notes and references - The man page for ltl2tgba has some new notes and references
about TGBA and about monitors. about TGBA and about monitors.

8
wrap/python/ajax/spot.in
View file

@ -1,6 +1,6 @@
#!@PYTHON@ #!@PYTHON@
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et # Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -405,9 +405,15 @@ pel = spot.empty_parse_error_list()
f = spot.parse(formula, pel, env) f = spot.parse(formula, pel, env)
if pel: if pel:
# Try the LBT parser in case someone is throwing LBT formulas at us.
pel2 = spot.empty_parse_error_list()
g = spot.parse_lbt(formula, pel2, env)
if pel2:
unbufprint('<div class="parse-error">') unbufprint('<div class="parse-error">')
err = spot.format_parse_errors(spot.get_cout(), formula, pel) err = spot.format_parse_errors(spot.get_cout(), formula, pel)
unbufprint('</div>') unbufprint('</div>')
else:
f = g
# Do not continue if we could not parse anything sensible. # Do not continue if we could not parse anything sensible.
if not f: if not f: