equal
deleted
inserted
replaced
311 if (t1 == 0.0 || t2 == 0.0) 0 |
311 if (t1 == 0.0 || t2 == 0.0) 0 |
312 else t1 compare t2 |
312 else t1 compare t2 |
313 } |
313 } |
314 |
314 |
315 def compare(name1: String, name2: String): Int = |
315 def compare(name1: String, name2: String): Int = |
316 compare_timing(name2, name1) match { |
316 outdegree(name2) compare outdegree(name1) match { |
317 case 0 => |
317 case 0 => |
318 outdegree(name2) compare outdegree(name1) match { |
318 compare_timing(name2, name1) match { |
319 case 0 => |
319 case 0 => |
320 timeout(name2) compare timeout(name1) match { |
320 timeout(name2) compare timeout(name1) match { |
321 case 0 => name1 compare name2 |
321 case 0 => name1 compare name2 |
322 case ord => ord |
322 case ord => ord |
323 } |
323 } |