From 98c8725d0c86265f5aaba510efd6af25313fb50e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 Dec 2018 17:09:56 +0100 Subject: [PATCH] print_dot_psl: fix numbering of commutative operands * spot/tl/dot.cc: Here. * tests/python/formulas.ipynb: Add test case. * NEWS: Mention the bug. --- NEWS | 6 +- spot/tl/dot.cc | 3 +- tests/python/formulas.ipynb | 126 ++++++++++++++++++++---------------- 3 files changed, 79 insertions(+), 56 deletions(-) diff --git a/NEWS b/NEWS index 9e67c0ef3..70d4f5cf9 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.7.0.dev (not yet release) - Nothing yet. + Bugs fixed: + + - The print_dot_psl() function would incorrectly number all but the + first children of commutative n-ary operators: in this case no + numbering was expected. New in spot 2.7 (2018-12-11) diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc index be6e2ac6b..8d8f68c4e 100644 --- a/spot/tl/dot.cc +++ b/spot/tl/dot.cc @@ -122,7 +122,8 @@ namespace spot else if (childnum == -1) os_ << " [taillabel=\"R\"]"; os_ << ";\n"; - ++childnum; + if (childnum) + ++childnum; } return src; diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index 69836c91a..ea100f7e9 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -57,10 +57,10 @@ { "data": { "text/latex": [ - "$\\{a \\mathbin{\\mathsf{;}} b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{G} \\mathsf{F} b$" + "$\\{a \\mathbin{\\mathsf{;}} b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} (c \\land \\mathsf{G} \\mathsf{F} b)$" ], "text/plain": [ - "spot.formula(\"{a;b[*];c[+]}<>-> GFb\")" + "spot.formula(\"{a;b[*];c[+]}<>-> (c & GFb)\")" ] }, "execution_count": 3, @@ -69,7 +69,7 @@ } ], "source": [ - "g = spot.formula('{a;b*;c[+]}<>->GFb'); g" + "g = spot.formula('{a;b*;c[+]}<>->(GFb & c)'); g" ] }, { @@ -497,128 +497,146 @@ "name": "stdout", "output_type": "stream", "text": [ - "{a;b[*];c[+]}<>-> GFb\n" + "{a;b[*];c[+]}<>-> (c & GFb)\n" ] }, { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "EConcat\n", + "\n", + "EConcat\n", "\n", "\n", "\n", "1\n", - "\n", - "Concat\n", + "\n", + "Concat\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "L\n", + "\n", + "\n", + "L\n", "\n", "\n", "\n", "7\n", - "\n", - "G\n", + "\n", + "And\n", "\n", "\n", - "\n", + "\n", "0->7\n", - "\n", - "\n", - "R\n", + "\n", + "\n", + "R\n", "\n", "\n", "\n", "2\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "Star\n", + "\n", + "Star\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "5\n", - "\n", - "Star\n", + "\n", + "Star\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "4\n", - "\n", - "b\n", + "\n", + "b\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "c\n", + "\n", + "c\n", "\n", "\n", "\n", "5->6\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "F\n", + "\n", + "G\n", "\n", "\n", - "\n", + "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "8->4\n", - "\n", - "\n", + "\n", + "\n", + "9\n", + "\n", + "F\n", + "\n", + "\n", + "\n", + "8->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9->4\n", + "\n", + "\n", "\n", "\n", "" @@ -909,7 +927,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7" + "version": "3.7.1" } }, "nbformat": 4,