From abb5170565ab470038c9c34498ebcfbcf97d03e0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 5 Mar 2013 22:02:34 +0100
Subject: [PATCH] cgi: Add an nondeterministic monitor option

* src/tgbaalgos/postproc.hh (run): Rename the first argument as
input_disown to help Swig.
* wrap/python/spot.i: Wrap spot::postprocessor.
* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add an option for nondeterministic monitor.
* wrap/python/ajax/spot.in: Honor the new option, and rewrite the
monitor production using postprocessor.
---
 src/tgbaalgos/postproc.hh      |  8 ++++----
 wrap/python/ajax/ltl2tgba.html |  4 ++++
 wrap/python/ajax/protocol.txt  |  5 +++--
 wrap/python/ajax/spot.in       | 12 +++++++++---
 wrap/python/spot.i             | 10 +++++++++-
 5 files changed, 29 insertions(+), 10 deletions(-)

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: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  <INPUT type="radio" name="mf" value="d" checked>
 		  a deterministic monitor
 		</label><br>
+		<label class="rtip" title="A nondeterministic monitor is an NFA that accepts all the prefixes of the executions that satisfy the formula.">
+		  <INPUT type="radio" name="mf" value="n" checked>
+		  a nondeterministic monitor
+		</label><br>
 	      </div>
 	      <div id="tabs-oa">
 		Translate the (simplified) formula as:<br>
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('<div class="automata-stats">')
     dont_run_dot = print_stats(automaton)
     unbufprint('</div>')
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"