Commit ead2ca01 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

dot: better support of state-based acceptance

* src/tgbaalgos/dotty.cc: Here.
* src/tgbaalgos/sbacc.cc: Make the produced automata as state-based.
* src/tgbatest/readsave.test: Add a test.
parent fb7b7a94
......@@ -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_ << "<br/>";
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_ << "<br/>";
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<std::vector<std::string>>("state-names");
if (opt_name_)
name_ = aut_->get_named_prop<std::string>("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<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
start();
......
......@@ -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<unsigned, acc_cond::mark_t> pair_t;
std::map<pair_t, unsigned> s2n;
......
......@@ -403,3 +403,109 @@ digraph G {
}
EOF
diff output expected
cat >in <<EOF
HOA: v1
States: 10
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Fin(0) | (Fin(1) & Inf(2)) | Fin(3)
--BODY--
State: 0
[!0&!1] 1
[0&!1] 2
[!0&1] 3
[0&1] 4
State: 1 "test me" {0 3}
[!0&!1] 1
[0&!1] 2
[!0&1] 6
[0&1] 7
State: 2 {0 2 3}
[!0&!1] 1
[0&!1] 2
[!0&1] 6
[0&1] 7
State: 3 {3}
[t] 5
State: 4 "hihi" {2 3}
[t] 5
State: 5 {1 3}
[t] 5
State: 6 {0}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 7 {0 2}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 8 {0 3}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 9 {0 2 3}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
--END--
EOF
cat >expected <<EOF
digraph G {
rankdir=LR
label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
labelloc="t"
I [label="", style=invis, width=0]
I -> 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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment