ltl2tgba_fm.hh 5.48 KB
 Alexandre Duret-Lutz committed Jan 30, 2010 1 2 ``````// Copyright (C) 2010 Laboratoire de Recherche et Développement de // l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Feb 25, 2008 3 4 5 ``````// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. `````` Alexandre Duret-Lutz committed Nov 21, 2003 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``````// // 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 24 25 ``````#ifndef SPOT_TGBAALGOS_LTL2TGBA_FM_HH # define SPOT_TGBAALGOS_LTL2TGBA_FM_HH `````` Alexandre Duret-Lutz committed Aug 15, 2003 26 27 28 `````` #include "ltlast/formula.hh" #include "tgba/tgbaexplicit.hh" `````` Alexandre Duret-Lutz committed Sep 23, 2004 29 ``````#include "ltlvisit/apcollect.hh" `````` Alexandre Duret-Lutz committed May 04, 2005 30 ``````#include "ltlvisit/reduce.hh" `````` Alexandre Duret-Lutz committed Aug 15, 2003 31 32 33 34 `````` namespace spot { /// \brief Build a spot::tgba_explicit* from an LTL formula. `````` Alexandre Duret-Lutz committed Nov 17, 2004 35 `````` /// \ingroup tgba_ltl `````` Alexandre Duret-Lutz committed Aug 15, 2003 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 `````` /// /// This is based on the following paper. /// \verbatim /// @InProceedings{couvreur.99.fm, /// author = {Jean-Michel Couvreur}, /// title = {On-the-fly Verification of Temporal Logic}, /// pages = {253--271}, /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, /// booktitle = {Proceedings of the World Congress on Formal Methods in the /// Development of Computing Systems (FM'99)}, /// publisher = {Springer-Verlag}, /// series = {Lecture Notes in Computer Science}, /// volume = {1708}, /// year = {1999}, /// address = {Toulouse, France}, /// month = {September}, /// isbn = {3-540-66587-0} /// } `````` Alexandre Duret-Lutz committed May 07, 2004 54 `````` /// \endverbatim `````` Alexandre Duret-Lutz committed Feb 09, 2004 55 `````` /// `````` Alexandre Duret-Lutz committed Nov 17, 2004 56 `````` /// \param f The formula to translate into an automaton. `````` Alexandre Duret-Lutz committed Aug 09, 2004 57 58 59 60 `````` /// /// \param dict The spot::bdd_dict the constructed automata should use. /// /// \param exprop When set, the algorithm will consider all properties `````` Alexandre Duret-Lutz committed Feb 09, 2004 61 `````` /// combinations possible on each state, in an attempt to reduce `````` Alexandre Duret-Lutz committed Feb 16, 2004 62 63 `````` /// the non-determinism. The automaton will have the same size as /// without this option, but because the transition will be more `````` Alexandre Duret-Lutz committed May 07, 2004 64 65 `````` /// deterministic, the product automaton will be smaller (or, at worse, /// equal). `````` Alexandre Duret-Lutz committed Feb 16, 2004 66 `````` /// `````` Alexandre Duret-Lutz committed Aug 09, 2004 67 `````` /// \param symb_merge When false, states with the same symbolic `````` Alexandre Duret-Lutz committed Feb 16, 2004 68 69 `````` /// representation (these are equivalent formulae) will not be /// merged. `````` Alexandre Duret-Lutz committed May 07, 2004 70 `````` /// `````` Alexandre Duret-Lutz committed Aug 09, 2004 71 `````` /// \param branching_postponement When set, several transitions leaving `````` Alexandre Duret-Lutz committed May 07, 2004 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 `````` /// from the same state with the same label (i.e., condition + acceptance /// conditions) will be merged. This correspond to an optimization /// described in the following paper. /// \verbatim /// @InProceedings{ sebastiani.03.charme, /// author = {Roberto Sebastiani and Stefano Tonetta}, /// title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for /// Efficient LTL Model Checking}, /// booktitle = {Proceedings for the 12th Advanced Research Working /// Conference on Correct Hardware Design and Verification /// Methods (CHARME'03)}, /// pages = {126--140}, /// year = {2003}, /// editor = {G. Goos and J. Hartmanis and J. van Leeuwen}, /// volume = {2860}, /// series = {Lectures Notes in Computer Science}, /// month = {October}, /// publisher = {Springer-Verlag} /// } `````` Alexandre Duret-Lutz committed Aug 15, 2003 91 `````` /// \endverbatim `````` Alexandre Duret-Lutz committed May 10, 2004 92 `````` /// `````` Alexandre Duret-Lutz committed Aug 09, 2004 93 `````` /// \param fair_loop_approx When set, a really simple characterization of `````` Alexandre Duret-Lutz committed May 10, 2004 94 95 `````` /// unstable state is used to suppress all acceptance conditions from /// incoming transitions. `````` Alexandre Duret-Lutz committed Aug 09, 2004 96 `````` /// `````` Alexandre Duret-Lutz committed Sep 23, 2004 97 98 99 100 `````` /// \param unobs When non-zero, the atomic propositions in the LTL formula /// are interpreted as events that exclude each other. The events in the /// formula are observable events, and \c unobs can be filled with /// additional unobservable events. `````` Alexandre Duret-Lutz committed May 04, 2005 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 `````` /// /// \param reduce_ltl If this parameter is set, the LTL formulae representing /// each state of the automaton will be simplified using spot::ltl::reduce() /// before computing the successor. \a reduce_ltl should specify the type /// of reduction to apply as documented for spot::ltl::reduce(). /// This idea is taken from the following paper. /// \verbatim /// @InProceedings{ thirioux.02.fmics, /// author = {Xavier Thirioux}, /// title = {Simple and Efficient Translation from {LTL} Formulas to /// {B\"u}chi Automata}, /// booktitle = {Proceedings of the 7th International ERCIM Workshop in /// Formal Methods for Industrial Critical Systems (FMICS'02)}, /// series = {Electronic Notes in Theoretical Computer Science}, /// volume = {66(2)}, /// publisher = {Elsevier}, /// editor = {Rance Cleaveland and Hubert Garavel}, /// year = {2002}, /// month = jul, /// address = {M{\'a}laga, Spain} /// } /// \endverbatim /// `````` Alexandre Duret-Lutz committed Aug 11, 2004 124 `````` /// \return A spot::tgba_explicit that recognizes the language of \a f. `````` Alexandre Duret-Lutz committed Feb 09, 2004 125 `````` tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, `````` Alexandre Duret-Lutz committed May 07, 2004 126 `````` bool exprop = false, bool symb_merge = true, `````` Alexandre Duret-Lutz committed May 10, 2004 127 `````` bool branching_postponement = false, `````` Alexandre Duret-Lutz committed Sep 23, 2004 128 `````` bool fair_loop_approx = false, `````` Alexandre Duret-Lutz committed May 04, 2005 129 `````` const ltl::atomic_prop_set* unobs = 0, `````` Alexandre Duret-Lutz committed Jan 30, 2010 130 `````` int reduce_ltl = ltl::Reduce_None); `````` Alexandre Duret-Lutz committed Aug 15, 2003 131 132 ``````} `````` Alexandre Duret-Lutz committed Jan 03, 2005 133 ``#endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH``