/* Labeled Digraph ADT Interface, Immutable Method Chaining Functions
   CSci 555: Functional Programming, Spring 2016
   H. Conrad Cunningham, Professor
   Computer and Information Science
   University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

2016-03-23: Developed Scala version from 2015 Haskell version


SPECIFICATION OF LABELED DIGRAPH ADT

** Notation **

(ForAll x, y :: p(x,y)) is true if and only if predicate p(x,y) is
true for all values of x and y.

(Exists x, y :: p(x,y)) is true if and only if there is at least one
pair of values x and y for which p(x,y) is true.

(# x, y :: p(x,y)) yields a count of pairs (x,y) for which p(x,y) is
true.

"<=>" denotes logical equivalence. p <=> q is true if and only if the
logical (Boolean) values p and q are equal (i.e., both true or both
false).

"x IN C" is true if and only if value x is member of a collection C
(such as a set or sequence).  Similarly, "x NOT_IN C" denotes the
negation of "x IN C".

A type consists of a set of values and a set of operations. We
sometimes say a value is IN a type to mean the value is IN the set
associated with the type.

For sets C and D, "C UNION D" denotes set union, that is, a set that
includes all the element of both C and D.

For sets C and D, "C INTERSECT D" denotes set intersection, that is, a
set that includes all elements that are both in C and in D.

For sets C and D, "C - D" denotes set difference, that is, the set C
with all elements of set D removed.

For sets C and D, "C SUBSET_OF D" denotes that C is subset of D, that
is, all the elements of C also occur in D.

A tuple such as "(x,*)" appearing in a collection such as "{ (x,*) }"
denotes element x grouped with all possible values of the second
component.  Note: We could also write { (x,*) } using quantification
as { (x,c) :: c IN some_domain } or { (x,c) :: c IN some_domain }.

A function is a special case of a relation and relation is a set of
ordered pairs (tuples). We sometimes manipulate functions or relations
using set notation for convenience.

A total function is defined for all elements of its domain. A partial
function is defined for a subset of the elements of its domain.

** Abstract Model **

The abstract model for the Labeled Digraph ADT is parameterized by the
following types.

    VertexType is the set of possible vertices (i.e., vertex
        identifiers).

    VertexLabelType is the set of possible labels on vertices. (Values
        of this type may have several components.)

    EdgeLabelType is the set of possible labels on edges. (Values of
        this type may have several components.)

We model the state of the instance of the Labeled Digraph ADT with an
abstract value G such that G = (V,E,VL,EL) with G's components
satisfying the following Labeled Digraph Properties.

    V is a finite subset of values from the set VertexType. V denotes
        the vertices (or nodes) of the digraph.

    E is a binary relation on the set V. A pair (v1,v2) in E denotes
        that there is a directed edge from v1 to v2 in the digraph.

    VL is a total function from set V to the set VertexLabelType. 

    EL is a total function from set E to the set EdgeLabelType.

** Interface Invariant **

    Any valid labeled digraph instance G, appearing in either the
    arguments or return value of a public ADT operation, must satisfy 
    the Labeled Digraph Properties.

** Constructive Semantics of Operations **

The preconditions and postconditions of each ADT operation are given
below with the implementations of the operations.  These are part of
the (implementation-independent) specification of the ADT.

In these assertions, for a digraph g that satisfies the invariants,
G(g) denotes its abstract model (V,E,VL,EL) as described above.

*/


trait Digraph[A,B,C] {

/* A zero-parameter constructor has the following preconditions and
   postconditions.

   Pre:  True
   Post: G(this) = ({},{},{},{}) 
 */


/* isEmpty returns true if and only if this graph is empty.

   Pre:  G(this) =(V,E,VL,EL)
   Post: Result == (V == {} && E == {}) && G(this) = G(this')
 */

  def isEmpty: Boolean


/* addVertex(nv,nl) inserts vertex nv with label nl into this graph
   and returns the resulting graph.

   Pre:  G(this) = (V,E,VL,EL) && nv NOT_IN V 
   Post: G(Result) == (V UNION {nv}, E, VL UNION {(nv,nl)}, EL)  
 */

  def addVertex(nv: A, nl: B): Digraph[A,B,C]


/* removeVertex(ov) deletes vertex ov from this graph and returns the
   resulting graph.

   Pre:  G(this) = (V,E,VL,EL) && ov IN V
   Post: G(Result) == (V', E', VL', EL')
         where V'  = V  - {ov}
               E'  = E  - {(ov,*),(*,ov)}
               VL' = VL - {(ov,*)}
               EL' = EL - {((ov,*),*),((*,ov),*)}	       
 */

  def removeVertex(ov: A): Digraph[A,B,C]


/* updateVertex(ov,nl) changes the label on vertex ov in this graph
   to be nl and returns the resulting graph.

   Pre:  G(this) = (V,E,VL,EL) && ov IN V
   Post: G(Result) == (V - {ov}, E, VL', EL) && G(this) = G(this')
         where VL' = (VL - {(ov,VL(ov))}) UNION {(ov,nl)}
 */

