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

introduce containement checks functions

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2018-05-04 17:00:38 +02:00
parent 58d9a12495
commit d6f9618172
13 changed files with 547 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -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

4
bin/autfilt.cc
View file

@ -49,6 +49,7 @@
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/gtec/gtec.hh>
@ -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)

2
doc/org/tut.org
View file

@ -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

34
python/spot/__init__.py
View file

@ -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:
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 &

2
python/spot/impl.i
View file

@ -133,6 +133,7 @@
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/gfguarantee.hh>
#include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/magic.hh>
#include <spot/twaalgos/minimize.hh>
@ -574,6 +575,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/ltl2tgba_fm.hh>
%include <spot/twaalgos/gfguarantee.hh>
%include <spot/twaalgos/compsusp.hh>
%include <spot/twaalgos/contains.hh>
%include <spot/twaalgos/determinize.hh>
%include <spot/twaalgos/dualize.hh>
%include <spot/twaalgos/langmap.hh>

2
spot/twaalgos/Makefile.am
View file

@ -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 \

101
spot/twaalgos/contains.cc Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/twaalgos/contains.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/dualize.hh>
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<twa_graph>(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);
}
}

60
spot/twaalgos/contains.hh Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/twa/twagraph.hh>
#include <spot/tl/formula.hh>
/// \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);
/// @}
}

1
tests/Makefile.am
View file

@ -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 \

328
tests/python/contains.ipynb Normal file
View file

@ -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
}

31
tests/python/streett_totgba.py
View file

@ -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:

15
tests/python/sum.py
View file

@ -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,14 +54,6 @@ 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 = []
@ -75,7 +66,7 @@ for p in zip(phi1, phi2):
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 = []
@ -88,4 +79,4 @@ for p in zip(phi1, phi2):
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])

12
tests/python/toweak.py
View file

@ -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)