<jupyter_start><jupyter_text>If `rerun` is set to `False` the script uses the precomputed values. If set to `True`, all values are recomputed(takes more time)<jupyter_code>rerun = True<jupyter_output><empty_output><jupyter_text>Check if Buechic and Fribourg are installed.<jupyter_code>buechic = False

fribourg = False

# Refresh vars from store.

%store -r
### Tools' setting ###
tools = get_tools(automata=True, use_buechic=buechic, use_fribourg=fribourg)
tool_order = get_tool_order(use_buechic=buechic, use_fribourg=fribourg)


### Numbers to measure ###
cols = ['states','edges','transitions','nondet_states','exit_status','time','acc']
runners = {}
for origin in ['random']:
    for t in ['ba']:
        name = '{}_{}'.format(origin, t)
        runners[name] = \
            LtlcrossRunner(tools,\
                    res_filename='data/{}.csv'.format(name),\
                    formula_files=['automata/{}.ltl'.format(name)],\
                    cols=cols)
for name in runners.keys():
    print('{}: Working on {}'.format(datetime.now().strftime('[%d.%m.%Y %T]'),name))
    if rerun:
        runners[name].run_ltlcross(timeout='120')
    runners[name].parse_results()
def get_counts(r):
    v = r.values.states.copy()
    return v.dropna().count()[0]<jupyter_output><empty_output><jupyter_text>Cummulative results Gather the data into one big DataFrame<jupyter_code>data = pd.DataFrame()
for (name,r) in runners.items():
    row = pd.DataFrame(r.cummulative(),columns=[name]).transpose()
    data = data.append(row)
data<jupyter_output><empty_output><jupyter_text>Get the number of formulas such that all tools finished within timeout for each category.<jupyter_code>counts = pd.DataFrame(index=pd.Index([],name='source'),columns=['.n'])
for (name,r) in runners.items():
    c = get_counts(r)
    counts = counts.append(pd.DataFrame({'.n':c},index=[name]))
counts<jupyter_output><empty_output><jupyter_text>Converts the DataFrame to use MultiIndices for rows and columns<jupyter_code>from pandas.api.types import CategoricalDtype
automata_type = CategoricalDtype(categories=['ba'], ordered=True)
source_type = CategoricalDtype(categories=['random'], ordered=True)
def make_hierarchical(data):
    # Split index into origin & ltl2tgba's output type
    df = data.copy()
    df.index.name = 'origin'
    df.reset_index(inplace=True)
    df['type'] = df.origin.apply(lambda x: x.split('_')[1]).astype(automata_type)
    df['origin'] = df.origin.apply(lambda x: x.split('_')[0]).astype(source_type)
    df = df.set_index(['origin','type']).sort_index()
    # Split columns in tool & reductions
    df.columns = pd.MultiIndex.from_tuples([tuple(c.split('.')) for c in df.columns])
    return df
tmp = make_hierarchical(data.join(counts)).sort_index(axis=1)
tmp
ordered = tmp[['']+tool_order]
ordered
!mkdir figures
with open("figures/aut_table.fig", "w") as f:
    fixed_names = ordered.copy()
    fixed_names.columns.set_levels([[tool_names.get(item, item) for item in names] if i==0 else names
                                    for i, names in enumerate(fixed_names.columns.levels)], inplace=True)
    
    fixed = fixed_names.apply(pd.to_numeric, downcast="integer")
    
    fixed.to_latex(buf=f, escape=False, sparsify=True)
for name, r in runners.items():
    sc_plot(r, 'spot_ncsb.yes', 'pbs.yes', filename=f"figures/{name}_ncsb_pbs.fig", log="both")
    sc_plot(r, 'tgba_via_det.yes', 'pbs.yes', filename=f"figures/{name}_spot_pbs.fig", log="both")
    sc_plot(r, 'buechic.yes', 'pbs.yes', filename=f"figures/{name}_buechic_pbs.fig", log="both")
    sc_plot(r, 'fribourg.yes', 'pbs.yes', filename=f"figures/{name}_fribourg_pbs.fig", log="both")<jupyter_output><empty_output><jupyter_text>Timeouts<jupyter_code>TO_data = pd.DataFrame()
for (name,r) in runners.items():
    TO_data = TO_data.append(pd.DataFrame(r.get_error_count(err_type='timeout'),columns=[name]).transpose(),sort=True)
if not TO_data.empty:
    TO = make_hierarchical(TO_data).replace(0,pd.NaT).dropna(how='all').fillna(0)
else:
    TO = TO_data
TO<jupyter_output><empty_output><jupyter_text>Final resultsWe use the `display` function to propagate the results to notebooks that just run this one.<jupyter_code>display_markdown('''### Comparison of tools producing complements of given automata
Automata has been produced from formulae from literature and randomly generated.
There has been several timeouts.
''',raw=True)
display(ordered)
display_markdown('''### Timeouts
''',raw=True)
display(TO)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.15388026607538802, 'fraction_numerical': 0.0024390243902439024, 'mean_word_length': 5.170998632010944, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '7', 'dir': 'jupyter-structured-clean-dedup', 'id': '86123', 'license': 'MIT', 'n_tokens_mistral': 1615, 'n_tokens_neox': 1574, 'n_words': 309, 'path': 'experiments/Comparison_automata.ipynb', 'repo_name': 'mklokocka/pbs', 'size': '4510'}