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

cgi: do not display Inf(0) for state-based BA

Browse source 
* wrap/python/ajax/spotcgi.in: If the output is a state-based BA, i.e.,
displayed with double circles, then do not output "Inf(0)" as acceptance
condition as that is confusing.  Print "Büchi" instead.
This commit is contained in:
Alexandre Duret-Lutz 2015-08-06 16:29:55 +02:00
parent 3edd55fcd5
commit c0b77b2e62
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
wrap/python/ajax/spotcgi.in
View file

@ -332,9 +332,12 @@ def print_stats(automaton, detinfo = False, ta = False):
's' if stats.sub_transitions > 1 else '')) 's' if stats.sub_transitions > 1 else ''))
if hasattr(automaton, 'get_acceptance'): if hasattr(automaton, 'get_acceptance'):
acc = automaton.get_acceptance() acc = automaton.get_acceptance()
unbufprint(", acceptance condition: " + str(acc)) if automaton.is_sba() and automaton.acc().is_buchi():
if acc.is_true(): unbufprint(", acceptance condition: Büchi")
unbufprint(" (all cycles are accepting)") else:
unbufprint(", acceptance condition: " + str(acc))
if acc.is_true():
unbufprint(" (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...)