class GBN_GIDN_ITERATOR
  -- Emits nodes in unpredictable sequence from a graph

inherit
  GBN_ITERATOR [GBN_NODE]

creation {GBN_GEN_GNODE}
  make

feature {NONE}

  make ( graf : like the_graph ) is
    require
      nonvoid: graf /= Void
    do
      the_graph := graf
      if the_graph . node_count > 0 then
          cursor := 1
      end
  
      if not finished then
        the_graph . logon
      end
    ensure
      valid_graph: the_graph = graf
      empty_finished: the_graph.node_count = 0 implies finished
      finished_empty: finished implies the_graph . node_count = 0
      valid_node : finished or else the_graph.has_node ( item )
      protection: finished or else the_graph . is_protected
    end

 feature {ANY} 

  the_graph : GBN_GEN_DGRAPH
        -- only public to allow
        -- the ensure clauses with make and forth

  finished: BOOLEAN is
    do
       Result := cursor <= 0 or cursor > the_graph.node_count
    end

  forth is
    do
      cursor := cursor + 1
      if cursor > the_graph.node_count then
        the_graph.logoff
      end
    ensure
      -- forth has no postconditions in parent class, hence no then
      has_node: finished or else  the_graph . has_node ( item )
    end

  stop is
    do
      cursor := the_graph.node_count + 1
      the_graph . logoff
    end

  item : GBN_NODE is
    do
      Result := the_graph . nodes . item ( cursor )
    end
    

feature {NONE}
  cursor : integer
end -- class GBN_GIDN_ITERATOR [G]