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 [2]:
%%bash
ltl3ba -v
ltl3tela -v
ltl2tgba --version
ltlcross --version
In [3]:
# If there are already files with results, and rerun is False, ltlcross is not run again.
rerun = True
$\newcommand{\F}{\mathsf{F}}$ $\newcommand{\G}{\mathsf{G}}$ $\newcommand{\FG}{\mathsf{F,G}}$
We evaluate our translation on randomly generated formulae. We use Spot to generate them. The following function uses spot's randltl to generate and process formulae. It allows to filter the formulae using the function func (this feature is not used here) and also removes formulae $\top$ and $\bot$. Further, we remove all $\mathsf{M}$ and $\mathsf{W}$ operators as LTL3BA does not understand them. The relabel_bse function renames $\G(a \lor b)$ into $\G a$ and thus it keeps only on formula of such type.
In [4]:
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 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)\
.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():
print(form,file=file_h)
printed.add(form)
i += 1
In [5]:
fg_f = 'formulae/fg.ltl'
!mkdir -p formulae
total = 1000
generate(total,filename=fg_f,priorities='xor=0,implies=0,equiv=0,X=0,W=0,M=0,R=0,U=0,F=3,G=3')
We compare the $\F$- and $\FG$-merging translation to the basic one. We compare the sizes of SLAA (alternating) and TELA (nondeterministic). To really measure the impact of merging, the SPOT's reductions techniques are disabled here (-u0 -z0).
Here we use a wrapper script ltlcross_runner for ltlcross that uses the pandas library to manipulate data. It requires some settings.
In [6]:
### Tools' setting ###
ltl3tela_shared = "ltl3tela -p1 -t0 -u0 -z0 -f %f -a3 -n0 "
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,
}
### Order in which we want to sort the translations
MI_order = ["basic","F-merging",
"G-merging","FG-merging",
"FG-merging+compl"]
### File with measured statistics ###
merging_imp_alt = 'MI_alt-corr.csv'
Here we use the LtlcrossRunner object to run ltlcross, or parse already computed data.
In [7]:
MI_alt = LtlcrossRunner(tools,res_filename=merging_imp_alt,
formula_files=[fg_f],
cols=["states","transitions"])
if rerun:
MI_alt.run_ltlcross()
MI_alt.parse_results()
The cumulative number of states and transitions of all SLAA for each tool.
In [8]:
t1_alt = MI_alt.cummulative(col=["states","transitions"]).unstack(level=0).loc[MI_order,:]
t1_alt
Out[8]:
In [9]:
### Tools' setting ###
ltl3tela_shared = "ltl3tela -p2 -s0 -u0 -z0 -f %f -a3 -n0 "
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,
}
### File with measured statistics ###
merging_imp = 'MI_nondet-corr.csv'
cols=["states","transitions","nondet_aut"]
In [10]:
MI_nondet = LtlcrossRunner(tools,res_filename=merging_imp,
formula_files=[fg_f],
cols=cols)
if rerun:
MI_nondet.run_ltlcross()
MI_nondet.parse_results()
Here are the cumulative number of states, transitions, and number of deterministic automata for each translation.
In [11]:
tmp = MI_nondet.cummulative(col=cols).unstack(level=0).loc[MI_order,cols]
t1_nondet = tmp.loc[:,['states','transitions']]
t1_nondet["det. aut."] = total-tmp.nondet_aut
t1_nondet
Out[11]:
We merge the two tables and format the table labels for latex output.
In [12]:
t1 = pd.concat([t1_alt,t1_nondet],axis=1,keys=['SLAA (alternating)','TELA(nondeterministic)']).loc[MI_order,:]
t1
Out[12]:
In [13]:
row_map={"basic" : 'basic translation',
"F-merging" : '$\F$-merging',
"G-merging" : '$\G$-merging',
"FG-merging" : '$\FG$-merging',
"FG-merging+compl" : "$\FG$-merging + complement"}
t1.rename(row_map,inplace=True);
t1 = t1.rename_axis(['',"translation"],axis=1)
t1.index.name = None
t1
Out[13]:
In [23]:
print(t1.to_latex(escape=False,bold_rows=True),file=open('atva_t1.tex','w'))
We compare LTL3TELA with $\FG$-merging and the complement optimization to Spot and LTL3BA. We use the same set of formulae as before.
In [15]:
### Tools' setting ###
ltl3tela_shared = "ltl3tela -p2 -f %f -n0 "
end = " > %O"
tools = {"LTL3TELA" : ltl3tela_shared + end,
"LTL3TELA+compl" : ltl3tela_shared + "-n1 " + end,
"LTL3BA" : 'ltl3ba -H2 -f %s | autfilt --small > %O',
"SPOT-det" : 'ltl2tgba --deterministic -H %f>%O',
"SPOT-small" : 'ltl2tgba --small -H %f>%O',
}
tgba = ["LTL3BA","SPOT-det","SPOT-small"]
### File with measured statistics ###
comp_res = 'comp_nondet-corr.csv'
In [16]:
comp = LtlcrossRunner(tools,res_filename=comp_res,
formula_files=[fg_f],
cols=cols)
if rerun:
comp.run_ltlcross()
comp.parse_results()
We compute the cummulative numbers for each category (stored in cols) and we shape the data into nice table.
In [17]:
tmp = comp.cummulative(col=cols).unstack(level=0)
tmp = tmp.loc[tgba+['LTL3TELA',"LTL3TELA+compl"]+comp.mins,:][cols]
tmp2 = tmp.loc[:,['states','transitions']]
tmp2["deterministic"] = total-tmp.nondet_aut
tmp2
Out[17]:
For the paper, we choose only one configuration for each tool we do not use the virtual tools at all. Again, we create nicer labels.
In [18]:
# Rename
paper_tools = ['LTL3BA','SPOT-small','LTL3TELA+compl']
row_map = {
'LTL3BA' : 'LTL3BA',
'SPOT-small' : 'SPOT',
'LTL3TELA+compl': 'LTL3TELA'
}
t2 = tmp2.loc[paper_tools].rename(row_map)
# Get rid of the label for columns and keep `tool` only
t2 = t2.rename_axis("tool",axis=1)
t2.index.name=None
t2
Out[18]:
In [24]:
print(t2.to_latex(bold_rows=True),file=open('atva_t2.tex','w'))