Commit 8d2d9be3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl2tgba.html: Add a warning.

* wrap/python/ajax/spot.in: Warn about formulae that don't look
stuttering insensitive.
parent e30b9232
......@@ -480,6 +480,9 @@ cannot be translated using this algorithm. Please use Couveur/FM.'''
dict = spot.bdd_dict()
if output_type == 't' and not (f.is_ltl_formula() and f.is_X_free()):
unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
# Should the automaton be displayed as a SBA?
issba = False
......
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