Alexandre Duret-Lutz committed Aug 23, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Feb 17, 2014 2 ``````// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement `````` Alexandre Duret-Lutz committed Aug 23, 2013 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 ``````// 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 . `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Alexandre Duret-Lutz committed Aug 23, 2013 21 `````` `````` Alexandre Duret-Lutz committed Oct 30, 2014 22 ``````#include `````` Alexandre Duret-Lutz committed Aug 23, 2013 23 24 25 26 27 28 29 30 31 32 33 ``````#include "tgbaproxy.hh" namespace spot { /// \ingroup tgba_on_the_fly_algorithms /// \brief Mask a TGBA, keeping a given set of states. /// /// Mask the TGBA \a to_mask, keeping only the /// states from \a to_keep. The initial state /// can optionally be reset to \a init. `````` Alexandre Duret-Lutz committed Apr 22, 2015 34 35 `````` SPOT_API const_twa_ptr build_tgba_mask_keep(const const_twa_ptr& to_mask, `````` Alexandre Duret-Lutz committed Aug 23, 2013 36 37 38 39 40 41 42 43 44 `````` const state_set& to_keep, const state* init = 0); /// \ingroup tgba_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting a given set of states. /// /// Mask the TGBA \a to_mask, keeping only the states that are not /// in \a to_ignore. The initial state can optionally be reset to /// \a init. `````` Alexandre Duret-Lutz committed Apr 22, 2015 45 46 `````` SPOT_API const_twa_ptr build_tgba_mask_ignore(const const_twa_ptr& to_mask, `````` Alexandre Duret-Lutz committed Aug 23, 2013 47 48 49 `````` const state_set& to_ignore, const state* init = 0); `````` Alexandre Duret-Lutz committed Mar 27, 2014 50 51 52 53 `````` /// \ingroup tgba_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting some acceptance set of transitions. /// `````` Alexandre Duret-Lutz committed Oct 06, 2014 54 55 56 `````` /// This will ignore all transitions that have the TO_IGNORE /// acceptance mark. The initial state can optionally be reset to /// \a init. `````` Alexandre Duret-Lutz committed Mar 27, 2014 57 58 59 60 61 `````` /// /// Note that the acceptance condition of the automaton (i.e. the /// set of all acceptance set) is not changed, because so far this /// function is only needed in graph algorithms that do not call /// all_acceptance_conditions(). `````` Alexandre Duret-Lutz committed Apr 22, 2015 62 63 `````` SPOT_API const_twa_ptr build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask, `````` Alexandre Duret-Lutz committed Oct 06, 2014 64 `````` unsigned to_ignore, `````` Alexandre Duret-Lutz committed Mar 27, 2014 65 `````` const state* init = 0); `````` Alexandre Duret-Lutz committed Aug 23, 2013 66 ``}``