In [1]:
from ltlcross_runner import LtlcrossRunner
from IPython.display import display
import pandas as pd
import spot
import sys
spot.setup(show_default='.a')
pd.options.display.float_format = '{: .0f}'.format
pd.options.display.latex.multicolumn_format = 'c'
In [16]:
%%bash
ltl3ba -v
ltl3tela -v
ltl2tgba --version
ltl2dgra -v
delag -v
In [17]:
# If there are already files with results, and rerun is False, ltlcross is not run again.
rerun = True
In [18]:
fg_priorities = [1,2,4]
We compare the $\F$- and $\FG$-merging translation to the basic one. We compare the sizes of SLAA (alternating). We use a wrapper script ltlcross_runner for ltlcross that uses the pandas library to manipulate data. It requires some settings.
In [19]:
resfiles = {}
runners = {}
In [41]:
### Tools' setting ###
# a dict of a form (name : ltlcross cmd)
ltl3tela_shared = "ltl3tela -p2 -n0 -b0 -f %f "
#end = " | awk '!p;/^--END--/{p=1}' > %O"
end = " > %O"
tools = {"FG-merging" : ltl3tela_shared + end,
"ltl3tela" : ltl3tela_shared + "-n1 -b1" + end,
"FG-merging+compl" : ltl3tela_shared + "-n1" + end,
"F-merging" : ltl3tela_shared + "-G0" + end,
#"G-merging" : ltl3tela_shared + "-F0" + end,
"basic" : ltl3tela_shared + "-F0 -G0" + end,
"LTL3BA" : "ltl3ba -H2 -f %s" + end,
"Spot" : "ltl2tgba -f %f > %O",
"Delag" : "delag -I %F -O %O",
"Rabinizer4" : "ltl2dgra -I %F -O %O"
}
### Order in which we want to sort the translations
MI_order = ["LTL3BA","Spot",
"basic","F-merging","FG-merging",
"FG-merging+compl","ltl3tela",
"Delag","Rabinizer4"]
### Files with measured statistics ###
resfiles['lit'] = 'MI_na-lit.csv'
resfiles['randfg'] = 'MI_na-randfg.csv'
for i in fg_priorities:
resfiles['rand{}'.format(i)] = 'MI_na-rand{}.csv'.format(i)
### Measures to be measured
cols = ["states","transitions","nondet_states","nondet_aut","acc"]
In [42]:
for name,rfile in resfiles.items():
runners[name] = LtlcrossRunner(tools,res_filename=rfile,
formula_files=['formulae/{}.ltl'.format(name)],
cols=cols)
In [43]:
for r in runners.values():
if rerun:
r.run_ltlcross()
r.parse_results()
In [67]:
t1 = {}
for name,r in runners.items():
tmp = r.cummulative(col=cols).unstack(level=0).loc[MI_order,cols]
t1_part = tmp.loc[:,['states','acc']]
t1_part["det. aut."] = len(r.values)-tmp.nondet_aut
t1[name] = t1_part
In [68]:
t1_merged = pd.concat(t1.values(),axis=1,keys=t1.keys()).loc[MI_order,:]
t1_merged
Out[68]:
In [69]:
row_map={"basic" : 'basic translation',
"F-merging" : '$\F$-merging',
"G-merging" : '$\G$-merging',
"FG-merging" : '$\FG$-merging',
"FG-merging+compl" : "$\FG$-merging+compl."}
t1_merged.rename(row_map,inplace=True);
t1 = t1_merged.rename_axis(['',"translation"],axis=1)
t1.index.name = None
t1
Out[69]:
In [72]:
rand = t1.copy()
In [73]:
rand.columns = rand.columns.swaplevel()
rand.sort_index(axis=1,level=1,inplace=True,sort_remaining=False,ascending=True)
idx = pd.IndexSlice
corder = ['states','acc']
parts = [rand.loc[:,idx[[c]]] for c in corder]
rand = pd.concat(parts,names=corder,axis=1)
rand
Out[73]:
In [74]:
print(rand.to_latex(escape=False,bold_rows=False),file=open('fossacs_t2.tex','w'))
In [75]:
cp fossacs_t2.tex /home/xblahoud/research/ltl3tela_papers/
In [76]:
def fix_tools(tool):
return tool.replace('FG-','$\\FG$-').replace('F-','$\\F$-')
In [77]:
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 [80]:
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,
%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 [91]:
ltl3ba = 'LTL3BA'
fgm = 'FG-merging'
fm = 'F-merging'
basic = 'basic'
ltl3tela = 'FG-merging+compl'
size = (4,4)
clip_names = ('xmin','ymin','xmax','ymax')
kw = {}
size = (5,4.5)
kw['title'] = 'literature'
for name,fs in [('Delag','delag'),('Spot','spot')]:
sc_plot(runners['lit'],name,ltl3tela,'sc_lit-na-{}.tex'.format(fs),size=size,kw=kw.copy())
for suff in ['1','2','4','fg']:
kw['title'] = 'rand'+suff
sc_plot(runners['rand'+suff],name,ltl3tela,'sc_rand{}-na-{}.tex'.format(suff,fs),size=size,kw=kw.copy())
In [92]:
cp sc*-na*.tex /home/xblahoud/research/ltl3tela_papers/
In [ ]: