diff --git a/NEWS b/NEWS index f100b1734..3f0384069 100644 --- a/NEWS +++ b/NEWS @@ -196,6 +196,9 @@ New in spot 2.9.6.dev (not yet released) - Bindings for functions related to games. 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: - tgba_determinize() could create parity automata using more colors diff --git a/python/spot/impl.i b/python/spot/impl.i index e3c76fe2b..27f819207 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -1,5 +1,5 @@ // -*- 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). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (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 %include diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index d6eec94f7..69afa735d 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -1,5 +1,5 @@ # -*- 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). # # This file is part of Spot, a model checking library. @@ -53,8 +53,19 @@ except RuntimeError as e: s = str(e) 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() +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) +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: s = aut.state_acc_sets(0)