From 141baae57e8baaaac04a342f1d3b81c28cccea39 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Jun 2012 18:35:08 +0200 Subject: [PATCH] ltl2tgba.html: Use the new degeneralization routine. * wrap/python/spot.i: Export degeneralize(). * wrap/python/ajax/spot.in: Use it. --- wrap/python/ajax/spot.in | 4 ++-- wrap/python/spot.i | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 1199ebd96..ac54f4d60 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -616,13 +616,13 @@ if direct_simul: issba = False if degen or neverclaim: - degen = spot.tgba_sba_proxy(automaton) + degen = spot.degeneralize(automaton) issba = True else: degen = automaton if utf8: - spot.tgba_enable_utf8(automaton) + spot.tgba_enable_utf8(degen) # Buchi Automaton Output if output_type == 'a': diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 472d60556..44b2b0966 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -79,6 +79,7 @@ namespace std { #include "tgba/state.hh" #include "tgba/succiter.hh" #include "tgba/tgba.hh" +#include "tgba/sba.hh" #include "tgba/statebdd.hh" #include "tgba/taatgba.hh" #include "tgba/tgbabddcoredata.hh" @@ -90,6 +91,7 @@ namespace std { #include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dotty.hh" +#include "tgbaalgos/degen.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -193,6 +195,7 @@ using namespace spot; %feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba_succ_iterator::current_state; %feature("new") spot::simulation; +%feature("new") spot::degeneralize; %feature("new") spot::tgba_parse; // Help SWIG with namespace lookups. @@ -202,6 +205,7 @@ using namespace spot; %include "tgba/state.hh" %include "tgba/succiter.hh" %include "tgba/tgba.hh" +%include "tgba/sba.hh" %include "tgba/statebdd.hh" %include "tgba/taatgba.hh" %include "tgba/tgbabddcoredata.hh" @@ -235,6 +239,7 @@ using namespace spot; spot::explicit_conf, state_explicit_formula>; +%include "tgbaalgos/degen.hh" %include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dotty.hh" %include "tgbaalgos/dupexp.hh"