tgba2ta.hh 4.54 KB
 Alexandre Duret-Lutz committed Aug 21, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Mar 30, 2017 2 ``````// Copyright (C) 2010, 2012-2015, 2017 Laboratoire de Recherche et `````` Alexandre Duret-Lutz committed Jul 29, 2013 3 ``````// Développement de l'Epita (LRDE). `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 4 5 6 7 8 ``````// // 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 9 ``````// the Free Software Foundation; either version 3 of the License, or `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 10 11 12 13 14 15 16 17 ``````// (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 18 ``````// along with this program. If not, see . `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 19 `````` `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 21 `````` `````` Alexandre Duret-Lutz committed Dec 04, 2015 22 23 24 ``````#include #include #include `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 25 26 27 `````` namespace spot { `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 28 `````` /// \ingroup tgba_ta `````` Alexandre Duret-Lutz committed Jun 08, 2013 29 `````` /// \brief Build a spot::ta_explicit* (TA) from an LTL formula. `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 30 31 `````` /// /// This is based on the following paper. `````` Alexandre Duret-Lutz committed Jun 09, 2013 32 33 34 35 36 37 38 39 40 41 42 43 44 `````` /** \verbatim @InProceedings{ geldenhuys.06.spin, author = {Jaco Geldenhuys and Henri Hansen}, title = {Larger Automata and Less Work for {LTL} Model Checking}, booktitle = {Proceedings of the 13th International SPIN Workshop (SPIN'06)}, year = {2006}, pages = {53--70}, series = {Lecture Notes in Computer Science}, volume = {3925}, publisher = {Springer} } \endverbatim */ `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 45 46 47 48 49 50 `````` /// /// \param tgba_to_convert The TGBA automaton to convert into a TA automaton /// /// \param atomic_propositions_set The set of atomic propositions used in the /// input TGBA \a tgba_to_convert /// `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 51 52 `````` /// \param degeneralized When false, the returned automaton is a generalized /// form of TA, called GTA (Generalized Testing Automaton). `````` Alexandre Duret-Lutz committed Aug 21, 2012 53 `````` /// Like TGBA, GTA use Generalized Büchi acceptance `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 54 55 56 57 58 59 `````` /// conditions intead of Buchi-accepting states: there are several acceptance /// sets (of transitions), and a path is accepted if it traverses /// at least one transition of each set infinitely often or if it contains a /// livelock-accepting cycle (like a TA). The spot emptiness check algorithm /// for TA (spot::ta_check::check) can also be used to check GTA. /// `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 60 `````` /// \param artificial_initial_state_mode When set, the algorithm will build `````` Alexandre Duret-Lutz committed Mar 30, 2017 61 `````` /// a TA automaton with a unique initial state. This `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 62 63 64 65 `````` /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (see spot::ta::get_artificial_initial_state()) /// `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 66 67 68 69 70 71 72 73 `````` /// \param single_pass_emptiness_check When set, the product between the /// returned automaton and a kripke structure requires only the fist pass of /// the emptiness check algorithm (see the parameter \c disable_second_pass /// of the method spot::ta_check::check) /// /// /// \param artificial_livelock_state_mode When set, the returned TA automaton /// is a STA (Single-pass Testing Automata): a STA automaton is a TA `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 74 75 76 77 `````` /// where: for every livelock-accepting state s, if s is not also a /// Buchi-accepting state, then s has no successors. A STA product requires /// only one-pass emptiness check algorithm (see spot::ta_check::check) /// `````` Alexandre Duret-Lutz committed Apr 02, 2015 78 79 80 `````` /// \param no_livelock when set, this disable the replacement of /// stuttering components by livelock states. Use this flag to /// demonstrate an intermediate step of the construction. `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 81 82 83 `````` /// /// \return A spot::ta_explicit that recognizes the same language as the /// TGBA \a tgba_to_convert. `````` Alexandre Duret-Lutz committed Aug 15, 2014 84 `````` SPOT_API ta_explicit_ptr `````` Alexandre Duret-Lutz committed Apr 22, 2015 85 `````` tgba_to_ta(const const_twa_ptr& tgba_to_convert, bdd atomic_propositions_set, `````` Laurent XU committed Mar 10, 2016 86 87 88 89 90 `````` bool degeneralized = true, bool artificial_initial_state_mode = true, bool single_pass_emptiness_check = false, bool artificial_livelock_state_mode = false, bool no_livelock = false); `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 91 `````` `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 92 `````` /// \ingroup tgba_ta `````` Alexandre Duret-Lutz committed Jun 08, 2013 93 `````` /// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula. `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 94 `````` /// `````` Alexandre Duret-Lutz committed Jun 08, 2013 95 `````` /// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 96 97 98 `````` /// \param atomic_propositions_set The set of atomic propositions used in the /// input TGBA \a tgba_to_convert /// `````` Alexandre Duret-Lutz committed Aug 21, 2012 99 `````` /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 100 `````` /// language as the TGBA \a tgba_to_convert. `````` Alexandre Duret-Lutz committed Aug 15, 2014 101 `````` SPOT_API tgta_explicit_ptr `````` Alexandre Duret-Lutz committed Apr 22, 2015 102 `````` tgba_to_tgta(const const_twa_ptr& tgba_to_convert, `````` Laurent XU committed Mar 10, 2016 103 `````` bdd atomic_propositions_set); `````` Ala-Eddine Ben-Salem committed Jul 15, 2012 104 ``}``