tgta.hh 3.26 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Apr 22, 2015 2 3 ``````// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). `````` Ala-Eddine Ben-Salem committed Aug 21, 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 Aug 21, 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 MERCHANta_explicitBILITY // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public // License for more deta_explicitils. // // 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 Aug 21, 2012 19 `````` `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 21 `````` `````` Alexandre Duret-Lutz committed Dec 04, 2015 22 ``````#include `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 23 24 25 26 27 `````` namespace spot { /// \ingroup ta_essentials `````` Alexandre Duret-Lutz committed Jun 08, 2013 28 `````` /// \brief A Transition-based Generalized Testing Automaton (TGTA). `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 29 `````` /// `````` Alexandre Duret-Lutz committed Jun 09, 2013 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 `````` /// Transition-based Generalized Testing Automaton (TGTA) is a new /// kind of automaton that combines features from both TA and TGBA. /// From TA, we take the idea of labeling transitions with /// changesets, however we remove the use of livelock-acceptance /// (because it may require a two-pass emptiness check), and the /// implicit stuttering. From TGBA, we inherit the use of /// transition-based generalized acceptance conditions. The /// resulting Chimera, which we call "Transition-based Generalized /// Testing Automaton" (TGTA), accepts only stuttering-insensitive /// languages like TA, and inherits advantages from both TA and /// TGBA: it has a simple one-pass emptiness-check procedure (the /// same as algorithm the one for TGBA), and can benefit from /// reductions based on the stuttering of the properties pretty much /// like a TA. Livelock acceptance states, which are no longer /// supported are emulated using states with a Büchi accepting /// self-loop labeled by empty changeset. `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 46 47 48 49 50 51 52 53 54 55 56 57 58 `````` /// /// Browsing such automaton can be achieved using two functions: /// \c get_initial_state and \c /// succ_iter. The former returns the initial state(s) while the latter lists /// the successor states of any state. A second implementation of \c succ_iter /// returns only the successors reached through a changeset passed as /// a parameter. /// /// Note that although this is a transition-based automata, /// we never represent transitions! Transition informations are /// obtained by querying the iterator over the successors of /// a state. `````` Alexandre Duret-Lutz committed Apr 22, 2015 59 `````` class SPOT_API tgta : public twa `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 60 61 62 `````` { protected: `````` Alexandre Duret-Lutz committed Apr 23, 2015 63 64 65 66 `````` tgta(const bdd_dict_ptr& d) : twa(d) { } `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 67 `````` `````` Alexandre Duret-Lutz committed Oct 06, 2014 68 `````` public: `````` Alexandre Duret-Lutz committed Apr 23, 2015 69 70 71 `````` virtual ~tgta() { } `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 72 73 74 75 76 77 78 79 80 `````` /// \brief Get an iterator over the successors of \a state /// filtred by the value of the changeset on transitions between the /// \a state and his successors /// /// The iterator has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no /// longer needed. /// `````` Alexandre Duret-Lutz committed Apr 22, 2015 81 `````` virtual twa_succ_iterator* `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 82 83 84 `````` succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0; }; `````` Alexandre Duret-Lutz committed Aug 15, 2014 85 86 `````` typedef std::shared_ptr tgta_ptr; typedef std::shared_ptr const_tgta_ptr; `````` Ala-Eddine Ben-Salem committed Aug 21, 2012 87 ``}``