From ca6084160e342aa76cccb02ebda560565864dc26 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 14 Nov 2004 23:10:56 +0000 Subject: [PATCH] * wrap/python/cgi/ltl2tgba.in: Add options to check the produced automata for emptiness, using the existing algorithms. * wrap/python/spot.i: Declare spot::explicit_magic_search, and spot::explicit_se05_search as allocating their output. --- ChangeLog | 7 +++ wrap/python/cgi/ltl2tgba.in | 121 ++++++++++++++++++++++++++++++++---- wrap/python/spot.i | 2 + 3 files changed, 118 insertions(+), 12 deletions(-) diff --git a/ChangeLog b/ChangeLog index 51c78ae49..fc1062ee7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2004-11-14 Alexandre Duret-Lutz + + * wrap/python/cgi/ltl2tgba.in: Add options to check the produced + automata for emptiness, using the existing algorithms. + * wrap/python/spot.i: Declare spot::explicit_magic_search, + and spot::explicit_se05_search as allocating their output. + 2004-11-12 Alexandre Duret-Lutz * configure.ac: Check for srand48 and drand48. diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 7544130a8..295b7a20b 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -130,11 +130,7 @@ def print_stats(automaton): else: 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 + count = automaton.number_of_acceptance_conditions() if count > 0: print count, if count <= 1: @@ -142,6 +138,7 @@ def print_stats(automaton): else: print "acceptance conditions:", sys.stdout.flush() + acc = automaton.all_acceptance_conditions() spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc) else: print "no acceptance condition (all cycles are accepting)" @@ -163,9 +160,12 @@ def render_dot(basename): print '
(dot source)' sys.stdout.flush() -def render_automaton(basename, automata, dont_run_dot): +def render_automaton(basename, automata, dont_run_dot, deco = False): outfile = spot.ofstream(basename + '.txt') - spot.dotty_reachable(outfile, automata) + if not deco: + spot.dotty_reachable(outfile, automata) + else: + spot.dotty_reachable(outfile, automata, deco) del outfile if dont_run_dot: print ('

' + dont_run_dot + ''' to be rendered on-line. However @@ -236,6 +236,17 @@ translators = [ ('trans_lacim', 'Couvreur/LaCIM', color_lacim), ] +options_accepting_run = [ + ('print_acc_run', 'print an accepting run...', 0), + ('draw_acc_run', 'draw an accepting run...', 0), + ('emptiness_check', + ['... found using this algorithm: ', + 'couvreur99', + 'couvreur99_shy', + 'explicit_magic_search', + 'explicit_se05'], 'no') + ] + print ("""

Formula to translate:
""" @@ -321,13 +332,32 @@ def add_options(opt_group, opt_column, opt_color, opt_list): val = int(form.getfirst(opt, 0)) else: val = arg - if val: - str = " checked" + + s = '%s' % (opt_color, prefix); + if isinstance(desc, list): + s += '%s ' + val = desc[val] else: - str = "" + if val: + str = ' checked' + else: + str = '' + s += '%s' % (opt, str, + desc) + + column[opt_column].append((s + '')) globals()[opt] = val - s = '%s%s' - column[opt_column].append((s % (opt_color, prefix, opt, str, desc))) column[0].append("Algorithm") @@ -343,6 +373,7 @@ for opt, desc, color in translators: column[0].append(s % (color, opt, str, desc)) add_options('', 0, color, globals()['options_' + opt]) +add_options("Search accepting run?", 0, '', options_accepting_run) add_options("Common Options", 1, '', options_common) add_options("Formula Simplications", 1, '', options_reduce) add_options("Debugging Options", 1, '', options_debug) @@ -521,6 +552,71 @@ if show_lbtt: spot.lbtt_reachable(spot.get_cout(), degen) print '' + +if draw_acc_run or print_acc_run: + print '

Accepting run

' + ec_msg = "Running " + emptiness_check + ec_a = automaton + if emptiness_check == 'couvreur99': + ec = spot.couvreur99_check(automaton) + elif emptiness_check == 'couvreur99_shy': + ec = spot.couvreur99_check_shy(automaton) + elif (emptiness_check == 'explicit_magic_search' + or emptiness_check == 'explicit_se05'): + ec_a = 0 + if degen: + ec_a = degen + ec_msg += ' on degeneralized automaton' + else: + count = automaton.number_of_acceptance_conditions() + if (count <= 1): + ec_a = automaton + else: + ec_a = 0 + print ('Cannot run ' + emptiness_check + + ' on automata with more than 1 acceptance ' + + 'condition. Please select "draw degeneralized ' + + 'Büchi automaton" if you want to try this' + + ' algorithm on the degeneralized version of the' + + ' automaton.') + if ec_a: + if emptiness_check == 'explicit_magic_search': + ec = spot.explicit_magic_search(ec_a) + elif emptiness_check == 'explicit_se05': + ec = spot.explicit_se05_search(ec_a) + else: + ec = 0 + else: + print emptiness_check, "unsupported" + sys.stdout.flush() + assert 0 + if ec: + print '%s: ' % ec_msg + sys.stdout.flush() + ec_res = ec.check() + if not ec_res: + print "no accepting run found.
" + else: + ec_run = ec_res.accepting_run() + print "accepting run found.
" + if ec_run: + if print_acc_run: + print '
'; sys.stdout.flush()
+                    s = spot.ostringstream()
+                    spot.print_tgba_run(s, ec_a, ec_run)
+                    print cgi.escape(s.str())
+                    del s
+                    print '
'; sys.stdout.flush() + if draw_acc_run: + deco = spot.tgba_run_dotty_decorator(ec_run) + dont_run_dot = print_stats(ec_a) + render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco) + del deco + del ec_run + del ec_res + del ec + del ec_a + sys.stdout.flush() spot.destroy(f) @@ -528,4 +624,5 @@ spot.destroy(f) del degen del automaton +del dict print_footer() diff --git a/wrap/python/spot.i b/wrap/python/spot.i index f92bc9601..9418592e4 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -132,6 +132,8 @@ using namespace spot; %feature("new") spot::tgba_dupexp_dfs; %feature("new") spot::emptiness_check::check; %feature("new") spot::emptiness_check_result::accepting_run; +%feature("new") spot::explicit_magic_search; +%feature("new") spot::explicit_se05_search; // Help SWIG with namespace lookups. #define ltl spot::ltl