diff --git a/NEWS b/NEWS index b4f51a0d8..2670a741f 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,10 @@ New in spot 2.8.5.dev (not yet released) Bugs fixed: + - calling spot.translate() with two conflicting preferences like + spot.translate(..., 'det', 'any') triggered a syntax error in the + Python code to handle this error. + - degeneralize_tba() was incorrectly not honnoring the "skip_level" optimization after creating an accepting transition; as a consequence, some correct output could be larger than necessary diff --git a/python/spot/__init__.py b/python/spot/__init__.py index cb7044fdf..3b31cefbf 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2014-2019 Laboratoire de +# Copyright (C) 2014-2020 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -622,7 +622,7 @@ def _postproc_translate_options(obj, default_type, *args): nonlocal pref_, pref_name_ if pref_ is not None and pref_name_ != val: raise ValueError("preference cannot be both {} and {}" - .format(pref_name, val)) + .format(pref_name_, val)) elif val == 'small': pref_ = postprocessor.Small elif val == 'deterministic': diff --git a/tests/python/except.py b/tests/python/except.py index f4ece980b..926aa864d 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -179,3 +179,12 @@ except RuntimeError as e: assert "requires a semi-deterministic input" in str(e) else: report_missing_exception() + +try: + spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any') +except ValueError as e: + s = str(e) + assert 'det' in s + assert 'any' in s +else: + report_missing_exception()