1#!/usr/bin/env python3 2# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de 3# l'Epita (LRDE). 4# 5# This file is part of Spot, a model checking library. 6# 7# Spot is free software; you can redistribute it and/or modify it 8# under the terms of the GNU General Public License as published by 9# the Free Software Foundation; either version 3 of the License, or 10# (at your option) any later version. 11# 12# Spot is distributed in the hope that it will be useful, but WITHOUT 13# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15# License for more details. 16# 17# You should have received a copy of the GNU General Public License 18# along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20import argparse 21import csv 22import re 23from collections import namedtuple 24 25# Pylatex Imports 26from pylatex import Document, Package, Tabular, MultiColumn 27from pylatex.utils import bold, NoEscape 28from pylatex.base_classes import CommandBase, Arguments 29from pylatex.base_classes.command import Parameters 30 31 32# ---------------------------------------------------------PARSE_CONFIG 33Bench = namedtuple('Bench', ['name', 'code', 'xoptions']) 34 35 36class BenchConfig(object): 37 """ 38 A class used to parse the 'bench.config' file. 39 """ 40 def __init__(self, filename): 41 """ 42 Any BenchConfig object file will have the following arguments: 43 44 -self.l which represents the list of all bench in the config file. 45 Each bench having three variables: name, code & xoptions. 46 47 -self.sh which contains shell codes that must be executed before 48 each bench. 49 """ 50 self.l = [] 51 self.sh = [] 52 with open(filename, 'r') as inputfile: 53 lines = inputfile.readlines() 54 for line in lines: 55 if line[0] == '#' or line.isspace(): 56 continue 57 elif line[0:2] == "sh": 58 sh = re.search('sh (.+?)$', line).group(1) 59 continue 60 else: 61 name = re.search('(.+?):', line).group(1) 62 code = re.search(':(.+?)>', line).group(1) 63 xoptions = re.search('>(.+?)$', line).group(1) 64 b = Bench(name=name, code=code, xoptions=xoptions) 65 self.l.append(b) 66 self.sh.append(sh) 67 sh = "" 68# ---------------------------------------------------------PARSE_CONFIG 69 70 71# --------------------------------------------------------------PYLATEX 72class ColorArgument(Parameters): 73 """ 74 A class implementing custom arguments formating for LaTeX command. 75 """ 76 def dumps(self): 77 params = self._list_args_kwargs() 78 if len(params) <= 0 or len(params) > 2: 79 return '' 80 string = '{' + params[0] + '} ' + params[1] 81 return string 82 83 84class SetColor(CommandBase): 85 """ 86 A class representing a LaTeX command used to colorize table's cells. 87 """ 88 _latex_name = 'cellcolor' 89 90 def dumps(self): 91 arguments = self.arguments.dumps() 92 res = '\\' + self._latex_name + arguments[1:-1] 93 return res 94 95 96class DefineColor(CommandBase): 97 """ 98 A class representing a LaTeX command used to define a color. 99 """ 100 _latex_name = 'definecolor' 101 102 103def ne(string): 104 """ 105 A wrapper around pylatex class NoEscape. It helps to tell pylatex to 106 not escape a string. 107 108 Be careful: 109 ne(string) + ne(string) = ne(string) 110 but 111 ne(string) + simple_string = simple_string 112 """ 113 return NoEscape(string) 114# --------------------------------------------------------------PYLATEX 115 116 117# --------------------------------------------------------------SUMMARY 118def add_winner(res, winner, loser): 119 """ 120 Each time this function is called, it increments the scrore 121 of one method against another one. 122 """ 123 res_length = len(res) 124 header_length = len(res[0]) 125 for i in range(1, res_length): # except the first row (header) 126 if winner in res[i]: 127 for j in range(1, header_length): 128 if loser in res[0][j]: 129 if type(res[i][j]) is str: 130 res[i][j] = 1 131 else: 132 res[i][j] = res[i][j] + 1 133 break 134 135 136def is_better(to_be_compared, val): 137 """ 138 Check that two to_be_compared is higher than val (5% tolerance). 139 """ 140 if val == 0: 141 return to_be_compared == 0 142 else: 143 return to_be_compared / val < 0.95 144 145 146def cmp_to_others(id_cmp, instance_cmp, what_cmp, line, config, res): 147 """ 148 Function used to compare a time of one method to others method. 149 """ 150 len_l = len(config.l) 151 for i in range(0, len_l): 152 index = get_st_index_of('min' + what_cmp + '.' + config.l[i].code, 153 line) 154 if index == id_cmp: 155 continue 156 if '-' not in line[index] and '!' not in line[index]: 157 val_cmp = float(line[id_cmp + 7]) 158 other = float(line[index + 7]) 159 if is_better(val_cmp, other): 160 add_winner(res, instance_cmp, config.l[i].code) 161 else: 162 add_winner(res, instance_cmp, config.l[i].code) 163 164 165def get_summary(config, test): 166 """ 167 Function used to get the summary of 'test' that can be either DBA, 168 or DTGBA. 169 """ 170 res = [] 171 len_l = len(config.l) 172 173 # Header 174 header = [''] 175 for i in range(0, len_l): 176 header.append(config.l[i].code) 177 header.append('total') 178 res.append(header) 179 180 # Prepare Body (fill with '-') 181 for i in range(0, len_l): 182 row = [config.l[i].code] 183 for j in range(0, len_l): 184 row.append('-') 185 row.append('') 186 res.append(row) 187 188 # Body 189 ifile = open('all.csv', 'r') 190 lines = ifile.readlines() 191 length = len(lines) 192 for i in range(0, length): 193 lines[i] = lines[i].split(',') 194 195 for i in range(0, length): 196 for j in range(0, len_l): 197 pattern = 'min' + test + '.' + config.l[j].code 198 199 st_id = get_st_index_of(pattern, lines[i]) 200 if '-' not in lines[i][st_id] and \ 201 '!' not in lines[i][st_id]: 202 cmp_to_others(st_id, config.l[j].code, test, 203 lines[i], config, res) 204 205 for row in res[1:]: 206 row[-1] = sum(x for x in row[1:-1] if type(x) is not str) 207 return res 208 209 210def write_summary(table2, config): 211 """ 212 Function that writes all the bench's summary. 213 """ 214 dba_summary = get_summary(config, 'DBA') 215 dtgba_summary = get_summary(config, 'DTGBA') 216 len_l = len(config.l) 217 table2.add_hline() 218 table2.add_row( 219 (MultiColumn(len_l + 2, align='|c|', data='DBA'),)) 220 table2.add_hline() 221 for i in range(0, len(dba_summary)): 222 table2.add_row(tuple(dba_summary[i])) 223 table2.add_hline() 224 table2.add_row((MultiColumn(len_l + 2),)) 225 table2.add_hline() 226 table2.add_row((MultiColumn(len_l + 2, align='|c|', data='DTGBA'),)) 227 table2.add_hline() 228 for line in dtgba_summary: 229 table2.add_row(tuple(line)) 230 table2.add_hline() 231# --------------------------------------------------------------SUMMARY 232 233 234# --------------------------------------------------------------RESULTS 235def get_st_index_of(pattern, line): 236 """ 237 A function used to get the first column of each benchmarked tool. 238 """ 239 size = len(line) 240 for i in range(0, size): 241 if pattern in line[i]: 242 return i + 1 243 raise ValueError('\'' + pattern + '\' is not found in log files') 244 245 246def dba_st_cmp_dtgba_st(pattern, line): 247 """ 248 Function that checks if minDTGBA.st * (minDTGBA.acc + 1) < minDBA.st. 249 It should not be the case normally! 250 """ 251 dba_st_id = get_st_index_of(pattern, line) 252 dba_st = line[dba_st_id] 253 dtgba_v = 0 254 dtgba_acc = 0 255 dba_v = 0 256 if '-' not in dba_st and '!' not in dba_st: 257 dba_v = int(dba_st) 258 if '-' not in line[dba_st_id + 10] \ 259 and '!' not in line[dba_st_id + 10]: 260 dtgba_v = int(line[dba_st_id + 10]) 261 dtgba_acc = int(line[dba_st_id + 13]) 262 return dtgba_v * (dtgba_acc + 1) < dba_v 263 return False 264 265 266def get_last_successful(n, category, pattern): 267 """ 268 A function used to get the last automaton size from satlog file. 269 """ 270 try: 271 log = open(str(n) + '.' + category + '.' + pattern 272 + '.satlog', 'r') 273 log_csv = csv.reader(log) 274 for line in log_csv: 275 min_val = line[2] 276 return '$\\le$' + min_val 277 except Exception: 278 return '' 279 280 281def check_all_st_are_eq(line, pattern): 282 """ 283 A function that: 284 - retrieve all column values that are just after any column containing 285 the pattern. 286 - check that all those values are exactly the same. 287 """ 288 size = len(line) 289 l = [] 290 for i in range(0, size): 291 if pattern in line[i]: 292 if '-' not in line[i + 1] and '!' not in line[i + 1] \ 293 and 'n/a' not in line[i + 1]: 294 try: 295 int(i + 1) 296 except Exception as e: 297 print(e) 298 exit() 299 l.append(line[i + 1]) 300 301 return all(x == l[0] for x in l) 302 303 304def add_other_cols(row, line, config): 305 """ 306 A function used to add all columns that dynamically depend on the 307 config.bench file. 308 """ 309 n = int(line[-1]) 310 category = ['DBA', 'DTGBA'] 311 312 dba_t = [] 313 dtgba_t = [] 314 dba_st = int(line[13]) 315 316 all_dba_st_eq = check_all_st_are_eq(line, 'minDBA') 317 all_dtgba_st_eq = check_all_st_are_eq(line, 'minDTGBA') 318 319 len_l = len(config.l) 320 for i in range(0, len_l): 321 for elt in category: 322 if 'DBA' in elt: 323 width = 3 324 elif 'DTGBA' in elt: 325 width = 4 326 st_id = get_st_index_of('min' + elt + '.' + config.l[i].code, line) 327 if '-' in line[st_id]: 328 s = ne(get_last_successful(n, elt, config.l[i].code)) 329 row.append(MultiColumn(width, align='c|', 330 data=ne('(killed') + s + ne(')'))) 331 elif '!' in line[st_id]: 332 s = ne(get_last_successful(n, elt, config.l[i].code)) 333 row.append(MultiColumn(width, align='c|', 334 data=ne('(intmax') + s + ne(')'))) 335 else: 336 cur_st = int(line[st_id]) 337 338 if 'DBA' in elt and \ 339 dba_st_cmp_dtgba_st('min' + elt + '.' 340 + config.l[i].code, line): 341 row.append(SetColor( 342 arguments=ColorArgument('Purpl', str(cur_st)))) 343 elif ((not all_dba_st_eq) and 'DBA' in elt) \ 344 or ((not all_dtgba_st_eq) and 'DTGBA' in elt) \ 345 or cur_st > dba_st: 346 row.append(SetColor( 347 arguments=ColorArgument('Red', str(cur_st)))) 348 elif cur_st < dba_st: 349 row.append(SetColor( 350 arguments=ColorArgument('Gray', str(cur_st)))) 351 else: 352 row.append(str(cur_st)) 353 354 row.append(line[st_id + 2]) # st + 2 = trans 355 time = '%.2f' % round(float(line[st_id + 7]), 2) 356 if width > 3: 357 row.append(line[st_id + 3]) 358 dtgba_t.append(time) 359 else: 360 dba_t.append(time) 361 row.append(time) 362 363 try: 364 dba = min(float(x) for x in dba_t) 365 except ValueError: 366 dba = -1 367 try: 368 dtgba = min(float(x) for x in dtgba_t) 369 except ValueError: 370 dtgba = -1 371 return dba, dtgba 372 373 374def get_dra_st(line, c): 375 """ 376 Get state of DRA. 377 """ 378 for i in range(0, len(line)): 379 if 'DRA' in line[i]: 380 if 'n/a' in line[i + 1]: 381 return '' 382 else: 383 return str(int(line[i + 1]) - 1 + int(c)) 384 385 386def get_type(type_f): 387 """ 388 A function used to categorized each formula. 389 """ 390 tmp = '' 391 if 'trad' in type_f: 392 tmp = 'T' 393 elif 'TCONG' in type_f: 394 tmp = 'P' 395 elif 'DRA' in type_f: 396 tmp = 'R' 397 elif 'WDBA' in type_f: 398 tmp = 'W' 399 else: 400 tmp = type_f 401 return tmp 402 403 404def val(line, v): 405 """ 406 A function used to retrieve any integer located at line[v]. 407 """ 408 try: 409 res = int(line[v]) 410 except Exception as e: 411 if '-' in line[v]: 412 return 1 413 else: 414 print(e) 415 exit() 416 return res 417 418 419def all_aut_are_det(line, config): 420 """ 421 A function that check that all automaton produced are determinist. 422 """ 423 if val(line, 8) == 0 or val(line, 18) == 0: 424 return False 425 size = len(config.l) 426 for i in range(1, size + 1): 427 if val(line, 18 + 10 * i) == 0: 428 return False 429 return True 430 431 432def clean_formula(f): 433 """ 434 A function used to clean any formula. 435 """ 436 res = '$' 437 f_iter = iter(f) 438 for it in f_iter: 439 if it == '&': 440 res += '\\land ' 441 elif it == '|': 442 res += '\\lor ' 443 elif it == '!': 444 res += '\\bar ' 445 elif it == '-' and next(f_iter, it) == '>': 446 res += '\\rightarrow ' 447 elif it == '<' and next(f_iter, it) == '-' and next(f_iter, it) == '>': 448 res += '\\leftrightarrow ' 449 else: 450 res += it 451 return ne(res + '$') 452 453 454def add_static_cols(row, line, config): 455 """ 456 A function used to add the 14 first static columns. Those columns don't 457 depend on the config.bench file. 458 """ 459 f = clean_formula(line[0]) # TODO: define math operators for formula 460 m = line[1] 461 f_type = line[2] 462 c = line[9] 463 if all_aut_are_det(line, config): 464 c_str = line[9] 465 else: 466 c_str = SetColor(arguments=ColorArgument('Red', line[9])) 467 dtgba_st = line[3] 468 dtgba_tr = line[5] 469 dtgba_acc = line[6] 470 dtgba_time = '%.2f' % round(float(line[10]), 2) 471 dba_st = line[13] 472 dba_tr = line[15] 473 dba_time = line[20] 474 475 row.append(f) # formula 476 row.append(m) 477 row.append(get_type(f_type)) # trad -> T, TCONG -> P, DRA -> R, WDBA -> W 478 row.append(c_str) # is complete or not 479 row.append(get_dra_st(line, c)) 480 row.append(dtgba_st) 481 row.append(dtgba_tr) 482 row.append(dtgba_acc) 483 row.append(dtgba_time) 484 row.append(dba_st) 485 row.append(dba_tr) 486 if '-' in dba_time or '!' in dba_time: 487 row.append(dba_time) 488 else: 489 row.append('%.2f' % round(float(dba_time), 2)) 490 491 # DBAminimizer 492 length = len(line) 493 for i in range(0, length): 494 if 'dbaminimizer' in line[i]: 495 if '-' in line[i + 1]: 496 row.append(MultiColumn(2, align='|c', data='(killed)')) 497 elif 'n/a' in line[i + 1]: 498 row.append('') 499 row.append('') 500 else: 501 minimizer_st = int(line[i + 1]) - 1 + int(c) 502 if minimizer_st < int(dba_st): 503 row.append(SetColor( 504 arguments=ColorArgument('Gray', str(minimizer_st)))) 505 elif minimizer_st > int(dba_st): 506 row.append(SetColor( 507 arguments=ColorArgument('Red', str(minimizer_st)))) 508 else: 509 row.append(minimizer_st) 510 row.append('%.2f' % round(float(line[i + 2]), 2)) 511 512 513def next_bench_considering_all(line, index): 514 """ 515 A function used to get the index of the next benchmark. It takes into 516 account '(killed)' MultiColumns... 517 """ 518 try: 519 line[index + 7] 520 except: 521 return index + 7 522 523 if is_not_MultiColumn(line, index): 524 if is_not_MultiColumn(line, index + 3): 525 return index + 7 526 else: 527 return index + 4 528 else: 529 if is_not_MultiColumn(line, index + 1): 530 return index + 5 531 else: 532 return index + 2 533 534 535def is_eq(to_be_compared, val): 536 """ 537 Check that two values are almost equal (5% tolerance). 538 """ 539 try: 540 return to_be_compared / val <= 1.05 # to_... is always >= val 541 except ZeroDivisionError: 542 return is_eq(to_be_compared + 1, val + 1) 543 544 545def is_not_MultiColumn(line, index): 546 """ 547 Check that the type(line[index]) is not MultiColumn. 548 """ 549 try: 550 return type(line[index]) is not MultiColumn 551 except IndexError as e: 552 print(e) 553 exit() 554 555 556def get_first_mindba(line): 557 """ 558 A function used to get the index of the first benchmark (just after 559 the static columns). 560 """ 561 if type(line[12]) is MultiColumn: 562 return 13 563 return 14 564 565 566def get_lines(config): 567 """ 568 Entry point for parsing the csv file. It returns all lines that will 569 be displayed. After this function, no more treatment are done on datas. 570 """ 571 all_l = [] 572 best_dba_l = [] 573 best_dtgba_l = [] 574 ifile = open('all.csv', 'r') 575 reader = csv.reader(ifile) 576 for line in reader: 577 row = [] 578 add_static_cols(row, line, config) # 14 first columns 579 dba_t, dtgba_t = add_other_cols(row, line, config) # All the rest 580 all_l.append(row) 581 best_dba_l.append(dba_t) 582 best_dtgba_l.append(dtgba_t) 583 584 all_lines_length = len(all_l) 585 for i in range(0, all_lines_length): 586 index = get_first_mindba(all_l[i]) 587 size = len(all_l[i]) 588 while index < size: 589 if best_dba_l[i] != -1: 590 if is_not_MultiColumn(all_l[i], index): 591 if is_eq(float(all_l[i][index + 2]), best_dba_l[i]): 592 all_l[i][index + 2] = SetColor( 593 arguments=ColorArgument('Green', 594 str(best_dba_l[i]))) 595 596 if best_dtgba_l[i] != -1: 597 if is_not_MultiColumn(all_l[i], index): 598 if is_not_MultiColumn(all_l[i], index + 3)\ 599 and is_eq(float(all_l[i][index + 6]), 600 best_dtgba_l[i]): 601 all_l[i][index + 6] = SetColor( 602 arguments=ColorArgument('Yelw', 603 str(best_dtgba_l[i]))) 604 else: 605 if is_not_MultiColumn(all_l[i], index + 1)\ 606 and is_eq(float(all_l[i][index + 4]), 607 best_dtgba_l[i]): 608 all_l[i][index + 4] = SetColor( 609 arguments=ColorArgument('Yelw', 610 str(best_dtgba_l[i]))) 611 612 index = next_bench_considering_all(all_l[i], index) 613 return all_l, best_dba_l, best_dtgba_l 614 615 616def write_header(table, config): 617 """ 618 Function that write the first lines of the document. 619 """ 620 # Static datas 621 data_row1 = ne('Column ') + bold('type') + \ 622 ne(' shows how the initial det. aut. was obtained: T = translation' 623 ' produces DTGBA; W = WDBA minimization works; P = powerset ' 624 'construction transforms TBA to DTBA; R = DRA to DBA.') 625 data_row2 = ne('Column ') + bold('C.') + \ 626 ne(' tells whether the output automaton is complete: rejecting ' 627 'sink states are always omitted (add 1 state when C=0 if you ' 628 'want the size of the complete automaton).') 629 row3 = [MultiColumn(14)] 630 row4 = ['', '', '', '', 'DRA', 631 MultiColumn(4, align='|c', data='DTGBA'), 632 MultiColumn(3, align='|c', data='DBA'), 633 MultiColumn(2, align='|c', 634 data=ne('DBA\\footnotesize minimizer'))] 635 row5 = ['formula', 'm', 'type', 'C.', 'st.', 'st.', 'tr.', 636 'acc.', 'time', 'st.', 'tr.', 'time', 'st.', 'time'] 637 638 # Datas that depends on the configuration file 639 len_l = len(config.l) 640 for i in range(0, len_l): 641 row3.append(MultiColumn(7, align='|c', data=config.l[i].name)) 642 row4.append(MultiColumn(3, align='|c', data='minDBA')) 643 row4.append(MultiColumn(4, align='|c', data='minDTGBA')) 644 row5.extend(['st.', 'tr.', 'time', 'st.', 'tr.', 'acc.', 'time']) 645 646 # Add the first 5 lines of the document. 647 n = 14 + len_l * 7 648 table.add_row((MultiColumn(n, align='c', data=data_row1),)) 649 table.add_row((MultiColumn(n, align='c', data=data_row2),)) 650 table.add_row((MultiColumn(n, align='l', data=''),)) # add empty line 651 table.add_row(tuple(row3)) 652 table.add_row(tuple(row4)) 653 table.add_row(tuple(row5)) 654 table.add_hline() 655 656 657def write_results(table, config): 658 """ 659 Function that writes all the bench's result. 660 """ 661 # Write header (first 5 lines) 662 write_header(table, config) 663 664 # Write all results 665 lines, best_dba_l, best_dtgba_l = get_lines(config) 666 for line in lines: 667 table.add_row(tuple(line)) 668# --------------------------------------------------------------RESULTS 669 670 671def add_fmt(nfields, doc): 672 """ 673 Function used to define the table's format depending on config.bench 674 file. 675 """ 676 if doc: 677 tmp = '|lrcr|r|rrrr|rrr|rr|' 678 for i in range(0, nfields): 679 tmp += 'rrr|rrrr|' 680 return tmp 681 else: 682 tmp = '|c|c|' 683 for i in range(0, nfields): 684 tmp += 'c|' 685 return tmp 686 687 688def generate_docs(config): 689 """ 690 Function used to generate two pdf: 691 692 -results.pdf: which shows all statistics about each formula with each 693 benchmarked method. 694 695 -summary.pdf: which count the number of times that each method is 696 better than another. 697 """ 698 # Let's create the documents (result & summary) 699 doc = Document(documentclass='standalone') 700 doc.packages.append(Package('amsmath')) 701 doc.packages.append(Package('color')) 702 doc.packages.append(Package('colortbl')) 703 doc2 = Document(documentclass='standalone') 704 705 # Declare colors in result document 706 doc.append(DefineColor( 707 arguments=Arguments('Gray', 'rgb', '0.7, 0.7, 0.7'))) 708 doc.append(DefineColor(arguments=Arguments('Green', 'rgb', '0.4, 1, 0.4'))) 709 doc.append(DefineColor(arguments=Arguments('Red', 'rgb', '0.8, 0, 0'))) 710 doc.append(DefineColor(arguments=Arguments('Yelw', 'rgb', '1, 0.98, 0.4'))) 711 doc.append(DefineColor(arguments=Arguments('Purpl', 'rgb', '1, 0.6, 1'))) 712 713 # Create Table with format : True is result format, False is summary format 714 table = Tabular(add_fmt(len(config.l), True)) 715 table2 = Tabular(add_fmt(len(config.l), False)) 716 717 # Write everything 718 write_results(table, config) 719 write_summary(table2, config) 720 721 # Output PDF 722 doc.append(table) 723 doc2.append(table2) 724 doc.generate_pdf('results') 725 doc2.generate_pdf('summary') 726 727 728def generate_bench(config, args): 729 """ 730 A function used to generate a complete benchmark. It outputs a shell 731 script. 732 """ 733 echo = "" 734 with open('stat-gen.sh', 'w') as script: 735 # Header. 736 script.write('''#!/bin/sh 737 738ltlfilt=../../bin/ltlfilt 739ltl2tgba=../../bin/ltl2tgba 740dstar2tgba=../../bin/dstar2tgba 741timeout='timeout -sKILL {}' 742stats=--stats=\"%s, %e, %t, %a, %c, %d, %p, %r, %R\" 743empty='-, -, -, -, -, -, -, -, -' 744tomany='!, !, !, !, !, !, !, !, !' 745dbamin=${} 746 747'''.format(str(args.timeout) + args.unit, '{DBA_MINIMIZER}')) 748 749 script.write('''get_stats() 750{ 751 type=$1 752 shift 753 SPOT_SATLOG=$n.$type.satlog $timeout \"$@\" \"$stats\"> stdin.$$ 2>stderr.$$ 754 if grep -q 'INT_MAX' stderr.$$; then 755 # Too many SAT-clause? 756 echo \"tomany\" 757 else 758 tmp=`cat stdin.$$` 759 echo ${tmp:-$empty} 760 fi 761 rm -f stdin.$$ stderr.$$ 762} 763 764get_dbamin_stats() 765{ 766 tmp=`./rundbamin.pl $timeout $dbamin \"$@\"` 767 mye='-, -' 768 echo ${tmp:-$mye} 769} 770 771n=$1 772f=$2 773type=$3 774accmax=$4 775 776case $type in 777 *WDBA*) 778 exit 0 779 ;; 780 *TCONG*|*trad*) # Not in WDBA 781 echo \"$f, $accmax, $type...\" 1>&2 782 input=`get_stats TBA $ltl2tgba \"$f\" -D -x '!wdba-minimize,tba-det'` 783 echo \"$f, $accmax, $type, $input, DBA, ...\" 1>&2\n 784 dba=`get_stats BA $ltl2tgba \"$f\" -BD -x '!wdba-minimize,tba-det'` 785 786''') 787 788 # Body. 789 echo = "$f, $accmax, $type, $input, DBA, $dba" 790 for i in range(0, len(config.l)): 791 script.write(" # " + config.l[i].name + "\n") 792 if config.sh[i]: 793 script.write(" " + config.sh[i] + "\n") 794 script.write(" echo \"" + echo + ", minDBA." + config.l[i].code 795 + "...\" 1>&2\n") 796 script.write(" mindba_" + config.l[i].code + "=`get_stats DBA." 797 + config.l[i].code + " $ltl2tgba \"$f\" -BD -x" 798 " '!wdba-minimize," + config.l[i].xoptions + "'`\n") 799 echo += ", minDBA." + config.l[i].code + ", $mindba_" \ 800 + config.l[i].code 801 script.write(" echo \"" + echo + ", minDTGBA." + config.l[i].code 802 + "...\" 1>&2\n") 803 script.write(" mindtgba_" + config.l[i].code + 804 "=`get_stats DTGBA." + config.l[i].code + 805 " $ltl2tgba \"$f\" -D -x '!wdba-minimize," + 806 config.l[i].xoptions + "'`\n\n") 807 echo += ", minDTGBA." + config.l[i].code + ", $mindtgba_" \ 808 + config.l[i].code 809 script.write(''' # Dbaminimizer 810 echo \"{}, dbaminimizer...\" 1>&2 811 case $type in 812 *TCONG*) dbamin=\"n/a, n/a\" dra=\"n/a\";; 813 *trad*) 814 $ltlfilt --remove-wm -f \"$f\" -l | 815 ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ 816 dbamin=`get_dbamin_stats dra.$$` 817 dra=`sed -n 's/States: \\(.*\\)/\\1/p' dra.$$` 818 rm dra.$$ 819 ;; 820 esac 821 ;; 822 *DRA*) 823 echo \"$f, $accmax, $type...\" 1>&2 824 $ltlfilt --remove-wm -f \"$f\" -l | 825 ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ 826 input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'` 827 echo \"$f, $accmax, $type, $input, DBA, ...\" 1>&2 828 dba=`get_stats BA $dstar2tgba dra.$$ -BD -x '!wdba-minimize'` 829 830'''.format(echo)) 831 832 echo = "$f, $accmax, $type, $input, DBA, $dba" 833 for i in range(0, len(config.l)): 834 script.write(" # " + config.l[i].name + "\n") 835 if config.sh[i]: 836 script.write(" " + config.sh[i] + "\n") 837 script.write(" echo \"" + echo + ", minDBA." + config.l[i].code 838 + "...\" 1>&2\n") 839 script.write(" mindba_" + config.l[i].code + "=`get_stats DBA." 840 + config.l[i].code + " $dstar2tgba dra.$$ -BD -x" 841 " '!wdba-minimize," + config.l[i].xoptions + "'`\n") 842 echo += ", minDBA." + config.l[i].code + ", $mindba_" \ 843 + config.l[i].code 844 script.write(" echo \"" + echo + ", minDTGBA." + config.l[i].code 845 + "...\" 1>&2\n") 846 script.write(" mindtgba_" + config.l[i].code + 847 "=`get_stats DTGBA." + config.l[i].code + 848 " $dstar2tgba dra.$$ -D -x '!wdba-minimize," + 849 config.l[i].xoptions + "'`\n\n") 850 echo += ", minDTGBA." + config.l[i].code + ", $mindtgba_" \ 851 + config.l[i].code 852 853 script.write(''' # Dbaminimizer 854 echo \"{}, dbaminimizer...\" 1>&2 855 dbamin=`get_dbamin_stats dra.$$` 856 dra=`sed -n 's/States: \\(.*\\)/\\1/p' dra.$$` 857 rm -f dra.$$ 858 ;; 859 *not*) 860 exit 0 861 ;; 862 *) 863 echo \"SHOULD NOT HAPPEND\" 864 exit 2 865 ;; 866esac 867 868'''.format(echo)) 869 echo += ", dbaminimizer, $dbamin, DRA, $dra, $n" 870 script.write("echo \"{}\" 1>&2\n".format(echo)) 871 script.write("echo \"{}\"\n".format(echo)) 872 print("Now run chmod +x stat-gen.sh") 873 874 875def parse_args(): 876 """ 877 Function that parse the command-line arguments and options. 878 """ 879 parser = argparse.ArgumentParser() 880 parser.add_argument('action', choices=['script', 'results']) 881 parser.add_argument('--timeout', type=int, help="Timeout (0-9)+") 882 parser.add_argument('--unit', type=str, help="Time unit (h|m|s)", 883 choices=['h', 'm', 's']) 884 args = parser.parse_args() 885 886 config = BenchConfig('config.bench') 887 if args.action == 'script': 888 if not args.timeout: 889 parser.error('bench requires --timeout') 890 if not args.unit: 891 parser.error('bench requires --unit') 892 generate_bench(config, args) 893 elif args.action == 'results': 894 generate_docs(config) 895 896 897if __name__ == '__main__': 898 parse_args() 899