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