dot: add support for alternating automata

* spot/twaalgos/dot.cc: Handle universal destinations.
Ignore option 's' for alternating automata.
* tests/core/alternating.test: New file.
* tests/Makefile.am: Add it.

spot/twaalgos/dot.cc

@@ -21,6 +21,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <ostream>
+#include <sstream>
 #include <stdexcept>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/dot.hh>
@@ -545,7 +546,7 @@ namespace spot
       void
       process_link(const twa_graph::edge_storage_t& t, int number)
       {
-        os_ << "  " << t.src << " -> " << t.dst;
+        os_ << "  " << t.src << " -> " << (int)t.dst;
         std::string label;
         if (!opt_state_labels_)
           label = bdd_format_formula(aut_->get_dict(), t.cond);
@@ -586,16 +587,38 @@ namespace spot
               os_ << '#' << aut_->get_graph().index_of_edge(t);
             os_ << '"';
           }
+
+        std::string highlight;
         if (highlight_edges_)
           {
             auto idx = aut_->get_graph().index_of_edge(t);
             auto iter = highlight_edges_->find(idx);
             if (iter != highlight_edges_->end())
-              os_ << ", style=bold, color=\""
+              {
+                std::ostringstream o;
+                o << "style=bold, color=\""
                   << palette[iter->second % palette_mod]
                   << '"';
+                highlight = o.str();
+                os_ << ", " << highlight;
               }
+          }
+        // No arrow tip of the common part of a universal transition
+        if ((int)t.dst < 0)
+          os_ << ", dir=none";
         os_ << "]\n";
+        if ((int)t.dst < 0)     // Universal destination
+          {
+            os_ << "    " << (int)t.dst
+                << "[label=<>,width=0,height=0,shape=none]\n";
+            for (unsigned d: aut_->univ_dests(t))
+              {
+                os_ << "    " << (int)t.dst << " -> " << d;
+                if (!highlight.empty())
+                  os_ << " [" << highlight << ']';
+                os_ << '\n';
+              }
+          }
       }
 
       void print(const const_twa_graph_ptr& aut)
@@ -663,7 +686,8 @@ namespace spot
               }
           }
         auto si =
-          std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
+          std::unique_ptr<scc_info>((opt_scc_ && !aut->is_alternating())
+                                    ? new scc_info(aut) : nullptr);
 
         start();
         if (si)

tests/Makefile.am

@@ -202,6 +202,7 @@ TESTS_misc = \
 TESTS_twa = \
   core/acc.test \
   core/acc2.test \
+  core/alternating.test \
   core/ltlcross3.test \
   core/taatgba.test \
   core/renault.test \

tests/core/alternating.test

@@ -0,0 +1,98 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+set -e
+
+cat >alt.hoa <<EOF
+HOA: v1.1
+States: 7
+Start: 0
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+AP: 2 "b" "a"
+properties: trans-labels explicit-labels state-acc univ-branch very-weak
+spot.highlight.edges: 2 5 7 2
+--BODY--
+State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
+ [(0)] 3&1
+ [(!0 & 1)] 5&3&1
+State: 1 "FG(a)" {0}
+ [(1)] 2
+ [t] 1
+State: 2 "G(a)"
+ [(1)] 2
+State: 3 "GF(b)"
+ [(0)] 3
+ [(!0)] 4&3
+State: 4 "F(b)" {0}
+ [(0)] 6
+ [(!0)] 4
+State: 5 "((a) U (b))" {0}
+ [(0)] 6
+ [(!0 & 1)] 5
+State: 6 "t"
+ [t] 6
+--END--
+EOF
+
+# The 's' option should be ignored for alternating automata
+autfilt --dot=bans alt.hoa >alt.dot
+
+cat >expect.dot <<EOF
+digraph G {
+  rankdir=LR
+  label="Fin(⓿)"
+  labelloc="t"
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
+  0 -> -1 [label="b", dir=none]
+    -1[label=<>,width=0,height=0,shape=none]
+    -1 -> 3
+    -1 -> 1
+  0 -> -4 [label="a & !b", style=bold, color="#F15854", dir=none]
+    -4[label=<>,width=0,height=0,shape=none]
+    -4 -> 5 [style=bold, color="#F15854"]
+    -4 -> 3 [style=bold, color="#F15854"]
+    -4 -> 1 [style=bold, color="#F15854"]
+  1 [label="FG(a)\n⓿"]
+  1 -> 2 [label="a"]
+  1 -> 1 [label="1"]
+  2 [label="G(a)"]
+  2 -> 2 [label="a"]
+  3 [label="GF(b)"]
+  3 -> 3 [label="b"]
+  3 -> -8 [label="!b", style=bold, color="#FAA43A", dir=none]
+    -8[label=<>,width=0,height=0,shape=none]
+    -8 -> 4 [style=bold, color="#FAA43A"]
+    -8 -> 3 [style=bold, color="#FAA43A"]
+  4 [label="F(b)\n⓿"]
+  4 -> 6 [label="b"]
+  4 -> 4 [label="!b"]
+  5 [label="((a) U (b))\n⓿"]
+  5 -> 6 [label="b"]
+  5 -> 5 [label="a & !b"]
+  6 [label="t"]
+  6 -> 6 [label="1"]
+}
+EOF
+
+diff expect.dot alt.dot