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 20 21 22 23 ``````// 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 . #ifndef SPOT_TGBA_TGBAMASK_HH # define SPOT_TGBA_TGBAMASK_HH #include "tgbaproxy.hh" `````` Alexandre Duret-Lutz committed Mar 27, 2014 24 ``````#include "bdd.h" `````` Alexandre Duret-Lutz committed Aug 23, 2013 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 `````` namespace spot { /// \ingroup tgba_on_the_fly_algorithms /// \brief A masked TGBA (abstract). /// /// Ignores some states from a TGBA. What state are preserved or /// ignored is controlled by the wanted() method. /// /// This is an abstract class. You should inherit from it and /// supply a wanted() method to specify which states to keep. class SPOT_API tgba_mask: public tgba_proxy { protected: /// \brief Constructor. /// \param masked The automaton to mask /// \param init Any state to use as initial state. This state will be /// destroyed by the destructor. tgba_mask(const tgba* masked, const state* init = 0); public: virtual ~tgba_mask(); virtual state* get_init_state() const; virtual tgba_succ_iterator* `````` Alexandre Duret-Lutz committed Feb 17, 2014 52 `````` succ_iter(const state* local_state) const; `````` Alexandre Duret-Lutz committed Aug 23, 2013 53 `````` `````` Alexandre Duret-Lutz committed Mar 27, 2014 54 `````` virtual bool wanted(const state* s, const bdd& acc) const = 0; `````` Alexandre Duret-Lutz committed Aug 23, 2013 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` protected: const state* init_; }; /// \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. SPOT_API const tgba* build_tgba_mask_keep(const tgba* to_mask, 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. SPOT_API const tgba* build_tgba_mask_ignore(const tgba* to_mask, const state_set& to_ignore, const state* init = 0); `````` Alexandre Duret-Lutz committed Mar 27, 2014 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 `````` /// \ingroup tgba_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting some acceptance set of transitions. /// /// This will ignore all transitions labeled by the acceptance ACC /// such that ACC & TO_IGNORE != bddfalse. The initial state can /// optionally be reset to \a init. /// /// 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(). SPOT_API const tgba* build_tgba_mask_acc_ignore(const tgba* to_mask, const bdd to_ignore, const state* init = 0); `````` Alexandre Duret-Lutz committed Aug 23, 2013 99 100 101 ``````} #endif // SPOT_TGBA_TGBAMASK_HH``````