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