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