* wrap/python/cgi/ltl2tgba.in (print_stats): Compute and display
the number of acceptance conditions.
This commit is contained in:
parent
49192cc35f
commit
59125b2a6c
2 changed files with 24 additions and 4 deletions
|
|
@ -1,5 +1,8 @@
|
||||||
2004-02-02 Alexandre Duret-Lutz <adl@gnu.org>
|
2004-02-02 Alexandre Duret-Lutz <adl@gnu.org>
|
||||||
|
|
||||||
|
* 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/bddnqueen.py, wrap/python/tests/interdep.py,
|
||||||
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
|
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
|
||||||
wrap/python/tests/ltlsimple.py: Specify coding system to
|
wrap/python/tests/ltlsimple.py: Specify coding system to
|
||||||
|
|
|
||||||
|
|
@ -59,15 +59,31 @@ def escaped_print_set(dict, what):
|
||||||
def print_stats(automaton):
|
def print_stats(automaton):
|
||||||
stats = spot.stats_reachable(automaton)
|
stats = spot.stats_reachable(automaton)
|
||||||
print "<p>", stats.states,
|
print "<p>", stats.states,
|
||||||
if stats.states == 1:
|
if stats.states <= 1:
|
||||||
print " state,",
|
print " state,",
|
||||||
else:
|
else:
|
||||||
print " states,",
|
print " states,",
|
||||||
print stats.transitions,
|
print stats.transitions,
|
||||||
if stats.transitions == 1:
|
if stats.transitions <= 1:
|
||||||
print " transition",
|
print " transition,",
|
||||||
else:
|
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 "</p>"
|
print "</p>"
|
||||||
sys.stdout.flush()
|
sys.stdout.flush()
|
||||||
|
|
||||||
|
|
@ -96,6 +112,7 @@ os.close(sys.stderr.fileno())
|
||||||
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
|
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
|
||||||
|
|
||||||
import spot
|
import spot
|
||||||
|
import buddy
|
||||||
|
|
||||||
print "<TITLE>LTL-to-Büchi test</TITLE>"
|
print "<TITLE>LTL-to-Büchi test</TITLE>"
|
||||||
print "<H1>Input</H1>"
|
print "<H1>Input</H1>"
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue