alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

translate: speed up some -G -D cases

Browse source 
When gf-guarentee works and produce a deterministic automaton, use it
right away without comparing it with the automaton produced by the
regular translation.  This used to be the case for all -D scenarios
except -G -D.

Reported by Florian Renkin.

* spot/twaalgos/translate.cc: Use the result of
gf_guarantee_to_ba_maybe() or fg_safety_to_dca_maybe() whenever -D is
used.
* spot/twaalgos/postproc.cc: Call remove_unused_ap() in finalize(), to
iron out some slight output differences.
* tests/core/ltl2tgba2.test, tests/python/toparity.py: Lower expected
results in the test cases.
* tests/python/automata.ipynb, tests/core/prodor.test: Adjust to new
order.
This commit is contained in:
Alexandre Duret-Lutz 2021-01-27 11:03:11 +01:00
parent 238a9ffc1d
commit 93d8f43285
6 changed files with 50 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

7
spot/twaalgos/postproc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement // Copyright (C) 2012-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -208,6 +208,8 @@ namespace spot
twa_graph_ptr twa_graph_ptr
postprocessor::finalize(twa_graph_ptr tmp) const postprocessor::finalize(twa_graph_ptr tmp) const
{ {
if (PREF_ != Any && level_ != Low)
tmp->remove_unused_ap();
if (COMP_) if (COMP_)
tmp = complete(tmp); tmp = complete(tmp);
bool want_parity = type_ & Parity; bool want_parity = type_ & Parity;
@ -364,7 +366,6 @@ namespace spot
if (m->num_states() <= a->num_states()) if (m->num_states() <= a->num_states())
a = m; a = m;
} }
a->remove_unused_ap();
} }
return finalize(a); return finalize(a);
} }
@ -666,8 +667,6 @@ namespace spot
sim = dba ? dba : sim; sim = dba ? dba : sim;
sim->remove_unused_ap();
if (type_ == CoBuchi) if (type_ == CoBuchi)
{ {
unsigned ns = sim->num_states(); unsigned ns = sim->num_states();

11
spot/twaalgos/translate.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement // Copyright (C) 2013-2018, 2020-2021 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -383,17 +383,14 @@ namespace spot
|| type_ == GeneralizedBuchi) || type_ == GeneralizedBuchi)
aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(),
det, state_based_); det, state_based_);
if (aut2 && (type_ & (Buchi | Parity)) if (aut2 && (pref_ & Deterministic))
&& (pref_ & Deterministic))
return finalize(aut2); return finalize(aut2);
if (!aut2 && (type_ == Generic if (!aut2 && (type_ == Generic
|| type_ & (Parity | CoBuchi))) || type_ & (Parity | CoBuchi)))
{ {
aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(),
state_based_); state_based_);
if (aut2 if (aut2 && (pref_ & Deterministic))
&& (type_ & (CoBuchi | Parity))
&& (pref_ & Deterministic))
return finalize(aut2); return finalize(aut2);
} }
} }

6
tests/core/ltl2tgba2.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de # Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -376,8 +376,8 @@ cat >formulas <<EOF
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14, 4,8 GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14, 4,8
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30, 8,16 GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30, 8,16
GF(((a & Xb) | XXc) & Xd), 3,58, 4,64, 3,58, 5,80, 4,64 GF(((a & Xb) | XXc) & Xd), 3,58, 4,64, 3,58, 5,80, 4,64
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12, 2,4 GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,6, 2,4
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8, 3,6 G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8, 2,4
G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0, 1,0 G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0, 1,0
FG(a | Fb), 3,15, 3,15, 3,15, 3,15, 1,4 FG(a | Fb), 3,15, 3,15, 3,15, 3,15, 1,4
FG(a & Fb), 2,7, 2,7, 3,9, 3,9, 1,4 FG(a & Fb), 2,7, 2,7, 3,9, 3,9, 1,4

22
tests/core/prodor.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2017-2018, 2021 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -63,21 +63,21 @@ properties: trans-labels explicit-labels trans-acc complete
properties: stutter-invariant properties: stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
[!0] 0
[0] 0 {0} [0] 0 {0}
[!0] 0
[0&1] 1 {0}
[!0&1] 1 [!0&1] 1
[0&1] 1 {0}
State: 1 State: 1
[!0&1] 1 {0}
[0&1] 1 {0} [0&1] 1 {0}
[!0&!1] 2 {0} [!0&1] 1 {0}
[0&!1] 2 {0} [0&!1] 2 {0}
[!0&!1] 2 {0}
State: 2 State: 2
[!0] 2
[0] 2 {0} [0] 2 {0}
[!0] 2
--END-- --END--
EOF EOF
diff por.hoa exp diff -u por.hoa exp
test 2 = `autfilt -c --intersect por.hoa gfa.hoa fgb.hoa` test 2 = `autfilt -c --intersect por.hoa gfa.hoa fgb.hoa`
@ -94,13 +94,13 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
[!0] 0
[0] 0 [0] 0
[!0&1] 1 [!0] 0
[0&1] 1 [0&1] 1
State: 1
[!0&1] 1 [!0&1] 1
State: 1
[0&1] 1 {0} [0&1] 1 {0}
[!0&1] 1
--END-- --END--
EOF EOF
diff pand.hoa exp diff pand.hoa exp

52
tests/python/automata.ipynb
View file

@ -178,7 +178,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc69c0f16c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43cde71b0> >"
] ]
}, },
"execution_count": 2, "execution_count": 2,
@ -657,7 +657,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d909240> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c131fc0> >"
] ]
}, },
"execution_count": 6, "execution_count": 6,
@ -733,7 +733,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d9099c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c1563c0> >"
] ]
}, },
"execution_count": 7, "execution_count": 7,
@ -816,7 +816,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc69e19d9c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c131ba0> >"
] ]
}, },
"execution_count": 8, "execution_count": 8,
@ -1349,7 +1349,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d916150> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156e40> >"
] ]
}, },
"execution_count": 12, "execution_count": 12,
@ -1463,7 +1463,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d916450> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c163300> >"
] ]
}, },
"execution_count": 13, "execution_count": 13,
@ -1594,7 +1594,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d916a20> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c163810> >"
] ]
}, },
"execution_count": 14, "execution_count": 14,
@ -1816,7 +1816,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91ca20> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c1694b0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1974,7 +1974,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c9c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c163210> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2132,7 +2132,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91cd80> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c169180> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2280,7 +2280,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91ccc0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c169360> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2469,7 +2469,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91cb40> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c169210> >"
] ]
}, },
"execution_count": 19, "execution_count": 19,
@ -2545,7 +2545,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d925690> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c169fc0> >"
] ]
}, },
"execution_count": 20, "execution_count": 20,
@ -3095,7 +3095,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c480> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156ea0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3195,7 +3195,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c510> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156210> >"
] ]
}, },
"execution_count": 24, "execution_count": 24,
@ -3254,21 +3254,21 @@
"<title>0&#45;&gt;0</title>\n", "<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M55.26,-35.78C54.71,-45.31 55.79,-54 58.5,-54 60.49,-54 61.6,-49.32 61.83,-43.05\"/>\n", "<path fill=\"none\" stroke=\"black\" d=\"M55.26,-35.78C54.71,-45.31 55.79,-54 58.5,-54 60.49,-54 61.6,-49.32 61.83,-43.05\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"61.74,-35.78 64.98,-42.74 61.78,-39.28 61.83,-42.78 61.83,-42.78 61.83,-42.78 61.78,-39.28 58.68,-42.82 61.74,-35.78 61.74,-35.78\"/>\n", "<polygon fill=\"black\" stroke=\"black\" points=\"61.74,-35.78 64.98,-42.74 61.78,-39.28 61.83,-42.78 61.83,-42.78 61.83,-42.78 61.78,-39.28 58.68,-42.82 61.74,-35.78 61.74,-35.78\"/>\n",
"<text text-anchor=\"start\" x=\"55\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n", "<text text-anchor=\"start\" x=\"53\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"<text text-anchor=\"start\" x=\"50.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n", "</g>\n",
"<!-- 0&#45;&gt;0 -->\n", "<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n", "<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n", "<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M53.18,-35.42C50.15,-52.79 51.93,-72 58.5,-72 64.2,-72 66.29,-57.55 64.77,-42.39\"/>\n", "<path fill=\"none\" stroke=\"black\" d=\"M53.49,-35.58C50.05,-56.72 51.71,-84 58.5,-84 64.54,-84 66.53,-62.36 64.46,-42.69\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"63.82,-35.42 67.89,-41.93 64.29,-38.89 64.76,-42.36 64.76,-42.36 64.76,-42.36 64.29,-38.89 61.64,-42.78 63.82,-35.42 63.82,-35.42\"/>\n", "<polygon fill=\"black\" stroke=\"black\" points=\"63.51,-35.58 67.56,-42.1 63.97,-39.05 64.43,-42.52 64.43,-42.52 64.43,-42.52 63.97,-39.05 61.31,-42.93 63.51,-35.58 63.51,-35.58\"/>\n",
"<text text-anchor=\"start\" x=\"53\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n", "<text text-anchor=\"start\" x=\"55\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"50.5\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n", "</g>\n",
"</g>\n", "</g>\n",
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c2d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe440654c60> >"
] ]
}, },
"execution_count": 25, "execution_count": 25,
@ -3439,7 +3439,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d9164e0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c1316c0> >"
] ]
}, },
"execution_count": 27, "execution_count": 27,
@ -3522,7 +3522,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c480> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156ea0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3587,7 +3587,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c480> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156ea0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3674,7 +3674,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc68d91c480> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe43c156ea0> >"
] ]
}, },
"execution_count": 29, "execution_count": 29,
@ -3707,7 +3707,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.8.6" "version": "3.9.1+"
} }
}, },
"nbformat": 4, "nbformat": 4,

6
tests/python/toparity.py
View file

@ -1,6 +1,6 @@
#!/usr/bin/python3 #!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de # Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de
# l'EPITA. # l'EPITA.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -112,7 +112,7 @@ def test(aut, expected_num_states=[], full=True):
spot.reduce_parity_here(p1) spot.reduce_parity_here(p1)
assert spot.are_equivalent(aut, p1) assert spot.are_equivalent(aut, p1)
if expected_num is not None: if expected_num is not None:
# print(p1.num_states(), expected_num) print(p1.num_states(), expected_num)
assert p1.num_states() == expected_num assert p1.num_states() == expected_num
if full: if full:
# Make sure passing opt is the same as setting # Make sure passing opt is the same as setting
@ -391,4 +391,4 @@ for f in spot.randltl(5, 2000):
a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')
b = spot.to_parity_old(a, True) b = spot.to_parity_old(a, True)
assert a.equivalent_to(b) assert a.equivalent_to(b)
test(a, [7, 7, 3, 7, 8, 7, 3]) test(a, [7, 7, 3, 7, 7, 7, 3])