diff --git a/NEWS b/NEWS
index b1dbd61e8..44b18925d 100644
--- a/NEWS
+++ b/NEWS
@@ -159,6 +159,9 @@ New in spot 2.9.8.dev (not yet released)
- print_dot() will display states from player 1 using a diamond
shape.
+ - print_dot() learned to display automata that correspond to Mealy
+ machines specifically.
+
- print_dot() has a new option "i" to define id=... attributes for
states (S followed by the state number), edges (E followed by the
edge number), and SCCs (SCC followed by SCC number). The option
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 5eed4f65c..103ab89d1 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -126,6 +126,8 @@ namespace spot
unsigned max_states_ = -1U; // related to max_states_given_
bool opt_shared_univ_dest_ = true;
+ bool opt_mealy_ = false;
+ bdd opt_mealy_output_;
public:
@@ -456,9 +458,8 @@ namespace spot
}
std::ostream&
- format_label(std::ostream& os, bdd label) const
+ format_label(std::ostream& os, formula f) const
{
- formula f = bdd_to_formula(label, aut_->get_dict());
if (opt_latex_)
{
print_sclatex_psl(os << '$', f) << '$';
@@ -475,6 +476,12 @@ namespace spot
return escape_for_output(os, s);
}
+ std::ostream&
+ format_label(std::ostream& os, bdd label) const
+ {
+ return format_label(os, bdd_to_formula(label, aut_->get_dict()));
+ }
+
std::ostream&
format_state_label(std::ostream& os, unsigned s) const
{
@@ -490,6 +497,67 @@ namespace spot
return format_label(os, label);
}
+ std::ostream&
+ format_mealy(std::ostream& os,
+ bdd in,
+ bdd out) const
+ {
+ format_label(os, in);
+ if (opt_html_labels_)
+ os << "| / | ";
+ else
+ os << " / ";
+ format_label(os, out);
+ return os;
+ }
+
+ std::ostream&
+ format_mealy(std::ostream& os, bdd cond) const
+ {
+ if (opt_html_labels_)
+ os << ("| ");
+ // Is the label is separable?
+ bdd in = bdd_exist(cond, opt_mealy_output_);
+ bdd out = bdd_existcomp(cond, opt_mealy_output_);
+ if (cond == (in & out))
+ {
+ format_mealy(os, in, out);
+ }
+ else
+ {
+ // Otherwise, present it as a sum of separable labels.
+ std::map in_out;
+ bdd sup = bdd_support(cond);
+ for (bdd cond: minterms_of(cond, sup))
+ {
+ bdd in = bdd_exist(cond, opt_mealy_output_);
+ bdd out = bdd_existcomp(cond, opt_mealy_output_);
+ if (auto p = in_out.emplace(in, out); !p.second)
+ p.first->second |= out;
+ }
+ std::map out_in;
+ for (auto [in, out]: in_out)
+ if (auto p = out_in.emplace(out, in); !p.second)
+ p.first->second |= in;
+ bool first = true;
+ for (auto [out, in]: out_in)
+ {
+ if (!first)
+ {
+ if (opt_html_labels_)
+ os << (" | | ");
+ else
+ os << '\n';
+ }
+ format_mealy(os, in, out);
+ first = false;
+ }
+ }
+ return os;
+ }
+
std::string string_dst(int dst, int color_num = -1)
{
std::ostringstream tmp_dst;
@@ -816,15 +884,28 @@ namespace spot
}
os_ << " [" << label_pre_;
if (!opt_state_labels_ && opt_showlabel_)
- format_label(os_, t.cond);
+ {
+ if (opt_mealy_)
+ format_mealy(os_, t.cond);
+ else
+ format_label(os_, t.cond);
+ }
if (!mark_states_)
if (auto a = t.acc)
{
if (!opt_state_labels_ && opt_showlabel_)
- os_ << nl_;
+ {
+ if (opt_mealy_ && opt_html_labels_)
+ os_ << " | | ";
+ else
+ os_ << nl_;
+ }
output_mark(a);
}
- os_ << label_post_;
+ if (opt_mealy_ && opt_html_labels_)
+ os_ << " |
>";
+ else
+ os_ << label_post_;
if (opt_ordered_edges_ || opt_numbered_edges_)
{
os_ << ", taillabel=\"";
@@ -929,6 +1010,16 @@ namespace spot
return p.second >= palette_mod / 2;
}) != e;
}
+ // setup Mealy machine rendering.
+ if (!aut->get_named_prop>("state-player"))
+ if (auto p = aut->get_named_prop("synthesis-outputs"))
+ {
+ if (aut->acc().is_t())
+ opt_show_acc_ = false;
+ bdd out = *p;
+ opt_mealy_output_ = out;
+ opt_mealy_ = true;
+ }
incomplete_ =
aut->get_named_prop>("incomplete-states");
state_player_ =
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 25ce31fe5..18ad8a9f0 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -413,6 +413,7 @@ TESTS_python = \
python/ltlparse.py \
python/ltlsimple.py \
python/mealy.py \
+ python/_mealy.ipynb \
python/merge.py \
python/mergedge.py \
python/minato.py \
diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb
new file mode 100644
index 000000000..96a95b09e
--- /dev/null
+++ b/tests/python/_mealy.ipynb
@@ -0,0 +1,421 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "99baf49c",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "import spot\n",
+ "spot.setup()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "066489fd",
+ "metadata": {},
+ "source": [
+ "Test the Mealy printer."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "08d7d512",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "g = spot.ltl_to_game('G((a|c) <-> (b|d))', [\"b\", \"d\"])"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "4e5b66f4",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "True"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.solve_game(g)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "ce2ff962",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7f3d8c04f720> >"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.highlight_strategy(g)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "3bcbeef2",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "x = spot.apply_strategy(g, True, False)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "47d298f0",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7f3d8c04f630> >"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "f0d098ac",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "x.merge_edges()"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "adf92ac7",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7f3d8c04f630> >"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "6e8cd892",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7f3d76e561e0> >"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.apply_strategy(g, True, True)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "5948f923",
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.9.2"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb
index 46e8f6841..3ee2d3eb5 100644
--- a/tests/python/synthesis.ipynb
+++ b/tests/python/synthesis.ipynb
@@ -696,7 +696,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f8d9c0983f0> >"
+ " *' at 0x7f4e7018b5a0> >"
]
},
"metadata": {},
@@ -1371,214 +1371,300 @@
"\n",
"\n",
- "\n"
],
"text/plain": [
- " *' at 0x7f8d9c0720c0> >"
+ " *' at 0x7f4e700b8cf0> >"
]
},
"execution_count": 14,
|