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

cgi: update for recent changes

Browse source 
* wrap/python/ajax/spot.in: Adjust to recent changes.
This commit is contained in:
Alexandre Duret-Lutz 2015-06-13 23:50:06 +02:00
parent 89592881c7
commit 200fcbfe49
1 changed files with 11 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -288,11 +288,11 @@ However you may download the <a href="''' + cgi.escape(autprefix)
def render_automaton(automaton, dont_run_dot): def render_automaton(automaton, dont_run_dot):
dotsrc = spot.ostringstream() dotsrc = spot.ostringstream()
if isinstance(automaton, spot.ta): # TA/GTA if isinstance(automaton, spot.ta): # TA/GTA
spot.print_dot(dotsrc, automaton) spot.print_dot(dotsrc, automaton, "Brf(Lato)")
elif hasattr(automaton, 'get_ta'): # TGTA elif hasattr(automaton, 'get_ta'): # TGTA
spot.print_dot(dotsrc, automaton.get_ta()) spot.print_dot(dotsrc, automaton.get_ta(), "Brf(Lato)")
else: # TGBA else: # TGBA
spot.print_dot(dotsrc, automaton, "N") spot.print_dot(dotsrc, automaton, "Brf(Lato)")
render_dot_maybe(dotsrc.str(), dont_run_dot) render_dot_maybe(dotsrc.str(), dont_run_dot)
def render_formula(f): def render_formula(f):
@ -302,6 +302,8 @@ def render_formula(f):
def print_stats(automaton, detinfo = False, ta = False): def print_stats(automaton, detinfo = False, ta = False):
if ta: # TA/GTA if ta: # TA/GTA
if hasattr(automaton, 'get_ta'): # TGTA
automaton = automaton.get_ta()
stats = spot.stats_reachable(automaton) stats = spot.stats_reachable(automaton)
detinfo = False detinfo = False
else: else:
@ -325,16 +327,11 @@ def print_stats(automaton, detinfo = False, ta = False):
's' if stats.transitions > 1 else '', 's' if stats.transitions > 1 else '',
stats.sub_transitions, stats.sub_transitions,
's' if stats.sub_transitions > 1 else '')) 's' if stats.sub_transitions > 1 else ''))
if hasattr(automaton, 'acc'): if hasattr(automaton, 'get_acceptance'):
count = automaton.acc().num_sets() acc = automaton.get_acceptance()
if count > 0: unbufprint(", acceptance condition: " + str(acc))
unbufprint(", %d acceptance condition" % count) if acc.is_true():
if count > 1: unbufprint(" (all cycles are accepting)")
unbufprint("s")
unbufprint(": " +
automaton.acc().format(automaton.acc().all_sets()))
else:
unbufprint(", no acceptance condition (all cycles are accepting)")
unbufprint("</p>\n") unbufprint("</p>\n")
# Decide whether we will render the automaton or not. # Decide whether we will render the automaton or not.
# (A webserver is not a computation center...) # (A webserver is not a computation center...)
@ -722,7 +719,7 @@ else:
if output_type == 'a': if output_type == 'a':
if buchi_type == 'i': if buchi_type == 'i':
s = spot.ostringstream() s = spot.ostringstream()
spot.print_never_claim(s, degen, f) spot.print_never_claim(s, degen)
unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str())) unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
del s del s
else: # 't' or 's' else: # 't' or 's'