diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 27eb82af8..faf1a5552 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -187,6 +187,22 @@ namespace spot } } + void + output_set(acc_cond::mark_t a) const + { + if (!opt_all_bullets) + os_ << '{'; + const char* space = ""; + for (auto v: a.sets()) + { + if (!opt_all_bullets) + os_ << space; + output_set(os_, v); + space = ","; + } + if (!opt_all_bullets) + os_ << '}'; + } const char* html_set_color(int v) const @@ -221,6 +237,23 @@ namespace spot output_html_set_aux(os_, v); } + void + output_html_set(acc_cond::mark_t a) const + { + if (!opt_all_bullets) + os_ << '{'; + const char* space = ""; + for (auto v: a.sets()) + { + if (!opt_all_bullets) + os_ << space; + output_html_set(v); + space = ","; + } + if (!opt_all_bullets) + os_ << '}'; + } + void start() { @@ -305,15 +338,61 @@ namespace spot void process_state(unsigned s) { - os_ << " " << s << " [label=\""; - if (sn_ && s < sn_->size() && !(*sn_)[s].empty()) - os_ << escape_str((*sn_)[s]); + if (mark_states_ && (opt_bullet || aut_->acc().num_sets() != 1)) + { + acc_cond::mark_t acc = 0U; + for (auto& t: aut_->out(s)) + { + acc = t.acc; + break; + } + + bool has_name = sn_ && s < sn_->size() && !(*sn_)[s].empty(); + + os_ << " " << s << " [label="; + if (!opt_html_labels_) + { + os_ << '"'; + if (has_name) + escape_str(os_, (*sn_)[s]); + else + os_ << s; + if (acc) + { + os_ << "\\n"; + output_set(acc); + } + os_ << '"'; + } + else + { + os_ << '<'; + if (has_name) + escape_html(os_, (*sn_)[s]); + else + os_ << s; + if (acc) + { + os_ << "
"; + output_html_set(acc); + } + os_ << '>'; + } + os_ << "]\n"; + + } else - os_ << s; - os_ << '"'; - if (mark_states_ && aut_->state_is_accepting(s)) - os_ << ", peripheries=2"; - os_ << "]\n"; + { + os_ << " " << s << " [label=\""; + if (sn_ && s < sn_->size() && !(*sn_)[s].empty()) + escape_str(os_, (*sn_)[s]); + else + os_ << s; + os_ << '"'; + if (mark_states_ && aut_->state_is_accepting(s)) + os_ << ", peripheries=2"; + os_ << "]\n"; + } } void @@ -329,18 +408,7 @@ namespace spot if (auto a = t.acc) { os_ << "\\n"; - if (!opt_all_bullets) - os_ << '{'; - const char* space = ""; - for (auto v: a.sets()) - { - if (!opt_all_bullets) - os_ << space; - output_set(os_, v); - space = ","; - } - if (!opt_all_bullets) - os_ << '}'; + output_set(a); } os_ << "\"]\n"; } @@ -352,18 +420,7 @@ namespace spot if (auto a = t.acc) { os_ << "
"; - if (!opt_all_bullets) - os_ << '{'; - const char* space = ""; - for (auto v: a.sets()) - { - if (!opt_all_bullets) - os_ << space; - output_html_set(v); - space = ","; - } - if (!opt_all_bullets) - os_ << '}'; + output_html_set(a); } os_ << ">]\n"; } @@ -375,7 +432,7 @@ namespace spot sn_ = aut->get_named_prop>("state-names"); if (opt_name_) name_ = aut_->get_named_prop("automaton-name"); - mark_states_ = !opt_force_acc_trans_ && aut_->is_sba(); + mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc(); auto si = std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); start(); diff --git a/src/tgbaalgos/sbacc.cc b/src/tgbaalgos/sbacc.cc index b37c4a10d..a6038ba7b 100644 --- a/src/tgbaalgos/sbacc.cc +++ b/src/tgbaalgos/sbacc.cc @@ -32,6 +32,8 @@ namespace spot auto res = make_tgba_digraph(old->get_dict()); res->copy_ap_of(old); res->copy_acceptance_of(old); + res->prop_copy(old, {false, true, true, true}); + res->prop_state_based_acc(); typedef std::pair pair_t; std::map s2n; diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 76be7bc02..63479c277 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -403,3 +403,109 @@ digraph G { } EOF diff output expected + + +cat >in <expected < 0 + 0 [label="0"] + 0 -> 1 [label="!a & !b"] + 0 -> 2 [label="a & !b"] + 0 -> 3 [label="!a & b"] + 0 -> 4 [label="a & b"] + 1 [label="test me\n⓿❸"] + 1 -> 1 [label="!a & !b"] + 1 -> 2 [label="a & !b"] + 1 -> 6 [label="!a & b"] + 1 -> 7 [label="a & b"] + 2 [label="2\n⓿❷❸"] + 2 -> 1 [label="!a & !b"] + 2 -> 2 [label="a & !b"] + 2 -> 6 [label="!a & b"] + 2 -> 7 [label="a & b"] + 3 [label="3\n❸"] + 3 -> 5 [label="1"] + 4 [label="hihi\n❷❸"] + 4 -> 5 [label="1"] + 5 [label="5\n❶❸"] + 5 -> 5 [label="1"] + 6 [label="6\n⓿"] + 6 -> 8 [label="!a & !b"] + 6 -> 6 [label="!a & b"] + 6 -> 9 [label="a & !b"] + 6 -> 7 [label="a & b"] + 7 [label="7\n⓿❷"] + 7 -> 8 [label="!a & !b"] + 7 -> 6 [label="!a & b"] + 7 -> 9 [label="a & !b"] + 7 -> 7 [label="a & b"] + 8 [label="8\n⓿❸"] + 8 -> 8 [label="!a & !b"] + 8 -> 6 [label="!a & b"] + 8 -> 9 [label="a & !b"] + 8 -> 7 [label="a & b"] + 9 [label="9\n⓿❷❸"] + 9 -> 8 [label="!a & !b"] + 9 -> 6 [label="!a & b"] + 9 -> 9 [label="a & !b"] + 9 -> 7 [label="a & b"] +} +EOF + +$autfilt --dot=ba in >out +diff out expected