diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index f3c21d304..81a0c00dc 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -445,6 +445,11 @@ an identifier: aUb is an atomic proposition, unlike
minimize obligation properties
+
+
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 9f536a86d..fd8b74162 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -71,3 +71,4 @@ Automaton simplifications (pick many)
as=ps Prune SCC
as=wd WDBA minimiztion
+ as=rs Simulation reduction
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index dfab26486..692664cd5 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -411,11 +411,14 @@ if output_type == 'm':
# Automaton simplifications
prune_scc = False
wdba_minimize = False
+simul_minimize = False
for s in form.getlist('as'):
if s == 'ps':
prune_scc = True
elif s == 'wd':
wdba_minimize = True
+ elif s == 'rs':
+ simul_minimize = True
if output_type == 'a':
buchi_type = form.getfirst('af', 't')
@@ -447,6 +450,10 @@ if wdba_minimize:
minimized = 0
degen = False # No need to degeneralize anymore
issba = True
+ simul_minimize = False # No need to simulate anymore
+
+if simul_minimize:
+ automaton = spot.simulation(automaton)
if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton)
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 00a5d30b4..64b0ad59f 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -101,6 +101,7 @@
#include "tgbaalgos/save.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/stats.hh"
+#include "tgbaalgos/simulation.hh"
using namespace spot::ltl;
using namespace spot;
@@ -186,7 +187,7 @@ using namespace spot;
%feature("new") spot::tgba::get_init_state;
%feature("new") spot::tgba::succ_iter;
%feature("new") spot::tgba_succ_iterator::current_state;
-
+%feature("new") spot::simulation;
// Help SWIG with namespace lookups.
#define ltl spot::ltl
%include "tgba/bdddict.hh"
@@ -230,6 +231,7 @@ using namespace spot;
%include "tgbaalgos/save.hh"
%include "tgbaalgos/sccfilter.hh"
%include "tgbaalgos/stats.hh"
+%include "tgbaalgos/simulation.hh"
#undef ltl
%extend spot::ltl::formula {