note description: "[ Descendant of GRAPH[V] where V is now COMPARABLE. Mathematical model for a Directed Graph = (vertices, edges) where vertices is a set of comparable vertices in generic parameter V, and edges is a relation in vertices: vertices: SET [V] edges: REL [V, V] Inherits 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 redefined as sorted sequence of (comprable) vertices to uniquely define shortest paths etc. Derived queries such as: reachable (src: V): SEQ[V] shortest_path(v1, v2: V): detachable SEQ[V] 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. Also has queries for cycles and topological sort. ]" author: "JSO and JW" date: "$Date$" revision: "$Revision$" class interface COMPARABLE_GRAPH [V -> COMPARABLE] create make_empty -- (from GRAPH) make_from_tuple_array (a: ARRAY [TUPLE [V, V]]) -- (from GRAPH) convert make_from_tuple_array ({attached ARRAY [TUPLE [V, V]]}) feature -- Access generating_type: TYPE [detachable COMPARABLE_GRAPH [V]] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal (other: COMPARABLE_GRAPH [V]): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) frozen standard_is_equal (other: COMPARABLE_GRAPH [V]): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) feature -- Duplication copy (other: COMPARABLE_GRAPH [V]) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other frozen deep_copy (other: COMPARABLE_GRAPH [V]) -- Effect equivalent to that of: -- copy (other . deep_twin) -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY deep_equal: deep_equal (Current, other) frozen deep_twin: COMPARABLE_GRAPH [V] -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) frozen standard_copy (other: COMPARABLE_GRAPH [V]) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_standard_equal: standard_is_equal (other) frozen standard_twin: COMPARABLE_GRAPH [V] -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) frozen twin: COMPARABLE_GRAPH [V] -- New object equal to Current -- twin calls copy; to change copying/twinning semantics, redefine copy. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations frozen default: detachable COMPARABLE_GRAPH [V] -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.default for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class feature -- Conversion to array. array_compare (a, b: ARRAY [TUPLE [V, V]]): BOOLEAN -- compare two arrays of tuple -- (from GRAPH) as_array: ARRAY [TUPLE [V, V]] -- Return edges as an array of tuples -- (from GRAPH) feature -- Iterable new_cursor: ITERATION_CURSOR [V] -- Fresh cursor associated with current structure -- (from GRAPH) ensure -- from ITERABLE result_attached: Result /= Void feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Sorted outgoing edges adjacent (v: V): SEQ [V] -- Sorted list of outgoing edges from v require -- from GRAPH True ensure -- from GRAPH 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 ensure then sorted: across 1 |..| (Result.count - 1) as i all Result [i.item] < Result [i.item + 1] end feature -- advanced queries cycle (v: V): detachable SEQ [V] -- Return a cycle starting from v if any. -- (from GRAPH) 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. -- (from GRAPH) is_acyclic: BOOLEAN -- Does the graph contain no cycles? -- (from GRAPH) ensure -- from GRAPH Result = across vertices is l_v all not attached cycle (l_v) end is_equal (other: COMPARABLE_GRAPH [V]): BOOLEAN -- Is other attached to an object considered -- equal to current object? -- (from GRAPH) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result is_reachable (v1, v2: V): BOOLEAN -- (from GRAPH) require -- from GRAPH has_vertex (v1) and has_vertex (v2) ensure -- from GRAPH Result = attached shortest_path (v1, v2) is_subgraph alias "|<:" (other: COMPARABLE_GRAPH [V]): BOOLEAN -- (from GRAPH) is_topologically_sorted (seq: like topologically_sorted): BOOLEAN -- (from GRAPH) is_valid_path (seq: SEQ [V]): BOOLEAN -- Does seq denote a valid path in graph? -- (from GRAPH) require -- from GRAPH at_least_one_vertex: not seq.is_empty ensure -- from GRAPH 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) paths (v1, v2: V): SET [SEQ [V]] -- Return the set of all acyclic paths (ones not containing cycles) between v1 and v2. -- (from GRAPH) ensure -- from GRAPH 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 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) -- (from GRAPH) require -- from GRAPH has_vertex (src) ensure -- from GRAPH 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 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. -- (from GRAPH) ensure -- from GRAPH 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 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 -- (from GRAPH) ensure -- from GRAPH 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 topologically_sorted: SEQ [V] -- Return a sequence <<..., vi, ..., vj, ...>> such that -- (vi, vj) in edges => i < j -- A topological sort is performed. -- (from GRAPH) require -- from GRAPH is_acyclic ensure -- from GRAPH is_topologically_sorted (Result) 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) -- (from GRAPH) vertices_incoming_edge_count: INTEGER_32 -- total number of incoming edges of all vertices in vertices -- Result = (Σv ∈ vertices : incoming(v).count) -- (from GRAPH) vertices_outgoing_edge_count: INTEGER_32 -- total number of outgoing edges of all vertices in vertices -- Result = (Σv ∈ vertices : outgoing(v).count) -- (from GRAPH) feature -- basic queries edge_count: INTEGER_32 -- number of outgoing edges -- (from GRAPH) edge_extended alias "|\/|" (e: PAIR [V, V]): COMPARABLE_GRAPH [V] -- extend if not already in -- (from GRAPH) require -- from GRAPH valid_vertices: has_vertex (e.first) and has_vertex (e.second) edge_removed alias "|\" (e: PAIR [V, V]): COMPARABLE_GRAPH [V] -- (from GRAPH) has_edge (p: PAIR [V, V]): BOOLEAN -- does graph have pair p -- can use p as tuple -- (from GRAPH) has_vertex (v: V): BOOLEAN -- (from GRAPH) in_degree_count (v: V): INTEGER_32 -- number of incoming edges of vertex v -- (from GRAPH) require -- from GRAPH has_vertex (v) incoming (v: V): REL [V, V] -- The set of incoming edges to v -- (from GRAPH) ensure -- from GRAPH consistent_counts: Result.count = (edges @> v).count destination_is_v: across Result as e all e.item.second ~ v end is_empty: BOOLEAN -- is the graph empty? -- (from GRAPH) out_degree_count (v: V): INTEGER_32 -- number of outgoing edges of vertex v -- (from GRAPH) require -- from GRAPH has_vertex (v) outgoing (v: V): REL [V, V] -- The set of outgoing edges from v -- (from GRAPH) ensure -- from GRAPH consistent_counts: Result.count = (edges @< v).count source_is_v: across Result as e all e.item.first ~ v end vertex_count: INTEGER_32 -- (from GRAPH) vertex_extended alias "+" (v: V): COMPARABLE_GRAPH [V] -- extend if not already in -- (from GRAPH) vertex_removed alias "-" (v: V): COMPARABLE_GRAPH [V] -- (from GRAPH) feature -- commands edge_extend (e: PAIR [V, V]) -- connect vertex e.first to e.second -- if not already in -- (from GRAPH) require -- from GRAPH valid_vertices: has_vertex (e.first) and has_vertex (e.second) ensure -- from GRAPH edges ~ old edges.deep_twin + create {PAIR [V, V]}.make_from_tuple ([e.first, e.second]) vertices ~ old vertices.deep_twin edge_remove (e: PAIR [V, V]) -- (from GRAPH) vertex_extend (v: V) -- insert vertex v into graph -- if not already in -- (from GRAPH) ensure -- from GRAPH vertices ~ old vertices.deep_twin + v edges ~ old edges.deep_twin vertex_remove (v: V) -- Remove vertex v and all relevant edges -- (from GRAPH) ensure -- from GRAPH vertices ~ old vertices.deep_twin - v edges ~ (old edges.deep_twin @>> v) @<< v feature -- infinity Infinity: INTEGER_64 -- (from GRAPH) Zero: INTEGER_64 -- (from GRAPH) feature -- model edges: REL [V, V] -- (from GRAPH) vertices: SET [V] -- (from GRAPH) feature -- out debug_output: STRING_8 -- String that should be displayed in debugger to represent Current. -- (from GRAPH) ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from GRAPH) ensure -- from ANY out_not_void: Result /= Void invariant -- from GRAPH 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 -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) end -- class COMPARABLE_GRAPH
Generated by ISE EiffelStudio