diff --git a/python/spot/__init__.py b/python/spot/__init__.py index b8064e6d4..9263b6878 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -490,6 +490,7 @@ def _postproc_translate_options(obj, default_type, *args): comp_ = 0 unam_ = 0 sbac_ = 0 + colo_ = 0 def type_set(val): nonlocal type_ @@ -551,8 +552,10 @@ def _postproc_translate_options(obj, default_type, *args): optm_ = postprocessor.Low def misc_set(val): - nonlocal comp_, unam_, sbac_ - if val == 'complete': + nonlocal comp_, unam_, sbac_, colo_ + if val == 'colored': + colo_ = postprocessor.Colored + elif val == 'complete': comp_ = postprocessor.Complete elif val == 'sbacc' or val == 'state-based-acceptance': sbac_ = postprocessor.SBAcc @@ -564,6 +567,7 @@ def _postproc_translate_options(obj, default_type, *args): 'any': pref_set, 'ba': type_set, 'complete': misc_set, + 'colored': misc_set, 'deterministic': pref_set, 'generic': type_set, 'high': optm_set, @@ -617,7 +621,7 @@ def _postproc_translate_options(obj, default_type, *args): optm_ = postprocessor.High obj.set_type(type_) - obj.set_pref(pref_ | comp_ | unam_ | sbac_) + obj.set_pref(pref_ | comp_ | unam_ | sbac_ | colo_) obj.set_level(optm_) @@ -636,8 +640,9 @@ def translate(formula, *args, dict=_bdd_dict): (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' (optimization level) - - any combination of 'Complete', 'Unambiguous', and - 'StateBasedAcceptance' (or 'SBAcc' for short) + - any combination of 'Complete', 'Unambiguous', + 'StateBasedAcceptance' (or 'SBAcc' for short), and + 'Colored' (only for parity acceptance) The default corresponds to 'tgba', 'small' and 'high'. """ @@ -668,8 +673,9 @@ def postprocess(automaton, *args, formula=None): (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' (optimization level) - - any combination of 'Complete' and 'StateBasedAcceptance' - (or 'SBAcc' for short) + - any combination of 'Complete', 'StateBasedAcceptance' + (or 'SBAcc' for short), and 'Colored (only for parity + acceptance) The default corresponds to 'generic', 'small' and 'high'. diff --git a/python/spot/impl.i b/python/spot/impl.i index 2bd09ef03..de6fdc039 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique -// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Copyright (C) 2009-2018 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é +// Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -599,6 +599,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/tests/python/parity.py b/tests/python/parity.py index 6a09718cf..b1ede2f44 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -26,8 +26,9 @@ for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'): assert a1.acc().is_parity() a2 = spot.translate(f).postprocess('parity') assert a2.acc().is_parity() - a3 = spot.translate(f, 'det').postprocess('parity') + a3 = spot.translate(f, 'det').postprocess('parity', 'colored') assert a3.acc().is_parity() + assert spot.is_colored(a3) a = spot.translate('GFa & GFb') try: