diff --git a/ChangeLog b/ChangeLog index a7a8dc960..2e53c2a7d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2006-01-10 Alexandre Duret-Lutz + + * wrap/python/spot.i: Wrap spot::emptiness_check_instantiator. + * wrap/python/cgi/ltl2tgba.in: Offers all 6 emptiness + check algorithms, and a text box for options. + 2006-01-05 Alexandre Duret-Lutz * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_cycle): diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 295b7a20b..502ca8472 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -1,6 +1,6 @@ #!@PYTHON@ # -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -241,10 +241,15 @@ options_accepting_run = [ ('draw_acc_run', 'draw an accepting run...', 0), ('emptiness_check', ['... found using this algorithm: ', - 'couvreur99', - 'couvreur99_shy', - 'explicit_magic_search', - 'explicit_se05'], 'no') + 'Cou99', + 'CVWY90', + 'GV04', + 'SE05', + 'Tau03', + 'Tau03_opt'], 'no'), + ('emptiness_check_options', + '...with these ' + + 'options:', ''), ] print ("""

@@ -328,10 +333,11 @@ def add_options(opt_group, opt_column, opt_color, opt_list): else: prefix = '    ' for opt, desc, arg, in opt_list: - if formula: - val = int(form.getfirst(opt, 0)) - else: - val = arg + if not isinstance(arg, str): + if formula: + val = int(form.getfirst(opt, 0)) + else: + val = arg s = '%s' % (opt_color, prefix); if isinstance(desc, list): @@ -341,19 +347,24 @@ def add_options(opt_group, opt_column, opt_color, opt_list): val = n for i in desc[1:]: if n == val: - str = ' selected' + chk = ' selected' else: - str = '' - s += '

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'): + err = "" + opt = emptiness_check + "(" + emptiness_check_options + ")" + eci, err = spot.emptiness_check_instantiator.construct(opt) + + ec_msg = "Running " + opt + + if not eci: + print ('Cannot parse "' + opt + '" near "' + err + + '".') + else: ec_a = 0 - if degen: - ec_a = degen - ec_msg += ' on degeneralized automaton' + n_acc = automaton.number_of_acceptance_conditions() + n_max = eci.max_acceptance_conditions() + if (n_acc <= n_max): + ec_a = automaton else: - count = automaton.number_of_acceptance_conditions() - if (count <= 1): - ec_a = automaton + if degen: + ec_a = degen + ec_msg += ' on degeneralized automaton' else: - ec_a = 0 print ('Cannot run ' + emptiness_check - + ' on automata with more than 1 acceptance ' - + 'condition. Please select "draw degeneralized ' + + ' on automata with more than ' + n_max + ' acceptance ' + + 'conditions. 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 + ec = eci.instantiate(ec_a) + if ec: print '%s: ' % ec_msg sys.stdout.flush() diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 90c1ab909..5e0c792fb 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique +// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -94,6 +94,14 @@ using namespace spot::ltl; using namespace spot; %} +// For spot::emptiness_check_instantiator::construct and any other +// function that return errors via a "char **err" argument. +%typemap(in, numinputs=0) char** OUTPUT (char* temp) + "$1 = &temp;"; +%typemap(argout, fragment="t_output_helper") char** OUTPUT + "$result = t_output_helper($result, SWIG_FromCharPtr(*$1));"; +%apply char** OUTPUT { char** err }; + %include "misc/version.hh" %include "misc/bddalloc.hh" %include "misc/minato.hh" @@ -139,6 +147,9 @@ using namespace spot; %feature("new") spot::explicit_magic_search; %feature("new") spot::explicit_se05_search; +%feature("new") spot::emptiness_check_instantiator::construct; +%feature("new") spot::emptiness_check_instantiator::instanciate; + // Help SWIG with namespace lookups. #define ltl spot::ltl %include "tgba/bdddict.hh"