diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index b8a156af3..9d76a7eab 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -568,6 +568,7 @@ an identifier: aUb is an atomic proposition, unlike
Couvreur/LaCIM
Tauriainen/TAA
LTL3BA
+ Comp.Susp.
Fold
@@ -646,6 +647,28 @@ an identifier: aUb is an atomic proposition, unlike
direct simulation on BA
+
+
+
+
+
+
+
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 72d40f990..374ffb283 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -63,6 +63,7 @@ Translator algorithm (pick one)
t=la Couvreur/LaCIM
t=ta Tauriainen/TAA
t=l3 LTL3BA
+ t=cs Compositional Suspension
Couvreur/FM options if t=fm (pick many)
@@ -95,6 +96,14 @@ LTL3BA processing options if t=l3 (pick many)
l3=o on-the-fly simplifications
l3=p a-posteriori simplifications
+Compositional Suspension options (pick many)
+
+ cs=w WDBA minimization
+ cs=s simulation
+ cs=e early start of suspended automatas
+ cs=c do not compose suspended formulae (for debugging)
+ cs=o compose obligation subformulae
+
Automaton simplifications (pick many)
as=ps Prune SCC
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 12fd131a5..2057f9a48 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -91,7 +91,7 @@ if not script:
return True
return False
- server_address=('',8000)
+ server_address=('', 8000)
if not os.access(imgdir, os.F_OK):
# 493 = 0755 but we would have to write 0755 or 0o755
# depending on the python version...
@@ -577,6 +577,23 @@ elif translator == 'l3':
unbufprint('
')
automaton = 0
finish()
+elif translator == 'cs':
+ donot_inject = False
+ cs_nowdba = True
+ cs_nosimul = True
+ cs_early_start = False
+ for cs in form.getlist('cs'):
+ if cs == 'c':
+ donot_inject = True
+ elif cs == 'w':
+ cs_nowdba = False
+ elif cs == 's':
+ cs_nosimul = False
+ elif cs == 'e':
+ cs_early_start = True
+
+ automaton = spot.compsusp(f, dict, cs_nowdba, cs_nosimul,
+ cs_early_start, donot_inject)
# Monitor output
if output_type == 'm':
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index a078f1edf..e91149c6a 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -98,6 +98,7 @@ namespace std {
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
+#include "tgbaalgos/compsusp.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh"
@@ -197,6 +198,7 @@ using namespace spot;
%feature("new") spot::ltl_to_taa;
%feature("new") spot::ltl_to_tgba_fm;
%feature("new") spot::ltl_to_tgba_lacim;
+%feature("new") spot::compsusp;
%feature("new") spot::minimize_wdba;
%feature("new") spot::minimize_monitor;
%feature("new") spot::scc_filter;
@@ -294,6 +296,7 @@ using namespace spot;
%include "tgbaalgos/ltl2taa.hh"
%include "tgbaalgos/ltl2tgba_fm.hh"
%include "tgbaalgos/ltl2tgba_lacim.hh"
+%include "tgbaalgos/compsusp.hh"
%include "tgbaalgos/magic.hh"
%include "tgbaalgos/minimize.hh"
%include "tgbaalgos/neverclaim.hh"