00001
00005 package edu.mit.csail.sdg.squander.examples.graph;
00006
00007 import java.io.Serializable;
00008 import java.util.ArrayList;
00009 import java.util.LinkedHashSet;
00010 import java.util.Set;
00011
00012 import edu.mit.csail.sdg.annotations.Ensures;
00013 import edu.mit.csail.sdg.annotations.Modifies;
00014 import edu.mit.csail.sdg.annotations.SpecField;
00015 import edu.mit.csail.sdg.squander.Squander;
00016 import edu.mit.csail.sdg.squander.annotations.Fresh;
00017 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00018 import edu.mit.csail.sdg.squander.annotations.Options;
00019
00025 @SpecField("edgeSet : set Node -> Node | " +
00026 "(all e : this.edges.elts | e.src -> e.dst in this.edgeSet) &&" +
00027 "#this.edgeSet = #this.edges.elts")
00028 public class Graph__2 implements Serializable {
00029
00030 private static final long serialVersionUID = -6332798241722968023L;
00031
00032
00033
00034
00035 public static class Node implements Serializable {
00036 private static final long serialVersionUID = 8914980217070845458L;
00037
00038 public int label;
00039
00040 public Node(int label) { this.label = label; }
00041
00042 @Override
00043 public int hashCode() {
00044 final int prime = 31;
00045 int result = 1;
00046 result = prime * result + label;
00047 return result;
00048 }
00049
00050 @Override
00051 public boolean equals(Object obj) {
00052 if (this == obj)
00053 return true;
00054 if (obj == null)
00055 return false;
00056 if (getClass() != obj.getClass())
00057 return false;
00058 Node other = (Node) obj;
00059 if (label != other.label)
00060 return false;
00061 return true;
00062 }
00063
00064 @Override
00065 public String toString() {
00066 return "(" + String.valueOf(label) + ")";
00067 }
00068 }
00069
00070
00071
00072
00073 public static class Edge implements Serializable {
00074 private static final long serialVersionUID = -5337889501186870289L;
00075
00076 public final Node src;
00077 public final Node dst;
00078
00079 public Edge(Node src, Node dest) {
00080 this.src = src;
00081 this.dst = dest;
00082 }
00083
00084 @Override
00085 public int hashCode() {
00086 final int prime = 31;
00087 int result = 1;
00088 result = prime * result + ((dst == null) ? 0 : dst.hashCode());
00089 result = prime * result + ((src == null) ? 0 : src.hashCode());
00090 return result;
00091 }
00092
00093 @Override
00094 public boolean equals(Object obj) {
00095 if (this == obj)
00096 return true;
00097 if (obj == null)
00098 return false;
00099 if (getClass() != obj.getClass())
00100 return false;
00101 Edge other = (Edge) obj;
00102 if (dst == null) {
00103 if (other.dst != null)
00104 return false;
00105 } else if (!dst.equals(other.dst))
00106 return false;
00107 if (src == null) {
00108 if (other.src != null)
00109 return false;
00110 } else if (!src.equals(other.src))
00111 return false;
00112 return true;
00113 }
00114
00115 }
00116
00117 private Set<Node> nodes = new LinkedHashSet<Node>();
00118 private Set<Edge> edges = new LinkedHashSet<Edge>();
00119
00120 public Graph__2() {}
00121
00122 public Node newNode(int key) {
00123 Node n = new Node(key);
00124 addNode(n);
00125 return n;
00126 }
00127
00128 public void addNode(Node n) { nodes.add(n); }
00129 public void addEdge(Edge e) { edges.add(e); }
00130
00131 public Edge newEdge(Node a, Node b) {
00132 Edge e = new Edge(a, b);
00133 addEdge(e);
00134 return e;
00135 }
00136
00137 public boolean containsEdge(Node n1, Node n2) { return edges.contains(new Edge(n1, n2)); }
00138
00139 public Node[] nodes() { return nodes.toArray(new Node[0]); }
00140 public Edge[] edges() { return edges.toArray(new Edge[0]); }
00141
00142 public int numEdges() { return edges.size(); }
00143 public int numNodes() { return nodes.size(); }
00144 public int size() { return numNodes(); }
00145
00146 public void removeAllIncomingEdges(Node n) {
00147 for (Edge e : new ArrayList<Edge>(edges)) {
00148 if (e.dst.equals(n))
00149 edges.remove(e);
00150 }
00151 }
00152
00153 public void removeAllOutgoingEdges(Node n) {
00154 for (Edge e : new ArrayList<Edge>(edges)) {
00155 if (e.src.equals(n))
00156 edges.remove(e);
00157 }
00158 }
00159
00160 @Ensures( {
00161 "return[int] = this.nodes.elts",
00162 "return.length = #this.nodes.elts",
00163 "all i : int | i >= 0 && i < return.length - 1 => (return[i]->return[i+1]) in this.edgeSet"
00164 })
00165 @Modifies({"return.length", "return.elems"})
00166 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00167 @Options(ensureAllInts = false)
00168 public Node[] hamiltonian() {
00169 return Squander.exe(this);
00170 }
00171
00172 @Ensures( {
00173 "return[int] = this.nodes.elts",
00174 "return.length = #this.nodes.elts",
00175 "all i : int | all j : int | 0 <= i && i < j && j < return.length => (return[i]->return[j]) !in this.edgeSet"
00176 })
00177 @Modifies({"return.length", "return.elems"})
00178 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00179 public Node[] topsort() {
00180 return Squander.exe(this);
00181 }
00182
00183 @Ensures({
00184 "return[int] in this.nodes.elts",
00185 "all i : int | all j : int | 0 <= i && i < j && j < return.length => (return[i]->return[j]) in this.edgeSet + ~this.edgeSet",
00186 "#return[int] >= k"
00187 })
00188 @Modifies({"return.length", "return.elems"})
00189 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00190 public Node[] maxClique(int k) {
00191 return Squander.exe(this, new Class<?>[]{int.class}, new Object[]{k});
00192 }
00193
00194 @Override
00195 public String toString() {
00196 StringBuilder sb = new StringBuilder();
00197 sb.append(String.format("Nodes (%s): %s\n", nodes.size(), nodes.toString()));
00198 sb.append(String.format("Edges (%s):\n", edges.size()));
00199 for (Edge e : edges) {
00200 sb.append(String.format(" %s -> %s", e.src, e.dst));
00201 }
00202 return sb.toString();
00203 }
00204
00205 }