From dfcaed034e37437972f4600bdcebe75dda61dc42 Mon Sep 17 00:00:00 2001
From: Thomas Badie <badie@lrde.epita.fr>
Date: Sun, 15 Apr 2012 13:12:29 +0200
Subject: [PATCH] Add the simulation in the Spot web interface.

* wrap/python/ajax/spot.in: Add the simulation.
* wrap/python/ajax/protocol.txt: Add the direct simulation in the
automaton simplifications section.
* wrap/python/spot.i (simulation_new): Create a function which
takes an automaton and a call to the simulation with the good
template parameter.
* wrap/python/ajax/ltl2tgba.html: Add the direct simulation
checkbox.
---
 wrap/python/ajax/ltl2tgba.html | 5 +++++
 wrap/python/ajax/protocol.txt  | 1 +
 wrap/python/ajax/spot.in       | 7 +++++++
 wrap/python/spot.i             | 4 +++-
 4 files changed, 16 insertions(+), 1 deletion(-)

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: <span class="formula">aUb</span> is an atomic proposition, unlike
 		<INPUT type="checkbox" name="as" value="wd">
 		minimize obligation properties
               </label><br>
+	      <label class="rtip" title="<b>Direct Simulation</b> tries to reduce the automaton with simulation reduction.">
+		<INPUT type="checkbox" name="as" value="rs">
+		direct simulation
+              </label><br>
+
 	    </div>
 	  </div>
 	  <div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
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 {