safra: Add pretty printer for states

* src/tests/safra.cc, src/tests/safra.test: Add options and test.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

src/tests/safra.cc

@@ -30,14 +30,58 @@
 #include "twaalgos/degen.hh"
 
 
+int help()
+{
+  std::cerr << "safra [OPTIONS]\n";
+  std::cerr << "\t-f ltl_formula\tinput string is an ltl formulae\n";
+  std::cerr << "\t--hoa file.hoa\tinput file has hoa format\n";
+  std::cerr << "\t-p\tpretty print states\n";
+  std::cerr << "\t-H\toutput hoa format\n";
+  return 1;
+}
+
 int main(int argc, char* argv[])
 {
+  bool in_hoa = false;
+  bool in_ltl = false;
+  bool out_dot = true;
+  bool out_hoa = false;
+  bool pretty_print = false;
+
+  char* input = nullptr;
   if (argc <= 2)
-    return 1;
-  char* input = argv[2];
+    return help();
+  for (int i = 1; i < argc; ++i)
+    {
+      if (!strncmp(argv[i], "--hoa", 5))
+        {
+          in_hoa = true;
+          if (i + 1 >= argc)
+            return help();
+          input = argv[++i];
+        }
+      else if (!strncmp(argv[i], "-f", 2))
+        {
+          in_ltl = true;
+          if (i + 1 >= argc)
+            return help();
+          input = argv[++i];
+        }
+      else if (!strncmp(argv[i], "-H", 2))
+        {
+          out_dot = false;
+          out_hoa = true;
+        }
+      else if (!strncmp(argv[i], "-p", 2))
+        pretty_print = true;
+    }
+
+  if (!input)
+    help();
+
   auto dict = spot::make_bdd_dict();
   spot::twa_graph_ptr res;
-  if (!strncmp(argv[1], "-f", 2))
+  if (in_ltl)
     {
       spot::ltl::parse_error_list pel;
       const spot::ltl::formula* f =
@@ -48,24 +92,26 @@ 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);
+      res = spot::tgba_determinisation(tmp, pretty_print);
       f->destroy();
     }
-  else if (!strncmp(argv[1], "--hoa", 5))
+  else if (in_hoa)
     {
       spot::hoa_parse_error_list pel;
       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);
+      res = tgba_determinisation(aut->aut, pretty_print);
     }
   res->merge_transitions();
 
-  if (argc >= 4 && !strncmp(argv[3], "-H", 2))
+  if (out_hoa)
     {
       spot::hoa_reachable(std::cout, res, "t");
       std::cout << std::endl;
     }
-  else
+  else if (out_dot)
     spot::dotty_reachable(std::cout, res);
+  else
+    assert(false);
 }

src/tests/safra.test

@@ -119,3 +119,24 @@ EOF
 
 run 0 ../safra --hoa double_b.hoa -H > out.hoa
 diff out.hoa out.exp
+
+# Formulas from bench/dtgbasat/formulas
+cat >formulae <<EOF
+X((a M F((!c & !b) | (c & b))) W (G!c U b))
+X(((a & b) R (!a U !c)) R b)
+XXG(Fa U Xb)
+(!a M !b) W F!c
+(b & Fa & GFc) R a
+(a R (b W a)) W G(!a M (c | b))
+(Fa W b) R (Fc | !a)
+X(G(!a M !b) | G(a | G!a))
+Fa W Gb
+Ga | GFb
+a M G(F!b | X!a)
+G!a R XFb
+EOF
+run 0 ../safra --hoa double_b.hoa -H > out.hoa
+ltl2tgba=../../bin/ltl2tgba
+../../bin/ltlcross -F formulae \
+    "../safra -f %f -H > %O" \
+    "$ltl2tgba -f %f -H > %O"

src/twaalgos/safra.cc

@@ -17,6 +17,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include <algorithm>
 #include <deque>
 #include <utility>
 #include <unordered_map>
