diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index d709ccaa1..0cd3c8f23 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -21,6 +21,7 @@ // along with this program. If not, see . #include +#include #include #include #include @@ -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(opt_scc_ ? new scc_info(aut) : nullptr); + std::unique_ptr((opt_scc_ && !aut->is_alternating()) + ? new scc_info(aut) : nullptr); start(); if (si) diff --git a/tests/Makefile.am b/tests/Makefile.am index c4df74f53..cb7715cdb 100644 --- a/tests/Makefile.am +++ b/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 \ diff --git a/tests/core/alternating.test b/tests/core/alternating.test new file mode 100644 index 000000000..49d55afe3 --- /dev/null +++ b/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 . + +. ./defs +set -e + +cat >alt.hoa <alt.dot + +cat >expect.dot < 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