python: add colored parity support to postproc and translate

* python/spot/impl.i: Bind is_colored().
* python/spot/__init__.py: Add Colored support to postproc.
* tests/python/parity.py: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2018-01-08 11:37:22 +01:00
parent abe4e12cc9
commit f369db6cb1
3 changed files with 21 additions and 13 deletions

View file

@ -490,6 +490,7 @@ def _postproc_translate_options(obj, default_type, *args):
comp_ = 0 comp_ = 0
unam_ = 0 unam_ = 0
sbac_ = 0 sbac_ = 0
colo_ = 0
def type_set(val): def type_set(val):
nonlocal type_ nonlocal type_
@ -551,8 +552,10 @@ def _postproc_translate_options(obj, default_type, *args):
optm_ = postprocessor.Low optm_ = postprocessor.Low
def misc_set(val): def misc_set(val):
nonlocal comp_, unam_, sbac_ nonlocal comp_, unam_, sbac_, colo_
if val == 'complete': if val == 'colored':
colo_ = postprocessor.Colored
elif val == 'complete':
comp_ = postprocessor.Complete comp_ = postprocessor.Complete
elif val == 'sbacc' or val == 'state-based-acceptance': elif val == 'sbacc' or val == 'state-based-acceptance':
sbac_ = postprocessor.SBAcc sbac_ = postprocessor.SBAcc
@ -564,6 +567,7 @@ def _postproc_translate_options(obj, default_type, *args):
'any': pref_set, 'any': pref_set,
'ba': type_set, 'ba': type_set,
'complete': misc_set, 'complete': misc_set,
'colored': misc_set,
'deterministic': pref_set, 'deterministic': pref_set,
'generic': type_set, 'generic': type_set,
'high': optm_set, 'high': optm_set,
@ -617,7 +621,7 @@ def _postproc_translate_options(obj, default_type, *args):
optm_ = postprocessor.High optm_ = postprocessor.High
obj.set_type(type_) obj.set_type(type_)
obj.set_pref(pref_ | comp_ | unam_ | sbac_) obj.set_pref(pref_ | comp_ | unam_ | sbac_ | colo_)
obj.set_level(optm_) obj.set_level(optm_)
@ -636,8 +640,9 @@ def translate(formula, *args, dict=_bdd_dict):
(preferred characteristics of the produced automaton) (preferred characteristics of the produced automaton)
- at most one in 'Low', 'Medium', 'High' - at most one in 'Low', 'Medium', 'High'
(optimization level) (optimization level)
- any combination of 'Complete', 'Unambiguous', and - any combination of 'Complete', 'Unambiguous',
'StateBasedAcceptance' (or 'SBAcc' for short) 'StateBasedAcceptance' (or 'SBAcc' for short), and
'Colored' (only for parity acceptance)
The default corresponds to 'tgba', 'small' and 'high'. The default corresponds to 'tgba', 'small' and 'high'.
""" """
@ -668,8 +673,9 @@ def postprocess(automaton, *args, formula=None):
(preferred characteristics of the produced automaton) (preferred characteristics of the produced automaton)
- at most one in 'Low', 'Medium', 'High' - at most one in 'Low', 'Medium', 'High'
(optimization level) (optimization level)
- any combination of 'Complete' and 'StateBasedAcceptance' - any combination of 'Complete', 'StateBasedAcceptance'
(or 'SBAcc' for short) (or 'SBAcc' for short), and 'Colored (only for parity
acceptance)
The default corresponds to 'generic', 'small' and 'high'. The default corresponds to 'generic', 'small' and 'high'.

View file

@ -1,9 +1,9 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 // Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
// Laboratoire de Recherche et Développement de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Université Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -599,6 +599,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/sccfilter.hh> %include <spot/twaalgos/sccfilter.hh>
%include <spot/twaalgos/stats.hh> %include <spot/twaalgos/stats.hh>
%include <spot/twaalgos/isdet.hh> %include <spot/twaalgos/isdet.hh>
%include <spot/twaalgos/iscolored.hh>
%include <spot/twaalgos/isunamb.hh> %include <spot/twaalgos/isunamb.hh>
%include <spot/twaalgos/isweakscc.hh> %include <spot/twaalgos/isweakscc.hh>
%include <spot/twaalgos/simulation.hh> %include <spot/twaalgos/simulation.hh>

View file

@ -26,8 +26,9 @@ for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
assert a1.acc().is_parity() assert a1.acc().is_parity()
a2 = spot.translate(f).postprocess('parity') a2 = spot.translate(f).postprocess('parity')
assert a2.acc().is_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 a3.acc().is_parity()
assert spot.is_colored(a3)
a = spot.translate('GFa & GFb') a = spot.translate('GFa & GFb')
try: try: