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'
Hack that alows to parse ltl3ba automata without universal branching.
In [2]:
import os
os.environ['SPOT_HOA_TOLERANT']='TRUE'
In [3]:
%%bash
ltl3ba -v
ltl3tela -v
ltl2tgba --version
In [4]:
# If there are already files with results, and rerun is False, ltlcross is not run again.
rerun = False
In [5]:
def is_mergable(f, level=3):
'''Runs ltl3tela with the -m argument to detect
whether the given formula `f` is mergable.
level 1: F-mergeable
level 2: G-mergeable
level 3: F,G-mergeable
'''
if level == 3:
return is_mergable(f,2) or is_mergable(f,1)
res = !ltl3tela -m{level} -f "{f}"
return res[0] == '1'
In [6]:
is_mergable('FGa',2)
Out[6]:
In [7]:
tmp_file = 'formulae/tmp.ltl'
lit_pref = 'formulae/literature'
lit_file = lit_pref + '.ltl'
lit_merg_file = 'formulae/lit.ltl'
In [8]:
# The well-known set of formulae from literature
!genltl --dac-patterns --eh-patterns --sb-patterns --beem-patterns --hkrss-patterns > $tmp_file
In [9]:
# We add also negation of all the formulae.
# We remove all M and W operators as LTL3BA does not understand them.
# The `relabel-bool` option renames `G(a | b)` into `G a`.
!ltlfilt --negate $tmp_file | \
ltlfilt $tmp_file -F - --unique -r3 --remove-wm --relabel-bool=abc | \
ltlfilt -v --equivalent-to=0 | ltlfilt -v --equivalent-to=1> $lit_file
In [10]:
lit_f_mergable = [is_mergable(l,1) for l in open(lit_file)]
lit_mergable = [is_mergable(l,3) for l in open(lit_file)]
In [11]:
counts = '''Out of {} formulae known from literature, there are:
{} with F-merging,
{} with F,G-merging, and
{} with no merging possibility
'''
print(counts.format(
len(lit_mergable),
lit_f_mergable.count(True),
lit_mergable.count(True),
lit_mergable.count(False)))
In [12]:
with open(lit_merg_file,'w') as out:
for l in open(lit_file):
if is_mergable(l):
out.write(l)
In [13]:
def generate(n=100,func=(lambda x: True),filename=None,priorities='M=0,W=0,xor=0',ap=['a','b','c','d','e']):
if filename is not None:
if filename is sys.stdout:
file_h = filename
else:
file_h = open(filename,'w')
f = spot.randltl(ap,
ltl_priorities=priorities,
simplify=3,tree_size=15).relabel_bse(spot.Abc)\
.unabbreviate('WM')
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():
if filename is not None:
print(form,file=file_h)
printed.add(form)
i += 1
return list(printed)
In [14]:
def measure_rand(n=1000,priorities='M=0,W=0,xor=0',ap=['a','b','c','d','e']):
rand = generate(n,priorities=priorities,ap=ap)
rand_mergable = [is_mergable(l,3) for l in rand]
rand_f_mergable = [is_mergable(l,1) for l in rand]
counts = '''Out of {} random formulae, there are:
{} with F-merging,
{} with F,G-merging, and
{} with no merging possibility
'''
print(counts.format(
len(rand_mergable),
rand_f_mergable.count(True),
rand_mergable.count(True),
rand_mergable.count(False)))
return rand, rand_f_mergable, rand_mergable
In [15]:
def get_priorities(n):
'''Returns the `priority string` for ltlcross
where `n` is the priority of both F and G. The
operators W,M,xor have priority 0 and the rest
has the priority 1.
'''
return 'M=0,W=0,xor=0,G={0},F={0}'.format(n)
In [16]:
measure_rand();
In [17]:
measure_rand(priorities=get_priorities(2));
In [18]:
rand4 = measure_rand(priorities=get_priorities(4))
In [19]:
randfg = measure_rand(priorities='xor=0,implies=0,equiv=0,X=0,W=0,M=0,R=0,U=0,F=2,G=2')
In [20]:
fg_priorities = [1,2,4]
!mkdir -p formulae
#generate(total_r,filename=fg_f,priorities='xor=0,implies=0,equiv=0,X=0,W=0,M=0,R=0,U=0,F=3,G=3');
In [21]:
for i in fg_priorities:
generate(1000,func=lambda x:is_mergable(x,3),
filename='formulae/rand{}.ltl'.format(i),
priorities=get_priorities(i))
In [22]:
generate(1000,func=lambda x:is_mergable(x,3),
filename='formulae/randfg.ltl'.format(i),
priorities='xor=0,implies=0,equiv=0,X=0,W=0,M=0,R=0,U=0,F=2,G=2');
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 [23]:
resfiles = {}
runners = {}
In [24]:
### Tools' setting ###
# a dict of a form (name : ltlcross cmd)
ltl3tela_shared = "ltl3tela -p1 -t0 -n0 -a3 -f %f "
#end = " | awk '!p;/^--END--/{p=1}' > %O"
end = " > %O"
tools = {"FG-merging" : ltl3tela_shared + 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 -H1 -f %s" + end,
}
### Order in which we want to sort the translations
MI_order = ["LTL3BA",
"basic","F-merging","FG-merging"]
### Files with measured statistics ###
resfiles['lit'] = 'MI_alt-lit.csv'
resfiles['randfg'] = 'MI_alt-randfg.csv'
for i in fg_priorities:
resfiles['rand{}'.format(i)] = 'MI_alt-rand{}.csv'.format(i)
### Measures to be measured
cols = ["states","transitions","nondet_states","nondet_aut","acc"]
In [25]:
for name,rfile in resfiles.items():
runners[name] = LtlcrossRunner(tools,res_filename=rfile,
formula_files=['formulae/{}.ltl'.format(name)],
cols=cols)
In [26]:
for r in runners.values():
if rerun:
r.run_ltlcross()
r.parse_results()
In [27]:
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. automata"] = len(r.values)-tmp.nondet_aut
t1[name] = t1_part
In [28]:
t1_merged = pd.concat(t1.values(),axis=1,keys=t1.keys()).loc[MI_order,:]
t1_merged
Out[28]:
In [29]:
row_map={"basic" : 'basic',
"F-merging" : '$\F$-merging',
"G-merging" : '$\G$-merging',
"FG-merging" : '$\FG$-merging',
"FG-merging+compl" : "$\FG$-merging + complement"}
t1_merged.rename(row_map,inplace=True);
t1 = t1_merged.rename_axis(['',"translation"],axis=1)
t1.index.name = None
t1
Out[29]:
In [30]:
rand = t1.copy()
In [31]:
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[31]:
In [32]:
print(rand.to_latex(escape=False,bold_rows=False),file=open('fossacs_t1.tex','w'))
In [33]:
cp fossacs_t1.tex /home/xblahoud/research/ltl3tela_papers/
In [34]:
def fix_tools(tool):
return tool.replace('FG-','$\\FG$-').replace('F-','$\\F$-')
In [35]:
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 [43]:
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 [44]:
ltl3ba = 'LTL3BA'
fgm = 'FG-merging'
fm = 'F-merging'
basic = 'basic'
size = (4,4)
clip_names = ('xmin','ymin','xmax','ymax')
kw = {}
sc_plot(runners['lit'],basic,fgm,'sc_lit.tex',size=size,kw=kw.copy())
size = (4.3,4.5)
kw['title'] = 'literature'
sc_plot(runners['lit'],basic,fgm,'sc_lit.tex',size=size,kw=kw.copy())
for suff in ['1','2','4','fg']:
kw['title'] = 'rand'+suff
sc_plot(runners['rand'+suff],basic,fgm,'sc_rand{}.tex'.format(suff),size=size,kw=kw.copy())
In [45]:
cp sc_lit.tex sc_rand*.tex ~/research/ltl3tela_papers
In [46]:
r = runners['rand4']
In [40]:
r.smaller_than('basic','F-merging')
Out[40]: