diff --git a/ChangeLog b/ChangeLog index 80c787784..361db2f6b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2004-02-02 Alexandre Duret-Lutz + * wrap/python/cgi/ltl2tgba.in (print_stats): Compute and display + the number of acceptance conditions. + * wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: Specify coding system to diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index b2e48449c..427287ad0 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -59,15 +59,31 @@ def escaped_print_set(dict, what): def print_stats(automaton): stats = spot.stats_reachable(automaton) print "

", stats.states, - if stats.states == 1: + if stats.states <= 1: print " state,", else: print " states,", print stats.transitions, - if stats.transitions == 1: - print " transition", + if stats.transitions <= 1: + print " transition,", else: - print " transitions", + print " transitions,", + # compute the number of acceptance conditions + acc = all = automaton.all_acceptance_conditions() + count = 0 + while all != buddy.bddfalse: + all -= buddy.bdd_satone(all) + count += 1 + if count > 0: + print count, + if count <= 1: + print "acceptance condition:", + else: + print "acceptance conditions:", + sys.stdout.flush() + spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc) + else: + print "no acceptance condition (all cycles are accepting)" print "

" sys.stdout.flush() @@ -96,6 +112,7 @@ os.close(sys.stderr.fileno()) os.dup2(sys.stdout.fileno(), sys.stderr.fileno()) import spot +import buddy print "LTL-to-Büchi test" print "

Input

"