From 56df459c75574d1041bf097c14d77090f5ec6867 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 24 Nov 2016 21:13:13 +0100
Subject: [PATCH] print_hoa: add support for universal branches

* spot/twaalgos/hoa.cc: Implement it.
* tests/python/alternating.py: Test it.
---
 spot/twaalgos/hoa.cc        | 43 ++++++++++++++++++++++++++++---------
 tests/python/alternating.py | 19 ++++++++++++++++
 2 files changed, 52 insertions(+), 10 deletions(-)

diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index 4dc76e3b5..1bd1a332f 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -426,13 +426,21 @@ namespace spot
           }
         os << str;
       };
-    // We do not support alternating automata so far, and it's
-    // probable that nobody cares about the "no-univ-branch"
-    // properties.  The "univ-branch" properties seems more important
-    // to announce that the automaton might not be parsable by tools
-    // that do not support alternating automata.
-    if (verbose)
-      prop(" no-univ-branch");
+    // It's probable that nobody cares about the "no-univ-branch"
+    // property.  The "univ-branch" property seems more important to
+    // announce that the automaton might not be parsable by tools that
+    // do not support alternating automata.
+    if (aut->is_alternating())
+      {
+        prop(" univ-branch");
+      }
+    else if (verbose)
+      {
+        if (v1_1)
+          prop(" !univ-branch");
+        else
+          prop(" no-univ-branch");
+      }
     implicit_labels = md.use_implicit_labels;
     state_labels = md.use_state_labels;
     if (implicit_labels)
@@ -539,6 +547,20 @@ namespace spot
       }
 
     os << "--BODY--" << nl;
+
+    auto print_dst = [&](unsigned dst)
+      {
+        bool notfirst = false;
+        for (unsigned d: aut->univ_dests(dst))
+          {
+            if (notfirst)
+              os << '&';
+            else
+              notfirst = true;
+            os << d;
+          }
+      };
+
     auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
     for (unsigned i = 0; i < num_states; ++i)
       {
@@ -580,7 +602,8 @@ namespace spot
 
             for (auto& t: aut->out(i))
               {
-                os << '[' << md.sup[t.cond] << "] " << t.dst;
+                os << '[' << md.sup[t.cond] << "] ";
+                print_dst(t.dst);
                 if (this_acc == Hoa_Acceptance_Transitions)
                   md.emit_acc(os, t.acc);
                 os << nl;
@@ -591,7 +614,7 @@ namespace spot
             unsigned n = 0;
             for (auto& t: aut->out(i))
               {
-                os << t.dst;
+                print_dst(t.dst);
                 if (this_acc == Hoa_Acceptance_Transitions)
                   {
                     md.emit_acc(os, t.acc);
@@ -637,7 +660,7 @@ namespace spot
             unsigned n = out.size();
             for (unsigned i = 0; i < n;)
               {
-                os << out[i];
+                print_dst(out[i]);
                 if (this_acc != Hoa_Acceptance_States)
                   {
                     md.emit_acc(os, outm[i]) << nl;
diff --git a/tests/python/alternating.py b/tests/python/alternating.py
index 20015e079..2af675c3e 100755
--- a/tests/python/alternating.py
+++ b/tests/python/alternating.py
@@ -50,3 +50,22 @@ try:
 except RuntimeError:
     received = True
 assert received
+
+h = aut.to_str('hoa')
+print(h)
+assert h == """HOA: v1
+States: 3
+Start: 0
+AP: 2 "p1" "p2"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: univ-branch trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 1&2 {0}
+[1] 0&1
+State: 1
+[0&1] 0&2&1
+State: 2
+[0 | 1] 2
+--END--"""