import Base
import ./lib.bend as G

# Empty graph is defined with no nodes or edges.
law empty_nodes:
  { G.Graph.nodes(G.Graph.empty()) == Nil{} : List<&2, U32> }

law empty_edge_count:
  { G.Graph.edge_count(G.Graph.empty()) == 0n : Nat }

law empty_neighbors:
  { G.Graph.neighbors(G.Graph.empty(), 0) == Nil{} : List<&2, U32> }

law empty_has_edge:
  { G.Graph.has_edge(G.Graph.empty(), 0, 1) == False{} : Bool }

# A singleton graph contains exactly its node and no edges.
law singleton_nodes:
  { G.Graph.nodes(G.Graph.add_node(G.Graph.empty(), 7)) == 7 <> Nil{} : List<&2, U32> }

law singleton_edge_count:
  { G.Graph.edge_count(G.Graph.add_node(G.Graph.empty(), 7)) == 0n : Nat }

law singleton_neighbors:
  { G.Graph.neighbors(G.Graph.add_node(G.Graph.empty(), 7), 7) == Nil{} : List<&2, U32> }

law singleton_has_edge:
  { G.Graph.has_edge(G.Graph.add_node(G.Graph.empty(), 7), 7, 7) == False{} : Bool }

# add_edge adds missing endpoints in insertion order.
law edge_adds_nodes:
  { G.Graph.nodes(G.Graph.add_edge(G.Graph.empty(), 1, 2)) == 1 <> 2 <> Nil{} : List<&2, U32> }

law edge_adds_one_edge:
  { G.Graph.edge_count(G.Graph.add_edge(G.Graph.empty(), 1, 2)) == 1n : Nat }

law edge_is_present:
  { G.Graph.has_edge(G.Graph.add_edge(G.Graph.empty(), 1, 2), 1, 2) == True{} : Bool }

law edge_neighbors:
  { G.Graph.neighbors(G.Graph.add_edge(G.Graph.empty(), 1, 2), 1) == 2 <> Nil{} : List<&2, U32> }

law reverse_edge_is_absent:
  { G.Graph.has_edge(G.Graph.add_edge(G.Graph.empty(), 1, 2), 2, 1) == False{} : Bool }

# Re-adding an existing self-loop does not duplicate the edge.
law duplicate_edge_count:
  { G.Graph.edge_count(G.Graph.add_edge(G.Graph.add_edge(G.Graph.empty(), 3, 3), 3, 3)) == 1n : Nat }

law self_loop_neighbors:
  { G.Graph.neighbors(G.Graph.add_edge(G.Graph.empty(), 3, 3), 3) == 3 <> Nil{} : List<&2, U32> }