alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: add binding for spot::twa::prop_set

Browse source 
Fix #453.

* python/spot/impl.i: Here.
* NEWS: Mention them.
* tests/python/twagraph.py: Test them.
This commit is contained in:
Alexandre Duret-Lutz 2021-04-16 15:56:45 +02:00
parent b4b4730ecb
commit 093de290c1
3 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -196,6 +196,9 @@ New in spot 2.9.6.dev (not yet released)
- Bindings for functions related to games. - Bindings for functions related to games.
See https://spot.lrde.epita.fr/ipynb/games.html for examples. See https://spot.lrde.epita.fr/ipynb/games.html for examples.
- spot::twa::prop_set was previously abstent from the Python
binding. It is now available as spot.twa_prop_set (issue #453).
Bugs fixed: Bugs fixed:
- tgba_determinize() could create parity automata using more colors - tgba_determinize() could create parity automata using more colors

4
python/spot/impl.i
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009-2020 Laboratoire de Recherche et Développement // Copyright (C) 2009-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -526,6 +526,8 @@ namespace std {
} }
%} %}
%feature("flatnested") spot::twa::prop_set;
%rename (twa_prop_set) spot::twa::prop_set;
%include <spot/twa/twa.hh> %include <spot/twa/twa.hh>
%include <spot/tl/apcollect.hh> %include <spot/tl/apcollect.hh>

13
tests/python/twagraph.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita # Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de l'Epita
# (LRDE). # (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -53,8 +53,19 @@ except RuntimeError as e:
s = str(e) s = str(e)
assert "abstract interface" in s and "alternating automata" in s assert "abstract interface" in s and "alternating automata" in s
cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
assert aut.to_str() == cpy.to_str()
all = aut.set_buchi() all = aut.set_buchi()
assert aut.to_str() != cpy.to_str()
cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
aut.new_acc_edge(0, 1, bddtrue, True) aut.new_acc_edge(0, 1, bddtrue, True)
assert aut.num_edges() == 1 + cpy.num_edges()
aut.prop_universal(True)
cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False,
False, False, False))
assert cpy.prop_universal() != aut.prop_universal()
assert cpy.prop_universal() == spot.trival.maybe()
try: try:
s = aut.state_acc_sets(0) s = aut.state_acc_sets(0)