1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010, 2012-2017 Laboratoire de Recherche et 3 // Developpement de l Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <set> 23 24 #include <cassert> 25 #include <spot/misc/bddlt.hh> 26 #include <spot/twa/twa.hh> 27 28 namespace spot 29 { 30 31 // Forward declarations. See below. 32 class ta_succ_iterator; 33 34 /// \defgroup ta TA (Testing Automata) 35 /// 36 /// This type and its cousins are listed \ref ta_essentials "here". 37 /// This is an abstract interface. Its implementations are \ref 38 /// ta_representation "concrete representations". The 39 /// algorithms that work on spot::ta are \ref ta_algorithms 40 /// "listed separately". 41 42 /// \addtogroup ta_essentials Essential TA types 43 /// \ingroup ta 44 45 /// \ingroup ta_essentials 46 /// \brief A Testing Automaton. 47 /// 48 /// The Testing Automata (TA) were introduced by 49 /// Henri Hansen, Wojciech Penczek and Antti Valmari 50 /// in "Stuttering-insensitive automata for on-the-fly detection of livelock 51 /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in 52 /// Theoretical Computer Science.Elsevier. 53 /// 54 /// While a TGBA automaton observes the value of the atomic propositions, the 55 /// basic idea of TA is to detect the changes in these values; if a valuation 56 /// does not change between two consecutive valuations of an execution, 57 /// the TA stay in the same state. A TA transition \c (s,k,d) is labeled by a 58 /// "changeset" \c k: i.e. the set of atomic propositions that change between 59 /// states \c s and \c d, if the changeset is empty then the transition is 60 /// called stuttering transition. 61 /// To detect execution that ends by stuttering in the same TA state, a 62 /// new kind of acceptance states is introduced: "livelock-acceptance states" 63 /// (in addition to the standard Buchi-acceptance states). 64 /// 65 /// Browsing such automaton can be achieved using two functions: 66 /// \c get_initial_states_set or \c get_artificial_initial_state, and \c 67 /// succ_iter. The former returns the initial state(s) while the latter lists 68 /// the successor states of any state (filtred by "changeset"). 69 /// 70 /// Note that although this is a transition-based automata, 71 /// we never represent transitions! Transition informations are 72 /// obtained by querying the iterator over the successors of 73 /// a state. 74 75 class SPOT_API ta 76 { 77 protected: 78 acc_cond acc_; 79 bdd_dict_ptr dict_; 80 81 public: ta(const bdd_dict_ptr & d)82 ta(const bdd_dict_ptr& d) 83 : dict_(d) 84 { 85 } 86 87 virtual ~ta()88 ~ta() 89 { 90 } 91 92 typedef std::set<state*, state_ptr_less_than> states_set_t; 93 typedef std::set<const state*, state_ptr_less_than> const_states_set_t; 94 95 /// \brief Get the initial states set of the automaton. 96 virtual const_states_set_t 97 get_initial_states_set() const = 0; 98 99 /// \brief Get the artificial initial state set of the automaton. 100 /// Return 0 if this artificial state is not implemented 101 /// (in this case, use \c get_initial_states_set) 102 /// The aim of adding this state is to have a unique initial state. This 103 /// artificial initial state have one transition to each real initial state, 104 /// and this transition is labeled by the corresponding initial condition. 105 /// (For more details, see the paper cited above) 106 virtual const spot::state* get_artificial_initial_state() const107 get_artificial_initial_state() const 108 { 109 return nullptr; 110 } 111 112 /// \brief Get an iterator over the successors of \a state. 113 /// 114 /// The iterator has been allocated with \c new. It is the 115 /// responsability of the caller to \c delete it when no 116 /// longer needed. 117 /// 118 virtual ta_succ_iterator* 119 succ_iter(const spot::state* state) const = 0; 120 121 /// \brief Get an iterator over the successors of \a state 122 /// filtred by the changeset on transitions 123 /// 124 /// The iterator has been allocated with \c new. It is the 125 /// responsability of the caller to \c delete it when no 126 /// longer needed. 127 /// 128 virtual ta_succ_iterator* 129 succ_iter(const spot::state* state, bdd changeset) const = 0; 130 131 /// \brief Get the dictionary associated to the automaton. 132 /// 133 /// State are represented as BDDs. The dictionary allows 134 /// to map BDD variables back to formulae, and vice versa. 135 /// This is useful when dealing with several automata (which 136 /// may use the same BDD variable for different formula), 137 /// or simply when printing. 138 bdd_dict_ptr get_dict() const139 get_dict() const 140 { 141 return dict_; 142 } 143 144 /// \brief Format the state as a string for printing. 145 /// 146 /// This formating is the responsability of the automata 147 /// that owns the state. 148 virtual std::string 149 format_state(const spot::state* s) const = 0; 150 151 /// \brief Return true if \a s is a Buchi-accepting state, otherwise false 152 virtual bool 153 is_accepting_state(const spot::state* s) const = 0; 154 155 /// \brief Return true if \a s is a livelock-accepting state 156 /// , otherwise false 157 virtual bool 158 is_livelock_accepting_state(const spot::state* s) const = 0; 159 160 /// \brief Return true if \a s is an initial state, otherwise false 161 virtual bool 162 is_initial_state(const spot::state* s) const = 0; 163 164 /// \brief Return a BDD condition that represents the valuation 165 /// of atomic propositions in the state \a s 166 virtual bdd 167 get_state_condition(const spot::state* s) const = 0; 168 169 /// \brief Release a state \a s 170 virtual void 171 free_state(const spot::state* s) const = 0; 172 173 acc() const174 const acc_cond& acc() const 175 { 176 return acc_; 177 } 178 acc()179 acc_cond& acc() 180 { 181 return acc_; 182 } 183 184 }; 185 186 typedef std::shared_ptr<ta> ta_ptr; 187 typedef std::shared_ptr<const ta> const_ta_ptr; 188 189 /// \ingroup ta_essentials 190 /// \brief Iterate over the successors of a state. 191 /// 192 /// This class provides the basic functionalities required to 193 /// iterate over the successors of a state, as well as querying 194 /// transition labels. Because transitions are never explicitely 195 /// encoded, labels (conditions and acceptance conditions) can only 196 /// be queried while iterating over the successors. 197 class ta_succ_iterator : public twa_succ_iterator 198 { 199 public: 200 virtual ~ta_succ_iterator()201 ~ta_succ_iterator() 202 { 203 } 204 }; 205 206 #ifndef SWIG 207 // A stack of Strongly-Connected Components 208 class scc_stack_ta 209 { 210 public: 211 struct connected_component 212 { 213 public: 214 connected_component(int index = -1) noexcept; 215 216 /// Index of the SCC. 217 int index; 218 219 bool is_accepting; 220 221 /// The bdd condition is the union of all acceptance conditions of 222 /// transitions which connect the states of the connected component. 223 acc_cond::mark_t condition; 224 225 std::list<const state*> rem; 226 }; 227 228 /// Stack a new SCC with index \a index. 229 void 230 push(int index); 231 232 /// Access the top SCC. 233 connected_component& 234 top(); 235 236 /// Access the top SCC. 237 const connected_component& 238 top() const; 239 240 /// Pop the top SCC. 241 void 242 pop(); 243 244 /// How many SCC are in stack. 245 size_t 246 size() const; 247 248 /// The \c rem member of the top SCC. 249 std::list<const state*>& 250 rem(); 251 252 /// Is the stack empty? 253 bool 254 empty() const; 255 256 typedef std::list<connected_component> stack_type; 257 stack_type s; 258 }; 259 #endif // !SWIG 260 261 /// \addtogroup ta_representation TA representations 262 /// \ingroup ta 263 264 /// \addtogroup ta_algorithms TA algorithms 265 /// \ingroup ta 266 267 /// \addtogroup ta_io Input/Output of TA 268 /// \ingroup ta_algorithms 269 270 /// \addtogroup tgba_ta Transforming TGBA into TA 271 /// \ingroup ta_algorithms 272 273 274 /// \addtogroup ta_generic Algorithm patterns 275 /// \ingroup ta_algorithms 276 277 /// \addtogroup ta_reduction TA simplifications 278 /// \ingroup ta_algorithms 279 280 /// \addtogroup ta_misc Miscellaneous algorithms on TA 281 /// \ingroup ta_algorithms 282 } 283