From 58b088128d49e2712e5b6af011962dc88c2f3dc1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 20 Jan 2015 11:35:34 +0100 Subject: [PATCH] dot: output marked states only for SBA * src/tgbaalgos/dotty.cc: Do not output marked states if an automaton has 0 acceptance set (like a monitor). * src/tgbatest/monitor.test, src/tgbatest/dstar.test: Adjust. --- src/tgbaalgos/dotty.cc | 3 +-- src/tgbatest/dstar.test | 6 +++--- src/tgbatest/monitor.test | 4 ++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 5341411a4..ae38516c4 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -132,8 +132,7 @@ namespace spot void print(const const_tgba_digraph_ptr& aut) { aut_ = aut; - mark_states_ = !opt_force_acc_trans_ && - (aut_->has_state_based_acc() || aut_->acc().num_sets() == 0); + mark_states_ = !opt_force_acc_trans_ && aut_->is_sba(); auto si = std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); start(); diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index 5aee1a7c4..2695fcc68 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -63,13 +63,13 @@ digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 0 - 0 [label="0", peripheries=2] + 0 [label="0"] 0 -> 0 [label="a & !b"] 0 -> 1 [label="!a & !b"] 0 -> 2 [label="b"] - 1 [label="1", peripheries=2] + 1 [label="1"] 1 -> 1 [label="1"] - 2 [label="2", peripheries=2] + 2 [label="2"] 2 -> 2 [label="1"] } EOF diff --git a/src/tgbatest/monitor.test b/src/tgbatest/monitor.test index 696d8e1c2..b9afbdd95 100755 --- a/src/tgbatest/monitor.test +++ b/src/tgbatest/monitor.test @@ -36,9 +36,9 @@ digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 1 - 0 [label="0", peripheries=2] + 0 [label="0"] 0 -> 0 [label="1"] - 1 [label="1", peripheries=2] + 1 [label="1"] 1 -> 0 [label="a"] } EOF