From 042c7a0f5bedaabdcbdf0ebd61ffda3bad1393e2 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Wed, 4 Jan 2017 14:16:32 +0100 Subject: [PATCH] Update dtgbasat benchmark * bench/dtgbasat/config.bench: Configuration file sample used by gen.py * bench/dtgbasat/gen.py: Script that can generate both bench script and pdf results. * bench/dtgbasat/stats.sh: Change stat.sh into stat-gen.sh that will be generated by gen.py script. * bench/dtgbasat/Makefile.am: Add new files. * bench/dtgbasat/README: Update README. * bench/dtgbasat/stat-gen.sh: Add stat script generated by gen.py and default config.bench file. --- bench/dtgbasat/Makefile.am | 2 +- bench/dtgbasat/README | 34 +- bench/dtgbasat/config.bench | 33 ++ bench/dtgbasat/gen.py | 898 ++++++++++++++++++++++++++++++++++++ bench/dtgbasat/stat-gen.sh | 297 ++++++++++++ bench/dtgbasat/stats.sh | 6 +- 6 files changed, 1257 insertions(+), 13 deletions(-) create mode 100644 bench/dtgbasat/config.bench create mode 100755 bench/dtgbasat/gen.py create mode 100644 bench/dtgbasat/stat-gen.sh diff --git a/bench/dtgbasat/Makefile.am b/bench/dtgbasat/Makefile.am index 8a4cea8a3..75ce40b37 100644 --- a/bench/dtgbasat/Makefile.am +++ b/bench/dtgbasat/Makefile.am @@ -17,6 +17,6 @@ ## along with this program. If not, see . EXTRA_DIST = formulas prepare.sh rundbamin.pl stat.sh stats.sh tabl.pl \ - tabl1.pl tabl2.pl tabl3.pl tabl4.pl + tabl1.pl tabl2.pl tabl3.pl tabl4.pl gen.py config.bench diff --git a/bench/dtgbasat/README b/bench/dtgbasat/README index af5c55061..4107f1ebb 100644 --- a/bench/dtgbasat/README +++ b/bench/dtgbasat/README @@ -9,6 +9,9 @@ Note that the encoding used in the SAT-based minimization have evolved since the paper, so if you want to reproduce exactly the benchmark from the paper, you should download a copy of Spot 1.2.3. +This benchmark has grown since FORTE'14. Some new SAT-based methods have +been implemented. This benchmark measures all the methods and identifies the +best. To reproduce, follow these instructions: @@ -55,19 +58,32 @@ To reproduce, follow these instructions: You should set such a limit with "ulimit" if you like. For instance % ulimit -v 41943040 -9) Actually run all experiments +9) Before running the experiment, as Spot has now more SAT-based minimization + methods, you may want to reduce or choose the methods to be benched. + Have a look at the 'config.bench' file. By default, it contains all the + possible methods. Leave it unchanged if you want to compare all methods. + If it is changed, you need to re-generate the stat-gen.sh file by running: + % ./gen.py script --timeout --unit - % make -j4 -f stat.mk +10) Actually run all experiments - This will build a CSV file called "all.csv". + % make -j4 -f stat.mk -10) You may generate LaTeX code for the tables with the scripts: - - tabl.pl: Full data. - - tabl1.pl, tabl2.pl, tabl3.pl, tabl4.pl: Partial tables as shown - in the paper. + This will build a CSV file called "all.csv". - All these script takes the CSV file all.csv as first argument, and - output LaTeX to their standard output. +11) You may generate LaTeX code for the tables with 'gen.py'. This script is + really helpful as it permits you to generate even partial results. If after + all benchmarks, you want to compare only two methods among the others, just + comment the others in the configuration file 'config.bench' and run this + script. + % ./gen.py results + + This scripts read the all.csv file generated at the end of the benchmark + and outputs two PDF documents: + -results.pdf: Which contains all statistics about each formula for each + method. + -resume.pdf which present two tables that count how many times a method + is better than another. For more instruction about how to use ltl2tgba and dstar2tgba to diff --git a/bench/dtgbasat/config.bench b/bench/dtgbasat/config.bench new file mode 100644 index 000000000..c96c2d988 --- /dev/null +++ b/bench/dtgbasat/config.bench @@ -0,0 +1,33 @@ +# This is a comment. +# This file is only used by the gen.py script. +# +# If you need to execute some shell code before a method, just write: +# 'sh "your_shell_code_in_one_line"' before that method. +# +# For each method, here is the syntax: +# "name_of_the_bench":"short_code">"some -x options" +# (see man spot-x for details)" + +sh export SPOT_SATSOLVER="glucose -verb=0 -model %I > %O" +Glucose (As before):glu>sat-minimize=4 + +sh export SPOT_SATSOLVER="picosat %I > %O" +PicoSAT (As before):pic>sat-minimize=4 + +sh unset SPOT_SATSOLVER +PicoLibrary:libp>sat-minimize=4 + +Incr Naive:incr1>sat-minimize=3,param=-1 +Incr param=1:incr2p1>sat-minimize=3,param=1 +Incr param=2:incr2p2>sat-minimize=3,param=2 +Incr param=4:incr2p4>sat-minimize=3,param=4 +Incr param=8:incr2p8>sat-minimize=3,param=8 +Assume param=1:assp1>sat-minimize=2,param=1 +Assume param=2:assp2>sat-minimize=2,param=2 +Assume param=3:assp2>sat-minimize=2,param=2 +Assume param=4:assp4>sat-minimize=2,param=4 +Assume param=5:assp5>sat-minimize=2,param=5 +Assume param=6:assp6>sat-minimize=2,param=6 +Assume param=7:assp7>sat-minimize=2,param=7 +Assume param=8:assp8>sat-minimize=2,param=8 +Dichotomy:dicho>sat-minimize diff --git a/bench/dtgbasat/gen.py b/bench/dtgbasat/gen.py new file mode 100755 index 000000000..5751d8ea9 --- /dev/null +++ b/bench/dtgbasat/gen.py @@ -0,0 +1,898 @@ +#!/usr/bin/env python3 +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import argparse +import csv +import re +from collections import namedtuple + +# Pylatex Imports +from pylatex import Document, Package, Tabular, MultiColumn +from pylatex.utils import bold, NoEscape +from pylatex.base_classes import CommandBase, Arguments +from pylatex.base_classes.command import Parameters + + +# ---------------------------------------------------------PARSE_CONFIG +Bench = namedtuple('Bench', ['name', 'code', 'xoptions']) + + +class BenchConfig(object): + """ + A class used to parse the 'bench.config' file. + """ + def __init__(self, filename): + """ + Any BenchConfig object file will have the following arguments: + + -self.l which represents the list of all bench in the config file. + Each bench having three variables: name, code & xoptions. + + -self.sh which contains shell codes that must be executed before + each bench. + """ + self.l = [] + self.sh = [] + with open(filename, 'r') as inputfile: + lines = inputfile.readlines() + for line in lines: + if line[0] == '#' or line.isspace(): + continue + elif line[0:2] == "sh": + sh = re.search('sh (.+?)$', line).group(1) + continue + else: + name = re.search('(.+?):', line).group(1) + code = re.search(':(.+?)>', line).group(1) + xoptions = re.search('>(.+?)$', line).group(1) + b = Bench(name=name, code=code, xoptions=xoptions) + self.l.append(b) + self.sh.append(sh) + sh = "" +# ---------------------------------------------------------PARSE_CONFIG + + +# --------------------------------------------------------------PYLATEX +class ColorArgument(Parameters): + """ + A class implementing custom arguments formating for LaTeX command. + """ + def dumps(self): + params = self._list_args_kwargs() + if len(params) <= 0 or len(params) > 2: + return '' + string = '{' + params[0] + '} ' + params[1] + return string + + +class SetColor(CommandBase): + """ + A class representing a LaTeX command used to colorize table's cells. + """ + _latex_name = 'cellcolor' + + def dumps(self): + arguments = self.arguments.dumps() + res = '\\' + self._latex_name + arguments[1:-1] + return res + + +class DefineColor(CommandBase): + """ + A class representing a LaTeX command used to define a color. + """ + _latex_name = 'definecolor' + + +def ne(string): + """ + A wrapper around pylatex class NoEscape. It helps to tell pylatex to + not escape a string. + + Be careful: + ne(string) + ne(string) = ne(string) + but + ne(string) + simple_string = simple_string + """ + return NoEscape(string) +# --------------------------------------------------------------PYLATEX + + +# ---------------------------------------------------------------RESUME +def add_winner(res, winner, looser): + """ + Each time this function is called, it increments the scrore + of one method against another one. + """ + res_length = len(res) + header_length = len(res[0]) + for i in range(1, res_length): # except the first row (header) + if winner in res[i]: + for j in range(1, header_length): + if looser in res[0][j]: + if type(res[i][j]) is str: + res[i][j] = 1 + else: + res[i][j] = res[i][j] + 1 + break + + +def is_better(to_be_compared, val): + """ + Check that two to_be_compared is higher than val (5% tolerance). + """ + if val == 0: + return to_be_compared == 0 + else: + return to_be_compared / val < 0.95 + + +def cmp_to_others(id_cmp, instance_cmp, what_cmp, line, config, res): + """ + Function used to compare a time of one method to others method. + """ + len_l = len(config.l) + for i in range(0, len_l): + index = get_st_index_of('min' + what_cmp + '.' + config.l[i].code, + line) + if index == id_cmp: + continue + if '-' not in line[index] and '!' not in line[index]: + val_cmp = float(line[id_cmp + 7]) + other = float(line[index + 7]) + if is_better(val_cmp, other): + add_winner(res, instance_cmp, config.l[i].code) + else: + add_winner(res, instance_cmp, config.l[i].code) + + +def get_resume(config, test): + """ + Function used to get the resume of 'test' that can be either DBA, + or DTGBA. + """ + res = [] + len_l = len(config.l) + + # Header + header = [''] + for i in range(0, len_l): + header.append(config.l[i].code) + header.append('total') + res.append(header) + + # Prepare Body (fill with '-') + for i in range(0, len_l): + row = [config.l[i].code] + for j in range(0, len_l): + row.append('-') + row.append('') + res.append(row) + + # Body + ifile = open('all.csv', 'r') + lines = ifile.readlines() + length = len(lines) + for i in range(0, length): + lines[i] = lines[i].split(',') + + for i in range(0, length): + for j in range(0, len_l): + pattern = 'min' + test + '.' + config.l[j].code + + st_id = get_st_index_of(pattern, lines[i]) + if '-' not in lines[i][st_id] and \ + '!' not in lines[i][st_id]: + cmp_to_others(st_id, config.l[j].code, test, + lines[i], config, res) + + for row in res[1:]: + row[-1] = sum(x for x in row[1:-1] if type(x) is not str) + return res + + +def write_resume(table2, config): + """ + Function that writes all the bench's resume. + """ + dba_resume = get_resume(config, 'DBA') + dtgba_resume = get_resume(config, 'DTGBA') + len_l = len(config.l) + table2.add_hline() + table2.add_row( + (MultiColumn(len_l + 2, align='|c|', data='DBA'),)) + table2.add_hline() + for i in range(0, len(dba_resume)): + table2.add_row(tuple(dba_resume[i])) + table2.add_hline() + table2.add_row((MultiColumn(len_l + 2),)) + table2.add_hline() + table2.add_row((MultiColumn(len_l + 2, align='|c|', data='DTGBA'),)) + table2.add_hline() + for line in dtgba_resume: + table2.add_row(tuple(line)) + table2.add_hline() +# ---------------------------------------------------------------RESUME + + +# --------------------------------------------------------------RESULTS +def get_st_index_of(pattern, line): + """ + A function used to get the first column of each benchmarked tool. + """ + size = len(line) + for i in range(0, size): + if pattern in line[i]: + return i + 1 + raise ValueError('\'' + pattern + '\' is not found in log files') + + +def dba_st_cmp_dtgba_st(pattern, line): + """ + Function that checks if minDTGBA.st * (minDTGBA.acc + 1) < minDBA.st. + It should not be the case normally! + """ + dba_st_id = get_st_index_of(pattern, line) + dba_st = line[dba_st_id] + dtgba_v = 0 + dtgba_acc = 0 + dba_v = 0 + if '-' not in dba_st and '!' not in dba_st: + dba_v = int(dba_st) + if '-' not in line[dba_st_id + 10] \ + and '!' not in line[dba_st_id + 10]: + dtgba_v = int(line[dba_st_id + 10]) + dtgba_acc = int(line[dba_st_id + 13]) + return dtgba_v * (dtgba_acc + 1) < dba_v + return False + + +def get_last_successful(n, category, pattern): + """ + A function used to get the last automaton size from satlog file. + """ + try: + log = open(str(n) + '.' + category + '.' + pattern + + '.satlog', 'r') + log_csv = csv.reader(log) + for line in log_csv: + min_val = line[1] + return ', $\\le$ ' + min_val + except Exception: + return '' + + +def check_all_st_are_eq(line, pattern): + """ + A function that: + - retrieve all column values that are just after any column containing + the pattern. + - check that all those values are exactly the same. + """ + size = len(line) + l = [] + for i in range(0, size): + if pattern in line[i]: + if '-' not in line[i + 1] and '!' not in line[i + 1] \ + and 'n/a' not in line[i + 1]: + try: + int(i + 1) + except Exception as e: + print(e) + exit() + l.append(line[i + 1]) + + return all(x == l[0] for x in l) + + +def add_other_cols(row, line, config): + """ + A function used to add all columns that dynamically depend on the + config.bench file. + """ + n = int(line[-1]) + category = ['DBA', 'DTGBA'] + + dba_t = [] + dtgba_t = [] + dba_st = int(line[13]) + + all_dba_st_eq = check_all_st_are_eq(line, 'minDBA') + all_dtgba_st_eq = check_all_st_are_eq(line, 'minDTGBA') + + len_l = len(config.l) + for i in range(0, len_l): + for elt in category: + if 'DBA' in elt: + width = 3 + elif 'DTGBA' in elt: + width = 4 + st_id = get_st_index_of('min' + elt + '.' + config.l[i].code, line) + if '-' in line[st_id]: + s = ne(get_last_successful(n, elt, config.l[i].code)) + row.append(MultiColumn(width, align='c|', + data=ne('(killed ') + s + ne(')'))) + elif '!' in line[st_id]: + s = ne(get_last_successful(n, elt, config.l[i].code)) + row.append(MultiColumn(width, align='c|', + data=ne('(intmax ') + s + ne(')'))) + else: + cur_st = int(line[st_id]) + + if 'DBA' in elt and \ + dba_st_cmp_dtgba_st('min' + elt + '.' + + config.l[i].code, line): + row.append(SetColor( + arguments=ColorArgument('Purpl', str(cur_st)))) + elif ((not all_dba_st_eq) and 'DBA' in elt) \ + or ((not all_dtgba_st_eq) and 'DTGBA' in elt) \ + or cur_st > dba_st: + row.append(SetColor( + arguments=ColorArgument('Red', str(cur_st)))) + elif cur_st < dba_st: + row.append(SetColor( + arguments=ColorArgument('Gray', str(cur_st)))) + else: + row.append(str(cur_st)) + + row.append(line[st_id + 2]) # st + 2 = trans + time = '%.2f' % round(float(line[st_id + 7]), 2) + if width > 3: + row.append(line[st_id + 3]) + dtgba_t.append(time) + else: + dba_t.append(time) + row.append(time) + + try: + dba = min(float(x) for x in dba_t) + except ValueError: + dba = -1 + try: + dtgba = min(float(x) for x in dtgba_t) + except ValueError: + dtgba = -1 + return dba, dtgba + + +def get_dra_st(line, c): + """ + Get state of DRA. + """ + for i in range(0, len(line)): + if 'DRA' in line[i]: + if 'n/a' in line[i + 1]: + return '' + else: + return str(int(line[i + 1]) - 1 + int(c)) + + +def get_type(type_f): + """ + A function used to categorized each formula. + """ + tmp = '' + if 'trad' in type_f: + tmp = 'T' + elif 'TCONG' in type_f: + tmp = 'P' + elif 'DRA' in type_f: + tmp = 'R' + elif 'WDBA' in type_f: + tmp = 'W' + else: + tmp = type_f + return tmp + + +def val(line, v): + """ + A function used to retrieve any integer located at line[v]. + """ + try: + res = int(line[v]) + except Exception as e: + if '-' in line[v]: + return 1 + else: + print(e) + exit() + return res + + +def all_aut_are_det(line, config): + """ + A function that check that all automaton produced are determinist. + """ + if val(line, 8) == 0 or val(line, 18) == 0: + return False + size = len(config.l) + for i in range(1, size + 1): + if val(line, 18 + 10 * i) == 0: + return False + return True + + +def clean_formula(f): + """ + A function used to clean any formula. + """ + res = '$' + f_iter = iter(f) + for it in f_iter: + if it == '&': + res += '\\land ' + elif it == '|': + res += '\\lor ' + elif it == '!': + res += '\\bar ' + elif it == '-' and next(f_iter, it) == '>': + res += '\\rightarrow ' + elif it == '<' and next(f_iter, it) == '-' and next(f_iter, it) == '>': + res += '\\leftrightarrow ' + else: + res += it + return ne(res + '$') + + +def add_static_cols(row, line, config): + """ + A function used to add the 14 first static columns. Those columns don't + depend on the config.bench file. + """ + f = clean_formula(line[0]) # TODO: define math operators for formula + m = line[1] + f_type = line[2] + c = line[9] + if all_aut_are_det(line, config): + c_str = line[9] + else: + c_str = SetColor(arguments=ColorArgument('Red', line[9])) + dtgba_st = line[3] + dtgba_tr = line[5] + dtgba_acc = line[6] + dtgba_time = '%.2f' % round(float(line[10]), 2) + dba_st = line[13] + dba_tr = line[15] + dba_time = line[20] + + row.append(f) # formula + row.append(m) + row.append(get_type(f_type)) # trad -> T, TCONG -> P, DRA -> R, WDBA -> W + row.append(c_str) # is complete or not + row.append(get_dra_st(line, c)) + row.append(dtgba_st) + row.append(dtgba_tr) + row.append(dtgba_acc) + row.append(dtgba_time) + row.append(dba_st) + row.append(dba_tr) + if '-' in dba_time or '!' in dba_time: + row.append(dba_time) + else: + row.append('%.2f' % round(float(dba_time), 2)) + + # DBAminimizer + length = len(line) + for i in range(0, length): + if 'dbaminimizer' in line[i]: + if '-' in line[i + 1]: + row.append(MultiColumn(2, align='|c', data='(killed)')) + elif 'n/a' in line[i + 1]: + row.append('') + row.append('') + else: + minimizer_st = int(line[i + 1]) - 1 + int(c) + if minimizer_st < int(dba_st): + row.append(SetColor( + arguments=ColorArgument('Gray', str(minimizer_st)))) + elif minimizer_st > int(dba_st): + row.append(SetColor( + arguments=ColorArgument('Red', str(minimizer_st)))) + else: + row.append(minimizer_st) + row.append('%.2f' % round(float(line[i + 2]), 2)) + + +def next_bench_considering_all(line, index): + """ + A function used to get the index of the next benchmark. It takes into + account '(killed)' MultiColumns... + """ + try: + line[index + 7] + except: + return index + 7 + + if is_not_MultiColumn(line, index): + if is_not_MultiColumn(line, index + 3): + return index + 7 + else: + return index + 4 + else: + if is_not_MultiColumn(line, index + 1): + return index + 5 + else: + return index + 2 + + +def is_eq(to_be_compared, val): + """ + Check that two values are almost equal (5% tolerance). + """ + try: + return to_be_compared / val <= 1.05 # to_... is always >= val + except ZeroDivisionError: + return is_eq(to_be_compared + 1, val + 1) + + +def is_not_MultiColumn(line, index): + """ + Check that the type(line[index]) is not MultiColumn. + """ + try: + return type(line[index]) is not MultiColumn + except IndexError as e: + print(e) + exit() + + +def get_first_mindba(line): + """ + A function used to get the index of the first benchmark (just after + the static columns). + """ + if type(line[12]) is MultiColumn: + return 13 + return 14 + + +def get_lines(config): + """ + Entry point for parsing the csv file. It returns all lines that will + be displayed. After this function, no more treatment are done on datas. + """ + all_l = [] + best_dba_l = [] + best_dtgba_l = [] + ifile = open('all.csv', 'r') + reader = csv.reader(ifile) + for line in reader: + row = [] + add_static_cols(row, line, config) # 14 first columns + dba_t, dtgba_t = add_other_cols(row, line, config) # All the rest + all_l.append(row) + best_dba_l.append(dba_t) + best_dtgba_l.append(dtgba_t) + + all_lines_length = len(all_l) + for i in range(0, all_lines_length): + index = get_first_mindba(all_l[i]) + size = len(all_l[i]) + while index < size: + if best_dba_l[i] != -1: + if is_not_MultiColumn(all_l[i], index): + if is_eq(float(all_l[i][index + 2]), best_dba_l[i]): + all_l[i][index + 2] = SetColor( + arguments=ColorArgument('Green', + str(best_dba_l[i]))) + + if best_dtgba_l[i] != -1: + if is_not_MultiColumn(all_l[i], index): + if is_not_MultiColumn(all_l[i], index + 3)\ + and is_eq(float(all_l[i][index + 6]), + best_dtgba_l[i]): + all_l[i][index + 6] = SetColor( + arguments=ColorArgument('Yelw', + str(best_dtgba_l[i]))) + else: + if is_not_MultiColumn(all_l[i], index + 1)\ + and is_eq(float(all_l[i][index + 4]), + best_dtgba_l[i]): + all_l[i][index + 4] = SetColor( + arguments=ColorArgument('Yelw', + str(best_dtgba_l[i]))) + + index = next_bench_considering_all(all_l[i], index) + return all_l, best_dba_l, best_dtgba_l + + +def write_header(table, config): + """ + Function that write the first lines of the document. + """ + # Static datas + data_row1 = ne('Column ') + bold('type') + \ + ne(' shows how the initial det. aut. was obtained: T = translation' + ' produces DTGBA; W = WDBA minimization works; P = powerset ' + 'construction transforms TBA to DTBA; R = DRA to DBA.') + data_row2 = ne('Column ') + bold('C.') + \ + ne(' tells whether the output automaton is complete: rejecting ' + 'sink states are always omitted (add 1 state when C=0 if you ' + 'want the size of the complete automaton).') + row3 = [MultiColumn(14)] + row4 = ['', '', '', '', 'DRA', + MultiColumn(4, align='|c', data='DTGBA'), + MultiColumn(3, align='|c', data='DBA'), + MultiColumn(2, align='|c', + data=ne('DBA\\footnotesize minimizer'))] + row5 = ['formula', 'm', 'type', 'C.', 'st.', 'st.', 'tr.', + 'acc.', 'time', 'st.', 'tr.', 'time', 'st.', 'time'] + + # Datas that depends on the configuration file + len_l = len(config.l) + for i in range(0, len_l): + row3.append(MultiColumn(7, align='|c', data=config.l[i].name)) + row4.append(MultiColumn(3, align='|c', data='minDBA')) + row4.append(MultiColumn(4, align='|c', data='minDTGBA')) + row5.extend(['st.', 'tr.', 'time', 'st.', 'tr.', 'acc.', 'time']) + + # Add the first 5 lines of the document. + n = 14 + len_l * 7 + table.add_row((MultiColumn(n, align='c', data=data_row1),)) + table.add_row((MultiColumn(n, align='c', data=data_row2),)) + table.add_row((MultiColumn(n, align='l', data=''),)) # add empty line + table.add_row(tuple(row3)) + table.add_row(tuple(row4)) + table.add_row(tuple(row5)) + table.add_hline() + + +def write_results(table, config): + """ + Function that writes all the bench's result. + """ + # Write header (first 5 lines) + write_header(table, config) + + # Write all results + lines, best_dba_l, best_dtgba_l = get_lines(config) + for line in lines: + table.add_row(tuple(line)) +# --------------------------------------------------------------RESULTS + + +def add_fmt(nfields, doc): + """ + Function used to define the table's format depending on config.bench + file. + """ + if doc: + tmp = '|lrcr|r|rrrr|rrr|rr|' + for i in range(0, nfields): + tmp += 'rrr|rrrr|' + return tmp + else: + tmp = '|c|c|' + for i in range(0, nfields): + tmp += 'c|' + return tmp + + +def generate_docs(config): + """ + Function used to generate two pdf: + + -results.pdf: which shows all statistics about each formula with each + benchmarked method. + + -resume.pdf: which count the number of times that each method is better + than another. + """ + # Let's create the documents (result & resume) + doc = Document(documentclass='standalone') + doc.packages.append(Package('amsmath')) + doc.packages.append(Package('color')) + doc.packages.append(Package('colortbl')) + doc2 = Document(documentclass='standalone') + + # Declare colors in result document + doc.append(DefineColor( + arguments=Arguments('Gray', 'rgb', '0.7, 0.7, 0.7'))) + doc.append(DefineColor(arguments=Arguments('Green', 'rgb', '0.4, 1, 0.4'))) + doc.append(DefineColor(arguments=Arguments('Red', 'rgb', '0.8, 0, 0'))) + doc.append(DefineColor(arguments=Arguments('Yelw', 'rgb', '1, 0.98, 0.4'))) + doc.append(DefineColor(arguments=Arguments('Purpl', 'rgb', '1, 0.6, 1'))) + + # Create Table with format : True is result format, False is resume format + table = Tabular(add_fmt(len(config.l), True)) + table2 = Tabular(add_fmt(len(config.l), False)) + + # Write everything + write_results(table, config) + write_resume(table2, config) + + # Output PDF + doc.append(table) + doc2.append(table2) + doc.generate_pdf('results') + doc2.generate_pdf('resume') + + +def generate_bench(config, args): + """ + A function used to generate a complete benchmark. It outputs a shell + script. + """ + echo = "" + with open('stat-gen.sh', 'w') as script: + # Header. + script.write('''#!/bin/sh + +ltlfilt=../../bin/ltlfilt +ltl2tgba=../../bin/ltl2tgba +dstar2tgba=../../bin/dstar2tgba +timeout='timeout -sKILL {}' +stats=--stats=\"%s, %e, %t, %a, %c, %d, %p, %r, %R\" +empty='-, -, -, -, -, -, -, -, -' +tomany='!, !, !, !, !, !, !, !, !' +dbamin=${} + +'''.format(str(args.timeout) + args.unit, '{DBA_MINIMIZER}')) + + script.write('''get_stats() +{ + type=$1 + shift + SPOT_SATLOG=$n.$type.satlog $timeout \"$@\" \"$stats\"> stdin.$$ 2>stderr.$$ + if grep -q 'INT_MAX' stderr.$$; then + # Too many SAT-clause? + echo \"tomany\" + else + tmp=`cat stdin.$$` + echo ${tmp:-$empty} + fi + rm -f stdin.$$ stderr.$$ +} + +get_dbamin_stats() +{ + tmp=`./rundbamin.pl $timeout $dbamin \"$@\"` + mye='-, -' + echo ${tmp:-$mye} +} + +n=$1 +f=$2 +type=$3 +accmax=$4 + +case $type in + *WDBA*) + exit 0 + ;; + *TCONG*|*trad*) # Not in WDBA + echo \"$f, $accmax, $type...\" 1>&2 + input=`get_stats TBA $ltl2tgba \"$f\" -D -x '!wdba-minimize,tba-det'` + echo \"$f, $accmax, $type, $input, DBA, ...\" 1>&2\n + dba=`get_stats BA $ltl2tgba \"$f\" -BD -x '!wdba-minimize,tba-det'` + +''') + + # Body. + echo = "$f, $accmax, $type, $input, DBA, $dba" + for i in range(0, len(config.l)): + script.write(" # " + config.l[i].name + "\n") + if config.sh[i]: + script.write(" " + config.sh[i] + "\n") + script.write(" echo \"" + echo + ", minDBA." + config.l[i].code + + "...\" 1>&2\n") + script.write(" mindba_" + config.l[i].code + "=`get_stats DBA." + + config.l[i].code + " $ltl2tgba \"$f\" -BD -x" + " '!wdba-minimize," + config.l[i].xoptions + "'`\n") + echo += ", minDBA." + config.l[i].code + ", $mindba_" \ + + config.l[i].code + script.write(" echo \"" + echo + ", minDTGBA." + config.l[i].code + + "...\" 1>&2\n") + script.write(" mindtgba_" + config.l[i].code + + "=`get_stats DTGBA." + config.l[i].code + + " $ltl2tgba \"$f\" -D -x '!wdba-minimize," + + config.l[i].xoptions + "'`\n\n") + echo += ", minDTGBA." + config.l[i].code + ", $mindtgba_" \ + + config.l[i].code + script.write(''' # Dbaminimizer + echo \"{}, dbaminimizer...\" 1>&2 + case $type in + *TCONG*) dbamin=\"n/a, n/a\" dra=\"n/a\";; + *trad*) + $ltlfilt --remove-wm -f \"$f\" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ + dbamin=`get_dbamin_stats dra.$$` + dra=`sed -n 's/States: \\(.*\\)/\\1/p' dra.$$` + rm dra.$$ + ;; + esac + ;; + *DRA*) + echo \"$f, $accmax, $type...\" 1>&2 + $ltlfilt --remove-wm -f \"$f\" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ + input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'` + echo \"$f, $accmax, $type, $input, DBA, ...\" 1>&2 + dba=`get_stats BA $dstar2tgba dra.$$ -BD -x '!wdba-minimize'` + +'''.format(echo)) + + echo = "$f, $accmax, $type, $input, DBA, $dba" + for i in range(0, len(config.l)): + script.write(" # " + config.l[i].name + "\n") + if config.sh[i]: + script.write(" " + config.sh[i] + "\n") + script.write(" echo \"" + echo + ", minDBA." + config.l[i].code + + "...\" 1>&2\n") + script.write(" mindba_" + config.l[i].code + "=`get_stats DBA." + + config.l[i].code + " $dstar2tgba dra.$$ -BD -x" + " '!wdba-minimize," + config.l[i].xoptions + "'`\n") + echo += ", minDBA." + config.l[i].code + ", $mindba_" \ + + config.l[i].code + script.write(" echo \"" + echo + ", minDTGBA." + config.l[i].code + + "...\" 1>&2\n") + script.write(" mindtgba_" + config.l[i].code + + "=`get_stats DTGBA." + config.l[i].code + + " $dstar2tgba dra.$$ -D -x '!wdba-minimize," + + config.l[i].xoptions + "'`\n\n") + echo += ", minDTGBA." + config.l[i].code + ", $mindtgba_" \ + + config.l[i].code + + script.write(''' # Dbaminimizer + echo \"{}, dbaminimizer...\" 1>&2 + dbamin=`get_dbamin_stats dra.$$` + dra=`sed -n 's/States: \\(.*\\)/\\1/p' dra.$$` + rm -f dra.$$ + ;; + *not*) + exit 0 + ;; + *) + echo \"SHOULD NOT HAPPEND\" + exit 2 + ;; +esac + +'''.format(echo)) + echo += ", dbaminimizer, $dbamin, DRA, $dra, $n" + script.write("echo \"{}\" 1>&2\n".format(echo)) + script.write("echo \"{}\"\n".format(echo)) + print("Now run chmod +x stat-gen.sh") + + +def parse_args(): + """ + Function that parse the command-line arguments and options. + """ + parser = argparse.ArgumentParser() + parser.add_argument('action', choices=['script', 'results']) + parser.add_argument('--timeout', type=int, help="Timeout (0-9)+") + parser.add_argument('--unit', type=str, help="Time unit (h|m|s)", + choices=['h', 'm', 's']) + args = parser.parse_args() + + config = BenchConfig('config.bench') + if args.action == 'script': + if not args.timeout: + parser.error('bench requires --timeout') + if not args.unit: + parser.error('bench requires --unit') + generate_bench(config, args) + elif args.action == 'results': + generate_docs(config) + + +if __name__ == '__main__': + parse_args() diff --git a/bench/dtgbasat/stat-gen.sh b/bench/dtgbasat/stat-gen.sh new file mode 100644 index 000000000..486db9ae7 --- /dev/null +++ b/bench/dtgbasat/stat-gen.sh @@ -0,0 +1,297 @@ +#!/bin/sh + +ltlfilt=../../bin/ltlfilt +ltl2tgba=../../bin/ltl2tgba +dstar2tgba=../../bin/dstar2tgba +timeout='timeout -sKILL 15m' +stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r, %R" +empty='-, -, -, -, -, -, -, -, -' +tomany='!, !, !, !, !, !, !, !, !' +dbamin=${DBA_MINIMIZER} + +get_stats() +{ + type=$1 + shift + SPOT_SATLOG=$n.$type.satlog $timeout "$@" "$stats"> stdin.$$ 2>stderr.$$ + if grep -q 'INT_MAX' stderr.$$; then + # Too many SAT-clause? + echo "tomany" + else + tmp=`cat stdin.$$` + echo ${tmp:-$empty} + fi + rm -f stdin.$$ stderr.$$ +} + +get_dbamin_stats() +{ + tmp=`./rundbamin.pl $timeout $dbamin "$@"` + mye='-, -' + echo ${tmp:-$mye} +} + +n=$1 +f=$2 +type=$3 +accmax=$4 + +case $type in + *WDBA*) + exit 0 + ;; + *TCONG*|*trad*) # Not in WDBA + echo "$f, $accmax, $type..." 1>&2 + input=`get_stats TBA $ltl2tgba "$f" -D -x '!wdba-minimize,tba-det'` + echo "$f, $accmax, $type, $input, DBA, ..." 1>&2 + + dba=`get_stats BA $ltl2tgba "$f" -BD -x '!wdba-minimize,tba-det'` + + # Glucose (As before) + export SPOT_SATSOLVER="glucose -verb=0 -model %I > %O" + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu..." 1>&2 + mindba_glu=`get_stats DBA.glu $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu..." 1>&2 + mindtgba_glu=`get_stats DTGBA.glu $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=4'` + + # PicoSAT (As before) + export SPOT_SATSOLVER="picosat %I > %O" + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic..." 1>&2 + mindba_pic=`get_stats DBA.pic $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic..." 1>&2 + mindtgba_pic=`get_stats DTGBA.pic $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=4'` + + # PicoLibrary + unset SPOT_SATSOLVER + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp..." 1>&2 + mindba_libp=`get_stats DBA.libp $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp..." 1>&2 + mindtgba_libp=`get_stats DTGBA.libp $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=4'` + + # Incr Naive + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1..." 1>&2 + mindba_incr1=`get_stats DBA.incr1 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=3,param=-1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1..." 1>&2 + mindtgba_incr1=`get_stats DTGBA.incr1 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=3,param=-1'` + + # Incr param=1 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1..." 1>&2 + mindba_incr2p1=`get_stats DBA.incr2p1 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=3,param=1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1..." 1>&2 + mindtgba_incr2p1=`get_stats DTGBA.incr2p1 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=3,param=1'` + + # Incr param=2 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2..." 1>&2 + mindba_incr2p2=`get_stats DBA.incr2p2 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=3,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2..." 1>&2 + mindtgba_incr2p2=`get_stats DTGBA.incr2p2 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=3,param=2'` + + # Incr param=4 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4..." 1>&2 + mindba_incr2p4=`get_stats DBA.incr2p4 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=3,param=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4..." 1>&2 + mindtgba_incr2p4=`get_stats DTGBA.incr2p4 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=3,param=4'` + + # Incr param=8 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8..." 1>&2 + mindba_incr2p8=`get_stats DBA.incr2p8 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=3,param=8'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8..." 1>&2 + mindtgba_incr2p8=`get_stats DTGBA.incr2p8 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=3,param=8'` + + # Assume param=1 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1..." 1>&2 + mindba_assp1=`get_stats DBA.assp1 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1..." 1>&2 + mindtgba_assp1=`get_stats DTGBA.assp1 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=1'` + + # Assume param=2 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2..." 1>&2 + mindba_assp2=`get_stats DBA.assp2 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2..." 1>&2 + mindtgba_assp2=`get_stats DTGBA.assp2 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=2'` + + # Assume param=3 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2..." 1>&2 + mindba_assp2=`get_stats DBA.assp2 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2..." 1>&2 + mindtgba_assp2=`get_stats DTGBA.assp2 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=2'` + + # Assume param=4 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4..." 1>&2 + mindba_assp4=`get_stats DBA.assp4 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4..." 1>&2 + mindtgba_assp4=`get_stats DTGBA.assp4 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=4'` + + # Assume param=5 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5..." 1>&2 + mindba_assp5=`get_stats DBA.assp5 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=5'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5..." 1>&2 + mindtgba_assp5=`get_stats DTGBA.assp5 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=5'` + + # Assume param=6 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6..." 1>&2 + mindba_assp6=`get_stats DBA.assp6 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=6'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6..." 1>&2 + mindtgba_assp6=`get_stats DTGBA.assp6 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=6'` + + # Assume param=7 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7..." 1>&2 + mindba_assp7=`get_stats DBA.assp7 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=7'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7..." 1>&2 + mindtgba_assp7=`get_stats DTGBA.assp7 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=7'` + + # Assume param=8 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8..." 1>&2 + mindba_assp8=`get_stats DBA.assp8 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize=2,param=8'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8..." 1>&2 + mindtgba_assp8=`get_stats DTGBA.assp8 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize=2,param=8'` + + # Dichotomy + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho..." 1>&2 + mindba_dicho=`get_stats DBA.dicho $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho..." 1>&2 + mindtgba_dicho=`get_stats DTGBA.dicho $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize'` + + # Dbaminimizer + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho, $mindtgba_dicho, dbaminimizer..." 1>&2 + case $type in + *TCONG*) dbamin="n/a, n/a" dra="n/a";; + *trad*) + $ltlfilt --remove-wm -f "$f" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ + dbamin=`get_dbamin_stats dra.$$` + dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$` + rm dra.$$ + ;; + esac + ;; + *DRA*) + echo "$f, $accmax, $type..." 1>&2 + $ltlfilt --remove-wm -f "$f" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$ + input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'` + echo "$f, $accmax, $type, $input, DBA, ..." 1>&2 + dba=`get_stats BA $dstar2tgba dra.$$ -BD -x '!wdba-minimize'` + + # Glucose (As before) + export SPOT_SATSOLVER="glucose -verb=0 -model %I > %O" + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu..." 1>&2 + mindba_glu=`get_stats DBA.glu $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu..." 1>&2 + mindtgba_glu=`get_stats DTGBA.glu $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=4'` + + # PicoSAT (As before) + export SPOT_SATSOLVER="picosat %I > %O" + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic..." 1>&2 + mindba_pic=`get_stats DBA.pic $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic..." 1>&2 + mindtgba_pic=`get_stats DTGBA.pic $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=4'` + + # PicoLibrary + unset SPOT_SATSOLVER + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp..." 1>&2 + mindba_libp=`get_stats DBA.libp $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp..." 1>&2 + mindtgba_libp=`get_stats DTGBA.libp $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=4'` + + # Incr Naive + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1..." 1>&2 + mindba_incr1=`get_stats DBA.incr1 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=3,param=-1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1..." 1>&2 + mindtgba_incr1=`get_stats DTGBA.incr1 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=3,param=-1'` + + # Incr param=1 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1..." 1>&2 + mindba_incr2p1=`get_stats DBA.incr2p1 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=3,param=1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1..." 1>&2 + mindtgba_incr2p1=`get_stats DTGBA.incr2p1 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=3,param=1'` + + # Incr param=2 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2..." 1>&2 + mindba_incr2p2=`get_stats DBA.incr2p2 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=3,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2..." 1>&2 + mindtgba_incr2p2=`get_stats DTGBA.incr2p2 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=3,param=2'` + + # Incr param=4 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4..." 1>&2 + mindba_incr2p4=`get_stats DBA.incr2p4 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=3,param=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4..." 1>&2 + mindtgba_incr2p4=`get_stats DTGBA.incr2p4 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=3,param=4'` + + # Incr param=8 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8..." 1>&2 + mindba_incr2p8=`get_stats DBA.incr2p8 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=3,param=8'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8..." 1>&2 + mindtgba_incr2p8=`get_stats DTGBA.incr2p8 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=3,param=8'` + + # Assume param=1 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1..." 1>&2 + mindba_assp1=`get_stats DBA.assp1 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=1'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1..." 1>&2 + mindtgba_assp1=`get_stats DTGBA.assp1 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=1'` + + # Assume param=2 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2..." 1>&2 + mindba_assp2=`get_stats DBA.assp2 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2..." 1>&2 + mindtgba_assp2=`get_stats DTGBA.assp2 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=2'` + + # Assume param=3 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2..." 1>&2 + mindba_assp2=`get_stats DBA.assp2 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=2'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2..." 1>&2 + mindtgba_assp2=`get_stats DTGBA.assp2 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=2'` + + # Assume param=4 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4..." 1>&2 + mindba_assp4=`get_stats DBA.assp4 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=4'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4..." 1>&2 + mindtgba_assp4=`get_stats DTGBA.assp4 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=4'` + + # Assume param=5 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5..." 1>&2 + mindba_assp5=`get_stats DBA.assp5 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=5'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5..." 1>&2 + mindtgba_assp5=`get_stats DTGBA.assp5 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=5'` + + # Assume param=6 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6..." 1>&2 + mindba_assp6=`get_stats DBA.assp6 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=6'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6..." 1>&2 + mindtgba_assp6=`get_stats DTGBA.assp6 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=6'` + + # Assume param=7 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7..." 1>&2 + mindba_assp7=`get_stats DBA.assp7 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=7'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7..." 1>&2 + mindtgba_assp7=`get_stats DTGBA.assp7 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=7'` + + # Assume param=8 + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8..." 1>&2 + mindba_assp8=`get_stats DBA.assp8 $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize=2,param=8'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8..." 1>&2 + mindtgba_assp8=`get_stats DTGBA.assp8 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize=2,param=8'` + + # Dichotomy + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho..." 1>&2 + mindba_dicho=`get_stats DBA.dicho $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize'` + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho..." 1>&2 + mindtgba_dicho=`get_stats DTGBA.dicho $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-minimize'` + + # Dbaminimizer + echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho, $mindtgba_dicho, dbaminimizer..." 1>&2 + dbamin=`get_dbamin_stats dra.$$` + dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$` + rm -f dra.$$ + ;; + *not*) + exit 0 + ;; + *) + echo "SHOULD NOT HAPPEND" + exit 2 + ;; +esac + +echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho, $mindtgba_dicho, dbaminimizer, $dbamin, DRA, $dra, $n" 1>&2 +echo "$f, $accmax, $type, $input, DBA, $dba, minDBA.glu, $mindba_glu, minDTGBA.glu, $mindtgba_glu, minDBA.pic, $mindba_pic, minDTGBA.pic, $mindtgba_pic, minDBA.libp, $mindba_libp, minDTGBA.libp, $mindtgba_libp, minDBA.incr1, $mindba_incr1, minDTGBA.incr1, $mindtgba_incr1, minDBA.incr2p1, $mindba_incr2p1, minDTGBA.incr2p1, $mindtgba_incr2p1, minDBA.incr2p2, $mindba_incr2p2, minDTGBA.incr2p2, $mindtgba_incr2p2, minDBA.incr2p4, $mindba_incr2p4, minDTGBA.incr2p4, $mindtgba_incr2p4, minDBA.incr2p8, $mindba_incr2p8, minDTGBA.incr2p8, $mindtgba_incr2p8, minDBA.assp1, $mindba_assp1, minDTGBA.assp1, $mindtgba_assp1, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp2, $mindba_assp2, minDTGBA.assp2, $mindtgba_assp2, minDBA.assp4, $mindba_assp4, minDTGBA.assp4, $mindtgba_assp4, minDBA.assp5, $mindba_assp5, minDTGBA.assp5, $mindtgba_assp5, minDBA.assp6, $mindba_assp6, minDTGBA.assp6, $mindtgba_assp6, minDBA.assp7, $mindba_assp7, minDTGBA.assp7, $mindtgba_assp7, minDBA.assp8, $mindba_assp8, minDTGBA.assp8, $mindtgba_assp8, minDBA.dicho, $mindba_dicho, minDTGBA.dicho, $mindtgba_dicho, dbaminimizer, $dbamin, DRA, $dra, $n" diff --git a/bench/dtgbasat/stats.sh b/bench/dtgbasat/stats.sh index 4e12bc3b6..b38ba267a 100755 --- a/bench/dtgbasat/stats.sh +++ b/bench/dtgbasat/stats.sh @@ -17,15 +17,15 @@ while IFS=, read f type accmax accmin; do case $type in *TCONG*) - echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp + echo "$n.log:; ./stat-gen.sh $n '$f' $type $accmax >\$@" >> stats.tmp all="$all $n.log" n=`expr $n + 1` - echo "$n.log:; ./stat.sh $n '$f' DRA-CONG $accmax >\$@" >> stats.tmp + echo "$n.log:; ./stat-gen.sh $n '$f' DRA-CONG $accmax >\$@" >> stats.tmp all="$all $n.log" n=`expr $n + 1` ;; *) - echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp + echo "$n.log:; ./stat-gen.sh $n '$f' $type $accmax >\$@" >> stats.tmp all="$all $n.log" n=`expr $n + 1` ;;