From e0958ee7c63f4abbe28c43b34f8892b5b93ea997 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Oct 2018 18:16:46 +0200 Subject: [PATCH] python: add xargs support to translate() and postprocess() Fixes #361. * python/spot/__init__.py: Implement it. * tests/python/optionmap.py: Test it. * NEWS: Mention it. --- NEWS | 10 +++++++++ python/spot/__init__.py | 45 +++++++++++++++++++++++++++++++++------ tests/python/optionmap.py | 28 +++++++++++++++++++++++- 3 files changed, 75 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index ef16ea945..29f6afedd 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,16 @@ New in spot 2.6.3.dev (not yet released) - ltlfilt learned --liveness to match formulas representing liveness properties. + Python: + + - spot.translate() and spot.postprocess() now take an xargs= + argument similar to the -x option of ltl2tgba and autfilt, making + it easier to fine tune these operations. For instance + ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0 + would be written in Python as + spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') + (Note: those extra options are documented in the spot-x(7) man page.) + Library: - The LTL parser learned syntactic sugar for nested ranges of X diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 4980cad3e..dd979966d 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -101,6 +101,17 @@ if 'op_ff' not in globals(): _bdd_dict = make_bdd_dict() + +__om_init_tmp = option_map.__init__ +def __om_init_new(self, str=None): + __om_init_tmp(self) + if str: + res = self.parse_options(str) + if res: + raise RuntimeError("failed to parse option at: '" + str +"'") +option_map.__init__ = __om_init_new + + @_extend(twa, ta) class twa: def _repr_svg_(self, opt=None): @@ -688,7 +699,7 @@ def _postproc_translate_options(obj, default_type, *args): obj.set_level(optm_) -def translate(formula, *args, dict=_bdd_dict): +def translate(formula, *args, dict=_bdd_dict, xargs=None): """Translate a formula into an automaton. Keep in mind that 'Deterministic' expresses just a preference that @@ -708,12 +719,22 @@ def translate(formula, *args, dict=_bdd_dict): 'Colored' (only for parity acceptance) The default corresponds to 'tgba', 'small' and 'high'. + + Additional options can be supplied using a `spot.option_map`, or a + string (that will be converted to `spot.option_map`), as the `xargs` + argument. This is similar to the `-x` option of command-line tools; + so check out the spot-x(7) man page for details. """ - a = translator(dict) + if type(xargs) is str: + xargs = option_map(xargs) + a = translator(dict, xargs) _postproc_translate_options(a, postprocessor.TGBA, *args) if type(formula) == str: formula = parse_formula(formula) - return a.run(formula) + result = a.run(formula) + if xargs: + xargs.report_unused_options() + return result formula.translate = translate @@ -732,7 +753,7 @@ _add_formula('contains') _add_formula('are_equivalent', 'equivalent_to') -def postprocess(automaton, *args, formula=None): +def postprocess(automaton, *args, formula=None, xargs=None): """Post process an automaton. This applies a number of simlification algorithms, depending on @@ -758,12 +779,22 @@ def postprocess(automaton, *args, formula=None): If a formula denoted by this automaton is known, pass it to as the optional `formula` argument; it can help some algorithms by providing an easy way to complement the automaton. - """ - p = postprocessor() + + Additional options can be supplied using a `spot.option_map`, or a + string (that will be converted to `spot.option_map`), as the `xargs` + argument. This is similar to the `-x` option of command-line tools; + so check out the spot-x(7) man page for details. +""" + if type(xargs) is str: + xargs = option_map(xargs) + p = postprocessor(xargs) if type(automaton) == str: automaton = globals()['automaton'](automaton) _postproc_translate_options(p, postprocessor.Generic, *args) - return p.run(automaton, formula) + result = p.run(automaton, formula) + if xargs: + xargs.report_unused_options() + return result twa.postprocess = postprocess diff --git a/tests/python/optionmap.py b/tests/python/optionmap.py index 9bce94e0c..667ef0b19 100755 --- a/tests/python/optionmap.py +++ b/tests/python/optionmap.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2010, 2012, 2018 Laboratoire de Recherche et Développement # de l'EPITA. # Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -57,3 +57,29 @@ assert res == "opt == 1" res = o.parse_options("foo=3opt == 1") assert res == "3opt == 1" + +aut1 = spot.translate('GF(a <-> XXa)', 'det') +assert aut1.num_states() == 4 +aut2 = spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') +assert aut2.num_states() == 9 + +try: + spot.translate('GF(a <-> XXa)', 'det', xargs='foobar=1') +except RuntimeError as e: + assert "option 'foobar' was not used" in str(e) +else: + raise RuntimeError("missing exception") + +try: + spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=0') +except RuntimeError as e: + assert "option 'gf-guarantee' was not used" in str(e) +else: + raise RuntimeError("missing exception") + +try: + spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=x') +except RuntimeError as e: + assert "failed to parse option at: 'gf-guarantee=x'" in str(e) +else: + raise RuntimeError("missing exception")