ltl2tgba_fm.hh 3.72 KB
 Alexandre Duret-Lutz committed Feb 09, 2004 1 ``````// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed Nov 21, 2003 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 Aug 15, 2003 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 ``````#ifndef SPOT_TGBA_LTL2TGBA_FME_HH # define SPOT_TGBA_LTL2TGBA_FME_HH #include "ltlast/formula.hh" #include "tgba/tgbaexplicit.hh" namespace spot { /// \brief Build a spot::tgba_explicit* from an LTL formula. /// /// 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 49 `````` /// \endverbatim `````` Alexandre Duret-Lutz committed Feb 09, 2004 50 51 52 `````` /// /// If \a exprop is set, the algorithm will consider all properties /// combinations possible on each state, in an attempt to reduce `````` Alexandre Duret-Lutz committed Feb 16, 2004 53 54 `````` /// 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 55 56 `````` /// deterministic, the product automaton will be smaller (or, at worse, /// equal). `````` Alexandre Duret-Lutz committed Feb 16, 2004 57 58 59 60 `````` /// /// If \a symb_merge is set to false, states with the same symbolic /// representation (these are equivalent formulae) will not be /// merged. `````` Alexandre Duret-Lutz committed May 07, 2004 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` /// /// If \a branching_postponement is set, several transitions leaving /// 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 82 `````` /// \endverbatim `````` Alexandre Duret-Lutz committed May 10, 2004 83 84 85 86 `````` /// /// If \a fair_loop_approx is set, a really simple characterization of /// unstable state is used to suppress all acceptance conditions from /// incoming transitions. `````` Alexandre Duret-Lutz committed Feb 09, 2004 87 `````` tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, `````` Alexandre Duret-Lutz committed May 07, 2004 88 `````` bool exprop = false, bool symb_merge = true, `````` Alexandre Duret-Lutz committed May 10, 2004 89 90 `````` bool branching_postponement = false, bool fair_loop_approx = false); `````` Alexandre Duret-Lutz committed Aug 15, 2003 91 92 93 ``````} #endif // SPOT_TGBA_LTL2TGBA_HH``````