1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche 3 // et Développement 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 #include "config.h" 21 #include <cassert> 22 #include <spot/taalgos/reachiter.hh> 23 24 #include <iostream> 25 using namespace std; 26 27 namespace spot 28 { 29 // ta_reachable_iterator 30 ////////////////////////////////////////////////////////////////////// 31 ta_reachable_iterator(const const_ta_ptr & a)32 ta_reachable_iterator::ta_reachable_iterator(const const_ta_ptr& a) : 33 t_automata_(a) 34 { 35 } ~ta_reachable_iterator()36 ta_reachable_iterator::~ta_reachable_iterator() 37 { 38 auto s = seen.begin(); 39 while (s != seen.end()) 40 { 41 // Advance the iterator before deleting the "key" pointer. 42 const state* ptr = s->first; 43 ++s; 44 t_automata_->free_state(ptr); 45 } 46 } 47 48 void run()49 ta_reachable_iterator::run() 50 { 51 int n = 0; 52 start(); 53 54 const spot::state* artificial_initial_state = 55 t_automata_->get_artificial_initial_state(); 56 57 ta::const_states_set_t init_states_set; 58 59 if (artificial_initial_state) 60 { 61 init_states_set.insert(artificial_initial_state); 62 } 63 else 64 { 65 init_states_set = t_automata_->get_initial_states_set(); 66 } 67 68 for (auto init_state: init_states_set) 69 { 70 if (want_state(init_state)) 71 add_state(init_state); 72 seen[init_state] = ++n; 73 } 74 75 const state* t; 76 while ((t = next_state())) 77 { 78 assert(seen.find(t) != seen.end()); 79 int tn = seen[t]; 80 ta_succ_iterator* si = t_automata_->succ_iter(t); 81 process_state(t, tn); 82 for (si->first(); !si->done(); si->next()) 83 { 84 const state* current = si->dst(); 85 auto s = seen.find(current); 86 bool ws = want_state(current); 87 if (s == seen.end()) 88 { 89 seen[current] = ++n; 90 if (ws) 91 { 92 add_state(current); 93 process_link(tn, n, si); 94 } 95 } 96 else 97 { 98 if (ws) 99 process_link(tn, s->second, si); 100 t_automata_->free_state(current); 101 } 102 } 103 delete si; 104 } 105 end(); 106 } 107 108 bool want_state(const state *) const109 ta_reachable_iterator::want_state(const state*) const 110 { 111 return true; 112 } 113 114 void start()115 ta_reachable_iterator::start() 116 { 117 } 118 119 void end()120 ta_reachable_iterator::end() 121 { 122 } 123 124 void process_state(const state *,int)125 ta_reachable_iterator::process_state(const state*, int) 126 { 127 } 128 129 void process_link(int,int,const ta_succ_iterator *)130 ta_reachable_iterator::process_link(int, int, const ta_succ_iterator*) 131 { 132 } 133 134 // ta_reachable_iterator_depth_first 135 ////////////////////////////////////////////////////////////////////// 136 ta_reachable_iterator_depth_first(const const_ta_ptr & a)137 ta_reachable_iterator_depth_first::ta_reachable_iterator_depth_first( 138 const const_ta_ptr& a) : 139 ta_reachable_iterator(a) 140 { 141 } 142 143 void add_state(const state * s)144 ta_reachable_iterator_depth_first::add_state(const state* s) 145 { 146 todo.push(s); 147 } 148 149 const state* next_state()150 ta_reachable_iterator_depth_first::next_state() 151 { 152 if (todo.empty()) 153 return nullptr; 154 const state* s = todo.top(); 155 todo.pop(); 156 return s; 157 } 158 159 // ta_reachable_iterator_breadth_first 160 ////////////////////////////////////////////////////////////////////// 161 ta_reachable_iterator_breadth_first(const const_ta_ptr & a)162 ta_reachable_iterator_breadth_first::ta_reachable_iterator_breadth_first( 163 const const_ta_ptr& a) : 164 ta_reachable_iterator(a) 165 { 166 } 167 168 void add_state(const state * s)169 ta_reachable_iterator_breadth_first::add_state(const state* s) 170 { 171 todo.emplace_back(s); 172 } 173 174 const state* next_state()175 ta_reachable_iterator_breadth_first::next_state() 176 { 177 if (todo.empty()) 178 return nullptr; 179 const state* s = todo.front(); 180 todo.pop_front(); 181 return s; 182 } 183 184 } 185