1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2016 Laboratoire de Recherche et Developpement de l'EPITA. 3 // 4 // This file is part of Spot, a model checking library. 5 // 6 // Spot is free software; you can redistribute it and/or modify it 7 // under the terms of the GNU General Public License as published by 8 // the Free Software Foundation; either version 3 of the License, or 9 // (at your option) any later version. 10 // 11 // Spot is distributed in the hope that it will be useful, but WITHOUT 12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 14 // License for more details. 15 // 16 // You should have received a copy of the GNU General Public License 17 // along with this program. If not, see <http://www.gnu.org/licenses/>. 18 19 #pragma once 20 21 #include <spot/twaalgos/emptiness.hh> 22 23 namespace spot 24 { 25 /// \brief A rewritten version of the Couvreur emptiness check. 26 /// 27 /// It is optimized to run on explicit automata (avoiding the memory 28 /// allocations of the virtual, abstract interface. 29 /// It also has specializations for weak and terminal automata. 30 SPOT_API 31 emptiness_check_ptr 32 get_couvreur99_new(const const_twa_ptr& a, option_map o); 33 34 /// \brief Same as above, but always uses the abstract interface. 35 /// 36 /// This function is provided to test the efficiency of specializing our 37 /// algorithms for explicit automata. It uses the same optimizations for 38 /// weak and terminal automata as the one above. 39 SPOT_API 40 emptiness_check_ptr 41 get_couvreur99_new_abstract(const const_twa_ptr& a, option_map o); 42 43 /// \brief A shortcut to run the optimized emptiness check directly. 44 /// 45 /// This is the same as get_couvreur99_new(a, {})->check(). 46 SPOT_API 47 emptiness_check_result_ptr 48 couvreur99_new_check(const const_twa_ptr& a); 49 } 50