diff --git a/NEWS b/NEWS index 718118058..d54f1b670 100644 --- a/NEWS +++ b/NEWS @@ -48,6 +48,9 @@ New in spot 2.9.3.dev (not yet released) - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which used to take ages are now instantaneous. (See issue #412.) + - remove_fin() learned to remove more unnecessary edges by using + propagate_marks_vector(). + Bugs fixed: - Handle xor and <-> in a more natural way when translating diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 647675610..e812fdd05 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -26,6 +26,7 @@ #include #include #include +#include // #define TRACE #ifdef TRACE @@ -621,6 +622,17 @@ namespace spot bool sbacc = res->prop_state_acc().is_true(); scc_info si(aut, scc_info_options::TRACK_STATES); unsigned nscc = si.scc_count(); + + // Help remove more useless transition by propagating marks. + auto propmarks = propagate_marks_vector(aut, &si); + + // Edges that are already satisfying the acceptance of the + // main copy do not need to be duplicated in the clones, so + // we fill allacc_edge to remember those. Of course this is + // only needed if the main copy can be accepting and if we + // will create clones. + std::vector allacc_edge(aut->edge_vector().size(), false); + std::vector state_map(nst); for (unsigned n = 0; n < nscc; ++n) { @@ -668,10 +680,11 @@ namespace spot a = (t.acc & main_sets) | main_add; res->new_edge(s, t.dst, t.cond, a); // remember edges that are completely accepting - if (check_main_acc && main_acc.accepting(a)) - allacc_edge[aut->edge_number(t)] = true; + if (check_main_acc) + if (unsigned en = aut->edge_number(t); + main_acc.accepting(a | (propmarks[en] & main_sets))) + allacc_edge[en] = true; } - // We do not need any other copy if the SCC is non-accepting, // of if it does not intersect any Fin. if (!intersects_fin) @@ -693,12 +706,16 @@ namespace spot auto ns = state_map[s]; for (auto& t: aut->out(s)) { - if ((t.acc & r) || si.scc_of(t.dst) != n - // edges that are already accepting in the - // main copy need not be copied in the - // clone, since cycles going through them - // are already accepted. - || allacc_edge[aut->edge_number(t)]) + if (unsigned en = aut->edge_number(t); + // Ignore edges have r, or that + // necessarily go through r. + ((t.acc | propmarks[en]) & r) + // Ignore edges between SCCs. + || si.scc_of(t.dst) != n + // Ignore edges that are already accepting + // in the main copy need not be copied in + // the clone. + || allacc_edge[en]) continue; auto nd = state_map[t.dst]; res->new_edge(ns, nd, t.cond, (t.acc & k) | a); diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 52ca43b89..928820e6d 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -877,14 +877,12 @@ State: 0 State: 1 [2] 0 [!2] 1 -[0&2] 2 [0&!2] 3 [2] 4 [!2] 5 State: 2 [0] 2 {0 2} State: 3 -[0&2] 2 {0 2} [0&!2] 3 {0} State: 4 [1 | 2] 4 {1 2} @@ -1457,7 +1455,7 @@ State: 3 [1] 3 --END-- HOA: v1 -States: 6 +States: 5 Start: 0 AP: 3 "a" "b" "c" acc-name: Buchi @@ -1468,25 +1466,20 @@ State: 0 [t] 0 [!1&!2] 1 [0] 2 -[1 | 2] 4 +[1 | 2] 3 State: 1 [2] 0 [!2] 1 -[0&2] 2 -[0&!2] 3 -[2] 4 -[!2] 5 +[2] 3 +[!2] 4 State: 2 [0] 2 {0} State: 3 -[0&2] 2 -[0&!2] 3 +[1 | 2] 3 {0} +[!1&!2] 4 State: 4 -[1 | 2] 4 {0} -[!1&!2] 5 -State: 5 -[2] 4 {0} -[!2] 5 +[2] 3 {0} +[!2] 4 --END-- EOF diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index c903015cc..ded6bcc4e 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c04b0> >" + " *' at 0x7f5bd494e1b0> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c09f0> >" + " *' at 0x7f5bd494e090> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c00f0> >" + " *' at 0x7f5bd494e7e0> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c0c00> >" + " *' at 0x7f5bd494eae0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c05a0> >" + " *' at 0x7f5bd494ede0> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c0ab0> >" + " *' at 0x7f5bd494e630> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382df240> >" + " *' at 0x7f5bd49052d0> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfc90> >" + " *' at 0x7f5bd4905cf0> >" ] }, "metadata": {}, @@ -1831,188 +1831,174 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ") | (Inf(\n", - "❶\n", - ")&Inf(\n", - "❷\n", - "))\n", - "[Fin-less 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ") | (Inf(\n", + "❶\n", + ")&Inf(\n", + "❷\n", + "))\n", + "[Fin-less 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "❷\n", + "\n", + "\n", + "1\n", + "❷\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", - "❷\n", + "\n", + "\n", + "a\n", + "❶\n", + "❷\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "❷\n", + "\n", + "\n", + "!a\n", + "❷\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "❷\n", + "\n", + "\n", + "b\n", + "❷\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "❷\n", + "\n", + "\n", + "a & b\n", + "❷\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "❶\n", - "❷\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "❷\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "4->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f37382dfc30> >" + " *' at 0x7f5bd4905cc0> >" ] }, "metadata": {}, @@ -2027,171 +2013,150 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "2\n", "\n", "\n", - "\n", + "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "1->4\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "\n", + "\n", "2->4\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", - "\n", + "\n", "3->4\n", - "\n", - "\n", - "!a | !b\n", + "\n", + "\n", + "!a | !b\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f37382dfed0> >" + " *' at 0x7f5bd4905f90> >" ] }, "metadata": {}, @@ -2206,11 +2171,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2255,91 +2220,91 @@ "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", + "\n", "3->0\n", - "\n", + "\n", "\n", - "!b\n", + "!b\n", "\n", "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", + "3->2\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f37382dfa80> >" + " *' at 0x7f5bd4905ae0> >" ] }, "metadata": {}, @@ -2528,7 +2493,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382df1b0> >" + " *' at 0x7f5bd4905720> >" ] }, "execution_count": 19, @@ -2604,7 +2569,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfae0> >" + " *' at 0x7f5bd4905a80> >" ] }, "execution_count": 20, @@ -3154,7 +3119,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfe10> >" + " *' at 0x7f5bd49055d0> >" ] }, "metadata": {}, @@ -3254,7 +3219,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382c0e10> >" + " *' at 0x7f5bd4905ed0> >" ] }, "execution_count": 24, @@ -3327,7 +3292,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfba0> >" + " *' at 0x7f5bd4905420> >" ] }, "execution_count": 25, @@ -3498,7 +3463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfc00> >" + " *' at 0x7f5bd494e990> >" ] }, "execution_count": 27, @@ -3581,7 +3546,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfe10> >" + " *' at 0x7f5bd49055d0> >" ] }, "metadata": {}, @@ -3646,7 +3611,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfe10> >" + " *' at 0x7f5bd49055d0> >" ] }, "metadata": {}, @@ -3733,7 +3698,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f37382dfe10> >" + " *' at 0x7f5bd49055d0> >" ] }, "execution_count": 29, @@ -3766,7 +3731,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.4" + "version": "3.8.5" } }, "nbformat": 4, diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 7eb9ab4d2..4cede285c 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -92,4 +92,4 @@ State: 2 """) b = spot.remove_fin(a) size = (b.num_states(), b.num_edges()) -assert size == (5, 17); +assert size == (5, 15); diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 7af498c46..ce33c63ac 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -158,7 +158,10 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do $GREP '[ ]if ([^()]*).*{' $tmp && diag 'Opening { should be on its own line.' - $GREP '[ ]if (.*).*;' $tmp && + $GREP '[ ]if ([^()]*).*;' $tmp && + diag 'if body should be on another line.' + + $GREP '[ ]if ([^()]*([^()]*)[^()]*).*;' $tmp && diag 'if body should be on another line.' $GREP '[ ]else.*;' $tmp &&