diff --git a/ChangeLog b/ChangeLog index 06f325128..65565272e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2011-03-04 Alexandre Duret-Lutz + + * wrap/python/ajax/spot.in: Use the degeneralized automaton if + available while computing the emptiness check. + 2011-03-04 Alexandre Duret-Lutz Speedup build_result() called by minimize_dfa(). diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 290411b2b..6fda08063 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -347,22 +347,22 @@ if output_type == 'r': print_acc_run = True elif s == 'd': draw_acc_run = True - - + + err = "" - opt = (form.getfirst('ec', 'Cou99') + "(" + + opt = (form.getfirst('ec', 'Cou99') + "(" + form.getfirst('eo', '') + ")") eci, err = spot.emptiness_check_instantiator.construct(opt) if not eci: - print ('
Cannot parse "' + opt + '" near "' + print ('
Cannot parse "' + opt + '" near "' + err + '".
') else: ec_a = 0 n_acc = degen.number_of_acceptance_conditions() n_max = eci.max_acceptance_conditions() if (n_acc <= n_max): - ec_a = automaton + ec_a = degen else: print ('
Cannot run ' + opt + ' on automata with more than ' + str(n_max)