note
	description: "[
		Mathematical model for a Directed Graph = (vertices, edges)
		where vertices is a set of vertices in generic parameter V, 
		and edges is a relation in vertices:
			vertices: SET [V]
			edges: REL [V, V]
		Has immutable queries and commands 
		to add and remove vertices and edges. 
		Also derived queries for outgoing and incoming edges:
			outgoing (v: V): REL[V, V]
			incoming (v: V): REL[V, V]
			adjacent (v: V): SEQ [V]
		adjacent is a sequence of vertices that may be
		ordered in descendants such as COMPARABLE_GRAPH[G].
		Derived queries such as: 
			reachable (src: V): SEQ[V]
			shortest_path(v1, v2: V): detachable SEQ[V]
			is_a_shortest_path (v1, v2: V; seq: SEQ[V]): BOOLEAN
			cycle (v: V): detachable SEQ[V]
			is_acyclic: BOOLEAN
			topologically_sorted: SEQ[V]
			is_topologically_sorted (seq: SEQ[V]): BOOLEAN
		where reachable uses breadth-first search starting with vertex src,
		to return the set of all nodes reachable from src.
		shortest_path returns the shortest path between v1 and v2 if it exists.
	]"
	author: "JSO and JW"
	date: "$Date$"
	revision: "$Revision$"

class interface
	GRAPH [V -> attached ANY]

create 
	make_empty,
	make_from_tuple_array

convert
	make_from_tuple_array ({attached ARRAY [TUPLE [V, V]]})

feature -- Iterable

	new_cursor: ITERATION_CURSOR [V]
			-- Fresh cursor associated with current structure
	
feature -- Conversion to array.

	as_array: ARRAY [TUPLE [V, V]]
			-- Return edges as an array of tuples

	array_compare (a, b: ARRAY [TUPLE [V, V]]): BOOLEAN
			-- compare two arrays of tuple
	
feature -- model

	edges: REL [V, V]

	vertices: SET [V]
	
feature -- basic queries

	edge_count: INTEGER_32
			-- number of outgoing edges

	vertex_count: INTEGER_32

	is_empty: BOOLEAN
			-- is the graph empty?

	has_vertex (v: V): BOOLEAN

	has_edge (p: PAIR [V, V]): BOOLEAN
			-- does graph have pair p
			-- can use p as tuple

	outgoing (v: V): REL [V, V]
			-- The set of outgoing edges from v
		ensure
			consistent_counts: Result.count = (edges @< v).count
			source_is_v: across
					Result as e
				all
					e.item.first ~ v
				end

	incoming (v: V): REL [V, V]
			-- The set of incoming edges to v
		ensure
			consistent_counts: Result.count = (edges @> v).count
			destination_is_v: across
					Result as e
				all
					e.item.second ~ v
				end

	in_degree_count (v: V): INTEGER_32
			-- number of incoming edges of vertex v
		require
				has_vertex (v)

	out_degree_count (v: V): INTEGER_32
			-- number of outgoing edges of vertex v
		require
				has_vertex (v)

	adjacent (v: V): SEQ [V]
			-- The list of vertices adjacent to v via outgoing edges.
			-- This list is not necessarily sorted.
		ensure
			consistent_counts: Result.count = outgoing (v).count
			source_is_v: across
					Result as x
				all
					outgoing (v).has (create {PAIR [V, V]}.make_from_tuple ([v, x.item]))
				end

	vertex_extended alias "+" (v: V): like Current
			-- extend if not already in

	edge_extended alias "|\/|" (e: PAIR [V, V]): like Current
			-- extend if not already in
		require
			valid_vertices: has_vertex (e.first) and has_vertex (e.second)

	vertex_removed alias "-" (v: V): like Current

	edge_removed alias "|\" (e: PAIR [V, V]): like Current
	
