1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement de 3 // l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <spot/twa/twa.hh> 23 24 namespace spot 25 { 26 /// \brief Convert an alternating automaton to a weak alternating automaton. 27 /// 28 /// The input automaton must have a generalized co-Büchi or Büchi acceptance 29 /// condition. 30 /// The automaton will be converted into a weak Büchi automaton. If the input 31 /// automaton is already weak, it will simply be copied. 32 /// 33 /// For details about the algorithm used, see the following papers: 34 /// \cite kupferman.01.tocl , 35 /// \cite kupferman.05.tcs . 36 /// 37 /// Although at the end of the above paper there is a hint at an optimization 38 /// that greatly reduces the number of transition in the resulting automaton, 39 /// but in return makes the run of remove_alternation algorithm way slower. 40 /// Hence, the optimization is disabled by default. 41 /// 42 /// \param aut the automaton to convert to weak 43 /// \param less whether to activate the optimization on the number of 44 /// transitions or not, disabled by default 45 SPOT_API 46 twa_graph_ptr to_weak_alternating(const_twa_graph_ptr& aut, 47 bool less = false); 48 } 49