alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl2tgba.html: Use the new degeneralization routine.

Browse source 
* wrap/python/spot.i: Export degeneralize().
* wrap/python/ajax/spot.in: Use it.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-26 18:35:08 +02:00
parent bc5a4ba416
commit 141baae57e
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
wrap/python/ajax/spot.in
View file

@ -616,13 +616,13 @@ if direct_simul:
issba = False issba = False
if degen or neverclaim: if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton) degen = spot.degeneralize(automaton)
issba = True issba = True
else: else:
degen = automaton degen = automaton
if utf8: if utf8:
spot.tgba_enable_utf8(automaton) spot.tgba_enable_utf8(degen)
# Buchi Automaton Output # Buchi Automaton Output
if output_type == 'a': if output_type == 'a':

5
wrap/python/spot.i
View file

@ -79,6 +79,7 @@ namespace std {
#include "tgba/state.hh" #include "tgba/state.hh"
#include "tgba/succiter.hh" #include "tgba/succiter.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgba/sba.hh"
#include "tgba/statebdd.hh" #include "tgba/statebdd.hh"
#include "tgba/taatgba.hh" #include "tgba/taatgba.hh"
#include "tgba/tgbabddcoredata.hh" #include "tgba/tgbabddcoredata.hh"
@ -90,6 +91,7 @@ namespace std {
#include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dottydec.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/degen.hh"
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
@ -193,6 +195,7 @@ using namespace spot;
%feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba::succ_iter;
%feature("new") spot::tgba_succ_iterator::current_state; %feature("new") spot::tgba_succ_iterator::current_state;
%feature("new") spot::simulation; %feature("new") spot::simulation;
%feature("new") spot::degeneralize;
%feature("new") spot::tgba_parse; %feature("new") spot::tgba_parse;
// Help SWIG with namespace lookups. // Help SWIG with namespace lookups.
@ -202,6 +205,7 @@ using namespace spot;
%include "tgba/state.hh" %include "tgba/state.hh"
%include "tgba/succiter.hh" %include "tgba/succiter.hh"
%include "tgba/tgba.hh" %include "tgba/tgba.hh"
%include "tgba/sba.hh"
%include "tgba/statebdd.hh" %include "tgba/statebdd.hh"
%include "tgba/taatgba.hh" %include "tgba/taatgba.hh"
%include "tgba/tgbabddcoredata.hh" %include "tgba/tgbabddcoredata.hh"
@ -235,6 +239,7 @@ using namespace spot;
spot::explicit_conf<tgba_explicit<state_explicit_formula>, spot::explicit_conf<tgba_explicit<state_explicit_formula>,
state_explicit_formula>; state_explicit_formula>;
%include "tgbaalgos/degen.hh"
%include "tgbaalgos/dottydec.hh" %include "tgbaalgos/dottydec.hh"
%include "tgbaalgos/dotty.hh" %include "tgbaalgos/dotty.hh"
%include "tgbaalgos/dupexp.hh" %include "tgbaalgos/dupexp.hh"