equal
deleted
inserted
replaced
203 Node v=heap.top(); |
203 Node v=heap.top(); |
204 ValueType oldvalue=heap[v]; |
204 ValueType oldvalue=heap[v]; |
205 heap.pop(); |
205 heap.pop(); |
206 distance.set(v, oldvalue); |
206 distance.set(v, oldvalue); |
207 |
207 |
208 for(OutEdgeIt e(G,v); G.valid(e); G.next(e)) { |
208 for(OutEdgeIt e = G.template first<OutEdgeIt>(v); |
|
209 G.valid(e); G.next(e)) { |
209 Node w=G.head(e); |
210 Node w=G.head(e); |
210 |
211 |
211 switch(heap.state(w)) { |
212 switch(heap.state(w)) { |
212 case heap.PRE_HEAP: |
213 case heap.PRE_HEAP: |
213 // reach.set(w,true); |
214 // reach.set(w,true); |