1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2015 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 <vector> 23 #include <spot/tl/formula.hh> 24 #include <spot/twa/twagraph.hh> 25 26 namespace spot 27 { 28 class SPOT_API remove_ap 29 { 30 std::set<formula> props_exist; 31 std::set<formula> props_pos; 32 std::set<formula> props_neg; 33 public: 34 void add_ap(const char* ap_csv); 35 empty() const36 bool empty() const 37 { 38 return props_exist.empty() && props_pos.empty() && props_neg.empty(); 39 } 40 41 twa_graph_ptr strip(const_twa_graph_ptr aut) const; 42 }; 43 } 44