diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index 3bc6d684f..e7c55e022 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -84,8 +84,8 @@ namespace spot
level_ = level;
}
- /// Return the optimized automaton and delete \a input.
- const tgba* run(const tgba* input, const ltl::formula* f);
+ /// Return the optimized automaton and delete \a input_disown.
+ const tgba* run(const tgba* input_disown, const ltl::formula* f);
private:
output_type type_;
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index d1258d882..b8a156af3 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -504,6 +504,10 @@ an identifier: aUb is an atomic proposition, unlike
a deterministic monitor
+
Translate the (simplified) formula as:
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 41de01640..72d40f990 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -36,9 +36,10 @@ Type of automaton if o=a (pick one)
af=s SBA
af=i Spin neverclaim
-Type of monitor if o=m (pick one -- no choice)
+Type of monitor if o=m (pick one)
- mf=d
+ mf=d deterministic
+ mf=n nondeterministic
Type of automaton for run if o=r (pick one)
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 4cba401b9..ae3bcde4b 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -571,9 +571,15 @@ elif translator == 'l3':
# Monitor output
if output_type == 'm':
- issba = False
- automaton = spot.scc_filter(automaton)
- automaton = spot.minimize_monitor(automaton)
+ issba = True
+ mf = form.getfirst('mf', 'd')
+ pp = spot.postprocessor()
+ pp.set_type(spot.postprocessor.Monitor)
+ if mf == 'd':
+ pp.set_pref(spot.postprocessor.Deterministic)
+ elif mf == 'n':
+ pp.set_pref(spot.postprocessor.Small)
+ automaton = pp.run(automaton, f)
unbufprint('
')
dont_run_dot = print_stats(automaton)
unbufprint('
')
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index c2b9916d0..a078f1edf 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -108,6 +108,7 @@ namespace std {
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
#include "tgbaalgos/simulation.hh"
+#include "tgbaalgos/postproc.hh"
#include "tgbaparse/public.hh"
@@ -211,6 +212,12 @@ using namespace spot;
%feature("new") spot::tgba_parse;
%feature("new") spot::tgba_to_ta;
%feature("new") spot::tgba_to_tgta;
+%feature("new") spot::postprocessor::run;
+
+// The argument to postprocessor::run() will be deleted.
+// Apparently SWIG can only disown arguments based on their
+// names...
+%apply SWIGTYPE *DISOWN { SWIGTYPE * input_disown };
// Help SWIG with namespace lookups.
#define ltl spot::ltl
@@ -297,6 +304,7 @@ using namespace spot;
%include "tgbaalgos/stats.hh"
%include "tgbaalgos/isdet.hh"
%include "tgbaalgos/simulation.hh"
+%include "tgbaalgos/postproc.hh"
%include "tgbaparse/public.hh"