@@ -28,6 +29,97 @@ namespace spot
 {
   namespace
   {
+    using power_set = std::map<safra_state, int>;
+    const char* const sub[10] =
+    {
+      "\u2080",
+      "\u2081",
+      "\u2082",
+      "\u2083",
+      "\u2084",
+      "\u2085",
+      "\u2086",
+      "\u2087",
+      "\u2088",
+      "\u2089",
+    };
+
+    std::string subscript(unsigned start)
+    {
+      std::string res;
+      do
+        {
+          res = sub[start % 10] + res;
+          start /= 10;
+        }
+      while (start);
+      return res;
+    }
+
+    void print(unsigned start, const safra_state::nodes_t& nodes,
+               std::ostringstream& os, std::vector<unsigned>& idx)
+    {
+      std::string s = subscript(start);
+      os << '[' << s;
+      std::vector<unsigned> new_idx;
+      std::vector<unsigned> todo;
+      unsigned next = -1U;
+      bool first = true;
+      for (auto& i: idx)
+        {
+          auto it = std::lower_bound(nodes.at(i).cbegin(), nodes.at(i).cend(),
+                                     start + 1);
+          if (it == nodes.at(i).cend())
+            {
+              if (first)
+                {
+                  os << i;
+                  first = false;
+                }
+              else
+                os << ' ' << i;
+            }
+          else if (*it == (start + 1))
+            new_idx.push_back(i);
+          else
+            {
+              todo.push_back(i);
+              next = std::min(next, *it);
+            }
+        }
+      if (!new_idx.empty())
+        print(start + 1, nodes, os, new_idx);
+      if (next != -1U)
+        {
+          std::vector<unsigned> todo2;
+          std::vector<unsigned> todo_next;
+          unsigned new_next = -1U;
+          while (!todo.empty())
+            {
+              for (auto& i: todo)
+                {
+                  auto it = std::lower_bound(nodes.at(i).cbegin(),
+                                             nodes.at(i).cend(), next);
+                  if (*it == next)
+                    todo_next.push_back(i);
+                  else
+                    {
+                      todo2.push_back(i);
+                      next = std::min(new_next, *it);
+                    }
+                }
+              print(next, nodes, os, todo_next);
+
+              next = new_next;
+              new_next = -1;
+              todo = todo2;
+              todo2.clear();
+              todo_next.clear();
+            }
+        }
+      os << s << ']';
+    }
+
     // Returns true if lhs has a smaller nesting pattern than rhs
     // If lhs and rhs are the same, return false.
     bool nesting_cmp(const std::vector<node_helper::brace_t>& lhs,
@@ -53,6 +145,25 @@ namespace spot
           t.acc &= mask;
         }
     }
+
+    std::vector<std::string>*
+    print_debug(std::map<safra_state, int>& states)
+    {
+      std::vector<std::string>* res = nullptr;
+      res = new std::vector<std::string>(states.size());
+      std::vector<unsigned> idx;
+      for (auto& p: states)
+        {
+          std::ostringstream os;
+          for (auto& n: p.first.nodes_)
+            idx.push_back(n.first);
+          print(0, p.first.nodes_, os, idx);
+          (*res)[p.second] = os.str();
+          idx.clear();
+        }
+      return res;
+    }
+
   }
   auto
   safra_state::compute_succs(const const_twa_graph_ptr& aut,
@@ -255,23 +366,8 @@ namespace spot
     return nodes_ < other.nodes_;
   }
 
-  void safra_state::print_debug(unsigned state_id) const
-  {
-    std::cerr << "State: " << state_id << "{ ";
-    for (auto& n: nodes_)
-      {
-        std::cerr << n.first << " [";
-        for (auto& b: n.second)
-          {
-            std::cerr << b << ' ';
-          }
-        std::cerr << "], ";
-      }
-    std::cerr << "}\n";
-  }
-
   twa_graph_ptr
-  tgba_determinisation(const const_twa_graph_ptr& a)
+  tgba_determinisation(const const_twa_graph_ptr& a, bool pretty_print)
   {
     // Degeneralize
     const_twa_graph_ptr aut;
@@ -331,7 +427,6 @@ namespace spot
 
     // Given a safra_state get its associated state in output automata.
     // Required to create new transitions from 2 safra-state
-    typedef std::map<safra_state, int> power_set;
     power_set seen;
     safra_state init(aut->get_init_state_number(), true);
     unsigned num = res->new_state();
@@ -374,11 +469,12 @@ namespace spot
               res->new_transition(src_num, dst_num, num2bdd[s.second]);
           }
       }
-    //
     remove_dead_acc(res, sets);
     res->set_acceptance(sets, acc_cond::acc_code::parity(false, false, sets));
     res->prop_deterministic(true);
     res->prop_state_based_acc(false);
+    if (pretty_print)
+      res->set_named_prop("state-names", print_debug(seen));
     return res;
   }
 }

src/twaalgos/safra.hh

@@ -40,10 +40,9 @@ namespace spot
   class safra_state
   {
   public:
-    typedef std::vector<std::pair<safra_state, unsigned>> succs_t;
+    using nodes_t = std::map<unsigned, std::vector<node_helper::brace_t>>;
+    using succs_t =  std::vector<std::pair<safra_state, unsigned>>;
     bool operator<(const safra_state& other) const;
-    // Print each sub-state with their associated braces of a safra state
-    void print_debug(unsigned state_id) const;
     // Printh the number of states in each brace
     safra_state(unsigned state_number, bool init_state = false);
     // Given a certain transition_label, compute all the successors of that
@@ -63,7 +62,7 @@ namespace spot
     // A list of nodes similar to the ones of a
     // safra tree.  These are constructed in the same way as the powerset
     // algorithm.
-    std::map<unsigned, std::vector<node_helper::brace_t>> nodes_;
+    nodes_t nodes_;
     // A counter that indicates the nomber of states within a brace.
     // This enables us to compute the red value
     std::vector<size_t> nb_braces_;
@@ -73,5 +72,6 @@ namespace spot
   };
 
   SPOT_API twa_graph_ptr
-  tgba_determinisation(const const_twa_graph_ptr& aut);
+  tgba_determinisation(const const_twa_graph_ptr& aut,
+                       bool pretty_print = false);
 }