Commit 35fea2f5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

cgi: test formulas for stutter invariance

* wrap/python/ajax/spotcgi.in: Here.
parent de00bd3e
......@@ -500,6 +500,11 @@ if output_type == 'f':
unbufprint('<li>not an obligation</li>')
minimized = 0
automaton = 0
if not f.is_syntactic_stutter_invariant():
if spot.is_stutter_invariant(f):
unbufprint('<li>stutter invariant</li>')
else:
unbufprint('<li>stutter sensitive</li>')
unbufprint('</ul>\n')
finish()
......@@ -514,8 +519,9 @@ cannot be translated using this algorithm. Please use Couveur/FM.'''
dict = spot.make_bdd_dict()
if output_type == 't' and not f.is_syntactic_stutter_invariant():
unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
if output_type == 't' and not spot.is_stutter_invariant(f):
unbufprint('<b>Warning:</b> Testing automata are only valid '
+ 'for stutter-insensitive formulas, but the input is not.</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