In [313]:
from ltlcross_runner import LtlcrossRunner
from IPython.display import display
import pandas as pd
import spot
import sys
import re
import tempfile
spot.setup(show_default='.a')
pd.options.display.float_format = '{: .0f}'.format
pd.options.display.latex.multicolumn_format = 'c'
from tables_utils import split_cols, high_min, high_max, highlight_by_level
from tables_utils import fix_latex, fix_type, fix_tool
from tables_utils import cummulative_to_latex
With rerun = True, all experiments are executed again (takes several hours). With False, the data are taken from the *.csv files:
In [350]:
rerun = False
nd_rerun = False
det_rerun = False
In [315]:
import os
os.environ['SPOT_HOA_TOLERANT']='TRUE'
In [316]:
%%bash
ltl3ba -v
ltl3tela -v
ltl2tgba --version | head -n1
delag -v
ltl2dgra -v
The generate function may be used to generate random formulae. Uncomment the function call below to generate different set of formulae.
In [317]:
def generate(n=1000,func=(lambda x: True),filename=None,priorities='',ap=['a','b','c','d','e']):
if filename is None:
file_h = sys.stdout
else:
file_h = open(filename,'w')
f = spot.randltl(ap,
ltl_priorities=priorities,
simplify=3,tree_size=15).relabel_bse(spot.Abc)
i = 0
printed = set()
while(i < n):
form = next(f)
if form in printed:
continue
if func(form) and not form.is_tt() and not form.is_ff():
print(form,file=file_h)
printed.add(form)
i += 1
In [318]:
datasets = [ {
'name': 'rand1',
'form': 'formulae/ictac19/rand1.ltl',
'csv' : 'formulae/ictac19/rand1.csv',
'fgmopt.nonalt.csv': 'formulae/ictac19/rand1.fgmopt.nonalt.csv',
'fgmopt.det.csv': 'formulae/ictac19/rand1.fgmopt.det.csv',
}, {
'name': 'rand2',
'form': 'formulae/ictac19/rand2.ltl',
'csv' : 'formulae/ictac19/rand2.csv',
'fgmopt.nonalt.csv': 'formulae/ictac19/rand2.fgmopt.nonalt.csv',
'fgmopt.det.csv': 'formulae/ictac19/rand2.fgmopt.det.csv',
}, {
'name': 'rand4',
'form': 'formulae/ictac19/rand4.ltl',
'csv' : 'formulae/ictac19/rand4.csv',
'fgmopt.nonalt.csv': 'formulae/ictac19/rand4.fgmopt.nonalt.csv',
'fgmopt.det.csv': 'formulae/ictac19/rand4.fgmopt.det.csv',
}, {
'name': 'randfg',
'form': 'formulae/ictac19/randfg.ltl',
'csv' : 'formulae/ictac19/randfg.csv',
'fgmopt.nonalt.csv': 'formulae/ictac19/randfg.fgmopt.nonalt.csv',
'fgmopt.det.csv': 'formulae/ictac19/randfg.fgmopt.det.csv',
}, {
'name': 'literature',
'form': 'formulae/ictac19/literature.ltl',
'csv' : 'formulae/ictac19/literature.csv',
'fgmopt.nonalt.csv': 'formulae/ictac19/lit.fgmopt.nonalt.csv',
'fgmopt.det.csv': 'formulae/ictac19/lit.fgmopt.det.csv',
} ]
In [319]:
tools = {
"ltl3ba": "ltldo 'ltl3ba -H1' -f %f > %O",
"basic": "ltl3tela -p1 -c0 -d1 -F0 -G0 -i1 -X1 -f %f > %O",
"fmerg": "ltl3tela -p1 -c0 -d1 -G0 -i1 -X1 -f %f > %O",
"fgmerg": "ltl3tela -p1 -d1 -i1 -X1 -c0 -f %f > %O",
"fgmerg_opt": "ltl3tela -p1 -i1 -X1 -f %f > %O"
}
order = ["ltl3ba", "basic", "fmerg", "fgmerg", "fgmerg_opt"]
cols = ["states", "edges", "acc"]
cols_ = cols + ["nonalt", "det"] # we will count these fields later
In [320]:
nd_tools = {
"ltl3ba": "ltldo 'ltl3ba -H2' -f %f > %O",
"ltl3tela_alt": "ltl3tela -p1 -i1 -X1 -f %f | autfilt --high --simplify-acceptance > %O",
"ltl3tela": "ltl3tela -i1 -X1 -f %f > %O",
"ltl2tgba": "ltl2tgba -G %f > %O"
}
nd_order = ["ltl3tela_alt", "ltl3tela", "ltl2tgba", "ltl3ba"]
In [321]:
det_tools = {
"ltl3tela_alt": "ltl3tela -p1 -i1 -X1 -f %f | autfilt --high --simplify-acceptance > %O",
"ltl3tela_d": "ltl3tela -i1 -X1 -D1 -f %f > %O",
"ltl2tgba_d": "ltl2tgba -DG %f > %O",
"delag": "delag -i %f > %O",
"rabinizer4": "ltl2dgra -i %f > %O"
}
det_order = ["ltl3tela_alt", "ltl3tela_d", "ltl2tgba_d", "delag", "rabinizer4"]
In [322]:
for d in datasets:
d['data'] = LtlcrossRunner(tools, formula_files = [d['form']], res_filename = d['csv'], cols = cols)
if rerun:
d['data'].run_ltlcross(automata = True, timeout = '60')
d['data'].parse_results()
For all datasets, let us count the number of existential (i.e. automata without universal branching) and deterministic automata produced by the translation to alternating automaton.
In [323]:
for d in datasets:
for tool in tools:
d['data'].values[('nonalt', tool)] = list(map(lambda aut : \
1 if type(aut) == str and spot.automaton(aut + '\n').is_existential() else 0, d['data'].automata[tool]))
for tool in tools:
d['data'].values[('det', tool)] = list(map(lambda aut: \
1 if type(aut) == str and spot.automaton(aut + '\n').is_deterministic() else 0, d['data'].automata[tool]))
In [324]:
for d in datasets:
if d['name'] == 'literature':
# we filter formulae to those where FG-merging+opt helped compared to LTL3BA
litdf = d['data'].values
d['data'].values = litdf[litdf[('states', 'fgmerg_opt')] < litdf[('states', 'basic')]]
print("Number of mergeable formulae from literature: {}".format(len(d['data'].values)))
d['dc'] = d['data'].cummulative(col = cols_).unstack(level = 0).loc[order, cols_]
In [325]:
m = datasets[0]['dc'].copy()
m.columns = m.columns.map(lambda c : c + '.' + datasets[0]['name'])
for i in range(1, len(datasets)):
ds = datasets[i]['dc'].copy()
ds.columns = ds.columns.map(lambda c : c + '.' + datasets[i]['name'])
m = pd.merge(m, ds, on = 'tool')
In [326]:
t1 = split_cols(m, '.').loc[order, ['states', 'acc']].sort_index(1, ascending = [False, True])
In [327]:
t2 = split_cols(m, '.').loc[order, ['det', 'nonalt']].sort_index(1)
In [328]:
t1
Out[328]:
In [329]:
t2
Out[329]:
In [330]:
print(t1.to_latex())
In [331]:
print(t2.to_latex())
In [365]:
def fix_tools(tool):
return tool.replace('fgmerg_opt', '$\\FG$-merging+simpl.').replace('FG-','$\\FG$-').replace('F-','$\\F$-')
In [366]:
def sc_plot(r,t1,t2,filename=None,include_equal = True,col='states',log=None,size=(5.5,5),kw=None,clip=None, add_count=True):
merged = isinstance(r,list)
if merged:
vals = pd.concat([run.values[col] for run in r])
vals.index = vals.index.droplevel(0)
vals = vals.groupby(vals.index).first()
else:
vals = r.values[col]
to_plot = vals.loc(axis=1)[[t1,t2]] if include_equal else\
vals[vals[t1] != vals[t2]].loc(axis=1)[[t1,t2]]
to_plot['count'] = 1
to_plot.dropna(inplace=True)
to_plot = to_plot.groupby([t1,t2]).count().reset_index()
if filename is not None:
print(scatter_plot(to_plot, log=log, size=size,kw=kw,clip=clip, add_count=add_count),file=open(filename,'w'))
else:
return scatter_plot(to_plot, log=log, size=size,kw=kw,clip=clip, add_count=add_count)
In [367]:
def scatter_plot(df, short_toolnames=True, log=None, size=(5.5,5),kw=None,clip=None,add_count = True):
t1, t2, _ = df.columns.values
if short_toolnames:
t1 = fix_tools(t1.split('/')[0])
t2 = fix_tools(t2.split('/')[0])
vals = ['({},{}) [{}]\n'.format(v1,v2,c) for v1,v2,c in df.values]
plots = '''\\addplot[
scatter, scatter src=explicit,
only marks, fill opacity=0.5,
draw opacity=0] coordinates
{{{}}};'''.format(' '.join(vals))
start_line = 0 if log is None else 1
line = '\\addplot[darkgreen,domain={}:{}]{{x}};'.format(start_line, min(df.max(axis=0)[:2])+1)
axis = 'axis'
mins = 'xmin=0,ymin=0,'
clip_str = ''
if clip is not None:
clip_str = '\\draw[red,thick] ({},{}) rectangle ({},{});'.format(*clip)
if log:
if log == 'both':
axis = 'loglogaxis'
mins = 'xmin=1,ymin=1,'
else:
axis = 'semilog{}axis'.format(log)
mins = mins + '{}min=1,'.format(log)
args = ''
if kw is not None:
if 'title' in kw and add_count:
kw['title'] = '{{{} ({})}}'.format(kw['title'],df['count'].sum())
args = ['{}={},\n'.format(k,v) for k,v in kw.items()]
args = ''.join(args)
res = '''%\\begin{{tikzpicture}}
\\pgfplotsset{{every axis legend/.append style={{
cells={{anchor=west}},
draw=none,
}}}}
\\pgfplotsset{{colorbar/width=.3cm}}
\\pgfplotsset{{title style={{align=center,
font=\\small}}}}
\\pgfplotsset{{compat=1.14}}
\\begin{{{0}}}[
{1}
colorbar,
colormap={{example}}{{
color(0)=(blue)
color(500)=(green)
color(1000)=(red)
}},
%thick,
axis x line* = bottom,
axis y line* = left,
width={2}cm, height={3}cm,
xlabel={{{4}}},
ylabel={{{5}}},
cycle list={{%
{{darkgreen, solid}},
{{blue, densely dashed}},
{{red, dashdotdotted}},
{{brown, densely dotted}},
{{black, loosely dashdotted}}
}},
{6}%
]
{7}%
{8}%
{9}%
\\end{{{0}}}
%\\end{{tikzpicture}}
'''.format(axis,mins,
size[0],size[1],t1,t2,
args,plots,line,
clip_str)
return res
In [368]:
fgm = 'fgmerg_opt'
basic = 'basic'
size = (4,4)
clip_names = ('xmin','ymin','xmax','ymax')
kw = {}
sc_plot(datasets[4]['data'],basic,fgm,'sc_lit.tex',size=size,kw=kw.copy())
size = (5.4,5.6)
kw['title'] = 'literature'
sc_plot(datasets[4]['data'],basic,fgm,'sc_lit.tex',size=size,kw=kw.copy())
i = 0
for suff in ['1','2','4','fg']:
kw['title'] = 'rand'+suff
sc_plot(datasets[i]['data'],basic,fgm,'sc_rand{}.tex'.format(suff),size=size,kw=kw.copy())
i += 1
In [355]:
#d = datasets[0]['data'].values
#x = d[d[('nonalt', 'fgmerg_opt')] == 1]
for ds in datasets:
d = ds['data'].values
with tempfile.NamedTemporaryFile('w+', delete = False) as fd:
for (_, formula), _ in d[d[('nonalt', 'fgmerg_opt')] == 1].iterrows():
fd.write("{}\n".format(formula))
ds['fgmopt.nonalt.form'] = fd.name
#print(fd.name)
with tempfile.NamedTemporaryFile('w+', delete = False) as fd:
for (_, formula), _ in d[d[('det', 'fgmerg_opt')] == 1].iterrows():
fd.write("{}\n".format(formula))
ds['fgmopt.det.form'] = fd.name
#print(fd.name)
In [337]:
for d in datasets:
d['fgmopt.nonalt.data'] = LtlcrossRunner(nd_tools, formula_files = [d['fgmopt.nonalt.form']], res_filename = d['fgmopt.nonalt.csv'], cols = cols)
if nd_rerun:
d['fgmopt.nonalt.data'].run_ltlcross(automata = True, timeout = '60')
d['fgmopt.nonalt.data'].parse_results()
In [338]:
for d in datasets:
d['fgmopt.nonalt.dc'] = d['fgmopt.nonalt.data'].cummulative(col = cols).unstack(level = 0).loc[nd_order, cols]
In [339]:
nd_m = datasets[0]['fgmopt.nonalt.dc'].copy()
nd_m.columns = nd_m.columns.map(lambda c : c + '.' + datasets[0]['name'])
for i in range(1, len(datasets)):
ds = datasets[i]['fgmopt.nonalt.dc'].copy()
ds.columns = ds.columns.map(lambda c : c + '.' + datasets[i]['name'])
nd_m = pd.merge(nd_m, ds, on = 'tool')
In [340]:
nd_t = split_cols(nd_m, '.').loc[nd_order, ['states', 'acc']].sort_index(1, ascending = [False, True])
In [341]:
nd_t
Out[341]:
In [342]:
for d in datasets:
d['fgmopt.det.data'] = LtlcrossRunner(det_tools, formula_files = [d['fgmopt.det.form']], res_filename = d['fgmopt.det.csv'], cols = cols)
if det_rerun:
d['fgmopt.det.data'].run_ltlcross(automata = True, timeout = '60')
d['fgmopt.det.data'].parse_results()
In [343]:
for d in datasets:
d['fgmopt.det.dc'] = d['fgmopt.det.data'].cummulative(col = cols).unstack(level = 0).loc[det_order, cols]
In [344]:
det_m = datasets[0]['fgmopt.det.dc'].copy()
det_m.columns = det_m.columns.map(lambda c : c + '.' + datasets[0]['name'])
for i in range(1, len(datasets)):
ds = datasets[i]['fgmopt.det.dc'].copy()
ds.columns = ds.columns.map(lambda c : c + '.' + datasets[i]['name'])
det_m = pd.merge(det_m, ds, on = 'tool')
In [345]:
det_t = split_cols(det_m, '.').loc[det_order, ['states', 'acc']].sort_index(1, ascending = [False, True])
In [346]:
det_t
Out[346]:
In [348]:
print(nd_t.to_latex())
In [349]:
print(det_t.to_latex())
In [ ]: