bfssteps.hh 4.11 KB
 Alexandre Duret-Lutz committed Jan 27, 2011 1 2 ``````// Copyright (C) 2011 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Jan 03, 2005 3 ``````// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed Nov 24, 2004 4 5 6 7 8 9 10 ``````// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // 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 `````` Alexandre Duret-Lutz committed Oct 12, 2012 11 ``````// the Free Software Foundation; either version 3 of the License, or `````` Alexandre Duret-Lutz committed Nov 24, 2004 12 13 14 15 16 17 18 19 ``````// (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 `````` Alexandre Duret-Lutz committed Oct 12, 2012 20 ``````// along with this program. If not, see . `````` Alexandre Duret-Lutz committed Nov 24, 2004 21 22 23 24 `````` #ifndef SPOT_TGBAALGOS_BFSSTEPS_HH # define SPOT_TGBAALGOS_BFSSTEPS_HH `````` Denis Poitrenaud committed Dec 20, 2004 25 26 ``````#include #include "tgba/state.hh" `````` Alexandre Duret-Lutz committed Nov 24, 2004 27 28 29 30 ``````#include "emptiness.hh" namespace spot { `````` Alexandre Duret-Lutz committed Nov 24, 2004 31 32 33 34 35 36 `````` /// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps. /// \ingroup tgba_misc /// /// This class should be used to compute the shortest path /// between a state of a spot::tgba and the first transition or /// state that matches some conditions. `````` Alexandre Duret-Lutz committed Nov 24, 2004 37 38 39 40 `````` /// /// These conditions should be specified by defining bfs_steps::match() /// in a subclass. Also the search can be restricted to some set of /// states with a proper definition of bfs_steps::filter(). `````` Alexandre Duret-Lutz committed Nov 24, 2004 41 42 43 44 45 46 `````` class bfs_steps { public: bfs_steps(const tgba* a); virtual ~bfs_steps(); `````` Alexandre Duret-Lutz committed Nov 24, 2004 47 48 49 50 51 52 `````` /// \brief Start the search from \a start, and append the /// resulting path (if any) to \a l. /// /// \return the destination state of the last step (not included /// in \a l) if a matching path was found, or 0 otherwise. const state* search(const state* start, tgba_run::steps& l); `````` Alexandre Duret-Lutz committed Nov 24, 2004 53 `````` `````` Alexandre Duret-Lutz committed Nov 24, 2004 54 55 56 57 58 59 60 61 62 63 64 `````` /// \brief Return a state* that is unique for \a a. /// /// bfs_steps does not do handle the memory for the states it /// generates, this is the job of filter(). Here \a s is a new /// state* that search() has just allocated (using /// tgba_succ_iterator::current_state()), and the return of this /// function should be a state* that does not need to be freed by /// search(). /// /// If you already have a map or a set which uses states as keys, /// you should probably arrange for filter() to return these keys, `````` Alexandre Duret-Lutz committed Jan 27, 2011 65 66 `````` /// and destroy \a s. Otherwise you will have to define such a /// set, just to be able to destroy all the state* in a subclass. `````` Alexandre Duret-Lutz committed Nov 24, 2004 67 68 69 `````` /// /// This function can return 0 if the given state should not be /// explored. `````` Alexandre Duret-Lutz committed Nov 24, 2004 70 71 `````` virtual const state* filter(const state* s) = 0; `````` Alexandre Duret-Lutz committed Nov 24, 2004 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 `````` /// \brief Whether a new transition completes a path. /// /// This function is called immediately after each call to /// filter() that does not return 0. /// /// \param step the source state (as returned by filter()), and the /// labels of the outgoing transition /// \param dest the destination state (as returned by filter()) /// \return true iff a path that included this step should be accepted. /// /// The search() algorithms stops as soon as match() returns true, /// and when this happens the list argument of search() is be /// augmented with the shortest past that ends with this /// transition. virtual bool match(tgba_run::step& step, const state* dest) = 0; `````` Denis Poitrenaud committed Dec 20, 2004 87 `````` `````` Alexandre Duret-Lutz committed Jan 03, 2005 88 89 90 91 92 93 94 95 96 97 98 `````` /// \brief Append the resulting path to the resulting run. /// /// This is called after match() has returned true, to append the /// resulting path to \a l. This seldom needs to be overridden, /// unless you do not want \a l to be updated (in which case an empty /// finalize() will do). virtual void finalize(const std::map& father, const tgba_run::step& s, const state* start, tgba_run::steps& l); `````` Denis Poitrenaud committed Dec 20, 2004 99 `````` `````` Alexandre Duret-Lutz committed Nov 24, 2004 100 `````` protected: `````` Alexandre Duret-Lutz committed Nov 24, 2004 101 `````` const tgba* a_; ///< The spot::tgba we are searching into. `````` Alexandre Duret-Lutz committed Nov 24, 2004 102 103 `````` }; `````` Alexandre Duret-Lutz committed Nov 24, 2004 104 `````` `````` Alexandre Duret-Lutz committed Nov 24, 2004 105 106 107 ``````} #endif // SPOT_TGBAALGOS_BFSSTEPS_HH``````