dot: add option to number transitions
* src/tgbaalgos/dotty.cc: Add option 'o'. * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it. * src/taalgos/dotty.cc: Ignore this option. * src/tgbatest/readsave.test: Test it.
This commit is contained in:
parent
dfd080e005
commit
ecfd9b7776
5 changed files with 51 additions and 40 deletions
|
|
@ -56,8 +56,9 @@ static const argp_option options[] =
|
||||||
"(a) acceptance display, (b) acceptance sets as bullets,"
|
"(a) acceptance display, (b) acceptance sets as bullets,"
|
||||||
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
|
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
|
||||||
"(v) vertical layout, (n) with name, (N) without name, "
|
"(v) vertical layout, (n) with name, (N) without name, "
|
||||||
"(r) rainbow colors for acceptance set, "
|
"(o) ordered transitions, "
|
||||||
"(R) color acceptance set by Inf/Fin, (s) with SCCs, "
|
"(r) rainbow colors for acceptance sets, "
|
||||||
|
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
|
||||||
"(t) force transition-based acceptance.", 0 },
|
"(t) force transition-based acceptance.", 0 },
|
||||||
{ "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL,
|
{ "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL,
|
||||||
"Output the automaton in HOA format. Add letters to select "
|
"Output the automaton in HOA format. Add letters to select "
|
||||||
|
|
|
||||||
|
|
@ -78,8 +78,9 @@ static const argp_option options[] =
|
||||||
"(a) acceptance display, (b) acceptance sets as bullets,"
|
"(a) acceptance display, (b) acceptance sets as bullets,"
|
||||||
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
|
"(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, "
|
||||||
"(v) vertical layout, (n) with name, (N) without name, "
|
"(v) vertical layout, (n) with name, (N) without name, "
|
||||||
"(r) rainbow colors for acceptance set, "
|
"(o) ordered transitions, "
|
||||||
"(R) color acceptance set by Inf/Fin, (s) with SCCs, "
|
"(r) rainbow colors for acceptance sets, "
|
||||||
|
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
|
||||||
"(t) force transition-based acceptance.", 0 },
|
"(t) force transition-based acceptance.", 0 },
|
||||||
{ "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL,
|
{ "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL,
|
||||||
"Output the automaton in HOA format. Add letters to select "
|
"Output the automaton in HOA format. Add letters to select "
|
||||||
|
|
|
||||||
|
|
@ -88,6 +88,7 @@ namespace spot
|
||||||
case 'b':
|
case 'b':
|
||||||
case 'n':
|
case 'n':
|
||||||
case 'N':
|
case 'N':
|
||||||
|
case 'o':
|
||||||
case 'r':
|
case 'r':
|
||||||
case 'R':
|
case 'R':
|
||||||
case 's':
|
case 's':
|
||||||
|
|
|
||||||
|
|
@ -60,6 +60,7 @@ namespace spot
|
||||||
bool opt_rainbow = false;
|
bool opt_rainbow = false;
|
||||||
bool opt_bullet = false;
|
bool opt_bullet = false;
|
||||||
bool opt_all_bullets = false;
|
bool opt_all_bullets = false;
|
||||||
|
bool opt_numbered_trans = false;
|
||||||
std::string opt_font_;
|
std::string opt_font_;
|
||||||
|
|
||||||
const char* const palette9[9] =
|
const char* const palette9[9] =
|
||||||
|
|
@ -137,6 +138,9 @@ namespace spot
|
||||||
case 'N':
|
case 'N':
|
||||||
opt_name_ = false;
|
opt_name_ = false;
|
||||||
break;
|
break;
|
||||||
|
case 'o':
|
||||||
|
opt_numbered_trans = true;
|
||||||
|
break;
|
||||||
case 'r':
|
case 'r':
|
||||||
opt_html_labels_ = true;
|
opt_html_labels_ = true;
|
||||||
opt_rainbow = true;
|
opt_rainbow = true;
|
||||||
|
|
@ -396,7 +400,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(const tgba_digraph::trans_storage_t& t)
|
process_link(const tgba_digraph::trans_storage_t& t, int number)
|
||||||
{
|
{
|
||||||
std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
|
std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
|
||||||
os_ << " " << t.src << " -> " << t.dst;
|
os_ << " " << t.src << " -> " << t.dst;
|
||||||
|
|
@ -410,7 +414,7 @@ namespace spot
|
||||||
os_ << "\\n";
|
os_ << "\\n";
|
||||||
output_set(a);
|
output_set(a);
|
||||||
}
|
}
|
||||||
os_ << "\"]\n";
|
os_ << '"';
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -422,8 +426,11 @@ namespace spot
|
||||||
os_ << "<br/>";
|
os_ << "<br/>";
|
||||||
output_html_set(a);
|
output_html_set(a);
|
||||||
}
|
}
|
||||||
os_ << ">]\n";
|
os_ << '>';
|
||||||
}
|
}
|
||||||
|
if (opt_numbered_trans)
|
||||||
|
os_ << ",taillabel=\"" << number << '"';
|
||||||
|
os_ << "]\n";
|
||||||
}
|
}
|
||||||
|
|
||||||
void print(const const_tgba_digraph_ptr& aut)
|
void print(const const_tgba_digraph_ptr& aut)
|
||||||
|
|
@ -471,8 +478,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (!si || !si->reachable_state(n))
|
if (!si || !si->reachable_state(n))
|
||||||
process_state(n);
|
process_state(n);
|
||||||
|
int trans_num = 0;
|
||||||
for (auto& t: aut_->out(n))
|
for (auto& t: aut_->out(n))
|
||||||
process_link(t);
|
process_link(t, trans_num++);
|
||||||
}
|
}
|
||||||
end();
|
end();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -464,48 +464,48 @@ digraph G {
|
||||||
I [label="", style=invis, width=0]
|
I [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label="0"]
|
||||||
0 -> 1 [label="!a & !b"]
|
0 -> 1 [label="!a & !b",taillabel="0"]
|
||||||
0 -> 2 [label="a & !b"]
|
0 -> 2 [label="a & !b",taillabel="1"]
|
||||||
0 -> 3 [label="!a & b"]
|
0 -> 3 [label="!a & b",taillabel="2"]
|
||||||
0 -> 4 [label="a & b"]
|
0 -> 4 [label="a & b",taillabel="3"]
|
||||||
1 [label="test me\n⓿❸"]
|
1 [label="test me\n⓿❸"]
|
||||||
1 -> 1 [label="!a & !b"]
|
1 -> 1 [label="!a & !b",taillabel="0"]
|
||||||
1 -> 2 [label="a & !b"]
|
1 -> 2 [label="a & !b",taillabel="1"]
|
||||||
1 -> 6 [label="!a & b"]
|
1 -> 6 [label="!a & b",taillabel="2"]
|
||||||
1 -> 7 [label="a & b"]
|
1 -> 7 [label="a & b",taillabel="3"]
|
||||||
2 [label="2\n⓿❷❸"]
|
2 [label="2\n⓿❷❸"]
|
||||||
2 -> 1 [label="!a & !b"]
|
2 -> 1 [label="!a & !b",taillabel="0"]
|
||||||
2 -> 2 [label="a & !b"]
|
2 -> 2 [label="a & !b",taillabel="1"]
|
||||||
2 -> 6 [label="!a & b"]
|
2 -> 6 [label="!a & b",taillabel="2"]
|
||||||
2 -> 7 [label="a & b"]
|
2 -> 7 [label="a & b",taillabel="3"]
|
||||||
3 [label="3\n❸"]
|
3 [label="3\n❸"]
|
||||||
3 -> 5 [label="1"]
|
3 -> 5 [label="1",taillabel="0"]
|
||||||
4 [label="hihi\n❷❸"]
|
4 [label="hihi\n❷❸"]
|
||||||
4 -> 5 [label="1"]
|
4 -> 5 [label="1",taillabel="0"]
|
||||||
5 [label="5\n❶❸"]
|
5 [label="5\n❶❸"]
|
||||||
5 -> 5 [label="1"]
|
5 -> 5 [label="1",taillabel="0"]
|
||||||
6 [label="6\n⓿"]
|
6 [label="6\n⓿"]
|
||||||
6 -> 8 [label="!a & !b"]
|
6 -> 8 [label="!a & !b",taillabel="0"]
|
||||||
6 -> 6 [label="!a & b"]
|
6 -> 6 [label="!a & b",taillabel="1"]
|
||||||
6 -> 9 [label="a & !b"]
|
6 -> 9 [label="a & !b",taillabel="2"]
|
||||||
6 -> 7 [label="a & b"]
|
6 -> 7 [label="a & b",taillabel="3"]
|
||||||
7 [label="7\n⓿❷"]
|
7 [label="7\n⓿❷"]
|
||||||
7 -> 8 [label="!a & !b"]
|
7 -> 8 [label="!a & !b",taillabel="0"]
|
||||||
7 -> 6 [label="!a & b"]
|
7 -> 6 [label="!a & b",taillabel="1"]
|
||||||
7 -> 9 [label="a & !b"]
|
7 -> 9 [label="a & !b",taillabel="2"]
|
||||||
7 -> 7 [label="a & b"]
|
7 -> 7 [label="a & b",taillabel="3"]
|
||||||
8 [label="8\n⓿❸"]
|
8 [label="8\n⓿❸"]
|
||||||
8 -> 8 [label="!a & !b"]
|
8 -> 8 [label="!a & !b",taillabel="0"]
|
||||||
8 -> 6 [label="!a & b"]
|
8 -> 6 [label="!a & b",taillabel="1"]
|
||||||
8 -> 9 [label="a & !b"]
|
8 -> 9 [label="a & !b",taillabel="2"]
|
||||||
8 -> 7 [label="a & b"]
|
8 -> 7 [label="a & b",taillabel="3"]
|
||||||
9 [label="9\n⓿❷❸"]
|
9 [label="9\n⓿❷❸"]
|
||||||
9 -> 8 [label="!a & !b"]
|
9 -> 8 [label="!a & !b",taillabel="0"]
|
||||||
9 -> 6 [label="!a & b"]
|
9 -> 6 [label="!a & b",taillabel="1"]
|
||||||
9 -> 9 [label="a & !b"]
|
9 -> 9 [label="a & !b",taillabel="2"]
|
||||||
9 -> 7 [label="a & b"]
|
9 -> 7 [label="a & b",taillabel="3"]
|
||||||
}
|
}
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
$autfilt --dot=ba in >out
|
$autfilt --dot=bao in >out
|
||||||
diff out expected
|
diff out expected
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue