From c4e9083f4e8303fddfc5f6099b28551f3b67f664 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 23 Jan 2016 21:24:53 +0100 Subject: [PATCH] product: raise an exception if the dict are different Fixes #132. * python/spot.py (translate): Allow changing the dictionary. * tests/python/prodexpt.py: New file. * tests/Makefile.am: Add it. * spot/twa/twaproduct.cc, spot/twaalgos/product.cc: Add them. * NEWS: Mention the change. --- NEWS | 5 +++++ python/spot.py | 4 ++-- spot/twa/twaproduct.cc | 7 +++++-- spot/twaalgos/product.cc | 6 ++++-- tests/Makefile.am | 1 + tests/python/prodexpt.py | 38 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 55 insertions(+), 6 deletions(-) create mode 100644 tests/python/prodexpt.py diff --git a/NEWS b/NEWS index 05d9152ed..5bc920c00 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 1.99.7a (not yet released) + Library: + + * Building products with different dictionaries now raise an + exception instead of using an assertion that could be disabled. + Documentation: * There is a new page giving informal illustrations (and extra diff --git a/python/spot.py b/python/spot.py index 282f4c26f..e07203d4a 100644 --- a/python/spot.py +++ b/python/spot.py @@ -574,7 +574,7 @@ def _postproc_translate_options(obj, default_type, *args): obj.set_level(optm_) -def translate(formula, *args): +def translate(formula, *args, dict=_bdd_dict): """Translate a formula into an automaton. Keep in mind that 'Deterministic' expresses just a preference that @@ -592,7 +592,7 @@ def translate(formula, *args): The default corresponds to 'tgba', 'small' and 'high'. """ - a = translator(_bdd_dict) + a = translator(dict) _postproc_translate_options(a, postprocessor.TGBA, *args) if type(formula) == str: formula = parse_formula(formula) diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 3fb7bfecb..657d3ba33 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -283,6 +283,9 @@ namespace spot : twa(left->get_dict()), left_(left), right_(right), pool_(sizeof(state_product)) { + if (left->get_dict() != right->get_dict()) + throw std::runtime_error("twa_product: left and right automata should " + "share their bdd_dict"); assert(get_dict() == right_->get_dict()); // If one of the side is a Kripke structure, it is easier to deal diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 7be9f588b..7816e8a93 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -49,7 +49,9 @@ namespace spot std::unordered_map s2n; std::deque> todo; - assert(left->get_dict() == right->get_dict()); + if (left->get_dict() != right->get_dict()) + throw std::runtime_error("product: left and right automata should " + "share their bdd_dict"); auto res = make_twa_graph(left->get_dict()); res->copy_ap_of(left); res->copy_ap_of(right); diff --git a/tests/Makefile.am b/tests/Makefile.am index a1db96e75..1e881dcb9 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -302,6 +302,7 @@ TESTS_python = \ python/optionmap.py \ python/parsetgba.py \ python/piperead.ipynb \ + python/prodexpt.py \ python/product.ipynb \ python/randaut.ipynb \ python/randgen.py \ diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py new file mode 100644 index 000000000..2b11d4e61 --- /dev/null +++ b/tests/python/prodexpt.py @@ -0,0 +1,38 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2016 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 . + +import spot + +# make sure that we are not allowed to build the product of two automata with +# different dictionnaries. + +aut1 = spot.translate('Xa') +aut2 = spot.translate('Xb', dict=spot.make_bdd_dict()) + +try: + spot.product(aut1, aut2) + exit(2) +except RuntimeError: + pass + +try: + spot.otf_product(aut1, aut2) + exit(2) +except RuntimeError: + pass -- GitLab