From 36d20696bf76acd572e0fa996af3ed9b9ce41404 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 24 May 2019 21:42:42 +0200 Subject: [PATCH] word: introduce use_all_aps() This allows fixing issue #388 reported by Victor Khomenko. * spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New method. * tests/python/stutter-inv.ipynb: Use it. * tests/python/stutter.py: New file, with Victor's test case. * tests/Makefile.am: Add python/stutter.py. --- spot/twaalgos/word.cc | 13 +++++++++- spot/twaalgos/word.hh | 9 ++++++- tests/Makefile.am | 1 + tests/python/stutter-inv.ipynb | 23 +++++++++-------- tests/python/stutter.py | 47 ++++++++++++++++++++++++++++++++++ 5 files changed, 80 insertions(+), 13 deletions(-) create mode 100644 tests/python/stutter.py diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc index c2df89524..1f24f9537 100644 --- a/spot/twaalgos/word.cc +++ b/spot/twaalgos/word.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -44,6 +44,17 @@ namespace spot { } + void + twa_word::use_all_aps(bdd aps, bool positive) + { + bdd def = positive ? + static_cast(bddtrue) : static_cast(bddfalse); + for (bdd& i: prefix) + i = bdd_satoneset(i, aps, def); + for (bdd& i: cycle) + i = bdd_satoneset(i, aps, def); + } + void twa_word::simplify() { diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index 5e35c02c6..f6f70fc14 100644 --- a/spot/twaalgos/word.hh +++ b/spot/twaalgos/word.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -62,6 +62,13 @@ namespace spot /// single operand. void simplify(); + /// \brief Use all atomic proposition. + /// + /// Make sure each letters actually use all variables in \a aps. + /// By default, missing variables are introduced as negative, + /// but setting \a positive to true will reverse that. + void use_all_aps(bdd aps, bool positive = false); + typedef std::list seq_t; seq_t prefix; seq_t cycle; diff --git a/tests/Makefile.am b/tests/Makefile.am index 4b332e243..93d09623c 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -410,6 +410,7 @@ TESTS_python = \ python/split.py \ python/streett_totgba.py \ python/streett_totgba2.py \ + python/stutter.py \ python/rs_like.py \ python/sum.py \ python/toparity.py \ diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index d857b60e8..7d92119e5 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c1ee180> >" + " *' at 0x7fbbb85b6780> >" ] }, "metadata": {}, @@ -361,6 +361,7 @@ " print(f, \"is stutter invariant\")\n", " return\n", " word.simplify()\n", + " word.use_all_aps(pos.ap_vars())\n", " waut = word.as_automaton()\n", " if waut.intersects(pos):\n", " acc, rej, aut = \"accepted\", \"rejected\", neg\n", @@ -602,7 +603,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c250300> >" + " *' at 0x7fbbb8570cf0> >" ] }, "metadata": {}, @@ -811,7 +812,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c250300> >" + " *' at 0x7fbbb8570cf0> >" ] }, "metadata": {}, @@ -963,7 +964,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c1e1f60> >" + " *' at 0x7fbbb85b6750> >" ] }, "metadata": {}, @@ -1061,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c1e1840> >" + " *' at 0x7fbbb8570450> >" ] }, "metadata": {}, @@ -1271,7 +1272,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c1ee990> >" + " *' at 0x7fbbb857f120> >" ] }, "metadata": {}, @@ -1400,7 +1401,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c2502a0> >" + " *' at 0x7fbbb8570510> >" ] }, "metadata": {}, @@ -1531,7 +1532,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c20eb10> >" + " *' at 0x7fbbb850fae0> >" ] }, "metadata": {}, @@ -1791,7 +1792,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c20eea0> >" + " *' at 0x7fbbb850fb10> >" ] }, "metadata": {}, @@ -2105,7 +2106,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0a9c20eea0> >" + " *' at 0x7fbbb850fb10> >" ] }, "metadata": {}, @@ -2346,7 +2347,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.1" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/stutter.py b/tests/python/stutter.py new file mode 100644 index 000000000..3b1079000 --- /dev/null +++ b/tests/python/stutter.py @@ -0,0 +1,47 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2019 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 . + +# Test that the spot.gen package works, in particular, we want +# to make sure that the objects created from spot.gen methods +# are usable with methods from the spot package. + + +import spot + +def explain_stut(f): + f = spot.formula(f) + pos = spot.translate(f) + neg = spot.translate(spot.formula.Not(f)) + word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word() + if word is None: + print(f, "is stutter invariant") + return + word.simplify() + # This line used to be missing, causing issue #388. + word.use_all_aps(pos.ap_vars()) + waut = word.as_automaton() + aut = neg if waut.intersects(pos) else pos + word2 = spot.sl2(waut).intersecting_word(aut) + word2.simplify() + return(word, word2) + +# Test from issue #388 +w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc') +assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}' +assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}'