1 package gov.nasa.ltl.graph; 20 21 import java.io.BufferedReader ; 22 import java.io.FileOutputStream ; 23 import java.io.FileReader ; 24 import java.io.IOException ; 25 import java.io.InputStreamReader ; 26 import java.io.PrintStream ; 27 import java.util.Iterator ; 28 import java.util.LinkedList ; 29 import java.util.List ; 30 31 34 public class Graph { 35 public static final int SM_FORMAT = 0; 36 37 public static final int FSP_FORMAT = 1; 38 39 public static final int XML_FORMAT = 2; 40 41 public static final int SPIN_FORMAT = 3; 42 43 private List nodes; 44 45 private Node init; 46 47 private Attributes attributes; 48 49 public Graph(Attributes a) { 50 init(a); 51 } 52 53 public Graph() { 54 init(null); 55 } 56 57 public synchronized void setAttributes(Attributes a) { 58 attributes = new Attributes(a); 59 } 60 61 public synchronized void setBooleanAttribute(String name, boolean value) { 62 attributes.setBoolean(name, value); 63 } 64 65 public boolean getBooleanAttribute(String name) { 66 return attributes.getBoolean(name); 67 } 68 69 public int getEdgeCount() { 70 int count = 0; 71 72 for (Iterator i = new LinkedList (nodes).iterator(); i.hasNext();) { 73 count += ((Node) i.next()).getOutgoingEdgeCount(); 74 } 75 76 return count; 77 } 78 79 public synchronized void setInit(Node n) { 80 if (nodes.contains(n)) { 81 init = n; 82 number(); 83 } 84 } 85 86 public Node getInit() { 87 return init; 88 } 89 90 public synchronized void setIntAttribute(String name, int value) { 91 attributes.setInt(name, value); 92 } 93 94 public int getIntAttribute(String name) { 95 return attributes.getInt(name); 96 } 97 98 public Node getNode(int id) { 99 for (Iterator i = nodes.iterator(); i.hasNext();) { 100 Node n = (Node) i.next(); 101 102 if (n.getId() == id) { 103 return n; 104 } 105 } 106 107 return null; 108 } 109 110 public int getNodeCount() { 111 return nodes.size(); 112 } 113 114 public List getNodes() { 115 return new LinkedList (nodes); 116 } 117 118 public synchronized void setStringAttribute(String name, String value) { 119 attributes.setString(name, value); 120 } 121 122 public String getStringAttribute(String name) { 123 return attributes.getString(name); 124 } 125 126 public static Graph load() throws IOException { 127 return load(new BufferedReader (new InputStreamReader (System.in))); 128 } 129 130 public static Graph load(String fname) throws IOException { 131 return load(new BufferedReader (new FileReader (fname))); 132 } 133 134 public synchronized void dfs(Visitor v) { 135 if (init == null) { 136 return; 137 } 138 139 forAllNodes(new EmptyVisitor() { 140 public void visitNode(Node n) { 141 n.setBooleanAttribute("_reached", false); 142 } 143 }); 144 145 dfs(init, v); 146 147 forAllNodes(new EmptyVisitor() { 148 public void visitNode(Node n) { 149 n.setBooleanAttribute("_reached", false); 150 } 151 }); 152 } 153 154 public synchronized void forAll(Visitor v) { 155 for (Iterator i = new LinkedList (nodes).iterator(); i.hasNext();) { 156 Node n = (Node) i.next(); 157 158 v.visitNode(n); 159 160 n.forAllEdges(v); 161 } 162 } 163 164 public synchronized void forAllEdges(Visitor v) { 165 for (Iterator i = new LinkedList (nodes).iterator(); i.hasNext();) { 166 Node n = (Node) i.next(); 167 168 n.forAllEdges(v); 169 } 170 } 171 172 public synchronized void forAllNodes(Visitor v) { 173 for (Iterator i = new LinkedList (nodes).iterator(); i.hasNext();) { 174 Node n = (Node) i.next(); 175 v.visitNode(n); 176 } 177 } 178 179 public synchronized void save(int format) { 180 save(System.out, format); 181 } 182 183 public synchronized void save() { 184 save(System.out, SM_FORMAT); 185 } 186 187 public synchronized void save(String fname, int format) throws IOException { 188 save(new PrintStream (new FileOutputStream (fname)), format); 189 } 190 191 public synchronized void save(String fname) throws IOException { 192 save(new PrintStream (new FileOutputStream (fname)), SM_FORMAT); 193 } 194 195 synchronized void addNode(Node n) { 196 nodes.add(n); 197 198 if (init == null) { 199 init = n; 200 } 201 202 number(); 203 } 204 205 synchronized void removeNode(Node n) { 206 nodes.remove(n); 207 208 if (init == n) { 209 if (nodes.size() != 0) { 210 init = (Node) nodes.get(0); 211 } else { 212 init = null; 213 } 214 } 215 216 number(); 217 } 218 219 private void init(Attributes a) { 220 if (a == null) { 221 attributes = new Attributes(); 222 } else { 223 attributes = a; 224 } 225 226 nodes = new LinkedList (); 227 init = null; 228 } 229 230 private static Graph load(BufferedReader in) throws IOException { 231 int ns = readInt(in); 232 Node[] nodes = new Node[ns]; 233 234 Graph g = new Graph(readAttributes(in)); 235 236 for (int i = 0; i < ns; i++) { 237 int nt = readInt(in); 238 239 if (nodes[i] == null) { 240 nodes[i] = new Node(g, readAttributes(in)); 241 } else { 242 nodes[i].setAttributes(readAttributes(in)); 243 } 244 245 for (int j = 0; j < nt; j++) { 246 int nxt = readInt(in); 247 String gu = readString(in); 248 String ac = readString(in); 249 250 if (nodes[nxt] == null) { 251 nodes[nxt] = new Node(g); 252 } 253 254 new Edge(nodes[i], nodes[nxt], gu, ac, readAttributes(in)); 255 } 256 } 257 258 g.number(); 259 260 return g; 261 } 262 263 private synchronized void number() { 264 int cnt; 265 266 if (init != null) { 267 init.setId(0); 268 cnt = 1; 269 } else { 270 cnt = 0; 271 } 272 273 for (Iterator i = nodes.iterator(); i.hasNext();) { 274 Node n = (Node) i.next(); 275 276 if (n != init) { 277 n.setId(cnt++); 278 } 279 } 280 } 281 282 private static Attributes readAttributes(BufferedReader in) 283 throws IOException { 284 return new Attributes(readLine(in)); 285 } 286 287 private static int readInt(BufferedReader in) throws IOException { 288 return Integer.parseInt(readLine(in)); 289 } 290 291 private static String readLine(BufferedReader in) throws IOException { 292 String line; 293 294 do { 295 line = in.readLine(); 296 297 int idx = line.indexOf('#'); 298 299 if (idx != -1) { 300 line = line.substring(0, idx); 301 } 302 303 line = line.trim(); 304 } while (line.length() == 0); 305 306 return line; 307 } 308 309 private static String readString(BufferedReader in) throws IOException { 310 return readLine(in); 311 } 312 313 private synchronized void dfs(Node n, Visitor v) { 314 final Visitor visitor = v; 315 316 if (n.getBooleanAttribute("_reached")) { 317 return; 318 } 319 320 n.setBooleanAttribute("_reached", true); 321 322 v.visitNode(n); 323 324 n.forAllEdges(new EmptyVisitor() { 325 public void visitEdge(Edge e) { 326 dfs(e.getNext(), visitor); 327 } 328 }); 329 } 330 331 private synchronized void save(PrintStream out, int format) { 333 switch (format) { 334 case SM_FORMAT: 335 save_sm(out); 336 337 break; 338 339 case FSP_FORMAT: 340 save_fsp(out); 341 342 break; 343 344 case XML_FORMAT: 345 save_xml(out); 346 347 break; 348 349 case SPIN_FORMAT: 350 save_spin(out); 351 352 break; 353 354 default: 355 throw new RuntimeException ("Unknown format!"); 356 } 357 } 358 359 private synchronized void save_fsp(PrintStream out) { 361 boolean empty = false; 362 363 if (init != null) { 364 out.print("RES = S" + init.getId()); 365 } else { 366 out.print("Empty"); 367 empty = true; 368 } 369 370 for (Iterator i = nodes.iterator(); i.hasNext();) { 371 out.println(","); 373 374 Node n = (Node) i.next(); 375 n.save(out, FSP_FORMAT); 376 } 377 378 out.println("."); 380 381 int nsets = getIntAttribute("nsets"); 382 383 if ((nsets == 0) && !empty) { 384 boolean first = true; 385 386 out.print("AS = { "); 388 389 for (Iterator i = nodes.iterator(); i.hasNext();) { 390 Node n = (Node) i.next(); 391 392 if (n.getBooleanAttribute("accepting")) { 393 if (!first) { 394 out.print(", "); 396 } else { 397 first = false; 398 } 399 400 out.print("S" + n.getId()); 402 } 403 } 404 405 out.println(" }"); 407 } else if (!empty) { 409 for (int k = 0; k < nsets; k++) { 410 boolean first = true; 411 412 out.print("AS" + k + " = { "); 414 415 for (Iterator i = nodes.iterator(); i.hasNext();) { 416 Node n = (Node) i.next(); 417 418 if (n.getBooleanAttribute("acc" + k)) { 419 if (!first) { 420 out.print(", "); 422 } else { 423 first = false; 424 } 425 426 out.print("S" + n.getId()); 428 } 429 } 430 431 out.println(" }"); 433 } 434 } 435 436 if (out != System.out) { 437 out.close(); 438 } 439 } 440 441 private synchronized void save_sm(PrintStream out) { 442 out.println(nodes.size()); 443 out.println(attributes); 444 445 if (init != null) { 446 init.save(out, SM_FORMAT); 447 } 448 449 for (Iterator i = nodes.iterator(); i.hasNext();) { 450 Node n = (Node) i.next(); 451 452 if (n != init) { 453 n.save(out, SM_FORMAT); 454 } 455 } 456 } 457 458 private synchronized void save_spin(PrintStream out) { 460 String ln = System.getProperty("line.separator"); 461 if (init != null) { 462 out.println("never {"); 463 } else { 464 out.println("Empty"); 465 return; 466 } 467 468 init.save(out, SPIN_FORMAT); 469 for (Iterator i = nodes.iterator(); i.hasNext();) { 470 Node n = (Node) i.next(); 471 472 if (init == n) { 473 continue; 474 } 475 476 n.save(out, SPIN_FORMAT); 477 out.println(); 478 } 479 480 out.println("}"); 481 } 482 483 private synchronized void save_xml(PrintStream out) { 484 out.println("<?xml version=\"1.0\"?>"); 485 out.println("<graph nodes=\"" + nodes.size() + "\">"); 486 attributes.save(out, XML_FORMAT); 487 488 for (Iterator i = nodes.iterator(); i.hasNext();) { 489 Node n = (Node) i.next(); 490 491 if (n != init) { 492 n.save(out, XML_FORMAT); 493 } else { 494 n.setBooleanAttribute("init", true); 495 n.save(out, XML_FORMAT); 496 n.setBooleanAttribute("init", false); 497 } 498 } 499 500 out.println("</graph>"); 501 } 502 } | Popular Tags |