From f29de22b8a1b0ccb56e9e5d17121cee97bfe5633 Mon Sep 17 00:00:00 2001
From: Alexandre Lewkowicz <lewkow_a@epita.fr>
Date: Sat, 6 Jun 2015 18:41:59 +0200
Subject: [PATCH] safra: Add bisimulation option

* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh: Here.
---
 src/tests/safra.cc    |  7 +++++--
 src/twaalgos/safra.cc | 10 +++++++---
 src/twaalgos/safra.hh |  1 +
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/tests/safra.cc b/src/tests/safra.cc
index 0e13ab9c2..811324718 100644
--- a/src/tests/safra.cc
+++ b/src/tests/safra.cc
@@ -42,6 +42,7 @@ int help()
 
 int main(int argc, char* argv[])
 {
+  bool sim = false;
   bool in_hoa = false;
   bool in_ltl = false;
   bool out_dot = true;
@@ -74,6 +75,8 @@ int main(int argc, char* argv[])
         }
       else if (!strncmp(argv[i], "-p", 2))
         pretty_print = true;
+      else if (!strncmp(argv[i], "-b", 2))
+        sim = true;
     }
 
   if (!input)
@@ -92,7 +95,7 @@ int main(int argc, char* argv[])
       spot::translator trans(dict);
       trans.set_pref(spot::postprocessor::Deterministic);
       auto tmp = trans.run(f);
-      res = spot::tgba_determinisation(tmp, pretty_print);
+      res = spot::tgba_determinisation(tmp, sim, pretty_print);
       f->destroy();
     }
   else if (in_hoa)
@@ -101,7 +104,7 @@ int main(int argc, char* argv[])
       auto aut = spot::hoa_parse(input, pel, dict);
       if (spot::format_hoa_parse_errors(std::cerr, input, pel))
         return 2;
-      res = tgba_determinisation(aut->aut, pretty_print);
+      res = tgba_determinisation(aut->aut, sim, pretty_print);
     }
   res->merge_transitions();
 
diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index c1eafbbbd..1c76340a3 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -24,6 +24,7 @@
 
 #include "safra.hh"
 #include "twaalgos/degen.hh"
+#include "twaalgos/simulation.hh"
 
 namespace spot
 {
@@ -60,7 +61,7 @@ namespace spot
                std::ostringstream& os, std::vector<unsigned>& idx)
     {
       std::string s = subscript(start);
-      os << '[' << s;
+      os << '{' << s;
       std::vector<unsigned> new_idx;
       std::vector<unsigned> todo;
       unsigned next = -1U;
@@ -117,7 +118,7 @@ namespace spot
               todo_next.clear();
             }
         }
-      os << s << ']';
+      os << s << '}';
     }
 
     // Returns true if lhs has a smaller nesting pattern than rhs
@@ -367,7 +368,8 @@ namespace spot
   }
 
   twa_graph_ptr
-  tgba_determinisation(const const_twa_graph_ptr& a, bool pretty_print)
+  tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
+                       bool pretty_print)
   {
     // Degeneralize
     const_twa_graph_ptr aut;
@@ -473,6 +475,8 @@ namespace spot
     res->set_acceptance(sets, acc_cond::acc_code::parity(false, false, sets));
     res->prop_deterministic(true);
     res->prop_state_based_acc(false);
+    if (bisimulation)
+      res = simulation(res);
     if (pretty_print)
       res->set_named_prop("state-names", print_debug(seen));
     return res;
diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh
index c13f35275..3b6b02359 100644
--- a/src/twaalgos/safra.hh
+++ b/src/twaalgos/safra.hh
@@ -73,5 +73,6 @@ namespace spot
 
   SPOT_API twa_graph_ptr
   tgba_determinisation(const const_twa_graph_ptr& aut,
+                       bool bisimulation = false,
                        bool pretty_print = false);
 }