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.Arrays;
00010 import java.util.HashSet;
00011 import java.util.LinkedHashSet;
00012 import java.util.Map;
00013 import java.util.Set;
00014
00015 import edu.mit.csail.sdg.annotations.Ensures;
00016 import edu.mit.csail.sdg.annotations.Modifies;
00017 import edu.mit.csail.sdg.squander.Squander;
00018 import edu.mit.csail.sdg.squander.annotations.Fresh;
00019 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00020 import edu.mit.csail.sdg.squander.annotations.Options;
00021
00028 public class Graph implements Serializable {
00029
00030 private static final long serialVersionUID = -6332798241722968023L;
00031
00032
00033
00034
00038 public static class Node implements Serializable {
00039 private static final long serialVersionUID = 8914980217070845458L;
00040
00041 public int label;
00042
00043 public Node(int label) { this.label = label; }
00044
00045 @Override
00046 public int hashCode() {
00047 final int prime = 31;
00048 int result = 1;
00049 result = prime * result + label;
00050 return result;
00051 }
00052
00053 @Override
00054 public boolean equals(Object obj) {
00055 if (this == obj)
00056 return true;
00057 if (obj == null)
00058 return false;
00059 if (getClass() != obj.getClass())
00060 return false;
00061 Node other = (Node) obj;
00062 if (label != other.label)
00063 return false;
00064 return true;
00065 }
00066
00067 @Override
00068 public String toString() {
00069 return "(" + String.valueOf(label) + ")";
00070 }
00071 }
00072
00073
00074
00075
00079 public static class Edge implements Serializable {
00080 private static final long serialVersionUID = -5337889501186870289L;
00081
00082 public final Node src;
00083 public final Node dst;
00084 public final int cost;
00085
00086 public Edge(Node src, Node dest, int cost) {
00087 this.src = src;
00088 this.dst = dest;
00089 this.cost = cost;
00090 }
00091
00092 public Edge(Node src, Node dest) {
00093 this(src, dest, 0);
00094 }
00095
00096 @Override
00097 public int hashCode() {
00098 final int prime = 31;
00099 int result = 1;
00100 result = prime * result + ((dst == null) ? 0 : dst.hashCode());
00101 result = prime * result + ((src == null) ? 0 : src.hashCode());
00102 return result;
00103 }
00104
00105 @Override
00106 public boolean equals(Object obj) {
00107 if (this == obj)
00108 return true;
00109 if (obj == null)
00110 return false;
00111 if (getClass() != obj.getClass())
00112 return false;
00113 Edge other = (Edge) obj;
00114 if (dst == null) {
00115 if (other.dst != null)
00116 return false;
00117 } else if (!dst.equals(other.dst))
00118 return false;
00119 if (src == null) {
00120 if (other.src != null)
00121 return false;
00122 } else if (!src.equals(other.src))
00123 return false;
00124 return true;
00125 }
00126
00127 @Override
00128 public String toString() {
00129 return String.format("%s --%s--> %s", src, cost, dst);
00130 }
00131
00132 }
00133
00134 private Set<Node> nodes = new LinkedHashSet<Node>();
00135 private Set<Edge> edges = new LinkedHashSet<Edge>();
00136
00137 private Node auxNode;
00138 public Node getAuxNode() { return auxNode; }
00139 public void setAuxNode(Node aux) { this.auxNode = aux; }
00140
00141 private int auxInt;
00142 public int getAuxInt() { return auxInt; }
00143 public void setAuxInt(int auxInt) { this.auxInt = auxInt; }
00144
00145 public Graph() {}
00146
00147 public Node newNode(int key) {
00148 Node n = new Node(key);
00149 addNode(n);
00150 return n;
00151 }
00152
00153 public void addNode(Node n) { nodes.add(n); }
00154 public void addEdge(Edge e) { edges.add(e); }
00155
00156 public void newUndirectedEdge(Node a, Node b) {
00157 newEdge(a, b);
00158 newEdge(b, a);
00159 }
00160
00161 public void newUndirectedEdge(Node a, Node b, int cost) {
00162 newEdge(a, b, cost);
00163 newEdge(b, a, cost);
00164 }
00165
00166 public Edge newEdge(Node a, Node b) {
00167 Edge e = new Edge(a, b);
00168 addEdge(e);
00169 return e;
00170 }
00171
00172 public Edge newEdge(Node a, Node b, int cost) {
00173 Edge e = new Edge(a, b, cost);
00174 addEdge(e);
00175 return e;
00176 }
00177
00178 public boolean containsEdge(Node n1, Node n2) { return edges.contains(new Edge(n1, n2)); }
00179 public Node findNode(int label) {
00180 for (Node n : nodes)
00181 if (n.label == label)
00182 return n;
00183 return null;
00184 }
00185
00186 public Node[] nodes() { return nodes.toArray(new Node[0]); }
00187 public Edge[] edges() { return edges.toArray(new Edge[0]); }
00188
00189 public int numEdges() { return edges.size(); }
00190 public int numNodes() { return nodes.size(); }
00191 public int size() { return numNodes(); }
00192
00193 public Set<Node> getNeighbors(Node src) {
00194 Set<Node> neighbrs = new HashSet<Node>();
00195 for (Edge e : edges)
00196 if (e.src == src)
00197 neighbrs.add(e.dst);
00198 return neighbrs;
00199 }
00200
00201 public void removeAllIncomingEdges(Node n) {
00202 for (Edge e : new ArrayList<Edge>(edges)) {
00203 if (e.dst.equals(n))
00204 edges.remove(e);
00205 }
00206 }
00207
00208 public void removeAllOutgoingEdges(Node n) {
00209 for (Edge e : new ArrayList<Edge>(edges)) {
00210 if (e.src.equals(n))
00211 edges.remove(e);
00212 }
00213 }
00214
00218 @Ensures( {
00219 "return[int] = this.nodes.elts",
00220 "return.length = #this.nodes.elts",
00221 "all i : int | i >= 0 && i < return.length - 1 => (exists e : this.edges.elts | e.src = return[i] && e.dst = return[i+1])"
00222 })
00223 @Modifies({"return.length", "return.elems"})
00224 @FreshObjects(cls = Node[].class, num = 1)
00225 @Options(ensureAllInts = false)
00226 public Node[] hamiltonian() {
00227 return Squander.exe(this);
00228 }
00229
00233 @Ensures( {
00234 "return[int] in this.edges.elts",
00235 "return[int].(src + dst) = this.nodes.elts",
00236 "return.length = #this.nodes.elts - 1",
00237 "all i : int | i >= 0 && i < return.length - 1 => return[i].dst = return[i+1].src"
00238 })
00239 @Modifies({"return.length", "return.elems"})
00240 @FreshObjects(cls = Edge[].class, num = 1)
00241 @Options(ensureAllInts = false)
00242 public Edge[] hamiltonian2() {
00243 return Squander.exe(this);
00244 }
00245
00249 @Ensures( {
00250 "return[int] in this.edges.elts",
00251 "return[int].(src + dst) = this.nodes.elts",
00252 "return.length = #this.nodes.elts",
00253 "all i : int | i >= 0 && i < return.length - 1 => return[i].dst = return[i+1].src",
00254 "startNode = return[0].src && startNode = return[return.length - 1].dst",
00255 "(sum i : int | return[i].cost) <= maxCost"
00256 })
00257 @Modifies( { "return.length", "return.elems" })
00258 @FreshObjects(cls = Edge[].class, num = 1)
00259 @Options(ensureAllInts = true)
00260 public Edge[] tsp(Node startNode, int maxCost) {
00261 return Squander.exe(this, startNode, maxCost);
00262 }
00263
00267 @Ensures( {
00268 "return[int] = this.nodes.elts",
00269 "return.length = #this.nodes.elts",
00270 "all i : int | all j : int | 0 <= i && i < j && j < return.length => (no e : this.edges.elts | e.src = return[i] && e.dst = return[j])"
00271 })
00272 @Modifies({"return.length", "return.elems"})
00273 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00274 public Node[] topsort() {
00275 return Squander.exe(this);
00276 }
00277
00281 @Ensures({
00282 "return[int] in this.nodes.elts",
00283 "all i : int | all j : int | 0 <= i && i < j && j < return.length => (exists e : this.edges.elts | (e.src = return[i] && e.dst = return [j]) || (e.dst = return[i] && e.src = return[j]))",
00284 "#return[int] >= k"
00285 })
00286 @Modifies({"return.length", "return.elems"})
00287 @Fresh(@FreshObjects(cls = Node[].class, num = 1))
00288 public Node[] maxClique(int k) {
00289 return Squander.exe(this, new Class<?>[]{int.class}, new Object[]{k});
00290 }
00291
00295 @Ensures({
00296 "return.keys = this.nodes.elts",
00297 "all c : return.vals | c > 0 && c <= k",
00298 "all e : this.edges.elts | return.elts[e.src] != return.elts[e.dst]"
00299 })
00300 @Modifies("return.elts")
00301 @Options(ensureAllInts=true)
00302 @FreshObjects(cls = Map.class, typeParams={Node.class, Integer.class}, num = 1)
00303 public Map<Node, Integer> color(int k) {
00304 return Squander.exe(this, k);
00305 }
00306
00307 @Override
00308 public String toString() {
00309 StringBuilder sb = new StringBuilder();
00310 sb.append(String.format("Nodes (%s): %s\n", nodes.size(), nodes.toString()));
00311 sb.append(String.format("Edges (%s):\n", edges.size()));
00312 for (Edge e : edges) {
00313 sb.append(String.format(" %s -> %s", e.src, e.dst));
00314 }
00315 return sb.toString();
00316 }
00317
00318 public static boolean checkTSP(Graph g, Edge[] hamcycle, int maxCost) {
00319 Edge prev = null;
00320 int cost = 0;
00321 Set<Node> visited = new HashSet<Node>();
00322 for (Edge curr : hamcycle) {
00323 if (prev != null) {
00324 if (prev.dst != curr.src)
00325 return false;
00326 }
00327 if (!visited.add(curr.src))
00328 return false;
00329 cost += curr.cost;
00330 prev = curr;
00331 }
00332 Set<Node> graphNodes = new HashSet<Node>(Arrays.asList(g.nodes()));
00333 if (!visited.equals(graphNodes))
00334 return false;
00335 if (cost > maxCost)
00336 return false;
00337 return true;
00338 }
00339
00340 }