From 2e3fc0d4d2afa4ff103460c5329ad17abcb3ac43 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Mar 2017 14:19:09 +0100 Subject: [PATCH] emptiness checks: replace assert-preconditions by exceptions * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc, spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance condition is not satisfied. * tests/python/misc-ec.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the change. --- NEWS | 5 ++++ spot/twaalgos/couvreurnew.cc | 5 ++++ spot/twaalgos/gv04.cc | 8 ++++-- spot/twaalgos/magic.cc | 8 ++++-- spot/twaalgos/se05.cc | 9 ++++--- spot/twaalgos/tau03.cc | 8 +++--- spot/twaalgos/tau03opt.cc | 4 ++- tests/Makefile.am | 1 + tests/python/misc-ec.py | 47 ++++++++++++++++++++++++++++++++++++ 9 files changed, 84 insertions(+), 11 deletions(-) create mode 100644 tests/python/misc-ec.py diff --git a/NEWS b/NEWS index a21ce9c34..60383375d 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,11 @@ New in spot 2.3.1.dev (not yet released) - the Python wrappers for spot::twa_graph::state_from_number and spot::twa_graph::state_acc_sets were broken in 2.3. + - instantiating an emptiness check on an automaton with unsupported + acceptance condition should throw an exception. This used to be + just an assertion, disabled in release builds; the difference + matters for the Python bindings. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index e38c208fc..ee0e91de5 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -540,12 +540,17 @@ namespace spot : emptiness_check(a, o) , ecs_(std::make_shared>(a)) { + if (a->acc().uses_fin_acceptance()) + throw std::runtime_error + ("couvreur99_new requires Fin-less acceptance"); } virtual emptiness_check_result_ptr check() override { + if (ecs_->aut->acc().get_acceptance().is_f()) + return nullptr; return check_impl(); } diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index ea3508cef..45e496954 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013-2017 Laboratoire de // recherche et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -67,7 +67,11 @@ namespace spot gv04(const const_twa_ptr& a, option_map o) : emptiness_check(a, o) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error + ("gv04 requires Büchi or weak automata"); } ~gv04() diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 705329818..24820aac4 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche et +// Copyright (C) 2011, 2013-2017 Laboratoire de recherche et // développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -59,7 +59,11 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error + ("magic_search requires Büchi or weak automata"); } virtual ~magic_search_() diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index ee77ff4f1..ec24263b7 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -59,7 +59,10 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error("se05 requires Büchi or weak automata"); } virtual ~se05_search() diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index d69a66b3b..8e07a2fac 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -58,7 +58,9 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() > 0); + if (!(a->num_sets() > 0 && a->acc().is_generalized_buchi())) + throw std::runtime_error + ("tau03 requires generalized Büchi with at least one set"); } virtual ~tau03_search() diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index fd3d2acc6..9b9907605 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -74,6 +74,8 @@ namespace spot use_weights(o.get("weights", 1)), use_red_weights(use_weights && o.get("redweights", 1)) { + if (a->acc().uses_fin_acceptance()) + throw std::runtime_error("tau03opt requires Fin-less acceptance"); } virtual ~tau03_opt_search() diff --git a/tests/Makefile.am b/tests/Makefile.am index aedabe53d..f59f871c0 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -339,6 +339,7 @@ TESTS_python = \ python/ltlparse.py \ python/ltlsimple.py \ python/minato.py \ + python/misc-ec.py \ python/optionmap.py \ python/otfcrash.py \ python/parsetgba.py \ diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py new file mode 100644 index 000000000..4c01e345f --- /dev/null +++ b/tests/python/misc-ec.py @@ -0,0 +1,47 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot +aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA') +ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut) +n = 0 +while True: + res = ec.check() + if not res: + break + print(res.accepting_run()) + n += 1 +assert n == 2 + +for name in ['SE05', 'CVWY90', 'GV04']: + aut = spot.translate("GFa && GFb") + try: + ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(aut) + print(ec.check().accepting_run()) + except RuntimeError as e: + assert "Büchi or weak" in str(e) + +aut = spot.translate("a", 'monitor') +try: + ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) +except RuntimeError as e: + assert "at least one" in str(e) + +aut = spot.translate("a", 'ba') +ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut)