From d6f9618172cd889ec4cea8873bbe75293666deb3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 4 May 2018 17:00:38 +0200 Subject: [PATCH] introduce containement checks functions * spot/twaalgos/contains.hh, spot/twaalgos/contains.cc: New files. * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them. * python/spot/__init__.py: Also attach these functions as methods, and support string arguments. * tests/python/contains.ipynb: New file. * tests/Makefile.am, doc/org/tut.org: Add it. * bin/autfilt.cc, tests/python/streett_totgba.py, tests/python/sum.py, tests/python/toweak.py: Use the new function. --- NEWS | 5 + bin/autfilt.cc | 4 +- doc/org/tut.org | 2 + python/spot/__init__.py | 36 +++- python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/contains.cc | 101 ++++++++++ spot/twaalgos/contains.hh | 60 ++++++ tests/Makefile.am | 1 + tests/python/contains.ipynb | 328 +++++++++++++++++++++++++++++++++ tests/python/streett_totgba.py | 31 +--- tests/python/sum.py | 23 +-- tests/python/toweak.py | 12 +- 13 files changed, 547 insertions(+), 60 deletions(-) create mode 100644 spot/twaalgos/contains.cc create mode 100644 spot/twaalgos/contains.hh create mode 100644 tests/python/contains.ipynb diff --git a/NEWS b/NEWS index aba708710..832dfb571 100644 --- a/NEWS +++ b/NEWS @@ -60,6 +60,11 @@ New in spot 2.5.3.dev (not yet released) options; there are demonstrated on the new https://spot.lrde.epita.fr/ipynb/satmin.html page. + - spot::contains() and spot::are_equivalent() can be used to + check language containement between two automata or formulas. + They are most welcome in Python, since we used to redefine + them every now and them. + Python: - New spot.jupyter package. This currently contains a function for diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 971a32637..e5b4e5451 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -49,6 +49,7 @@ #include #include #include +#include #include #include #include @@ -1342,8 +1343,7 @@ namespace matched &= !aut->intersects(opt->included_in); if (opt->equivalent_pos) matched &= !aut->intersects(opt->equivalent_neg) - && (!dualize(ensure_deterministic(aut, true))-> - intersects(opt->equivalent_pos)); + && spot::contains(opt->equivalent_pos, aut); if (matched && !opt->acc_words.empty()) for (auto& word_aut: opt->acc_words) diff --git a/doc/org/tut.org b/doc/org/tut.org index f290cbe91..b712dc7b2 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -64,6 +64,8 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/accparse.html][=accparse.ipynb=]] exercises the acceptance condition parser - [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][=acc_cond.ipynb=]] documents the interface for manipulating acceptance conditions +- [[https://spot.lrde.epita.fr/ipynb/contains.html][=contains.ipynb=]] demonstrates containment checks between formulas or + automata - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata in Python - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 3fd44a290..e43331a54 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -675,6 +675,27 @@ def translate(formula, *args, dict=_bdd_dict): formula.translate = translate +def contains(left, right): + from spot.impl import contains as contains_impl + if type(left) is str: + left = formula(left) + if type(right) is str: + right = formula(right) + return contains_impl(left, right) + +def are_equivalent(left, right): + from spot.impl import are_equivalent as equiv + if type(left) is str: + left = formula(left) + if type(right) is str: + right = formula(right) + return equiv(left, right) + +formula.contains = contains +formula.equivalent_to = are_equivalent +twa.contains = contains +twa.equivalent_to = are_equivalent + def postprocess(automaton, *args, formula=None): """Post process an automaton. @@ -713,15 +734,17 @@ twa.postprocess = postprocess # Wrap C++-functions into lambdas so that they get converted into # instance methods (i.e., self passed as first argument -# automatically), because only used-defined functions are converted as +# automatically), because only user-defined functions are converted as # instance methods. -def _add_twa_graph(meth): - setattr(twa_graph, meth, (lambda self, *args, **kwargs: - globals()[meth](self, *args, **kwargs))) +def _add_twa_graph(meth, name = None): + setattr(twa_graph, name or meth, (lambda self, *args, **kwargs: + globals()[meth](self, *args, **kwargs))) for meth in ('scc_filter', 'scc_filter_states', - 'is_deterministic', 'is_unambiguous'): + 'is_deterministic', 'is_unambiguous', + 'contains'): _add_twa_graph(meth) +_add_twa_graph('are_equivalent', 'equivalent_to') # Wrapper around a formula iterator to which we add some methods of formula # (using _addfilter and _addmap), so that we can write things like @@ -987,9 +1010,10 @@ def bdd_to_formula(b, dic=_bdd_dict): def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c + c.contains = c.contained + c.are_equivalent = c.equal return c(dic) - def mp_hierarchy_svg(cl=None): """ Return an some string containing an SVG picture of the Manna & diff --git a/python/spot/impl.i b/python/spot/impl.i index 9be7eb296..cc8e1e789 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -133,6 +133,7 @@ #include #include #include +#include #include #include #include @@ -574,6 +575,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index daff17f09..e8ee78164 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -39,6 +39,7 @@ twaalgos_HEADERS = \ complete.hh \ complement.hh \ compsusp.hh \ + contains.hh \ copy.hh \ cycles.hh \ degen.hh \ @@ -107,6 +108,7 @@ libtwaalgos_la_SOURCES = \ complete.cc \ complement.cc \ compsusp.cc \ + contains.cc \ cycles.cc \ degen.cc \ determinize.cc \ diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc new file mode 100644 index 000000000..957aa41b5 --- /dev/null +++ b/spot/twaalgos/contains.cc @@ -0,0 +1,101 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 Laboratoire de Recherche et Développement de +// l'Epita. +// +// 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 . + +#include "config.h" +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + static spot::const_twa_graph_ptr + ensure_deterministic(const spot::const_twa_graph_ptr& aut) + { + if (spot::is_deterministic(aut)) + return aut; + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + return p.run(std::const_pointer_cast(aut)); + } + + static spot::const_twa_graph_ptr + translate(formula f, const bdd_dict_ptr& dict) + { + return ltl_to_tgba_fm(f, dict); + } + } + + bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right) + { + return !left->intersects(dualize(ensure_deterministic(right))); + } + + bool contains(const_twa_graph_ptr left, formula right) + { + return !left->intersects(translate(formula::Not(right), left->get_dict())); + } + + bool contains(formula left, const_twa_graph_ptr right) + { + auto left_aut = translate(left, right->get_dict()); + return !left_aut->intersects(dualize(ensure_deterministic(right))); + } + + bool contains(formula left, formula right) + { + auto dict = make_bdd_dict(); + auto left_aut = translate(left, dict); + return !left_aut->intersects(translate(formula::Not(right), dict)); + } + + bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right) + { + // Start with a deterministic automaton at right if possible to + // avoid a determinization (in case the first containment check + // fails). + if (!is_deterministic(right)) + std::swap(left, right); + return contains(left, right) && contains(right, left); + } + + bool are_equivalent(const_twa_graph_ptr left, formula right) + { + // The first containement check does not involve a + // complementation, the second might. + return contains(left, right) && contains(right, left); + } + + bool are_equivalent(formula left, const_twa_graph_ptr right) + { + // The first containement check does not involve a + // complementation, the second might. + return contains(right, left) && contains(left, right); + } + + bool are_equivalent(formula left, formula right) + { + return contains(right, left) && contains(left, right); + } +} diff --git a/spot/twaalgos/contains.hh b/spot/twaalgos/contains.hh new file mode 100644 index 000000000..758339c73 --- /dev/null +++ b/spot/twaalgos/contains.hh @@ -0,0 +1,60 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 Laboratoire de Recherche et Développement de +// l'Epita. +// +// 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 . + +#pragma once + +#include +#include + +/// \defgroup containment Language containment checks +/// \ingroup twa_algorithms + +namespace spot +{ + /// \ingroup containment + /// \brief Test if the language of \a left is included in that of \a right. + /// + /// Both arguments can be either formulas or automata. Formulas + /// will be converted into automata. + /// + /// The inclusion check if performed by ensuring that the automaton + /// associated to \a left does not intersect the automaton + /// associated to the complement of \a right. It helps if \a right + /// is a deterministic automaton or a formula (because in both cases + /// complementation is easier). + /// @{ + SPOT_API bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right); + SPOT_API bool contains(const_twa_graph_ptr left, formula right); + SPOT_API bool contains(formula left, const_twa_graph_ptr right); + SPOT_API bool contains(formula left, formula right); + /// @} + + /// \ingroup containment + /// \brief Test if the language of \a left is equivalent to that of \a right. + /// + /// Both arguments can be either formulas or automata. Formulas + /// will be converted into automata. + /// @{ + SPOT_API bool are_equivalent(const_twa_graph_ptr left, + const_twa_graph_ptr right); + SPOT_API bool are_equivalent(const_twa_graph_ptr left, formula right); + SPOT_API bool are_equivalent(formula left, const_twa_graph_ptr right); + SPOT_API bool are_equivalent(formula left, formula right); + /// @} +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 7e4fa0b98..dceda1b95 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -332,6 +332,7 @@ TESTS_ipython = \ python/atva16-fig2b.ipynb \ python/automata-io.ipynb \ python/automata.ipynb \ + python/contains.ipynb \ python/decompose.ipynb \ python/formulas.ipynb \ python/gen.ipynb \ diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb new file mode 100644 index 000000000..bddf18b50 --- /dev/null +++ b/tests/python/contains.ipynb @@ -0,0 +1,328 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "spot.setup(show_default='.a')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Containement checks\n", + "\n", + "The `spot.contains()` function checks whether the language of its left argument is included in the language of its right argument. The arguments may mix automata and formulas; the latter can be given as strings." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "f = spot.formula('GFa'); aut_f = f.translate()\n", + "g = spot.formula('FGa'); aut_g = g.translate()" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.contains(f, g), spot.contains(g, f)" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.contains(aut_f, aut_g), spot.contains(aut_g, aut_f)" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.contains(aut_f, g), spot.contains(aut_g, f)" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.contains(f, aut_g), spot.contains(g, aut_f)" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.contains(\"GFa\", aut_g), spot.contains(\"FGa\", aut_f)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Those functions are also usable as methods:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "f.contains(aut_g), g.contains(aut_f)" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_f.contains(\"FGa\"), aut_g.contains(\"GFa\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Equivalence checks\n", + "\n", + "The `spot.are_equivalent()` tests the equivalence of the languages of its two arguments. Note that the corresponding method is called `equivalent_to()`." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, False)" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.are_equivalent(f, g), spot.are_equivalent(aut_f, aut_g)" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, False)" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "f.equivalent_to(aut_g), aut_f.equivalent_to(g)" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_f.equivalent_to('XXXGFa')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Containement checks between formulas with cache\n", + "\n", + "In the case of containement checks between formulas, `language_containement_checker` instances provide similar services, but they cache automata representing the formulas checked. This should be prefered when performing several containement checks using the same formulas." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [], + "source": [ + "lcc = spot.language_containment_checker()" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, True)" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "lcc.contains(f, g), lcc.contains(g, f)" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "lcc.are_equivalent(f, g)" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.6.5" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py index fe399aa33..7e1083a4e 100644 --- a/tests/python/streett_totgba.py +++ b/tests/python/streett_totgba.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -23,29 +23,6 @@ import os import shutil import sys -def parse_multiple_auts(hoa): - l = hoa.split('--END--') - a = [] - cpt = 0 - for x in l: - if x.isspace() or x == '': - continue - x = x + "--END--" - a.append(spot.automaton(x)) - - return a - -def ensure_deterministic(a): - if a.is_existential() and spot.is_deterministic(a): - return a - - return a.postprocess('Generic', 'deterministic', 'Low') - -def equivalent(a1, a2): - na1 = spot.dualize(ensure_deterministic(a1)) - na2 = spot.dualize(ensure_deterministic(a2)) - return (not a1.intersects(na2)) and (not a2.intersects(na1)) - def tgba(a): if not a.is_existential(): a = spot.remove_alternation(a) @@ -54,11 +31,11 @@ def tgba(a): def test_aut(aut): stgba = tgba(aut) - assert equivalent(stgba, aut) + assert stgba.equivalent_to(aut) os.environ["SPOT_STREETT_CONV_MIN"] = '1' sftgba = tgba(aut) del os.environ["SPOT_STREETT_CONV_MIN"] - assert equivalent(stgba, sftgba) + assert stgba.equivalent_to(sftgba) slike = spot.simplify_acceptance(aut) @@ -66,7 +43,7 @@ def test_aut(aut): os.environ["SPOT_STREETT_CONV_MIN"] = "1" slftgba = tgba(slike) del os.environ["SPOT_STREETT_CONV_MIN"] - assert equivalent(sltgba, slftgba) + assert sltgba.equivalent_to(slftgba) # Those automata are generated with ltl2dstar, which is NOT part of spot, # using the following command: diff --git a/tests/python/sum.py b/tests/python/sum.py index 43b96ae94..9aaa7e331 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -1,6 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -55,37 +54,29 @@ def produce_phi(rg, n): phi.append(f) return phi -def equivalent(a, phi): - negphi = spot.formula.Not(phi) - nega = spot.dualize(spot.tgba_determinize(a)) - a2 = spot.ltl_to_tgba_fm(phi, dict) - nega2 = spot.ltl_to_tgba_fm(negphi, dict) - return spot.product(a, nega2).is_empty()\ - and spot.product(nega, a2).is_empty() - phi1 = produce_phi(rg, 1000) phi2 = produce_phi(rg, 1000) inputres = [] aut = [] for p in zip(phi1, phi2): inputres.append(spot.formula.Or(p)) - a1 = spot.ltl_to_tgba_fm(p[0], dict) - a2 = spot.ltl_to_tgba_fm(p[1], dict) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) aut.append(spot.to_generalized_buchi( \ spot.remove_alternation(spot.sum(a1, a2), True))) for p in zip(aut, inputres): - assert equivalent(p[0], p[1]) + assert p[0].equivalent_to(p[1]) aut = [] inputres = [] for p in zip(phi1, phi2): inputres.append(spot.formula.And(p)) - a1 = spot.ltl_to_tgba_fm(p[0], dict) - a2 = spot.ltl_to_tgba_fm(p[1], dict) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) aut.append(spot.to_generalized_buchi( \ spot.remove_alternation(spot.sum_and(a1, a2), True))) for p in zip(aut, inputres): - assert equivalent(p[0], p[1]) + assert p[0].equivalent_to(p[1]) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index 537aabeec..0510a6850 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -29,16 +29,10 @@ GF!b (b & GF!b) | (!b & FGb) b | (a & XF(b R a)) | (!a & XG(!b U !a))""" -def equivalent(a, phi): - negphi = spot.formula.Not(phi) - nega = spot.dualize(a) - return not (spot.translate(negphi).intersects(a) - or spot.translate(phi).intersects(nega)) - def test_phi(phi): a = spot.translate(phi, 'TGBA', 'SBAcc') res = spot.to_weak_alternating(spot.dualize(a)) - assert equivalent(res, spot.formula.Not(spot.formula(phi))) + assert res.equivalent_to(spot.formula.Not(spot.formula(phi))) for p in phi1.split('\n'): print(p) @@ -87,4 +81,4 @@ State: 6 --END-- """) a2 = spot.to_weak_alternating(a2) -assert equivalent(a2, phi2) +assert a2.equivalent_to(phi2)