  def updateVertex(ov: A, nl: B): Digraph[A,B,C]


/* getVertexLabel(ov) returns the label from vertex ov in this graph.

   Pre:   G(this) = (V,E,VL,EL) && ov IN V && G(this) = G(this')
   Post:  Result == VL(ov)
 */

  def getVertexLabel(ov: A): B


/* hasVertex(v) returns true if and only if ov is a vertex of this
   graph.

   Pre:  G(this) = (V,E,VL,EL) && ov IN VertexLabelType
   Post: G(Result) == ov IN V && G(this) = G(this')
 */

  def hasVertex(v: A): Boolean 


/* addEdge(v1,v2,nl) inserts an edge from vertex v1 to vertex v2 in
   this graph and returns the resulting graph.

   Pre:  G(this) = (V,E,VL,EL) && v1 IN V && v2 IN V
                    && (v1,v2) NOT_IN E
   Post: G(Result) == (V, E', VL, EL') && G(this) = G(this')
         where E'  = E  UNION {(v1,v2)}
               EL' = EL UNION {((v1,v2),nl)}
 */

  def addEdge(v1: A, v2: A, nl: C): Digraph[A,B,C]


/* removeEdge(v1,v2) deletes the edge from vertex v1 to vertex v2 
   from this graph and returns the resulting graph.

   Pre:  G(this) = (V,E,VL,EL) V - {ov} && (v1,v2) IN E
   Post: G(Result) == (V, E - {(v1,v2)}, VL, EL - { ((v1,v2),*) }
 */

  def removeEdge(v1: A, v2: A): Digraph[A,B,C]


/* updateEdge(v1,v2,nl) changes the label on the edge from vertex v1
   to vertex v2 in this graph to have label nl and returns the 
   resulting graph.

   Pre:  G(this) = (V,E,VL,EL) && (v1,v2) IN E
   Post: G(Result) == (V, E, VL, EL') && G(this) = G(this')
         where EL' == (EL - {((v1,v2),*)}) UNION {((v2,v2),nl)
 */

  def updateEdge(v1: A, v2: A, nl: C): Digraph[A,B,C]


/* getEdgeLabel(v1,v2) returns the label on the edge from vertex v1
   to vertex v2 in this graph.

   Pre:  G(this) = (V,E,VL,EL) && (v1,v2) IN E
   Post: Result == EL((v1,v2)) && G(this) = G(this')
 */

  def getEdgeLabel(v1: A, v2: A): C


/* hasEdge(v1,v2) returns true if and only if there is an edge from
   a vertex v1 to a vertex v2 in this graph.

   Pre:  G(this) = (V,E,VL,EL) 
   Post: Result == (v1,v2) IN E && G(this) = G(this')
 */

  def hasEdge(v1: A, v2: A): Boolean


/* allVertices returns a sequence of all the vertices in this graph. 
   The sequence is represented by a builtin Scala list.

   Pre:  G(this) = (V,E,VL,EL)
   Post: (ForAll ov: ov IN Result <=> ov IN V) && 
         length(Result) == size(V) && G(this) = G(this')
 */

  def allVertices: List[A]


/* fromEdges(v1) returns a sequence of all vertices v2 such that
   there is an edge from vertex v1 to vertex v2 in this graph.
   The sequence is represented by a builtin Scala list.

   Pre:  G(this) = (V,E,VL,EL) && v1 IN V
   Post: (ForAll v2: v2 IN Result <=> (v1,v2) IN E) &&
         length(Result) == (# v2 :: (v1,v2) IN E) &&
	 G(this) = G(this')
 */

  def fromEdges(v1: A): List[A]


/* allVerticesLabels returns a sequence of all pairs (v,l) such
   that v is a vertex and l is it's label in this graph.
   The sequence is represented by a builtin Scala list.

   Pre:  G(this) = (V,E,VL,EL)
   Post: (ForAll v, l: (v,l) IN Result <=> (v,l) IN VL) && 
         length(Result) == size(VL) && G(this) = G(this')
 */

  def allVerticesLabels: List[(A,B)]


/* fromEdgesLabels(v1) returns a sequence of all pairs (v2,l) such
   that there is an edge (v1,v2) labeled with l in this graph.

   Pre:  G(this) = (V,E,VL,EL) && v1 IN V
   Post: (ForAll v2, l :: (v2,l) IN Result <=> ((v1,v2),l) IN EL) &&
         length(Result) == (# v2 :: (v1,v2 ) IN E) &&
	 G(this) = G(this')
 */

  def fromEdgesLabels(v1: A): List[(A,C)]
 

/* A class that extends this trait will likely need to override
   toString and/or equals to give them appropriate definitions.
 */
 
}