tau03opt.hh 3.43 KB
Newer Older
 Alexandre Duret-Lutz committed Jan 03, 2005 1 ``````// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Denis Poitrenaud committed Nov 18, 2004 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````// 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 // the Free Software Foundation; either version 2 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 Spot; see the file COPYING. If not, write to the Free // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. `````` Alexandre Duret-Lutz committed Jan 03, 2005 22 23 ``````#ifndef SPOT_TGBAALGOS_TAU03OPT_HH # define SPOT_TGBAALGOS_TAU03OPT_HH `````` Denis Poitrenaud committed Nov 18, 2004 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` namespace spot { class tgba; class emptiness_check; /// \addtogroup emptiness_check_algorithms /// @{ /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// /// \pre The automaton \a a must have at least one accepting condition. /// /// During the visit of \a a, the returned checker stores explicitely all /// the traversed states. The implemented algorithm is the following: /// /// \verbatim /// procedure check () /// begin `````` Denis Poitrenaud committed Nov 25, 2004 43 `````` /// weight = 0; // the null vector `````` Denis Poitrenaud committed Nov 18, 2004 44 45 46 47 48 49 50 `````` /// call dfs_blue(s0); /// end; /// /// procedure dfs_blue (s) /// begin /// s.color = cyan; /// s.acc = emptyset; `````` Denis Poitrenaud committed Nov 25, 2004 51 `````` /// s.weight = weight; `````` Denis Poitrenaud committed Nov 18, 2004 52 53 54 `````` /// for all t in post(s) do /// let (s, l, a, t) be the edge from s to t; /// if t.color == white then `````` Denis Poitrenaud committed Nov 25, 2004 55 56 57 `````` /// for all b in a do /// weight[b] = weight[b] + 1; /// end for; `````` Denis Poitrenaud committed Nov 18, 2004 58 `````` /// call dfs_blue(t); `````` Denis Poitrenaud committed Nov 25, 2004 59 60 61 62 63 64 `````` /// for all b in a do /// weight[b] = weight[b] - 1; /// end for; /// else /// Acc = s.acc U a; /// if t.color == cyan && `````` Alexandre Duret-Lutz committed Jan 18, 2005 65 `````` /// (Acc U support(weight -t.weight) U t.acc) == all_acc then `````` Denis Poitrenaud committed Nov 25, 2004 66 67 `````` /// report a cycle; /// else if Acc not included in t.acc then `````` Alexandre Duret-Lutz committed Jan 18, 2005 68 `````` /// t.acc := t.acc U Acc `````` Denis Poitrenaud committed Nov 25, 2004 69 70 `````` /// call dfs_red(t, Acc); /// end if; `````` Denis Poitrenaud committed Nov 18, 2004 71 72 73 74 75 `````` /// end if; /// end for; /// s.color = blue; /// end; /// `````` Denis Poitrenaud committed Nov 25, 2004 76 `````` /// procedure dfs_red(s, Acc) `````` Denis Poitrenaud committed Nov 18, 2004 77 78 79 `````` /// begin /// for all t in post(s) do /// let (s, l, a, t) be the edge from s to t; `````` Denis Poitrenaud committed Nov 25, 2004 80 81 82 83 `````` /// if t.color == cyan && /// (Acc U support(weight -t.weight) U t.acc) == all_acc then /// report a cycle; /// else if t.color != white and Acc not included in t.acc then `````` Alexandre Duret-Lutz committed Jan 18, 2005 84 `````` /// t.acc := t.acc U Acc `````` Denis Poitrenaud committed Nov 25, 2004 85 `````` /// call dfs_red(t, Acc); `````` Denis Poitrenaud committed Nov 18, 2004 86 87 88 89 90 `````` /// end if; /// end for; /// end; /// \endverbatim /// `````` Denis Poitrenaud committed Nov 25, 2004 91 92 93 94 95 96 97 `````` /// This algorithm is a generalisation to TGBA of the one implemented in /// spot::explicit_se05_search. It is based on the acceptance set labelling /// of states used in spot::explicit_tau03_search. Moreover, it introduce /// a slight optimisation based on vectors of integers counting for each /// acceptance condition how many time the condition has been visited in /// the path stored in the blue stack. Such a vector is associated to each /// state of this stack. `````` Denis Poitrenaud committed Nov 18, 2004 98 99 100 101 102 103 `````` /// emptiness_check* explicit_tau03_opt_search(const tgba *a); /// @} } `````` Alexandre Duret-Lutz committed Jan 03, 2005 104 ``#endif // SPOT_TGBAALGOS_TAU03OPT_HH``