1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et 3 // Développement de 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/ta/ta.hh> 23 #include <iosfwd> 24 25 namespace spot 26 { 27 28 /// \addtogroup ta_misc 29 /// @{ 30 31 struct SPOT_API ta_statistics 32 { 33 unsigned edges; 34 unsigned states; 35 unsigned acceptance_states; 36 37 std::ostream& dump(std::ostream& out) const; 38 }; 39 40 /// \brief Compute statistics for an automaton. 41 SPOT_API ta_statistics stats_reachable(const const_ta_ptr& t); 42 43 /// @} 44 } 45