From cab3ea7faf394d2bfaa1dc619b9dc48f026e9b6d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Dec 2022 12:04:15 +0100 Subject: [PATCH 01/20] acd: rewrite Python wrapper without jQuery * python/spot/__init__.py (acd): Rewrite javascript so that it does not use jQuery, to make it easier to use in jupyterlab, or with nbconvert. * tests/python/zlktree.ipynb: Adjust. * NEWS: Mention this. --- NEWS | 4 +- python/spot/__init__.py | 58 ++-- tests/python/zlktree.ipynb | 683 ++++++++++++++++++++++++++++--------- 3 files changed, 563 insertions(+), 182 deletions(-) diff --git a/NEWS b/NEWS index b1f7c2d79..0ac838737 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 2.11.3.dev (not yet released) - Nothing yet. + Python: + + - spot.acd() no longer depends on jQuery for interactivity. New in spot 2.11.3 (2022-12-09) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index edbf4a4e6..ef4cd772e 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -502,51 +502,57 @@ class acd: .acdacc polygon{fill:green;} ''' js = ''' -function acd{num}_clear(){{ - $("#acd{num} .node,#acdaut{num} .node,#acdaut{num} .edge") - .removeClass("acdhigh acdbold acdacc acdrej"); +function acdremclasses(sel, classes) {{ +document.querySelectorAll(sel).forEach(n=>{{n.classList.remove(...classes)}});}} +function acdaddclasses(sel, classes) {{ +document.querySelectorAll(sel).forEach(n=>{{n.classList.add(...classes)}});}} +function acdonclick(sel, fn) {{ + document.querySelectorAll(sel).forEach(n=> + {{n.addEventListener("click", fn)}}); +}} +function acd{num}_clear() {{ + acdremclasses("#acd{num} .node,#acdaut{num} .node,#acdaut{num} .edge", + ["acdhigh", "acdbold", "acdacc", "acdrej"]); }}; function acd{num}_state(state){{ - acd{num}_clear(); - $("#acd{num} .acdS" + state).addClass("acdhigh acdbold"); - $("#acdaut{num} #S" + state).addClass("acdbold"); + acd{num}_clear(); + acdaddclasses("#acd{num} .acdS" + state, ["acdhigh", "acdbold"]); + acdaddclasses("#acdaut{num} #S" + state, ["acdbold"]); }}; function acd{num}_edge(edge){{ - acd{num}_clear(); - var theedge = $('#acdaut{num} #E' + edge) - var classList = theedge.attr('class').split(/\s+/); - $.each(classList, function(index, item) {{ - if (item.startsWith('acdN')) {{ - $("#acd{num} #" + item.substring(3)).addClass("acdhigh acdbold"); - }} - }}); - theedge.addClass("acdbold"); + acd{num}_clear(); + var theedge = document.querySelector('#acdaut{num} #E' + edge); + theedge.classList.forEach(function(item, index) {{ + if (item.startsWith('acdN')) {{ + acdaddclasses("#acd{num} #" + item.substring(3), ["acdhigh", "acdbold"]); + }} + }}); + theedge.classList.add("acdbold"); }}; function acd{num}_node(node, acc){{ acd{num}_clear(); - $("#acdaut{num} .acdN" + node).addClass(acc - ? "acdacc acdbold" - : "acdrej acdbold"); - $("#acd{num} #N" + node).addClass("acdbold acdhigh"); + acdaddclasses("#acdaut{num} .acdN" + node, + [acc ? "acdacc" : "acdrej", "acdbold"]); + acdaddclasses("#acd{num} #N" + node, ["acdbold", "acdhigh"]); }};'''.format(num=num) me = 0 for n in range(self.node_count()): for e in self.edges_of_node(n): me = max(e, me) - js += '$("#acdaut{num} #E{e}").addClass("acdN{n}");'\ + js += 'acdaddclasses("#acdaut{num} #E{e}", ["acdN{n}"]);\n'\ .format(num=num, e=e, n=n) for e in range(1, me + 1): - js += '$("#acdaut{num} #E{e}")'\ - '.click(function(){{acd{num}_edge({e});}});'\ + js += 'acdonclick("#acdaut{num} #E{e}",'\ + 'function(){{acd{num}_edge({e});}});\n'\ .format(num=num, e=e) for s in range(self.get_aut().num_states()): - js += '$("#acdaut{num} #S{s}")'\ - '.click(function(){{acd{num}_state({s});}});'\ + js += 'acdonclick("#acdaut{num} #S{s}",'\ + 'function(){{acd{num}_state({s});}});\n'\ .format(num=num, s=s) for n in range(self.node_count()): v = int(self.node_acceptance(n)) - js += '$("#acd{num} #N{n}")'\ - '.click(function(){{acd{num}_node({n}, {v});}});'\ + js += 'acdonclick("#acd{num} #N{n}",'\ + 'function(){{acd{num}_node({n}, {v});}});\n'\ .format(num=num, n=n, v=v) html = '
{}
{}
'\ .format(style, diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index ae44ad37d..c9eb3503d 100644 --- a/tests/python/zlktree.ipynb +++ b/tests/python/zlktree.ipynb @@ -216,7 +216,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 2, @@ -640,7 +640,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14701b7510> >" + " *' at 0x7f82c009d7a0> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470220960> >" + " *' at 0x7f82c009c630> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14701b75d0> >" + " *' at 0x7f82c009c6c0> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470142240> >" + " *' at 0x7f82c009c480> >" ] }, "execution_count": 14, @@ -2096,7 +2096,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2427,7 +2427,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2513,7 +2513,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2624,7 +2624,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2662,7 +2662,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2700,7 +2700,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2928,7 +2928,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 18, @@ -4064,36 +4064,159 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut0 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd0 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut0 #E9\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E10\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E11\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E12\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E13\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E14\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E15\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E16\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E21\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E22\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E23\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E24\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E25\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E26\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E27\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E28\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E33\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E34\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E35\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E36\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut0 #E31\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut0 #E32\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut0 #E39\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut0 #E40\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut0 #E5\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut0 #E7\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut0 #E17\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut0 #E1\", [\"acdN3\"]);\n", + "acdaddclasses(\"#acdaut0 #E10\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E12\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E13\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E15\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E21\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E22\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut0 #E23\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut0 #E24\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut0 #E34\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut0 #E36\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut0 #E14\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut0 #E15\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut0 #E22\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut0 #E23\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut0 #E14\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut0 #E16\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut0 #E26\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut0 #E9\", [\"acdN8\"]);\n", + "acdaddclasses(\"#acdaut0 #E40\", [\"acdN9\"]);\n", + "acdaddclasses(\"#acdaut0 #E5\", [\"acdN10\"]);\n", + "acdaddclasses(\"#acdaut0 #E23\", [\"acdN11\"]);\n", + "acdaddclasses(\"#acdaut0 #E14\", [\"acdN12\"]);\n", + "acdaddclasses(\"#acdaut0 #E23\", [\"acdN13\"]);\n", + "acdaddclasses(\"#acdaut0 #E14\", [\"acdN14\"]);\n", + "acdonclick(\"#acdaut0 #E1\",function(){acd0_edge(1);});\n", + "acdonclick(\"#acdaut0 #E2\",function(){acd0_edge(2);});\n", + "acdonclick(\"#acdaut0 #E3\",function(){acd0_edge(3);});\n", + "acdonclick(\"#acdaut0 #E4\",function(){acd0_edge(4);});\n", + "acdonclick(\"#acdaut0 #E5\",function(){acd0_edge(5);});\n", + "acdonclick(\"#acdaut0 #E6\",function(){acd0_edge(6);});\n", + "acdonclick(\"#acdaut0 #E7\",function(){acd0_edge(7);});\n", + "acdonclick(\"#acdaut0 #E8\",function(){acd0_edge(8);});\n", + "acdonclick(\"#acdaut0 #E9\",function(){acd0_edge(9);});\n", + "acdonclick(\"#acdaut0 #E10\",function(){acd0_edge(10);});\n", + "acdonclick(\"#acdaut0 #E11\",function(){acd0_edge(11);});\n", + "acdonclick(\"#acdaut0 #E12\",function(){acd0_edge(12);});\n", + "acdonclick(\"#acdaut0 #E13\",function(){acd0_edge(13);});\n", + "acdonclick(\"#acdaut0 #E14\",function(){acd0_edge(14);});\n", + "acdonclick(\"#acdaut0 #E15\",function(){acd0_edge(15);});\n", + "acdonclick(\"#acdaut0 #E16\",function(){acd0_edge(16);});\n", + "acdonclick(\"#acdaut0 #E17\",function(){acd0_edge(17);});\n", + "acdonclick(\"#acdaut0 #E18\",function(){acd0_edge(18);});\n", + "acdonclick(\"#acdaut0 #E19\",function(){acd0_edge(19);});\n", + "acdonclick(\"#acdaut0 #E20\",function(){acd0_edge(20);});\n", + "acdonclick(\"#acdaut0 #E21\",function(){acd0_edge(21);});\n", + "acdonclick(\"#acdaut0 #E22\",function(){acd0_edge(22);});\n", + "acdonclick(\"#acdaut0 #E23\",function(){acd0_edge(23);});\n", + "acdonclick(\"#acdaut0 #E24\",function(){acd0_edge(24);});\n", + "acdonclick(\"#acdaut0 #E25\",function(){acd0_edge(25);});\n", + "acdonclick(\"#acdaut0 #E26\",function(){acd0_edge(26);});\n", + "acdonclick(\"#acdaut0 #E27\",function(){acd0_edge(27);});\n", + "acdonclick(\"#acdaut0 #E28\",function(){acd0_edge(28);});\n", + "acdonclick(\"#acdaut0 #E29\",function(){acd0_edge(29);});\n", + "acdonclick(\"#acdaut0 #E30\",function(){acd0_edge(30);});\n", + "acdonclick(\"#acdaut0 #E31\",function(){acd0_edge(31);});\n", + "acdonclick(\"#acdaut0 #E32\",function(){acd0_edge(32);});\n", + "acdonclick(\"#acdaut0 #E33\",function(){acd0_edge(33);});\n", + "acdonclick(\"#acdaut0 #E34\",function(){acd0_edge(34);});\n", + "acdonclick(\"#acdaut0 #E35\",function(){acd0_edge(35);});\n", + "acdonclick(\"#acdaut0 #E36\",function(){acd0_edge(36);});\n", + "acdonclick(\"#acdaut0 #E37\",function(){acd0_edge(37);});\n", + "acdonclick(\"#acdaut0 #E38\",function(){acd0_edge(38);});\n", + "acdonclick(\"#acdaut0 #E39\",function(){acd0_edge(39);});\n", + "acdonclick(\"#acdaut0 #E40\",function(){acd0_edge(40);});\n", + "acdonclick(\"#acdaut0 #S0\",function(){acd0_state(0);});\n", + "acdonclick(\"#acdaut0 #S1\",function(){acd0_state(1);});\n", + "acdonclick(\"#acdaut0 #S2\",function(){acd0_state(2);});\n", + "acdonclick(\"#acdaut0 #S3\",function(){acd0_state(3);});\n", + "acdonclick(\"#acdaut0 #S4\",function(){acd0_state(4);});\n", + "acdonclick(\"#acdaut0 #S5\",function(){acd0_state(5);});\n", + "acdonclick(\"#acdaut0 #S6\",function(){acd0_state(6);});\n", + "acdonclick(\"#acdaut0 #S7\",function(){acd0_state(7);});\n", + "acdonclick(\"#acdaut0 #S8\",function(){acd0_state(8);});\n", + "acdonclick(\"#acdaut0 #S9\",function(){acd0_state(9);});\n", + "acdonclick(\"#acd0 #N0\",function(){acd0_node(0, 0);});\n", + "acdonclick(\"#acd0 #N1\",function(){acd0_node(1, 1);});\n", + "acdonclick(\"#acd0 #N2\",function(){acd0_node(2, 1);});\n", + "acdonclick(\"#acd0 #N3\",function(){acd0_node(3, 1);});\n", + "acdonclick(\"#acd0 #N4\",function(){acd0_node(4, 1);});\n", + "acdonclick(\"#acd0 #N5\",function(){acd0_node(5, 1);});\n", + "acdonclick(\"#acd0 #N6\",function(){acd0_node(6, 1);});\n", + "acdonclick(\"#acd0 #N7\",function(){acd0_node(7, 1);});\n", + "acdonclick(\"#acd0 #N8\",function(){acd0_node(8, 1);});\n", + "acdonclick(\"#acd0 #N9\",function(){acd0_node(9, 0);});\n", + "acdonclick(\"#acd0 #N10\",function(){acd0_node(10, 0);});\n", + "acdonclick(\"#acd0 #N11\",function(){acd0_node(11, 0);});\n", + "acdonclick(\"#acd0 #N12\",function(){acd0_node(12, 0);});\n", + "acdonclick(\"#acd0 #N13\",function(){acd0_node(13, 0);});\n", + "acdonclick(\"#acd0 #N14\",function(){acd0_node(14, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 20, @@ -4968,7 +5091,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14701670f0> >" + " *' at 0x7f82c00bc870> >" ] }, "execution_count": 29, @@ -5607,7 +5730,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470167210> >" + " *' at 0x7f82c00bc060> >" ] }, "execution_count": 31, @@ -5807,7 +5930,9 @@ "cell_type": "code", "execution_count": 40, "id": "813d15ed", - "metadata": {}, + "metadata": { + "scrolled": false + }, "outputs": [ { "data": { @@ -6875,36 +7000,159 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut1 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd1 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut1 #E9\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E10\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E11\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E12\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E13\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E14\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E15\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E16\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E21\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E22\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E23\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E24\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E25\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E26\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E27\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E28\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E33\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E34\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E35\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E36\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut1 #E31\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut1 #E32\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut1 #E39\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut1 #E40\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut1 #E5\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut1 #E7\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut1 #E17\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut1 #E1\", [\"acdN3\"]);\n", + "acdaddclasses(\"#acdaut1 #E10\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E12\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E13\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E15\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E21\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E22\", [\"acdN4\"]);\n", + "acdaddclasses(\"#acdaut1 #E14\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut1 #E15\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut1 #E22\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut1 #E23\", [\"acdN5\"]);\n", + "acdaddclasses(\"#acdaut1 #E23\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut1 #E24\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut1 #E34\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut1 #E36\", [\"acdN6\"]);\n", + "acdaddclasses(\"#acdaut1 #E14\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut1 #E16\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut1 #E26\", [\"acdN7\"]);\n", + "acdaddclasses(\"#acdaut1 #E9\", [\"acdN8\"]);\n", + "acdaddclasses(\"#acdaut1 #E40\", [\"acdN9\"]);\n", + "acdaddclasses(\"#acdaut1 #E5\", [\"acdN10\"]);\n", + "acdaddclasses(\"#acdaut1 #E14\", [\"acdN11\"]);\n", + "acdaddclasses(\"#acdaut1 #E23\", [\"acdN12\"]);\n", + "acdaddclasses(\"#acdaut1 #E23\", [\"acdN13\"]);\n", + "acdaddclasses(\"#acdaut1 #E14\", [\"acdN14\"]);\n", + "acdonclick(\"#acdaut1 #E1\",function(){acd1_edge(1);});\n", + "acdonclick(\"#acdaut1 #E2\",function(){acd1_edge(2);});\n", + "acdonclick(\"#acdaut1 #E3\",function(){acd1_edge(3);});\n", + "acdonclick(\"#acdaut1 #E4\",function(){acd1_edge(4);});\n", + "acdonclick(\"#acdaut1 #E5\",function(){acd1_edge(5);});\n", + "acdonclick(\"#acdaut1 #E6\",function(){acd1_edge(6);});\n", + "acdonclick(\"#acdaut1 #E7\",function(){acd1_edge(7);});\n", + "acdonclick(\"#acdaut1 #E8\",function(){acd1_edge(8);});\n", + "acdonclick(\"#acdaut1 #E9\",function(){acd1_edge(9);});\n", + "acdonclick(\"#acdaut1 #E10\",function(){acd1_edge(10);});\n", + "acdonclick(\"#acdaut1 #E11\",function(){acd1_edge(11);});\n", + "acdonclick(\"#acdaut1 #E12\",function(){acd1_edge(12);});\n", + "acdonclick(\"#acdaut1 #E13\",function(){acd1_edge(13);});\n", + "acdonclick(\"#acdaut1 #E14\",function(){acd1_edge(14);});\n", + "acdonclick(\"#acdaut1 #E15\",function(){acd1_edge(15);});\n", + "acdonclick(\"#acdaut1 #E16\",function(){acd1_edge(16);});\n", + "acdonclick(\"#acdaut1 #E17\",function(){acd1_edge(17);});\n", + "acdonclick(\"#acdaut1 #E18\",function(){acd1_edge(18);});\n", + "acdonclick(\"#acdaut1 #E19\",function(){acd1_edge(19);});\n", + "acdonclick(\"#acdaut1 #E20\",function(){acd1_edge(20);});\n", + "acdonclick(\"#acdaut1 #E21\",function(){acd1_edge(21);});\n", + "acdonclick(\"#acdaut1 #E22\",function(){acd1_edge(22);});\n", + "acdonclick(\"#acdaut1 #E23\",function(){acd1_edge(23);});\n", + "acdonclick(\"#acdaut1 #E24\",function(){acd1_edge(24);});\n", + "acdonclick(\"#acdaut1 #E25\",function(){acd1_edge(25);});\n", + "acdonclick(\"#acdaut1 #E26\",function(){acd1_edge(26);});\n", + "acdonclick(\"#acdaut1 #E27\",function(){acd1_edge(27);});\n", + "acdonclick(\"#acdaut1 #E28\",function(){acd1_edge(28);});\n", + "acdonclick(\"#acdaut1 #E29\",function(){acd1_edge(29);});\n", + "acdonclick(\"#acdaut1 #E30\",function(){acd1_edge(30);});\n", + "acdonclick(\"#acdaut1 #E31\",function(){acd1_edge(31);});\n", + "acdonclick(\"#acdaut1 #E32\",function(){acd1_edge(32);});\n", + "acdonclick(\"#acdaut1 #E33\",function(){acd1_edge(33);});\n", + "acdonclick(\"#acdaut1 #E34\",function(){acd1_edge(34);});\n", + "acdonclick(\"#acdaut1 #E35\",function(){acd1_edge(35);});\n", + "acdonclick(\"#acdaut1 #E36\",function(){acd1_edge(36);});\n", + "acdonclick(\"#acdaut1 #E37\",function(){acd1_edge(37);});\n", + "acdonclick(\"#acdaut1 #E38\",function(){acd1_edge(38);});\n", + "acdonclick(\"#acdaut1 #E39\",function(){acd1_edge(39);});\n", + "acdonclick(\"#acdaut1 #E40\",function(){acd1_edge(40);});\n", + "acdonclick(\"#acdaut1 #S0\",function(){acd1_state(0);});\n", + "acdonclick(\"#acdaut1 #S1\",function(){acd1_state(1);});\n", + "acdonclick(\"#acdaut1 #S2\",function(){acd1_state(2);});\n", + "acdonclick(\"#acdaut1 #S3\",function(){acd1_state(3);});\n", + "acdonclick(\"#acdaut1 #S4\",function(){acd1_state(4);});\n", + "acdonclick(\"#acdaut1 #S5\",function(){acd1_state(5);});\n", + "acdonclick(\"#acdaut1 #S6\",function(){acd1_state(6);});\n", + "acdonclick(\"#acdaut1 #S7\",function(){acd1_state(7);});\n", + "acdonclick(\"#acdaut1 #S8\",function(){acd1_state(8);});\n", + "acdonclick(\"#acdaut1 #S9\",function(){acd1_state(9);});\n", + "acdonclick(\"#acd1 #N0\",function(){acd1_node(0, 0);});\n", + "acdonclick(\"#acd1 #N1\",function(){acd1_node(1, 1);});\n", + "acdonclick(\"#acd1 #N2\",function(){acd1_node(2, 1);});\n", + "acdonclick(\"#acd1 #N3\",function(){acd1_node(3, 1);});\n", + "acdonclick(\"#acd1 #N4\",function(){acd1_node(4, 1);});\n", + "acdonclick(\"#acd1 #N5\",function(){acd1_node(5, 1);});\n", + "acdonclick(\"#acd1 #N6\",function(){acd1_node(6, 1);});\n", + "acdonclick(\"#acd1 #N7\",function(){acd1_node(7, 1);});\n", + "acdonclick(\"#acd1 #N8\",function(){acd1_node(8, 1);});\n", + "acdonclick(\"#acd1 #N9\",function(){acd1_node(9, 0);});\n", + "acdonclick(\"#acd1 #N10\",function(){acd1_node(10, 0);});\n", + "acdonclick(\"#acd1 #N11\",function(){acd1_node(11, 0);});\n", + "acdonclick(\"#acd1 #N12\",function(){acd1_node(12, 0);});\n", + "acdonclick(\"#acd1 #N13\",function(){acd1_node(13, 0);});\n", + "acdonclick(\"#acd1 #N14\",function(){acd1_node(14, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 40, @@ -7817,7 +8065,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14700fe1e0> >" + " *' at 0x7f82c00be460> >" ] }, "execution_count": 45, @@ -8114,36 +8362,69 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut2 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd2 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut2 #E1\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E2\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E3\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E4\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E5\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E6\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut2 #E2\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut2 #E3\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut2 #E4\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut2 #E5\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut2 #E6\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut2 #E1\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut2 #E2\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut2 #E4\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut2 #E6\", [\"acdN2\"]);\n", + "acdonclick(\"#acdaut2 #E1\",function(){acd2_edge(1);});\n", + "acdonclick(\"#acdaut2 #E2\",function(){acd2_edge(2);});\n", + "acdonclick(\"#acdaut2 #E3\",function(){acd2_edge(3);});\n", + "acdonclick(\"#acdaut2 #E4\",function(){acd2_edge(4);});\n", + "acdonclick(\"#acdaut2 #E5\",function(){acd2_edge(5);});\n", + "acdonclick(\"#acdaut2 #E6\",function(){acd2_edge(6);});\n", + "acdonclick(\"#acdaut2 #S0\",function(){acd2_state(0);});\n", + "acdonclick(\"#acdaut2 #S1\",function(){acd2_state(1);});\n", + "acdonclick(\"#acdaut2 #S2\",function(){acd2_state(2);});\n", + "acdonclick(\"#acd2 #N0\",function(){acd2_node(0, 1);});\n", + "acdonclick(\"#acd2 #N1\",function(){acd2_node(1, 0);});\n", + "acdonclick(\"#acd2 #N2\",function(){acd2_node(2, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 47, @@ -8353,7 +8634,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14700feb40> >" + " *' at 0x7f82c00bdd40> >" ] }, "execution_count": 48, @@ -8628,36 +8909,69 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut3 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd3 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut3 #E1\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E2\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E3\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E4\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E5\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E6\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut3 #E1\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut3 #E2\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut3 #E4\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut3 #E6\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut3 #E2\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut3 #E3\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut3 #E4\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut3 #E5\", [\"acdN2\"]);\n", + "acdaddclasses(\"#acdaut3 #E6\", [\"acdN2\"]);\n", + "acdonclick(\"#acdaut3 #E1\",function(){acd3_edge(1);});\n", + "acdonclick(\"#acdaut3 #E2\",function(){acd3_edge(2);});\n", + "acdonclick(\"#acdaut3 #E3\",function(){acd3_edge(3);});\n", + "acdonclick(\"#acdaut3 #E4\",function(){acd3_edge(4);});\n", + "acdonclick(\"#acdaut3 #E5\",function(){acd3_edge(5);});\n", + "acdonclick(\"#acdaut3 #E6\",function(){acd3_edge(6);});\n", + "acdonclick(\"#acdaut3 #S0\",function(){acd3_state(0);});\n", + "acdonclick(\"#acdaut3 #S1\",function(){acd3_state(1);});\n", + "acdonclick(\"#acdaut3 #S2\",function(){acd3_state(2);});\n", + "acdonclick(\"#acd3 #N0\",function(){acd3_node(0, 1);});\n", + "acdonclick(\"#acd3 #N1\",function(){acd3_node(1, 0);});\n", + "acdonclick(\"#acd3 #N2\",function(){acd3_node(2, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 49, @@ -8841,7 +9155,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14700fea80> >" + " *' at 0x7f82c00bf300> >" ] }, "execution_count": 50, @@ -8993,7 +9307,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470107240> >" + " *' at 0x7f82c00be5b0> >" ] }, "execution_count": 51, @@ -9105,7 +9419,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 52, @@ -9271,7 +9585,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470107030> >" + " *' at 0x7f82c00bf5d0> >" ] }, "execution_count": 53, @@ -9535,36 +9849,63 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut4 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd4 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut4 #E1\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E2\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E3\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E4\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E5\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E6\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E7\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E8\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut4 #E6\", [\"acdN1\"]);\n", + "acdonclick(\"#acdaut4 #E1\",function(){acd4_edge(1);});\n", + "acdonclick(\"#acdaut4 #E2\",function(){acd4_edge(2);});\n", + "acdonclick(\"#acdaut4 #E3\",function(){acd4_edge(3);});\n", + "acdonclick(\"#acdaut4 #E4\",function(){acd4_edge(4);});\n", + "acdonclick(\"#acdaut4 #E5\",function(){acd4_edge(5);});\n", + "acdonclick(\"#acdaut4 #E6\",function(){acd4_edge(6);});\n", + "acdonclick(\"#acdaut4 #E7\",function(){acd4_edge(7);});\n", + "acdonclick(\"#acdaut4 #E8\",function(){acd4_edge(8);});\n", + "acdonclick(\"#acdaut4 #S0\",function(){acd4_state(0);});\n", + "acdonclick(\"#acdaut4 #S1\",function(){acd4_state(1);});\n", + "acdonclick(\"#acd4 #N0\",function(){acd4_node(0, 1);});\n", + "acdonclick(\"#acd4 #N1\",function(){acd4_node(1, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 55, @@ -9708,7 +10049,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470107b70> >" + " *' at 0x7f82c00f4240> >" ] }, "execution_count": 57, @@ -9855,7 +10196,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f147010d240> >" + " *' at 0x7f82c00f4090> >" ] }, "execution_count": 58, @@ -10165,36 +10506,68 @@ "\n", "\n", "" + " acdaddclasses(\"#acdaut5 .acdN\" + node,\n", + " [acc ? \"acdacc\" : \"acdrej\", \"acdbold\"]);\n", + " acdaddclasses(\"#acd5 #N\" + node, [\"acdbold\", \"acdhigh\"]);\n", + "};acdaddclasses(\"#acdaut5 #E1\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E2\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E3\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E4\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E5\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E6\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E7\", [\"acdN0\"]);\n", + "acdaddclasses(\"#acdaut5 #E1\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut5 #E3\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut5 #E4\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut5 #E5\", [\"acdN1\"]);\n", + "acdaddclasses(\"#acdaut5 #E7\", [\"acdN2\"]);\n", + "acdonclick(\"#acdaut5 #E1\",function(){acd5_edge(1);});\n", + "acdonclick(\"#acdaut5 #E2\",function(){acd5_edge(2);});\n", + "acdonclick(\"#acdaut5 #E3\",function(){acd5_edge(3);});\n", + "acdonclick(\"#acdaut5 #E4\",function(){acd5_edge(4);});\n", + "acdonclick(\"#acdaut5 #E5\",function(){acd5_edge(5);});\n", + "acdonclick(\"#acdaut5 #E6\",function(){acd5_edge(6);});\n", + "acdonclick(\"#acdaut5 #E7\",function(){acd5_edge(7);});\n", + "acdonclick(\"#acdaut5 #S0\",function(){acd5_state(0);});\n", + "acdonclick(\"#acdaut5 #S1\",function(){acd5_state(1);});\n", + "acdonclick(\"#acdaut5 #S2\",function(){acd5_state(2);});\n", + "acdonclick(\"#acdaut5 #S3\",function(){acd5_state(3);});\n", + "acdonclick(\"#acd5 #N0\",function(){acd5_node(0, 1);});\n", + "acdonclick(\"#acd5 #N1\",function(){acd5_node(1, 0);});\n", + "acdonclick(\"#acd5 #N2\",function(){acd5_node(2, 0);});\n", + "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 60, @@ -10322,7 +10695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f147010d5a0> >" + " *' at 0x7f82c00f50b0> >" ] }, "execution_count": 61, @@ -10452,7 +10825,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f147010d6f0> >" + " *' at 0x7f82c00f52c0> >" ] }, "execution_count": 62, @@ -10732,7 +11105,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470116270> >" + " *' at 0x7f82c00f4960> >" ] }, "execution_count": 63, @@ -10826,7 +11199,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470116630> >" + " *' at 0x7f82c00f5a10> >" ] }, "execution_count": 64, @@ -10937,7 +11310,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f1470116450> >" + " *' at 0x7f82c00f5ce0> >" ] }, "execution_count": 66, @@ -10995,7 +11368,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.10.7" } }, "nbformat": 4, From 104e98aca61d4c526eaade2c6a4a703666a11528 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 4 Jan 2023 15:11:21 +0100 Subject: [PATCH 02/20] fix merging of initial states in state-based automata Fixes #522 reported by Raven Beutner. * spot/parseaut/parseaut.yy: Make sure all edges leaving the initial state have the same color. * THANKS: Add Raven. * NEWS: Mention the bug. * tests/core/522.test: New file. * tests/Makefile.am: Add it. --- NEWS | 6 ++++++ THANKS | 1 + spot/parseaut/parseaut.yy | 33 ++++++++++++++++++++++++------ tests/Makefile.am | 3 ++- tests/core/522.test | 43 +++++++++++++++++++++++++++++++++++++++ 5 files changed, 79 insertions(+), 7 deletions(-) create mode 100755 tests/core/522.test diff --git a/NEWS b/NEWS index 0ac838737..9775339fe 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,12 @@ New in spot 2.11.3.dev (not yet released) - spot.acd() no longer depends on jQuery for interactivity. + Bug fixes: + + - When merging initial states from state-based automata with + multiple initial states (because Spot supports only one), the HOA + parser could break state-based acceptance. (Issue #522.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/THANKS b/THANKS index 356d187a1..93155f9d1 100644 --- a/THANKS +++ b/THANKS @@ -48,6 +48,7 @@ Nikos Gorogiannis Ondřej Lengál Paul Guénézan Pierre Ganty +Raven Beutner Reuben Rowe Roei Nahum Rüdiger Ehlers diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 4d96b8c1c..7d5fac361 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2022 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2023 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -2610,7 +2610,7 @@ static void fix_initial_state(result_& r) start.resize(std::distance(start.begin(), res)); assert(start.size() >= 1); - if (start.size() == 1) + if (start.size() == 1) { if (r.opts.want_kripke) r.h->ks->set_init_state(start.front().front()); @@ -2627,13 +2627,13 @@ static void fix_initial_state(result_& r) "a single initial state"); return; } + auto& aut = r.h->aut; // Fiddling with initial state may turn an incomplete automaton // into a complete one. - if (r.complete.is_false()) - r.complete = spot::trival::maybe(); + if (aut->prop_complete().is_false()) + aut->prop_complete(spot::trival::maybe()); // Multiple initial states. We might need to add a fake one, // unless one of the actual initial state has no incoming edge. - auto& aut = r.h->aut; std::vector has_incoming(aut->num_states(), 0); for (auto& t: aut->edges()) for (unsigned ud: aut->univ_dests(t)) @@ -2672,6 +2672,9 @@ static void fix_initial_state(result_& r) { unsigned p = pp.front(); if (p != init) + // FIXME: If p has no incoming we should be able to + // change the source of the edges of p instead of + // adding new edges. for (auto& t: aut->out(p)) aut->new_edge(init, t.dst, t.cond); } @@ -2694,6 +2697,24 @@ static void fix_initial_state(result_& r) } combiner.new_dests(init, comb_or); } + + // Merging two states may break state-based acceptance + // make sure all outgoing edges have the same color. + if (aut->prop_state_acc().is_true()) + { + bool first = true; + spot::acc_cond::mark_t prev; + for (auto& e: aut->out(init)) + if (first) + { + first = false; + prev = e.acc; + } + else if (e.acc != prev) + { + e.acc = prev; + } + } } } @@ -2871,8 +2892,8 @@ namespace spot r.aut_or_ks->set_named_prop("aliases", p); } fix_acceptance(r); + fix_properties(r); // before fix_initial_state fix_initial_state(r); - fix_properties(r); if (r.h->aut && !r.h->aut->is_existential()) r.h->aut->merge_univ_dests(); return r.h; diff --git a/tests/Makefile.am b/tests/Makefile.am index 4c2fe830c..8a180ddda 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009-2022 Laboratoire de Recherche et Développement +## Copyright (C) 2009-2023 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -223,6 +223,7 @@ TESTS_misc = \ TESTS_twa = \ core/385.test \ core/521.test \ + core/522.test \ core/acc.test \ core/acc2.test \ core/bdddict.test \ diff --git a/tests/core/522.test b/tests/core/522.test new file mode 100755 index 000000000..5fe6ba945 --- /dev/null +++ b/tests/core/522.test @@ -0,0 +1,43 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2023 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +set -e + +# For issue #522. + +cat >552.hoa < out.hoa +grep 'States: 7' out.hoa From 403e55d555df75e5b910669aa3301d98a04f04c5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 17:47:46 +0100 Subject: [PATCH 03/20] * doc/org/spot.css: Do not define background twice. --- doc/org/spot.css | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/org/spot.css b/doc/org/spot.css index ca8b12395..569ca37a9 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -16,9 +16,9 @@ h1::before{content:"";position:absolute;z-index:-1;background-color:#ffe35e;left #table-of-contents #text-table-of-contents{text-align:left} #org-div-home-and-up{text-align:center;font-size:100%} .outline-2 h2{display:block;width:100%;position:relative} -.outline-2 h2::before{content:"";height:100%;width:calc(100% + 2em);position:absolute;z-index:-1;bottom:0em;left:-1em;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 50%,transparent 75%);transform:skew(10deg);border-radius:5px;} +.outline-2 h2::before{content:"";height:100%;width:calc(100% + 2em);position:absolute;z-index:-1;bottom:0em;left:-1em;background:linear-gradient(45deg,#ffe35e 50%,transparent 75%);transform:skew(10deg);border-radius:5px;} .outline-3 h3{display:block;width:auto;position:relative} -.outline-3 h3::before{content:"";position:absolute;z-index:-1;width:calc(100% + 2em);height:100%;left:-1em;bottom:0em;;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 25%,transparent 50%);transform:skew(10deg);border-radius:3px} +.outline-3 h3::before{content:"";position:absolute;z-index:-1;width:calc(100% + 2em);height:100%;left:-1em;bottom:0em;background:linear-gradient(45deg,#ffe35e 25%,transparent 50%);transform:skew(10deg);border-radius:3px} .outline-2 h2:hover::before,.outline-3 h3:hover::before{background-color:#ffe35e} pre{margin:1.2ex} pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto;margin-top:0;margin-bottom:0} From 344d82f2b49837e7e98bcfb0fb10a566e5c97560 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 17:48:14 +0100 Subject: [PATCH 04/20] simplify several comparison operators * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/simulation.cc: Simplify, as reported by sonarcloud. --- spot/twaalgos/dtbasat.cc | 8 ++------ spot/twaalgos/dtwasat.cc | 8 ++------ spot/twaalgos/simulation.cc | 10 ++-------- 3 files changed, 6 insertions(+), 20 deletions(-) diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index b2147ebb4..c4bf3d1bc 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018, 2021, 2022 Laboratoire de Recherche et +// Copyright (C) 2013-2018, 2021-2023 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -77,11 +77,7 @@ namespace spot return true; if (this->src_ref > other.src_ref) return false; - if (this->dst_ref < other.dst_ref) - return true; - if (this->dst_ref > other.dst_ref) - return false; - return false; + return this->dst_ref < other.dst_ref; } }; diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 25a299154..2ecf38fd1 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2022 Laboratoire de Recherche +// Copyright (C) 2013-2023 Laboratoire de Recherche // et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -98,11 +98,7 @@ namespace spot return true; if (this->acc_ref > other.acc_ref) return false; - if (this->acc_cand < other.acc_cand) - return true; - if (this->acc_cand > other.acc_cand) - return false; - return false; + return this->acc_cand < other.acc_cand; } }; diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index ca8928888..ed53929b3 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -93,13 +93,7 @@ namespace spot return true; if (states > r.states) return false; - - if (edges < r.edges) - return true; - if (edges > r.edges) - return false; - - return false; + return edges < r.edges; } inline bool operator>(const automaton_size& r) From 36e79ecca6314a220982131567e6302ac1ea4035 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 17:49:00 +0100 Subject: [PATCH 05/20] * spot/twaalgos/game.cc: Fix incorrect std::forward. --- spot/twaalgos/game.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index f5699bf49..df259b84a 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018, 2020-2022 Laboratoire de Recherche et +// Copyright (C) 2017-2018, 2020-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -1034,7 +1034,7 @@ namespace spot ("set_state_players(): There must be as many owners as states"); arena->set_named_prop("state-player", - new region_t(std::forward(owners))); + new region_t(std::move(owners))); } void set_state_player(twa_graph_ptr arena, unsigned state, bool owner) @@ -1101,7 +1101,7 @@ namespace spot throw std::runtime_error("set_strategy(): strategies need to have " "the same size as the automaton."); arena->set_named_prop("strategy", - new strategy_t(std::forward(strat))); + new strategy_t(std::move(strat))); } void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs) @@ -1152,7 +1152,7 @@ namespace spot ("set_state_winners(): There must be as many winners as states"); arena->set_named_prop("state-winner", - new region_t(std::forward(winners))); + new region_t(std::move(winners))); } void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner) From 4a78d1bff4fb113bdbd09b7989c527cfbd6339b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 23:34:10 +0100 Subject: [PATCH 06/20] fix some code smells reported by sonarcloud * bench/dtgbasat/gen.py, bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh: Various cleanups. --- bench/dtgbasat/gen.py | 6 ++-- bin/autcross.cc | 12 +++---- bin/autfilt.cc | 79 ++++++++++++++++++------------------------- bin/common_aoutput.cc | 12 +++---- bin/common_aoutput.hh | 8 ++--- 5 files changed, 51 insertions(+), 66 deletions(-) diff --git a/bench/dtgbasat/gen.py b/bench/dtgbasat/gen.py index e96bf2825..dabf77971 100755 --- a/bench/dtgbasat/gen.py +++ b/bench/dtgbasat/gen.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2016-2018, 2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -55,12 +55,12 @@ class BenchConfig(object): if line[0] == '#' or line.isspace(): continue elif line[0:2] == "sh": - sh = re.search('sh (.+?)$', line).group(1) + sh = re.search('sh (.+)$', line).group(1) continue else: name = re.search('(.+?):', line).group(1) code = re.search(':(.+?)>', line).group(1) - xoptions = re.search('>(.+?)$', line).group(1) + xoptions = re.search('>(.+)$', line).group(1) b = Bench(name=name, code=code, xoptions=xoptions) self.l.append(b) self.sh.append(sh) diff --git a/bin/autcross.cc b/bin/autcross.cc index 24cd9bcd4..b3e504bb3 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2017-2020, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -549,7 +549,7 @@ namespace { if (!quiet) std::cerr << "info: building " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) + << '*' << autname(j, !is_really_comp(j)) << " requires more acceptance sets than supported\n"; return false; } @@ -557,14 +557,14 @@ namespace if (verbose) std::cerr << "info: check_empty " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) << '\n'; + << '*' << autname(j, !is_really_comp(j)) << '\n'; auto w = aut_i->intersecting_word(aut_j); if (w) { std::ostream& err = global_error(); err << "error: " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) + << '*' << autname(j, !is_really_comp(j)) << (" is nonempty; both automata accept the infinite word:\n" " "); example() << *w << '\n'; @@ -613,7 +613,7 @@ namespace return src.str(); }(); - input_statistics.push_back(in_statistics()); + input_statistics.emplace_back(in_statistics()); input_statistics[round_num].input_source = std::move(source); if (auto name = input->get_named_prop("automaton-name")) @@ -658,7 +658,7 @@ namespace problems += prob; } spot::cleanup_tmpfiles(); - output_statistics.push_back(std::move(stats)); + output_statistics.emplace_back(std::move(stats)); if (verbose) { diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 7cff60e8b..b55d1bc9f 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -448,7 +448,7 @@ struct canon_aut std::vector edges; std::string acc; - canon_aut(const spot::const_twa_graph_ptr& aut) + explicit canon_aut(const spot::const_twa_graph_ptr& aut) : num_states(aut->num_states()) , edges(aut->edge_vector().begin() + 1, aut->edge_vector().end()) @@ -755,6 +755,22 @@ product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) return spot::product_or(left, right); } +static spot::twa_graph_ptr +word_to_aut(const char* word, const char *argname) +{ + try + { + return spot::parse_word(word, opt->dict)->as_automaton(); + } + catch (const spot::parse_error& e) + { + error(2, 0, "failed to parse the argument of --%s:\n%s", + argname, e.what()); + } + SPOT_UNREACHABLE(); + return nullptr; +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -776,17 +792,14 @@ parse_opt(int key, char* arg, struct argp_state*) opt_nth = parse_range(arg, 0, std::numeric_limits::max()); break; case 'u': - opt->uniq = std::unique_ptr(new std::set()); + opt->uniq = std::make_unique(); break; case 'v': opt_invert = true; break; case 'x': - { - const char* opt = extra_options.parse_options(arg); - if (opt) - error(2, 0, "failed to parse --options near '%s'", opt); - } + if (const char* opt = extra_options.parse_options(arg)) + error(2, 0, "failed to parse --options near '%s'", opt); break; case OPT_ALIASES: opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types); @@ -802,16 +815,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_art_sccs_set = true; break; case OPT_ACCEPT_WORD: - try - { - opt->acc_words.push_back(spot::parse_word(arg, opt->dict) - ->as_automaton()); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --accept-word:\n%s", - e.what()); - } + opt->acc_words.emplace_back(word_to_aut(arg, "accept-word")); break; case OPT_ACCEPTANCE_IS: { @@ -964,16 +968,7 @@ parse_opt(int key, char* arg, struct argp_state*) "%d should be followed by a comma and WORD", res); arg = endptr + 1; } - try - { - opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict) - ->as_automaton(), res); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --highlight-word:\n%s", - e.what()); - } + opt->hl_words.emplace_back(word_to_aut(arg, "highlight-word"), res); } break; case OPT_HIGHLIGHT_LANGUAGES: @@ -1157,16 +1152,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_art_sccs_set = true; break; case OPT_REJECT_WORD: - try - { - opt->rej_words.push_back(spot::parse_word(arg, opt->dict) - ->as_automaton()); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --reject-word:\n%s", - e.what()); - } + opt->rej_words.emplace_back(word_to_aut(arg, "reject-word")); break; case OPT_REM_AP: opt->rem_ap.add_ap(arg); @@ -1291,7 +1277,7 @@ namespace static bool match_acceptance(spot::twa_graph_ptr aut) { - auto& acc = aut->acc(); + const spot::acc_cond& acc = aut->acc(); switch (opt_acceptance_is) { case ACC_Any: @@ -1346,8 +1332,7 @@ namespace { bool max; bool odd; - bool is_p = acc.is_parity(max, odd, true); - if (!is_p) + if (!acc.is_parity(max, odd, true)) return false; switch (opt_acceptance_is) { @@ -1460,7 +1445,7 @@ namespace if (matched && opt_acceptance_is) matched = match_acceptance(aut); - if (matched && (opt_sccs_set | opt_art_sccs_set)) + if (matched && (opt_sccs_set || opt_art_sccs_set)) { spot::scc_info si(aut); unsigned n = si.scc_count(); @@ -1540,14 +1525,14 @@ namespace && spot::contains(aut, opt->equivalent_pos); if (matched && !opt->acc_words.empty()) - for (auto& word_aut: opt->acc_words) + for (const spot::twa_graph_ptr& word_aut: opt->acc_words) if (spot::product(aut, word_aut)->is_empty()) { matched = false; break; } if (matched && !opt->rej_words.empty()) - for (auto& word_aut: opt->rej_words) + for (const spot::twa_graph_ptr& word_aut: opt->rej_words) if (!spot::product(aut, word_aut)->is_empty()) { matched = false; @@ -1681,13 +1666,13 @@ namespace aut->accepting_run()->highlight(opt_highlight_accepting_run); if (!opt->hl_words.empty()) - for (auto& word_aut: opt->hl_words) + for (auto& [word_aut, color]: opt->hl_words) { if (aut->acc().uses_fin_acceptance()) error(2, 0, "--highlight-word does not yet work with Fin acceptance"); - if (auto run = spot::product(aut, word_aut.first)->accepting_run()) - run->project(aut)->highlight(word_aut.second); + if (auto run = spot::product(aut, word_aut)->accepting_run()) + run->project(aut)->highlight(color); } timer.stop(); diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index fcc79fc3c..60f83289e 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, const char* filename, int loc, - spot::process_timer& ptimer, + const spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix) { timer_ = ptimer; @@ -633,10 +633,10 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, outputnamer.print(haut, aut, f, filename, loc, ptimer, csv_prefix, csv_suffix); std::string fname = outputname.str(); - auto p = outputfiles.emplace(fname, nullptr); - if (p.second) - p.first->second.reset(new output_file(fname.c_str())); - out = &p.first->second->ostream(); + auto [it, b] = outputfiles.try_emplace(fname, nullptr); + if (b) + it->second.reset(new output_file(fname.c_str())); + out = &it->second->ostream(); } // Output it. diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index d33b687d2..f57beae84 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2018, 2020, 2022, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -155,7 +155,7 @@ public: print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, - const char* filename, int loc, spot::process_timer& ptimer, + const char* filename, int loc, const spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix); private: @@ -196,7 +196,7 @@ class automaton_printer std::map> outputfiles; public: - automaton_printer(stat_style input = no_input); + explicit automaton_printer(stat_style input = no_input); ~automaton_printer(); void From 7b0507a950a2734cdf2a7031d24286cd2ce88cb3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2023 23:43:31 +0100 Subject: [PATCH 07/20] bin: detect overflows in conversion functions * bin/common_conv.cc (to_int, to_unsigned): Here. * bin/common_range.cc (parse_range): And there. * tests/core/ltlgrind.test, tests/core/genaut.test, tests/core/randaut.test: Add test cases. --- bin/common_conv.cc | 15 ++++++++++++--- bin/common_range.cc | 22 ++++++++++++++-------- tests/core/genaut.test | 9 ++++++--- tests/core/ltlgrind.test | 5 ++++- tests/core/randaut.test | 7 +++++-- 5 files changed, 41 insertions(+), 17 deletions(-) diff --git a/bin/common_conv.cc b/bin/common_conv.cc index e63969b16..02b1815fd 100644 --- a/bin/common_conv.cc +++ b/bin/common_conv.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2018, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,10 +25,14 @@ int to_int(const char* s, const char* where) { char* endptr; - int res = strtol(s, &endptr, 10); + long int lres = strtol(s, &endptr, 10); if (*endptr) error(2, 0, "failed to parse '%s' as an integer (in argument of %s).", s, where); + int res = lres; + if (res != lres) + error(2, 0, "value '%s' is too large for an int (in argument of %s).", + s, where); return res; } @@ -45,11 +49,16 @@ unsigned to_unsigned (const char *s, const char* where) { char* endptr; - unsigned res = strtoul(s, &endptr, 10); + unsigned long lres = strtoul(s, &endptr, 10); if (*endptr) error(2, 0, "failed to parse '%s' as an unsigned integer (in argument of %s).", s, where); + unsigned res = lres; + if (res != lres) + error(2, 0, + "value '%s' is too large for a unsigned int (in argument of %s).", + s, where); return res; } diff --git a/bin/common_range.cc b/bin/common_range.cc index 8909a26c0..9419cc389 100644 --- a/bin/common_range.cc +++ b/bin/common_range.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2016 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2016, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -36,13 +36,16 @@ parse_range(const char* str, int missing_left, int missing_right) { range res; char* end; - res.min = strtol(str, &end, 10); + long lres = strtol(str, &end, 10); + res.min = lres; + if (res.min != lres) + error(2, 0, "start of range '%s' is too large for an int.", str); if (end == str) { // No leading number. It's OK as long as the string is not // empty. if (!*end) - error(1, 0, "invalid empty range"); + error(2, 0, "invalid empty range"); res.min = missing_left; } if (!*end) @@ -66,19 +69,22 @@ parse_range(const char* str, int missing_left, int missing_right) { // Parse the next integer. char* end2; - res.max = strtol(end, &end2, 10); + lres = strtol(end, &end2, 10); + res.max = lres; + if (res.max != lres) + error(2, 0, "end of range '%s' is too large for an int.", str); if (str == end2) - error(1, 0, "invalid range '%s' " + error(2, 0, "invalid range '%s' " "(should start with digits, dots, or colon)", str); if (end == end2) - error(1, 0, "invalid range '%s' (missing end?)", str); + error(2, 0, "invalid range '%s' (missing end?)", str); if (*end2) - error(1, 0, "invalid range '%s' (trailing garbage?)", str); + error(2, 0, "invalid range '%s' (trailing garbage?)", str); } } if (res.min < 0 || res.max < 0) - error(1, 0, "invalid range '%s': values must be positive", str); + error(2, 0, "invalid range '%s': values must be positive", str); return res; } diff --git a/tests/core/genaut.test b/tests/core/genaut.test index 5da9509ed..f364569e1 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2017-2020, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -60,7 +60,10 @@ genaut --l-nba='1..3?' 2>err && exit 1 grep 'invalid range.*trailing garbage' err genaut --l-nba='1..' 2>err && exit 1 grep 'invalid range.*missing end' err - +genaut --l-nba='9999999999999999999999999..' 2>err && exit 1 +grep 'start.*too large' err +genaut --l-nba='1..9999999999999999999999999' 2>err && exit 1 +grep 'end.*too large' err # Tests for autfilt -N/--nth genaut --ks-nca=1..5 | autfilt -N 2..4 > range1.hoa diff --git a/tests/core/ltlgrind.test b/tests/core/ltlgrind.test index 292756bc6..09e75ee4e 100755 --- a/tests/core/ltlgrind.test +++ b/tests/core/ltlgrind.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2019 Laboratoire de Recherche et Développement +# Copyright (C) 2014, 2015, 2019, 2023 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -198,3 +198,6 @@ checkopt_noparse -F input/2 --format '%<,%f,%>,%F,%L' <err && exit 1 +grep 'too large' err diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 7ff851646..50558e790 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2014-2018, 2020, 2022, 2023 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -29,6 +29,9 @@ grep "randaut: 3.1.*is not between 0 and 1 (in argument of -e" err randaut -n1a 3 2>err && exit 1 grep "randaut: failed to parse '1a' as an integer.* -n/--automata)" err +randaut -n99999999999999999999999999 3 2>err && exit 1 +grep "randaut:.*too large" err + randaut --spin -Q4 a b | ../ikwiad -H -XN - >out grep 'States: 4' out grep 'AP: 2' out From 39212bbcd27daa650f1851f57d0722424fb97ff0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Jan 2023 11:55:34 +0100 Subject: [PATCH 08/20] more code smells * bin/common_file.cc, bin/common_file.hh, bin/common_finput.cc, bin/common_finput.hh, bin/common_output.cc, bin/common_setup.cc, bin/common_setup.hh, bin/common_trans.cc, bin/common_trans.hh, bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlsynt.cc, bin/randltl.cc: Fix minor code issues reported by sonarcloud. --- bin/common_file.cc | 7 ++-- bin/common_file.hh | 13 +++---- bin/common_finput.cc | 10 ++---- bin/common_finput.hh | 16 +++++---- bin/common_output.cc | 20 +++++------ bin/common_setup.cc | 7 ++-- bin/common_setup.hh | 6 ++-- bin/common_trans.cc | 46 ++++++++++++------------ bin/common_trans.hh | 19 +++++----- bin/dstar2tgba.cc | 4 +-- bin/genaut.cc | 4 +-- bin/genltl.cc | 6 ++-- bin/ltl2tgba.cc | 8 ++--- bin/ltl2tgta.cc | 4 +-- bin/ltlcross.cc | 86 ++++++++++++++++---------------------------- bin/ltldo.cc | 14 +++----- bin/ltlfilt.cc | 20 +++++------ bin/ltlsynt.cc | 15 ++++---- bin/randltl.cc | 6 ++-- 19 files changed, 133 insertions(+), 178 deletions(-) diff --git a/bin/common_file.cc b/bin/common_file.cc index 005bb5479..4e56c6d54 100644 --- a/bin/common_file.cc +++ b/bin/common_file.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -21,7 +21,6 @@ #include #include - output_file::output_file(const char* name, bool force_append) { std::ios_base::openmode mode = std::ios_base::trunc; @@ -39,10 +38,10 @@ output_file::output_file(const char* name, bool force_append) os_ = &std::cout; return; } - of_ = new std::ofstream(name, mode); + of_ = std::make_unique(name, mode); if (!*of_) error(2, errno, "cannot open '%s'", name); - os_ = of_; + os_ = of_.get(); } diff --git a/bin/common_file.hh b/bin/common_file.hh index b8f9842b8..b6aa0bec3 100644 --- a/bin/common_file.hh +++ b/bin/common_file.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015-2016, 2022-2023 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,13 +21,13 @@ #include "common_sys.hh" #include +#include #include -#include class output_file { std::ostream* os_; - std::ofstream* of_ = nullptr; + std::unique_ptr of_; bool append_ = false; public: // Open a file for output. "-" is interpreted as stdout. @@ -37,11 +37,6 @@ public: void close(const std::string& name); - ~output_file() - { - delete of_; - } - bool append() const { return append_; diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 80aca5df7..dbcdb3849 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017, 2019, 2021, 2022 Laboratoire de Recherche +// Copyright (C) 2012-2017, 2019, 2021-2023 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -96,12 +96,6 @@ parse_formula(const std::string& s) (s, spot::default_environment::instance(), false, lenient); } -job_processor::job_processor() - : abort_run(false), real_filename(nullptr), - col_to_read(0), prefix(nullptr), suffix(nullptr) -{ -} - job_processor::~job_processor() { if (real_filename) @@ -370,7 +364,7 @@ int job_processor::run() { int error = 0; - for (auto& j: jobs) + for (const auto& j: jobs) { switch (j.type) { diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 2a5815fc3..9ecb5b025 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2017, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -56,9 +56,11 @@ spot::parsed_formula parse_formula(const std::string& s); class job_processor { protected: - bool abort_run; // Set to true in process_formula() to abort run(). + bool abort_run = false; // Set to true in process_formula() to abort run(). public: - job_processor(); + job_processor() = default; + job_processor(const job_processor&) = delete; + job_processor& operator=(const job_processor&) = delete; virtual ~job_processor(); @@ -84,10 +86,10 @@ public: virtual int run(); - char* real_filename; - long int col_to_read; - char* prefix; - char* suffix; + char* real_filename = nullptr; + long int col_to_read = 0; + char* prefix = nullptr; + char* suffix = nullptr; }; // Report and error message or add a default job depending on whether diff --git a/bin/common_output.cc b/bin/common_output.cc index e9c61a513..93cb2dfaf 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,6 +23,7 @@ #include "common_setup.hh" #include #include +#include #include #include #include @@ -297,9 +298,9 @@ namespace }; } -static formula_printer* format = nullptr; +static std::unique_ptr format; static std::ostringstream outputname; -static formula_printer* outputnamer = nullptr; +static std::unique_ptr outputnamer; static std::map> outputfiles; int @@ -320,7 +321,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) output_format = lbt_output; break; case 'o': - outputnamer = new formula_printer(outputname, arg); + outputnamer = std::make_unique(outputname, arg); break; case 'p': full_parenth = true; @@ -341,8 +342,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) output_format = wring_output; break; case OPT_FORMAT: - delete format; - format = new formula_printer(std::cout, arg); + format = std::make_unique(std::cout, arg); break; default: return ARGP_ERR_UNKNOWN; @@ -417,10 +417,10 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, formula_with_location fl = { f, filename, linenum, prefix, suffix }; outputnamer->print(fl, ptimer); std::string fname = outputname.str(); - auto p = outputfiles.emplace(fname, nullptr); - if (p.second) - p.first->second.reset(new output_file(fname.c_str())); - out = &p.first->second->ostream(); + auto [it, b] = outputfiles.try_emplace(fname, nullptr); + if (b) + it->second.reset(new output_file(fname.c_str())); + out = &it->second->ostream(); } output_formula(*out, f, ptimer, filename, linenum, prefix, suffix); *out << output_terminator; diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 24cacae85..af033a47f 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,13 +20,14 @@ #include "common_setup.hh" #include "common_aoutput.hh" -#include "argp.h" -#include "closeout.h" +#include +#include #include #include #include #include #include +#include #include static void diff --git a/bin/common_setup.hh b/bin/common_setup.hh index e2fce84e0..94cd16f4f 100644 --- a/bin/common_setup.hh +++ b/bin/common_setup.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2018, 2019 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012-2013, 2018-2019, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -34,5 +34,5 @@ int protected_main(char** progname, std::function mainfun); // Diagnose exceptions. [[noreturn]] void handle_any_exception(); -#define BEGIN_EXCEPTION_PROTECT try { (void)0; +#define BEGIN_EXCEPTION_PROTECT try { (void)0 #define END_EXCEPTION_PROTECT } catch (...) { handle_any_exception(); } diff --git a/bin/common_trans.cc b/bin/common_trans.cc index e34f3d77d..b93535173 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -53,7 +53,7 @@ struct shorthands_t }; #define SHORTHAND(PRE, POST) { PRE, std::regex("^" PRE), POST } -static shorthands_t shorthands_ltl[] = { +static const shorthands_t shorthands_ltl[] = { SHORTHAND("delag", " %f>%O"), SHORTHAND("lbt", " <%L>%O"), SHORTHAND("ltl2ba", " -f %s>%O"), @@ -73,7 +73,7 @@ static shorthands_t shorthands_ltl[] = { SHORTHAND("owl.* ltl-utilities\\b", " -f %f"), }; -static shorthands_t shorthands_autproc[] = { +static const shorthands_t shorthands_autproc[] = { SHORTHAND("autfilt", " %H>%O"), SHORTHAND("dra2dpa", " <%H>%O"), SHORTHAND("dstar2tgba", " %H>%O"), @@ -85,7 +85,7 @@ static shorthands_t shorthands_autproc[] = { " <%H>%O"), }; -static void show_shorthands(shorthands_t* begin, shorthands_t* end) +static void show_shorthands(const shorthands_t* begin, const shorthands_t* end) { std::cout << ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" @@ -100,7 +100,8 @@ static void show_shorthands(shorthands_t* begin, shorthands_t* end) } -tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, +tool_spec::tool_spec(const char* spec, + const shorthands_t* begin, const shorthands_t* end, bool is_ref) noexcept : spec(spec), cmd(spec), name(spec), reference(is_ref) { @@ -113,15 +114,15 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, { if (*pos == '{') ++count; - else if (*pos == '}') - if (!--count) - { - name = strndup(cmd + 1, pos - cmd - 1); - cmd = pos + 1; - while (*cmd == ' ' || *cmd == '\t') - ++cmd; - break; - } + else if (*pos == '}' && --count == 0) + { + name = strndup(cmd + 1, pos - cmd - 1); + cmd = pos + 1; + // skip leading whitespace + while (*cmd == ' ' || *cmd == '\t') + ++cmd; + break; + } } } // If there is no % in the string, look for a known @@ -147,11 +148,11 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, auto& p = *begin++; if (std::regex_search(basename, p.rprefix)) { - int m = strlen(p.suffix); - int q = strlen(cmd); + size_t m = strlen(p.suffix); + size_t q = strlen(cmd); char* tmp = static_cast(malloc(q + m + 1)); - strcpy(tmp, cmd); - strcpy(tmp + q, p.suffix); + memcpy(tmp, cmd, q); + memcpy(tmp + q, p.suffix, m + 1); cmd = tmp; allocated = true; break; @@ -490,9 +491,8 @@ read_stdout_of_command(char* const* args) if (close(cout_pipe[1]) < 0) error(2, errno, "closing write-side of pipe failed"); - std::string buffer(32, 0); std::string results; - int bytes_read; + ssize_t bytes_read; for (;;) { static char buffer[512]; @@ -612,7 +612,7 @@ get_arg(const char*& cmd) { const char* start = cmd; std::string arg; - while (int c = *cmd) + while (char c = *cmd) { switch (c) { @@ -642,14 +642,14 @@ get_arg(const char*& cmd) goto end_loop; case '\'': { - int d = 0; + char d = '\0'; while ((d = *++cmd)) { if (d == '\'') break; arg.push_back(d); } - if (d == 0) + if (d == '\0') return nullptr; } break; diff --git a/bin/common_trans.hh b/bin/common_trans.hh index 31c88c80c..0ebe59e8c 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -51,7 +51,8 @@ struct tool_spec // Whether the tool is a reference. bool reference; - tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, + tool_spec(const char* spec, + const shorthands_t* begin, const shorthands_t* end, bool is_ref) noexcept; tool_spec(const tool_spec& other) noexcept; tool_spec& operator=(const tool_spec& other); @@ -71,7 +72,7 @@ struct quoted_formula final: public spot::printable_value struct filed_formula final: public spot::printable { - filed_formula(const quoted_formula& ltl) : f_(ltl) + explicit filed_formula(const quoted_formula& ltl) : f_(ltl) { } @@ -89,9 +90,7 @@ struct filed_formula final: public spot::printable struct filed_automaton final: public spot::printable { - filed_automaton() - { - } + filed_automaton() = default; void print(std::ostream& os, const char* pos) const override; @@ -112,7 +111,7 @@ struct printable_result_filename final: unsigned translator_num; printable_result_filename(); - ~printable_result_filename(); + ~printable_result_filename() override; void reset(unsigned n); void cleanup(); @@ -126,7 +125,7 @@ protected: spot::bdd_dict_ptr dict; // Round-specific variables quoted_formula ltl_formula; - filed_formula filename_formula = ltl_formula; + filed_formula filename_formula{ltl_formula}; // Run-specific variables printable_result_filename output; public: @@ -151,9 +150,9 @@ protected: public: using spot::formater::has; - autproc_runner(// whether we accept the absence of output - // specifier - bool no_output_allowed = false); + explicit autproc_runner(// whether we accept the absence of output + // specifier + bool no_output_allowed = false); void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial); }; diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 5b60a0ecc..4b2ec9662 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019, 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019, 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,7 +117,7 @@ namespace spot::postprocessor& post; automaton_printer printer; - dstar_processor(spot::postprocessor& post) + explicit dstar_processor(spot::postprocessor& post) : hoa_processor(spot::make_bdd_dict()), post(post), printer(aut_input) { } diff --git a/bin/genaut.cc b/bin/genaut.cc index 26678c588..f8d6b93ff 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2017-2019, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -128,7 +128,7 @@ output_pattern(gen::aut_pattern_id pattern, int n) static void run_jobs() { - for (auto& j: jobs) + for (const auto& j: jobs) { int inc = (j.range.max < j.range.min) ? -1 : 1; int n = j.range.min; diff --git a/bin/genltl.cc b/bin/genltl.cc index 96d8bd7d3..ef8049171 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015-2019, 2022 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2015-2019, 2022-2023 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -317,7 +317,7 @@ output_pattern(gen::ltl_pattern_id pattern, int n, int n2) static void run_jobs() { - for (auto& j: jobs) + for (const auto& j: jobs) { int inc = (j.range.max < j.range.min) ? -1 : 1; int n = j.range.min; diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index d4fb2fc17..73a9a23c6 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2019, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -124,10 +124,10 @@ namespace { public: spot::translator& trans; - automaton_printer printer; + automaton_printer printer{ltl_input}; - trans_processor(spot::translator& trans) - : trans(trans), printer(ltl_input) + explicit trans_processor(spot::translator& trans) + : trans(trans) { } diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index ab925c7ac..60afcf9e8 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2020, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -168,7 +168,7 @@ namespace public: spot::translator& trans; - trans_processor(spot::translator& trans) + explicit trans_processor(spot::translator& trans) : trans(trans) { } diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 0dfa09985..3219beb75 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2020, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -264,55 +264,32 @@ end_error() struct statistics { - statistics() noexcept - : ok(false), - alternating(false), - status_str(nullptr), - status_code(0), - time(0), - states(0), - edges(0), - transitions(0), - acc(0), - scc(0), - nonacc_scc(0), - terminal_scc(0), - weak_scc(0), - strong_scc(0), - nondetstates(0), - nondeterministic(false), - terminal_aut(false), - weak_aut(false), - strong_aut(false) - { - } - // If OK is false, only the status_str, status_code, and time fields // should be valid. - bool ok; - bool alternating; - const char* status_str; - int status_code; - double time; - unsigned states; - unsigned edges; - unsigned long long transitions; - unsigned acc; - unsigned scc; - unsigned nonacc_scc; - unsigned terminal_scc; - unsigned weak_scc; - unsigned strong_scc; - unsigned nondetstates; - bool nondeterministic; - bool terminal_aut; - bool weak_aut; - bool strong_aut; + bool ok = false; + bool alternating = false; + const char* status_str = nullptr; + int status_code = 0; + double time = 0.0; + unsigned states = 0; + unsigned edges = 0; + unsigned long long transitions = 0; + unsigned acc = 0; + unsigned scc = 0; + unsigned nonacc_scc = 0; + unsigned terminal_scc = 0; + unsigned weak_scc = 0; + unsigned strong_scc = 0; + unsigned nondetstates = 0; + bool nondeterministic = false; + bool terminal_aut = false; + bool weak_aut = false; + bool strong_aut = false; std::vector product_states; std::vector product_transitions; std::vector product_scc; - bool ambiguous; - bool complete; + bool ambiguous = false; + bool complete = false; std::string hoa_str; static void @@ -581,7 +558,7 @@ namespace class xtranslator_runner final: public translator_runner { public: - xtranslator_runner(spot::bdd_dict_ptr dict) + explicit xtranslator_runner(spot::bdd_dict_ptr dict) : translator_runner(dict) { } @@ -1095,17 +1072,14 @@ namespace } // Make sure we do not translate the same formula twice. - if (!allow_dups) + if (!allow_dups && !unique_set.insert(f).second) { - if (!unique_set.insert(f).second) - { - if (!quiet) - std::cerr - << ("warning: This formula or its negation has already" - " been checked.\n Use --allow-dups if it " - "should not be ignored.\n\n"); - return 0; - } + if (!quiet) + std::cerr + << ("warning: This formula or its negation has already" + " been checked.\n Use --allow-dups if it " + "should not be ignored.\n\n"); + return 0; } int problems = 0; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index ffbd4873e..6e7bf5ec7 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020, 2022 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2020, 2022-2023 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -209,7 +209,7 @@ namespace class xtranslator_runner final: public translator_runner { public: - xtranslator_runner(spot::bdd_dict_ptr dict) + explicit xtranslator_runner(spot::bdd_dict_ptr dict) : translator_runner(dict, true) { } @@ -224,8 +224,6 @@ namespace format(command, tools[translator_num].cmd); std::string cmd = command.str(); - //std::cerr << "Running [" << l << translator_num << "]: " - // << cmd << std::endl; timer.start(); int es = exec_with_timeout(cmd.c_str()); timer.stop(); @@ -312,7 +310,7 @@ namespace spot::printable_value inputf; public: - processor(spot::postprocessor& post) + explicit processor(spot::postprocessor& post) : runner(dict), best_printer(best_stream, best_format), post(post) { printer.add_stat('T', &cmdname); @@ -323,9 +321,7 @@ namespace best_printer.declare('f', &inputf); } - ~processor() - { - } + ~processor() override = default; int process_string(const std::string& input, diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index c9064368d..81e895d42 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -586,7 +586,7 @@ namespace fset_t unique_set; spot::relabeling_map relmap; - ltl_processor(spot::tl_simplifier& simpl) + explicit ltl_processor(spot::tl_simplifier& simpl) : simpl(simpl) { } @@ -722,7 +722,7 @@ namespace matched &= !syntactic_si || f.is_syntactic_stutter_invariant(); if (matched && (ap_n.min > 0 || ap_n.max >= 0)) { - auto s = atomic_prop_collect(f); + spot::atomic_prop_set* s = atomic_prop_collect(f); int n = s->size(); delete s; matched &= (ap_n.min <= 0) || (n >= ap_n.min); @@ -761,7 +761,7 @@ namespace aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); if (matched && !opt->acc_words.empty()) - for (auto& word_aut: opt->acc_words) + for (const spot::twa_graph_ptr& word_aut: opt->acc_words) if (spot::product(aut, word_aut)->is_empty()) { matched = false; @@ -769,7 +769,7 @@ namespace } if (matched && !opt->rej_words.empty()) - for (auto& word_aut: opt->rej_words) + for (const spot::twa_graph_ptr& word_aut: opt->rej_words) if (!spot::product(aut, word_aut)->is_empty()) { matched = false; @@ -843,12 +843,12 @@ namespace { // Sort the formulas alphabetically. std::map m; - for (auto& p: relmap) - m.emplace(str_psl(p.first), p.second); - for (auto& p: m) + for (const auto& [newformula, oldname]: relmap) + m.emplace(str_psl(newformula), oldname); + for (const auto& [newname, oldname]: m) stream_formula(opt->output_define->ostream() - << "#define " << p.first << " (", - p.second, filename, + << "#define " << newname << " (", + oldname, filename, std::to_string(linenum).c_str()) << ")\n"; } one_match = true; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index aaea855a4..a2ec32cd1 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -152,7 +152,6 @@ static const struct argp_child children[] = { { &finput_argp_headless, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, - //{ &aoutput_o_format_argp, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, 0 }, { nullptr, 0, nullptr, 0 } }; @@ -425,10 +424,6 @@ namespace auto sub_o = sub_outs_str.begin(); std::vector mealy_machines; - auto print_game = want_game ? - [](const spot::twa_graph_ptr& game)->void { dispatch_print_hoa(game); } - : [](const spot::twa_graph_ptr&)->void{}; - for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { spot::mealy_like m_like @@ -466,9 +461,11 @@ namespace assert((spptr->at(arena->get_init_state_number()) == false) && "Env needs first turn"); } - print_game(arena); if (want_game) - continue; + { + dispatch_print_hoa(arena); + continue; + } if (!spot::solve_game(arena, *gi)) { if (show_status) @@ -625,7 +622,7 @@ namespace } static void - split_aps(std::string arg, std::vector& where) + split_aps(const std::string& arg, std::vector& where) { std::istringstream aps(arg); std::string ap; diff --git a/bin/randltl.cc b/bin/randltl.cc index 986c437c1..749fcf373 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2019, 2022 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2016, 2018-2019, 2022, 2023 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -65,7 +65,6 @@ enum { OPT_DUMP_PRIORITIES, OPT_DUPS, OPT_LTL_PRIORITIES, - OPT_PSL_PRIORITIES, OPT_SEED, OPT_SERE_PRIORITIES, OPT_TREE_SIZE, @@ -194,7 +193,6 @@ parse_opt(int key, char* arg, struct argp_state* as) case OPT_DUMP_PRIORITIES: opt_dump_priorities = true; break; - // case OPT_PSL_PRIORITIES: break; case OPT_SERE_PRIORITIES: opt_pS = arg; break; From 7e1d68479762a9ce5d66ec226d42ab23d0b38cbd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Jan 2023 11:59:49 +0100 Subject: [PATCH 09/20] dbranch: fix handling of states without successors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #524, reported by Rüdiger Ehlers. * spot/twaalgos/dbranch.cc: When merging an edge going to state without successors simply delete it. * bin/spot-x.cc: Typo in documentation. * tests/core/ltlcross.test: Add a test case. * NEWS: Mention the bug. --- NEWS | 4 ++++ bin/spot-x.cc | 4 ++-- spot/twaalgos/dbranch.cc | 39 +++++++++++++++++++++------------------ tests/core/ltlcross.test | 5 ++++- 4 files changed, 31 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 9775339fe..e6d484f12 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,10 @@ New in spot 2.11.3.dev (not yet released) multiple initial states (because Spot supports only one), the HOA parser could break state-based acceptance. (Issue #522.) + - delay_branching_here(), a new optimization of Spot 2.11 had an + incorrect handling of states without successors, causing some + segfaults. (Issue #524.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 1edb3f54e..964710dc1 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -53,7 +53,7 @@ implication-based simplifications are attempted. Defaults to 16.") }, { nullptr, 0, nullptr, 0, "Translation options:", 0 }, { DOC("ltl-split", "Set to 0 to disable the translation of automata \ as product or sum of subformulas.") }, - { DOC("branch-prop", "Set to 0 to disable branching-postponement \ + { DOC("branch-post", "Set to 0 to disable branching-postponement \ (done during translation, may create more states) and delayed-branching \ (almost similar, but done after translation to only remove states). \ Set to 1 to force branching-postponement, and to 2 \ diff --git a/spot/twaalgos/dbranch.cc b/spot/twaalgos/dbranch.cc index 465f8326e..19a0d9474 100644 --- a/spot/twaalgos/dbranch.cc +++ b/spot/twaalgos/dbranch.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2022-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -118,27 +118,30 @@ namespace spot continue; } unsigned mergedst = it2->second; - // we have to merge canddst into mergedst. This is as - // simple as: + // we have to merge canddst into mergedst. + // This is as simple as: // 1) connecting their list of transitions - unsigned& mergedfirst = g.state_storage(mergedst).succ; - unsigned& mergedlast = g.state_storage(mergedst).succ_tail; - unsigned& candfirst = g.state_storage(canddst).succ; unsigned& candlast = g.state_storage(canddst).succ_tail; - if (mergedlast) - aut->edge_storage(mergedlast).next_succ = candfirst; - else // mergedst had now successor - mergedfirst = candfirst; - mergedlast = candlast; - // 2) updating the source of the merged transitions - for (unsigned e2 = candfirst; e2 != 0;) + if (candlast) { - auto& edge = aut->edge_storage(e2); - edge.src = mergedst; - e2 = edge.next_succ; + unsigned& mergedfirst = g.state_storage(mergedst).succ; + unsigned& mergedlast = g.state_storage(mergedst).succ_tail; + unsigned& candfirst = g.state_storage(canddst).succ; + if (mergedlast) + aut->edge_storage(mergedlast).next_succ = candfirst; + else // mergedst had no successor + mergedfirst = candfirst; + mergedlast = candlast; + // 2) updating the source of the merged transitions + for (unsigned e2 = candfirst; e2 != 0;) + { + auto& edge = aut->edge_storage(e2); + edge.src = mergedst; + e2 = edge.next_succ; + } + // 3) deleting the edge to canddst. + candfirst = candlast = 0; } - // 3) deleting the edge to canddst. - candfirst = candlast = 0; it.erase(); // 4) updating succ_cand succ_cand[mergedst] += succ_cand[canddst]; diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test index 1a5806ba8..ebe20fb26 100755 --- a/tests/core/ltlcross.test +++ b/tests/core/ltlcross.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012-2014, 2016, 2019 Laboratoire de Recherche et +# Copyright (C) 2012-2014, 2016, 2019, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -65,3 +65,6 @@ ltlcross -D \ # Spot 2.8. We use ltl2tgba twice so ltlcross build cross-products. ltlcross --verbose ltl2tgba ltl2tgba \ -f '(G(F((a1)&(X(X(b1))))))&(G(F((a2)&(X(X(b2))))))&(G(F((a3)&(X(X(b3))))))' + +# Issue #524. +ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))' From eae91e97cd1b450ac75f121ac314c61691af3ff0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Jan 2023 15:25:06 +0100 Subject: [PATCH 10/20] robin_hood: update to version version 3.11.5 * spot/priv/robin_hood.hh: Update. * spot/priv/Makefile.am: Patch ROBIN_HOOD_IS_TRIVIALLY_COPYABLE to work around an issue with clang on Arch linux. --- spot/priv/Makefile.am | 10 ++++++++-- spot/priv/robin_hood.hh | 43 +++++++++++++++++++++++++++-------------- 2 files changed, 37 insertions(+), 16 deletions(-) diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am index d4e9cc77c..7ec7e6148 100644 --- a/spot/priv/Makefile.am +++ b/spot/priv/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2013-2019, 2021 Laboratoire de Recherche et +## Copyright (C) 2013-2019, 2021-2023 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -42,5 +42,11 @@ RH = $(GH)/robin-hood-hashing/master/src/include/robin_hood.h .PHONY: update update: wget $(RH) -O robin_hood.tmp || curl $(RH) -o robin_hood.tmp - sed 's/std::malloc/malloc/' robin_hood.tmp > $(srcdir)/robin_hood.hh +## Do not use std::malloc but malloc, because gnulib may replace it by +## rpl_malloc instead. Also disable to tests of __GNUC__ about +## ROBIN_HOOD_IS_TRIVIALLY_COPYABLE because (1) all versions of G++ we +## support have std::is_trivially_copyable, and (2) clang define +## __GNUC__ to some value that fail this test, and then warn that +## __has_trivial_copy is obsoleted. + sed 's/std::malloc/malloc/;/https:\/\/stackoverflow.com\/a\/31798726/{n;s/defined.*/false/}' robin_hood.tmp > $(srcdir)/robin_hood.hh rm -f robin_hood.tmp diff --git a/spot/priv/robin_hood.hh b/spot/priv/robin_hood.hh index 8c151d517..a4bc8beae 100644 --- a/spot/priv/robin_hood.hh +++ b/spot/priv/robin_hood.hh @@ -36,7 +36,7 @@ // see https://semver.org/ #define ROBIN_HOOD_VERSION_MAJOR 3 // for incompatible API changes #define ROBIN_HOOD_VERSION_MINOR 11 // for adding functionality in a backwards-compatible manner -#define ROBIN_HOOD_VERSION_PATCH 3 // for backwards-compatible bug fixes +#define ROBIN_HOOD_VERSION_PATCH 5 // for backwards-compatible bug fixes #include #include @@ -206,7 +206,7 @@ static Counts& counts() { // workaround missing "is_trivially_copyable" in g++ < 5.0 // See https://stackoverflow.com/a/31798726/48181 -#if defined(__GNUC__) && __GNUC__ < 5 +#if false # define ROBIN_HOOD_IS_TRIVIALLY_COPYABLE(...) __has_trivial_copy(__VA_ARGS__) #else # define ROBIN_HOOD_IS_TRIVIALLY_COPYABLE(...) std::is_trivially_copyable<__VA_ARGS__>::value @@ -1820,6 +1820,12 @@ public: InsertionState::key_found != idxAndState.second); } + template + iterator emplace_hint(const_iterator position, Args&&... args) { + (void)position; + return emplace(std::forward(args)...).first; + } + template std::pair try_emplace(const key_type& key, Args&&... args) { return try_emplace_impl(key, std::forward(args)...); @@ -1831,16 +1837,15 @@ public: } template - std::pair try_emplace(const_iterator hint, const key_type& key, - Args&&... args) { + iterator try_emplace(const_iterator hint, const key_type& key, Args&&... args) { (void)hint; - return try_emplace_impl(key, std::forward(args)...); + return try_emplace_impl(key, std::forward(args)...).first; } template - std::pair try_emplace(const_iterator hint, key_type&& key, Args&&... args) { + iterator try_emplace(const_iterator hint, key_type&& key, Args&&... args) { (void)hint; - return try_emplace_impl(std::move(key), std::forward(args)...); + return try_emplace_impl(std::move(key), std::forward(args)...).first; } template @@ -1854,16 +1859,15 @@ public: } template - std::pair insert_or_assign(const_iterator hint, const key_type& key, - Mapped&& obj) { + iterator insert_or_assign(const_iterator hint, const key_type& key, Mapped&& obj) { (void)hint; - return insertOrAssignImpl(key, std::forward(obj)); + return insertOrAssignImpl(key, std::forward(obj)).first; } template - std::pair insert_or_assign(const_iterator hint, key_type&& key, Mapped&& obj) { + iterator insert_or_assign(const_iterator hint, key_type&& key, Mapped&& obj) { (void)hint; - return insertOrAssignImpl(std::move(key), std::forward(obj)); + return insertOrAssignImpl(std::move(key), std::forward(obj)).first; } std::pair insert(const value_type& keyval) { @@ -1871,10 +1875,20 @@ public: return emplace(keyval); } + iterator insert(const_iterator hint, const value_type& keyval) { + (void)hint; + return emplace(keyval).first; + } + std::pair insert(value_type&& keyval) { return emplace(std::move(keyval)); } + iterator insert(const_iterator hint, value_type&& keyval) { + (void)hint; + return emplace(std::move(keyval)).first; + } + // Returns 1 if key is found, 0 otherwise. size_t count(const key_type& key) const { // NOLINT(modernize-use-nodiscard) ROBIN_HOOD_TRACE(this) @@ -2308,13 +2322,14 @@ private: auto const numElementsWithBuffer = calcNumElementsWithBuffer(max_elements); - // calloc also zeroes everything + // malloc & zero mInfo. Faster than calloc everything. auto const numBytesTotal = calcNumBytesTotal(numElementsWithBuffer); ROBIN_HOOD_LOG("std::calloc " << numBytesTotal << " = calcNumBytesTotal(" << numElementsWithBuffer << ")") mKeyVals = reinterpret_cast( - detail::assertNotNull(std::calloc(1, numBytesTotal))); + detail::assertNotNull(malloc(numBytesTotal))); mInfo = reinterpret_cast(mKeyVals + numElementsWithBuffer); + std::memset(mInfo, 0, numBytesTotal - numElementsWithBuffer * sizeof(Node)); // set sentinel mInfo[numElementsWithBuffer] = 1; From 9ca2927291f6338f69373683d45db686a0b5907f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Jan 2023 16:07:49 +0100 Subject: [PATCH 11/20] bin: update copyright year and laboratory name * bin/common_setup.cc: Here. --- bin/common_setup.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/common_setup.cc b/bin/common_setup.cc index af033a47f..c59ec0695 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -36,7 +36,7 @@ display_version(FILE *stream, struct argp_state*) fputs(program_name, stream); fputs(" (" PACKAGE_NAME ") " PACKAGE_VERSION "\n\ \n\ -Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita.\n\ +Copyright (C) 2023 Laboratoire de Recherche de l'Epita (LRE)\n\ License GPLv3+: \ GNU GPL version 3 or later .\n\ This is free software: you are free to change and redistribute it.\n\ From 315872a54b037a6a1206bfeb119618f8bf64b5ae Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Fri, 20 Jan 2023 15:57:46 +0100 Subject: [PATCH 12/20] ltlsynt: typo in doc * bin/ltlsynt.cc: here --- bin/ltlsynt.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index a2ec32cd1..35ac4194b 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -102,8 +102,8 @@ static const argp_option options[] = "whether to decompose the specification as multiple output-disjoint " "problems to solve independently (enabled by default)", 0 }, { "simplify", OPT_SIMPLIFY, "no|bisim|bwoa|sat|bisim-sat|bwoa-sat", 0, - "simplification to apply to the controler (no) nothing, " - "(bisim) bisimulation-based reduction, (bwoa) bissimulation-based " + "simplification to apply to the controller (no) nothing, " + "(bisim) bisimulation-based reduction, (bwoa) bisimulation-based " "reduction with output assignment, (sat) SAT-based minimization, " "(bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. Defaults " "to 'bwoa'.", 0 }, From a1c02856acfd5421f16c8fa22c182f3766b75e76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Jan 2023 11:35:14 +0100 Subject: [PATCH 13/20] autfilt: allow --highlight-word to work on Fin acceptance Fixes #523. * bin/autfilt.cc: Remove the restriction. * tests/core/acc_word.test: Add test case. * NEWS: Mention the fix. --- NEWS | 4 ++++ bin/autfilt.cc | 9 ++------- tests/core/acc_word.test | 20 +++++++++++++------- 3 files changed, 19 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index e6d484f12..10ecce97c 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,10 @@ New in spot 2.11.3.dev (not yet released) multiple initial states (because Spot supports only one), the HOA parser could break state-based acceptance. (Issue #522.) + - autfilt --highlight-word refused to work on automata with Fin + acceptance for historical reasons, however the code has been + perfectly able to handle this for a while. (Issue #523.) + - delay_branching_here(), a new optimization of Spot 2.11 had an incorrect handling of states without successors, causing some segfaults. (Issue #524.) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index b55d1bc9f..4487fad8b 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1667,13 +1667,8 @@ namespace if (!opt->hl_words.empty()) for (auto& [word_aut, color]: opt->hl_words) - { - if (aut->acc().uses_fin_acceptance()) - error(2, 0, - "--highlight-word does not yet work with Fin acceptance"); - if (auto run = spot::product(aut, word_aut)->accepting_run()) - run->project(aut)->highlight(color); - } + if (auto run = spot::product(aut, word_aut)->accepting_run()) + run->project(aut)->highlight(color); timer.stop(); if (opt->uniq) diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 53ce4b98e..5f3b6880b 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017, 2018, 2019 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2016-2019, 2023 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -91,6 +91,15 @@ State: 1 EOF diff expected out +ltl2tgba -G '(GF(a & X!a) -> GF(b & XXb)) & GFc' > aut.hoa +word='!a&!c;cycle{!a&b&!c;!a&c;!a&b&c}' +autfilt -H1.1 aut.hoa --highlight-word="$word" > out.hoa +grep spot.highlight.edges out.hoa >out.edges +cat >expected <stderr && exit 1 -test $? -eq 2 -grep 'highlight-word.*Fin' stderr - +# highlight-word used not to work with Fin acceptance, but it's ok now +ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1 ltlfilt -f 'GF!a' --accept-word 'cycle{!a}' From 126d9bc103b238a910b26cc54523883b42cba607 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Jan 2023 15:48:06 +0100 Subject: [PATCH 14/20] bin: fix number conversion routines on 32bit On 32bit archetectures, long int = int the current check for detecting values that overflow int will fail. Conversion routings should check errno. * bin/common_conv.cc, bin/common_range.cc: Here. --- bin/common_conv.cc | 12 ++++++++---- bin/common_range.cc | 6 ++++-- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/bin/common_conv.cc b/bin/common_conv.cc index 02b1815fd..b23a67c51 100644 --- a/bin/common_conv.cc +++ b/bin/common_conv.cc @@ -25,12 +25,13 @@ int to_int(const char* s, const char* where) { char* endptr; + errno = 0; long int lres = strtol(s, &endptr, 10); if (*endptr) error(2, 0, "failed to parse '%s' as an integer (in argument of %s).", s, where); int res = lres; - if (res != lres) + if (res != lres || errno == ERANGE) error(2, 0, "value '%s' is too large for an int (in argument of %s).", s, where); return res; @@ -49,13 +50,14 @@ unsigned to_unsigned (const char *s, const char* where) { char* endptr; + errno = 0; unsigned long lres = strtoul(s, &endptr, 10); if (*endptr) error(2, 0, "failed to parse '%s' as an unsigned integer (in argument of %s).", s, where); unsigned res = lres; - if (res != lres) + if (res != lres || errno == ERANGE) error(2, 0, "value '%s' is too large for a unsigned int (in argument of %s).", s, where); @@ -66,8 +68,9 @@ float to_float(const char* s, const char* where) { char* endptr; + errno = 0; float res = strtof(s, &endptr); - if (*endptr) + if (*endptr || errno == ERANGE) error(2, 0, "failed to parse '%s' as a float (in argument of %s)", s, where); return res; @@ -89,8 +92,9 @@ to_longs(const char* arg) while (*arg) { char* endptr; + errno = 0; long value = strtol(arg, &endptr, 10); - if (endptr == arg) + if (endptr == arg || errno) error(2, 0, "failed to parse '%s' as an integer.", arg); res.push_back(value); while (*endptr == ' ' || *endptr == ',') diff --git a/bin/common_range.cc b/bin/common_range.cc index 9419cc389..98e568b41 100644 --- a/bin/common_range.cc +++ b/bin/common_range.cc @@ -36,9 +36,10 @@ parse_range(const char* str, int missing_left, int missing_right) { range res; char* end; + errno = 0; long lres = strtol(str, &end, 10); res.min = lres; - if (res.min != lres) + if (res.min != lres || errno == ERANGE) error(2, 0, "start of range '%s' is too large for an int.", str); if (end == str) { @@ -69,9 +70,10 @@ parse_range(const char* str, int missing_left, int missing_right) { // Parse the next integer. char* end2; + errno = 0; lres = strtol(end, &end2, 10); res.max = lres; - if (res.max != lres) + if (res.max != lres || errno == ERANGE) error(2, 0, "end of range '%s' is too large for an int.", str); if (str == end2) error(2, 0, "invalid range '%s' " From 26660728674567f0a0ff97e1eb5a34aa38939955 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Jan 2023 15:54:39 +0100 Subject: [PATCH 15/20] * .gitlab-ci.yml: Use pipeline id to name volumes. --- .gitlab-ci.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a2006ee7f..348bacba1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -276,7 +276,7 @@ debpkg-stable: - stable script: - docker pull gitlab-registry.lre.epita.fr/spot/buildenv/debian:stable - - vol=spot-stable-$CI_COMMIT_SHA + - vol=spot-stable-$CI_COMMIT_SHA-$CI_PIPELINE_ID - docker volume create $vol - exitcode=0 - docker run -v $vol:/build/result --name helper-$vol gitlab-registry.lre.epita.fr/spot/buildenv/debian:stable ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? @@ -304,7 +304,7 @@ debpkg-stable-i386: needs: ["debpkg-stable"] script: - docker pull gitlab-registry.lre.epita.fr/spot/buildenv/debian-i386:stable - - vol=spot-stable-$CI_COMMIT_SHA + - vol=spot-stable-$CI_COMMIT_SHA-$CI_PIPELINE_ID - docker volume create $vol - exitcode=0 - docker create -v $vol:/build/result --name helper-$vol gitlab-registry.lre.epita.fr/spot/buildenv/debian-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? @@ -331,7 +331,7 @@ debpkg-unstable: - next script: - docker pull gitlab-registry.lre.epita.fr/spot/buildenv/debian - - vol=spot-unstable-$CI_COMMIT_SHA + - vol=spot-unstable-$CI_COMMIT_SHA-$CI_PIPELINE_ID - docker volume create $vol - exitcode=0 - docker run -v $vol:/build/result --name helper-$vol gitlab-registry.lre.epita.fr/spot/buildenv/debian ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? @@ -357,7 +357,7 @@ debpkg-unstable-i386: needs: ["debpkg-unstable"] script: - docker pull gitlab-registry.lre.epita.fr/spot/buildenv/debian-i386 - - vol=spot-unstable-$CI_COMMIT_SHA + - vol=spot-unstable-$CI_COMMIT_SHA-$CI_PIPELINE_ID - docker volume create $vol - exitcode=0 - docker create -v $vol:/build/result --name helper-$vol gitlab-registry.lre.epita.fr/spot/buildenv/debian-i386 ./bin-spot.sh -j${NBPROC-1} || exitcode=$? From 5969aa4925e52fbfd07e0edc6933fed3faf7ae20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 30 Jan 2023 17:51:48 +0100 Subject: [PATCH 16/20] work around gcc-snapshot warnings about dangling references * spot/twaalgos/game.hh, spot/twaalgos/game.cc (get_state_players, get_strategy, get_state_winners): Take argument by reference, not copy. * spot/twaalgos/synthesis.cc, spot/twaalgos/mealy_machine.cc: Replace auto by actual type for readability. --- spot/twaalgos/game.cc | 17 ++++++++++++++--- spot/twaalgos/game.hh | 12 ++++++++---- spot/twaalgos/mealy_machine.cc | 8 ++++---- spot/twaalgos/synthesis.cc | 10 +++++----- 4 files changed, 31 insertions(+), 16 deletions(-) diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index df259b84a..17f94a7e4 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1056,7 +1056,18 @@ namespace spot (*owners)[state] = owner; } - const region_t& get_state_players(const_twa_graph_ptr arena) + const region_t& get_state_players(const const_twa_graph_ptr& arena) + { + region_t *owners = arena->get_named_prop + ("state-player"); + if (!owners) + throw std::runtime_error + ("get_state_players(): state-player property not defined, not a game?"); + + return *owners; + } + + const region_t& get_state_players(twa_graph_ptr& arena) { region_t *owners = arena->get_named_prop ("state-player"); @@ -1081,7 +1092,7 @@ namespace spot } - const strategy_t& get_strategy(const_twa_graph_ptr arena) + const strategy_t& get_strategy(const const_twa_graph_ptr& arena) { auto strat_ptr = arena->get_named_prop("strategy"); if (!strat_ptr) @@ -1174,7 +1185,7 @@ namespace spot (*winners)[state] = winner; } - const region_t& get_state_winners(const_twa_graph_ptr arena) + const region_t& get_state_winners(const const_twa_graph_ptr& arena) { region_t *winners = arena->get_named_prop("state-winner"); if (!winners) diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index df5d27439..dbaccce75 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -163,14 +163,18 @@ namespace spot /// \ingroup games /// \brief Get the owner of all states + ///@{ SPOT_API - const region_t& get_state_players(const_twa_graph_ptr arena); + const region_t& get_state_players(const const_twa_graph_ptr& arena); + SPOT_API + const region_t& get_state_players(twa_graph_ptr& arena); + ///@} /// \ingroup games /// \brief Get or set the strategy /// @{ SPOT_API - const strategy_t& get_strategy(const_twa_graph_ptr arena); + const strategy_t& get_strategy(const const_twa_graph_ptr& arena); SPOT_API void set_strategy(twa_graph_ptr arena, const strategy_t& strat); SPOT_API @@ -214,5 +218,5 @@ namespace spot /// \ingroup games /// \brief Get the winner of all states SPOT_API - const region_t& get_state_winners(const_twa_graph_ptr arena); + const region_t& get_state_winners(const const_twa_graph_ptr& arena); } diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 1126ad8e0..386e44126 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2021, 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -3849,7 +3849,7 @@ namespace spot // 0 -> "Env" next is input props // 1 -> "Player" next is output prop - const auto& spref = get_state_players(mmw); + const region_t& spref = get_state_players(mmw); assert((spref.size() == mmw->num_states()) && "Inconsistent state players"); @@ -3989,9 +3989,9 @@ namespace spot const unsigned initl = left->get_init_state_number(); const unsigned initr = right->get_init_state_number(); - auto& spr = get_state_players(right); + const region_t& spr = get_state_players(right); #ifndef NDEBUG - auto& spl = get_state_players(left); + const region_t& spl = get_state_players(left); // todo auto check_out = [](const const_twa_graph_ptr& aut, const auto& sp) diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 88e22ff04..494cc0f1f 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2020-2022 Laboratoire de Recherche et +// Copyright (C) 2020-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -137,12 +137,12 @@ namespace{ // Note, this only deals with deterministic strategies // Note, assumes that env starts playing twa_graph_ptr - apply_strategy(const twa_graph_ptr& arena, + apply_strategy(const const_twa_graph_ptr& arena, bool unsplit, bool keep_acc) { - const auto& win = get_state_winners(arena); - const auto& strat = get_strategy(arena); - const auto& sp = get_state_players(arena); + const region_t& win = get_state_winners(arena); + const strategy_t& strat = get_strategy(arena); + const region_t& sp = get_state_players(arena); auto outs = get_synthesis_outputs(arena); if (!win[arena->get_init_state_number()]) From 058975c167bfe9af29475e593b133e4f249f4760 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Feb 2023 09:35:46 +0100 Subject: [PATCH 17/20] dbranch: fix handling of state-based acceptance Fixes issue #525. * spot/twaalgos/dbranch.hh, NEWS: Document. * spot/twaalgos/dbranch.cc: Detect cases where the acceptance should be changed from state-based to transition-based. * tests/python/dbranch.py: Add a test case. --- NEWS | 4 ++++ spot/twaalgos/dbranch.cc | 19 +++++++++++++++++-- spot/twaalgos/dbranch.hh | 15 ++++++++++----- tests/python/dbranch.py | 29 ++++++++++++++++++++++++++++- 4 files changed, 59 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 10ecce97c..c734fb995 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,10 @@ New in spot 2.11.3.dev (not yet released) incorrect handling of states without successors, causing some segfaults. (Issue #524.) + - Running delay_branching_here() on state-based automata (this was not + done in Spot so far) may require the output to use transition-based + acceptance. (Issue #525.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/spot/twaalgos/dbranch.cc b/spot/twaalgos/dbranch.cc index 19a0d9474..7cf1b262e 100644 --- a/spot/twaalgos/dbranch.cc +++ b/spot/twaalgos/dbranch.cc @@ -66,6 +66,10 @@ namespace spot hashmap_t first_dest[1 + is_game]; auto& g = aut->get_graph(); + // Merging outgoing transitions may cause the automaton to need + // transition-based acceptance. + bool need_trans = !aut->prop_state_acc().is_true(); + // setup a DFS std::vector seen(ns); std::stack todo; @@ -128,9 +132,18 @@ namespace spot unsigned& mergedlast = g.state_storage(mergedst).succ_tail; unsigned& candfirst = g.state_storage(canddst).succ; if (mergedlast) - aut->edge_storage(mergedlast).next_succ = candfirst; + { + aut->edge_storage(mergedlast).next_succ = candfirst; + // Do we need to require transition-based acceptance? + if (!need_trans) + need_trans = + (aut->edge_storage(candfirst).acc + != aut->edge_storage(mergedfirst).acc); + } else // mergedst had no successor - mergedfirst = candfirst; + { + mergedfirst = candfirst; + } mergedlast = candlast; // 2) updating the source of the merged transitions for (unsigned e2 = candfirst; e2 != 0;) @@ -149,6 +162,8 @@ namespace spot changed = true; } } + if (need_trans) + aut->prop_state_acc(false); return changed; } } diff --git a/spot/twaalgos/dbranch.hh b/spot/twaalgos/dbranch.hh index 9cd0efa5e..022c1a75b 100644 --- a/spot/twaalgos/dbranch.hh +++ b/spot/twaalgos/dbranch.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,10 +26,15 @@ namespace spot /// \ingroup twa_algorithms /// \brief Merge states to delay /// - /// If a state (x) has two outgoing transitions (x,l,m,y) and - /// (x,l,m,z) going to states (x) and (y) that have no other - /// incoming edges, then (y) and (z) can be merged (keeping the - /// union of their outgoing destinations). + /// In an automaton with transition-based acceptance, if a state (x) + /// has two outgoing transitions (x,l,m,y) and (x,l,m,z) going to + /// states (x) and (y) that have no other incoming edges, then (y) + /// and (z) can be merged (keeping the union of their outgoing + /// destinations). + /// + /// If the input automaton uses state-based acceptance, running this + /// function might make the acceptance transition-based, but only if + /// two states with different acceptance are merged at some point. /// /// \return true iff the automaton was modified. SPOT_API bool delay_branching_here(const twa_graph_ptr& aut); diff --git a/tests/python/dbranch.py b/tests/python/dbranch.py index ecf17d7d0..268c4a3c6 100644 --- a/tests/python/dbranch.py +++ b/tests/python/dbranch.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2022 Laboratoire de Recherche et +# Copyright (C) 2022, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -145,3 +145,30 @@ State: 5 State: 6 [t] 6 --END--""") + +# Running delay_branching_here on state-based acceptance may require +# the output to use transition-based acceptance. (Issue #525.) +a = spot.automaton(""" +HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" Acceptance: 1 Inf(0) --BODY-- +State: 0 [0] 1 [0] 2 State: 1 [1] 3 State: 2 {0} [!1] 3 State: 3 [t] 0 +--END--""") +copy = spot.make_twa_graph(a, spot.twa_prop_set.all()) +if spot.delay_branching_here(a): + a.purge_unreachable_states() +tc.assertTrue(spot.are_equivalent(a, copy)) +tc.assertEqual(a.to_str(), """HOA: v1 +States: 3 +Start: 0 +AP: 2 "b" "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[1] 1 +State: 1 +[0] 2 +[!0] 2 {0} +State: 2 +[t] 0 +--END--""") From 6fd0eebad4ccfe29bf98f6b17d1c603570236f0f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Feb 2023 14:40:20 +0100 Subject: [PATCH 18/20] to_finit: fix issue #526 * spot/twaalgos/remprop.cc: Use bdd_restrict instead of bdd_exists. * tests/core/ltlf.test: Add test case. * NEWS: Mention the bug. --- NEWS | 4 ++++ spot/twaalgos/remprop.cc | 6 ++--- tests/core/ltlf.test | 51 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 57 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index c734fb995..0886eb41d 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,10 @@ New in spot 2.11.3.dev (not yet released) done in Spot so far) may require the output to use transition-based acceptance. (Issue #525.) + - to_finite(), introduce in 2.11, had a bug that could break the + completeness of automata and trigger an exception from the HOA + printer. (Issue #526.) + New in spot 2.11.3 (2022-12-09) Bug fixes: diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 942a1b4b5..8d4be8fbc 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019, 2022 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2019, 2022, 2023 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -205,7 +205,7 @@ namespace spot } else { - e.cond = bdd_exist(e.cond, rem); + e.cond = bdd_restrict(e.cond, rem); } } diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test index 11f2132ac..74a2da79e 100755 --- a/tests/core/ltlf.test +++ b/tests/core/ltlf.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2022, 2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -173,3 +173,52 @@ grep -v '\[f\]' out4 > out3 cmp out3 out4 && exit 1 # make sure we did remove something autfilt out3 > out4 diff out4 expected3 + +# Issue #526 +ltlfilt -f '(i->XXo)|G(i<->Xo2)' --from-ltlf | ltl2tgba -D |\ + autfilt -C --to-finite > out +cat >exp < Date: Fri, 10 Feb 2023 08:49:26 +0100 Subject: [PATCH 19/20] Release spot 2.11.4 * NEWS, configure.ac, doc/org/setup.org: Update version. --- NEWS | 2 +- configure.ac | 4 ++-- doc/org/setup.org | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 0886eb41d..7a8ab4e46 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.11.3.dev (not yet released) +New in spot 2.11.4 (2023-02-10) Python: diff --git a/configure.ac b/configure.ac index 68fe4cab7..4643c0b66 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008-2022, Laboratoire de Recherche et Développement +# Copyright (C) 2008-2023, Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.11.3.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.11.4], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index 78091ea45..7b6a4fa70 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.11.3 -#+MACRO: LASTRELEASE 2.11.3 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.11.3.tar.gz][=spot-2.11.3.tar.gz=]] +#+MACRO: SPOTVERSION 2.11.4 +#+MACRO: LASTRELEASE 2.11.4 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.11.3.tar.gz][=spot-2.11.4.tar.gz=]] #+MACRO: LASTNEWS [[https://gitlab.lre.epita.fr/spot/spot/blob/spot-2-11-3/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2022-12-09 +#+MACRO: LASTDATE 2023-02-10 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From e44cb5152aeebada10578f7bbd2788b701edf0da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Feb 2023 08:51:29 +0100 Subject: [PATCH 20/20] Bump version to 2.11.4.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 7a8ab4e46..7f3be814d 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.11.4.dev (not yet released) + + Nothing yet. + New in spot 2.11.4 (2023-02-10) Python: diff --git a/configure.ac b/configure.ac index 4643c0b66..e47e2eb29 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.11.4], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.11.4.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])