feature -- advanced queries

	topologically_sorted: SEQ [V]
			-- Return a sequence <<..., vi, ..., vj, ...>> such that
			-- (vi, vj) in edges => i < j
			-- A topological sort is performed.
		require
				is_acyclic
		ensure
				is_topologically_sorted (Result)

	is_topologically_sorted (seq: like topologically_sorted): BOOLEAN

	reachable (src: V): SEQ [V]
			-- Breadth-First Search
			-- Starting with vertex src,
			-- return the set of all nodes reachable from src.
			-- Uses adjacent (a sorted list in COMPARABLE_GRAPH) rather than outgoing (always unsorted REL)
		require
				has_vertex (src)
		ensure
			every_vertex_in_result_is_reachable_from_src: across
					Result as v
				all
					is_reachable (src, v.item)
				end
			every_vertex_reachable_from_src_is_in_result: across
					vertices as v
				all
					is_reachable (src, v.item) implies Result.has (v.item)
				end

	paths (v1, v2: V): SET [SEQ [V]]
			-- Return the set of all acyclic paths (ones not containing cycles) between v1 and v2.
		ensure
			all_paths_are_valid: across
					Result as path
				all
					is_valid_path (path.item) and then path.item.first ~ v1 and then path.item.last ~ v2
				end

	shortest_path (v1, v2: V): detachable SEQ [V]
			-- Return the shortest path between v1 and v2 if it exists.
			-- Bredth-First Search is used without assuming that there are no self-loops.
		ensure
			void_result: not attached Result implies not (has_vertex (v1) and then has_vertex (v2) and then is_reachable (v1, v2))
			result_is_valid: attached Result implies is_valid_path (Result) and then Result.first ~ v1 and then Result.last ~ v2
			result_is_the_shortest: attached Result implies across
					paths (v1, v2) as path
				all
					Result.count <= path.item.count
				end

	is_a_shortest_path (v1, v2: V; seq: SEQ [V]): BOOLEAN
			-- does seq denote a shortest path between v1 and v2?
			-- When there are multiple shortest paths between v1 and v2,
			-- return TRUE if seq is any one of them.

	shortest_path_via_dijkstra (v1, v2: V): detachable SEQ [V]
			-- Return the shortest path between v1 and v2 if it exists.
			-- Dijkstra's algorithm is used without assuming that there are no self-loops.
			-- Cost of path: Result.count - 1
		ensure
			void_result: not attached Result implies not (has_vertex (v1) and then has_vertex (v2) and then is_reachable (v1, v2))
			result_is_valid: attached Result implies is_valid_path (Result) and then Result.first ~ v1 and then Result.last ~ v2
			result_is_the_shortest: attached Result implies across
					paths (v1, v2) as path
				all
					Result.count <= path.item.count
				end

	is_reachable (v1, v2: V): BOOLEAN
		require
				has_vertex (v1) and has_vertex (v2)
		ensure
				Result = attached shortest_path (v1, v2)

	is_valid_path (seq: SEQ [V]): BOOLEAN
			-- Does seq denote a valid path in graph?
		require
			at_least_one_vertex: not seq.is_empty
		ensure
			singleton_path: seq.count = 1 implies (vertices.has (seq [1]) = Result)
			longer_path: seq.count > 1 implies (Result = across
					2 |..| seq.count as i
				all
					edges.has (create {PAIR [V, V]}.make_from_tuple ([seq [i.item - 1], seq [i.item]]))
				end)

	is_subgraph alias "|<:" (other: like Current): BOOLEAN

	is_equal (other: like Current): BOOLEAN
			-- Is other attached to an object considered
			-- equal to current object?

	is_acyclic: BOOLEAN
			-- Does the graph contain no cycles?
		ensure
				Result = across
					vertices is l_v
				all
					not attached cycle (l_v)
				end

	cycle (v: V): detachable SEQ [V]
			-- Return a cycle starting from v if any.
	
feature -- commands

	vertex_extend (v: V)
			-- insert vertex v into graph
			-- if not already in
		ensure
				vertices ~ old vertices.deep_twin + v
				edges ~ old edges.deep_twin

	edge_extend (e: PAIR [V, V])
			-- connect vertex e.first to e.second
			-- if not already in
		require
			valid_vertices: has_vertex (e.first) and has_vertex (e.second)
		ensure
				edges ~ old edges.deep_twin + create {PAIR [V, V]}.make_from_tuple ([e.first, e.second])
				vertices ~ old vertices.deep_twin

	vertex_remove (v: V)
			-- Remove vertex v and all relevant edges
		ensure
				vertices ~ old vertices.deep_twin - v
				edges ~ (old edges.deep_twin @>> v) @<< v

	edge_remove (e: PAIR [V, V])
	
feature -- out

	out: STRING_8
			-- New string containing terse printable representation
			-- of current object

	debug_output: STRING_8
			-- String that should be displayed in debugger to represent Current.
	
feature -- infinity

	Infinity: INTEGER_64

	Zero: INTEGER_64
	
feature -- agent functions

	vertices_edge_count: INTEGER_32
			-- total number of incoming and outgoing edges of all vertices in vertices
			-- Result = (Σv ∈ vertices : outgoing(v).count + incoming(v).count)

	vertices_outgoing_edge_count: INTEGER_32
			-- total number of outgoing edges of all vertices in vertices
			-- Result = (Σv ∈ vertices : outgoing(v).count)

	vertices_incoming_edge_count: INTEGER_32
			-- total number of incoming edges of all vertices in vertices
			-- Result = (Σv ∈ vertices : incoming(v).count)
	
invariant
	empty_consistency: vertex_count = 0 implies edge_count = 0
	valid_edge_ends: edges.domain |\/| edges.range |<: vertices
		vertex_count = vertices.count
	consistency_incoming_outgoing: across
			vertices is l_vertex
		all
			across
				outgoing (l_vertex) is l_edge
			all
				incoming (l_edge.second).has (l_edge)
			end and across
				incoming (l_vertex) is l_edge
			all
				outgoing (l_edge.first).has (l_edge)
			end
		end
	consistency_incoming_outgoing2: across
			edges is l_edge
		all
			outgoing (l_edge.first).has (l_edge) and incoming (l_edge.second).has (l_edge)
		end
	count_property_symmetry_1: vertices_edge_count = 2 * edge_count
	count_property_symmetry_2: vertices_outgoing_edge_count = vertices_incoming_edge_count
	self_loops_are_incomng_and_outgoing: across
			vertices is l_vertex
		all
			across
				incoming (l_vertex) is l_edge
			some
				l_edge.first ~ l_edge.second
			end = across
				outgoing (l_vertex) is l_edge
			some
				l_edge.first ~ l_edge.second
			end
		end

end -- class GRAPH

Generated by ISE EiffelStudio