Commit 3908cc1b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: improve bdd_dict bindings

Fixes #372.

* python/spot/impl.i: Refactor the handling of exceptions using a
Lippincott function.  Map out_of_range to IndexError.  Add
PyObject* version for bdd_dict's register and unregister functions
so we can use Python objects as well.
* tests/python/bdddict.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the changes.
parent bd0f9594
Pipeline #5496 failed with stage
in 60 minutes and 29 seconds
New in spot 2.7.0.dev (not yet release)
Python:
- The following methods of spot::bdd_dict are now usable in Python when
fine controle over the lifetime of associations between BDD variable
and atomic propositions is needed.
- register_proposition(formula, for_me)
- register_anonymous_variables(count, for_me)
- register_all_propositions_of(other, for_me)
- unregister_all_my_variables(for_me)
- unregister_variable(var, for_me)
Bugs fixed:
- The print_dot_psl() function would incorrectly number all but the
first children of commutative n-ary operators: in this case no
numbering was expected.
- std::out_of_range C++ exceptions raised from Python code are now
converted into IndexError Python exceptions (instead of aborting
the program).
New in spot 2.7 (2018-12-11)
Command-line tools:
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2009-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
......@@ -409,23 +409,45 @@ namespace swig
$result = SWIG_FromCharPtr($1->c_str());
}
%exception {
%{
// This function is called whenever an exception has been caught.
// Doing all the conversion in a separate function (rather than
// in the %exception statement) saves a lot of space.
//
// The technique is also called "Lippincott function".
static void handle_any_exception()
{
try {
$action
throw;
}
catch (const spot::parse_error& e)
{
std::string er("\n");
er += e.what();
SWIG_exception(SWIG_SyntaxError, er.c_str());
SWIG_Error(SWIG_SyntaxError, er.c_str());
}
catch (const std::invalid_argument& e)
{
SWIG_exception(SWIG_ValueError, e.what());
SWIG_Error(SWIG_ValueError, e.what());
}
catch (const std::runtime_error& e)
{
SWIG_exception(SWIG_RuntimeError, e.what());
SWIG_Error(SWIG_RuntimeError, e.what());
}
catch (const std::out_of_range& e)
{
SWIG_Error(SWIG_IndexError, e.what());
}
}
%}
%exception {
try {
$action
}
catch (...) {
handle_any_exception();
SWIG_fail;
}
}
......@@ -790,6 +812,31 @@ def state_is_accepting(self, src) -> "bool":
std::string __str__() { return spot::str_psl(*self); }
}
%runtime %{
#include <memory>
// The bdd_dict object stores pointers to keep track of who
// uses which BDD variables. If this is a C++ object, we
// would like to use its this pointer (not the Python pointer).
// If this is a shared_ptr, we would like to use the address of
// of the pointed object, not that of the shared ptr. Finally,
// we also want to allow Python objects in there,
static void* ptr_for_bdddict(PyObject* obj)
{
void* ptr = obj;
if (SwigPyObject* swig_obj = SWIG_Python_GetSwigThis(obj))
{
ptr = swig_obj->ptr;
const char *type = SWIG_TypePrettyName(swig_obj->ty);
if (strncmp(type, "std::shared_ptr<", 16) == 0)
ptr = reinterpret_cast<std::shared_ptr<void>*>(ptr)->get();
}
return ptr;
}
%}
%extend spot::bdd_dict {
bool operator==(const spot::bdd_dict& b) const
{
......@@ -800,6 +847,33 @@ def state_is_accepting(self, src) -> "bool":
{
return self != &b;
}
int register_proposition(formula f, PyObject* for_me)
{
return $self->register_proposition(f, ptr_for_bdddict(for_me));
}
void unregister_all_my_variables(PyObject* me)
{
return $self->unregister_all_my_variables(ptr_for_bdddict(me));
}
void unregister_variable(int var, PyObject* me)
{
return $self->unregister_variable(var, ptr_for_bdddict(me));
}
void register_all_variables_of(PyObject* from_other, PyObject* for_me)
{
return $self->register_all_variables_of(ptr_for_bdddict(from_other),
ptr_for_bdddict(for_me));
}
int register_anonymous_variables(int n, PyObject* for_me)
{
return $self->register_anonymous_variables(n, ptr_for_bdddict(for_me));
}
}
%extend spot::twa {
......
## -*- coding: utf-8 -*-
## Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
## Copyright (C) 2009-2019 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
......@@ -365,6 +365,7 @@ TESTS_python = \
python/accparse2.py \
python/alarm.py \
python/alternating.py \
python/bdddict.py \
python/bdditer.py \
python/bddnqueen.py \
python/bugdet.py \
......
# -*- 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 <http://www.gnu.org/licenses/>.
# Make sure we can leep track of BDD association in Python using bdd_dict, as
# discussed in issue #372.
class bdd_holder:
def __init__(self, aut):
self.bdddict = d = aut.get_dict()
for ap in aut.ap():
d.register_proposition(ap, self)
def __del__(self):
self.bdddict.unregister_all_my_variables(self)
class bdd_holder2:
def __init__(self, aut):
self.bdddict = d = aut.get_dict()
d.register_all_variables_of(aut, self)
def __del__(self):
self.bdddict.unregister_all_my_variables(self)
class bdd_holder3:
def __init__(self, h2):
self.bdddict = d = h2.bdddict
d.register_all_variables_of(h2, self)
def __del__(self):
self.bdddict.unregister_all_my_variables(self)
def check_ok():
assert type(bdict.varnum(spot.formula.ap("a"))) is int
def check_nok():
try:
bdict.varnum(spot.formula.ap("a"))
except IndexError as e:
pass
else:
raise RuntimeError("missing exception")
def debug(txt):
# print(txt)
# bdict.dump(spot.get_cout())
pass
import spot
aut = spot.translate("a U b")
bdict = aut.get_dict()
debug("aut")
word = aut.accepting_word()
debug("word")
check_ok()
h = bdd_holder(aut)
debug("h")
check_ok()
h2 = bdd_holder2(aut)
debug("h2")
check_ok()
del aut
debug("-aut")
check_ok()
del word
debug("-word")
check_ok()
del h
debug("-h")
check_ok()
del h2
debug("-h2")
check_nok()
h2 = bdd_holder2(spot.translate("a U b").accepting_word())
debug("h2")
h3 = bdd_holder3(h2)
var = bdict.register_anonymous_variables(1, h3)
debug("h3")
assert var == 2
del h2
debug("-h2")
check_ok()
del h3
debug("-h3")
check_nok()
h2 = bdd_holder2(spot.translate("a U b").accepting_word())
debug("h2")
bdict.unregister_variable(bdict.varnum("b"), h2)
bdict.unregister_variable(bdict.varnum("a"), h2)
debug("-b,-a")
check_nok()
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment