From 74bd671350ae47ee337e351aff18e8ffbd9ebf56 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 21 Aug 2012 16:26:28 +0200
Subject: [PATCH] Add cosimulation and iterated_simulations to the web
 interface.

* wrap/python/spot.i (cosimulation, iterated_simulations): Declare.
* wrap/python/ajax/spot.in, wrap/python/ajax/protocol.txt,
wrap/python/ajax/ltl2tgba.html: Add options to trigger these two
optimizations.
---
 wrap/python/ajax/ltl2tgba.html | 23 ++++++++++++++++++++---
 wrap/python/ajax/protocol.txt  |  2 ++
 wrap/python/ajax/spot.in       | 19 ++++++++++++++++++-
 wrap/python/spot.i             |  2 ++
 4 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index daa2ab783..537c20d58 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -90,6 +90,16 @@
               $("#to-l,#to-s").attr('disabled', true);
             }
         })
+	$("#as-ds,#as-rs").change(function() {
+	    if ($(this).is(':checked')) {
+              $("#as-is").removeAttr('checked');
+            }
+        })
+	$("#as-is").change(function() {
+	    if ($(this).is(':checked')) {
+              $("#as-ds,#as-rs").removeAttr('checked');
+            }
+        })
 
 	function hideOrShowPanels(output, duration) {
 	    switch (output)
@@ -645,11 +655,18 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		<INPUT type="checkbox" name="as" value="wd">
 		determinize and minimize obligation properties
               </label><br>
-	      <label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA.  This might also improve the determinism as a side effect.">
-		<INPUT type="checkbox" name="as" value="ds">
+	      <label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA.  Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>suffixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b>.  This algorithm may also improve determinism as a side effect.">
+		<INPUT id="as-ds" type="checkbox" name="as" value="ds">
 		direct simulation
+              </label>
+	      <label class="rtip" title="Attempt to reduce the automaton by using <b>reverse simulation</b> on the TGBA.  Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>prefixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b> This can also improve codeterminism as a side effect.">
+		<INPUT id="as-rs" type="checkbox" name="as" value="rs">
+		reverse simulation
+              </label>
+	      <label class="rtip" title="Apply <b>direct</b> and <b>reverse simulation</b> alternatively until the automaton is not reduced further.">
+		<INPUT id="as-is" type="checkbox" name="as" value="is">
+		iterated simulations
               </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 7a9227105..41de01640 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -99,6 +99,8 @@ Automaton simplifications (pick many)
   as=ps   Prune SCC
   as=wd   WDBA minimiztion
   as=ds   Direct Simulation reduction
+  as=rs   Reverse Simulation reduction
+  as=is   Iterated Simulation reduction (disables ds and rs)
 
 Testing Automaton options (pick many)
 
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 4473f52f1..db4509d6f 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -579,6 +579,8 @@ if output_type == 'm':
 prune_scc = False
 wdba_minimize = False
 direct_simul = False
+reverse_simul = False
+iterated_simul = False
 for s in form.getlist('as'):
     if s == 'ps':
         prune_scc = True
@@ -586,6 +588,10 @@ for s in form.getlist('as'):
         wdba_minimize = True
     elif s == 'ds':
         direct_simul = True
+    elif s == 'rs':
+        reverse_simul = True
+    elif s == 'is':
+        iterated_simul = True
 
 ta_type = None
 buchi_type = None
@@ -631,9 +637,20 @@ if wdba_minimize:
         issba = True
         direct_simul = False # No need to simulate anymore
 
-if direct_simul:
+if direct_simul and not iterated_simul:
     automaton = spot.simulation(automaton)
     issba = False
+if reverse_simul and not iterated_simul:
+    automaton = spot.cosimulation(automaton)
+    issba = False
+if iterated_simul:
+    automaton = spot.iterated_simulations(automaton)
+    issba = False
+
+if prune_scc and (direct_simul or reverse_simul):
+    # Make a second pass after the simulation, since these might leave
+    # extra acceptance conditions.
+    automaton = spot.scc_filter(automaton, not degen)
 
 if degen or neverclaim:
     degen = spot.degeneralize(automaton)
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 83a9b6cc4..361cc2670 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -206,6 +206,8 @@ using namespace spot;
 %feature("new") spot::tgba::succ_iter;
 %feature("new") spot::tgba_succ_iterator::current_state;
 %feature("new") spot::simulation;
+%feature("new") spot::cosimulation;
+%feature("new") spot::iterated_simulations;
 %feature("new") spot::degeneralize;
 %feature("new") spot::tgba_parse;
 %feature("new") spot::tgba_to_ta;