Skip to content
Snippets Groups Projects
Commit 35c12ed7 authored by Jaime Arias's avatar Jaime Arias
Browse files

update noteboo

parent 1d8b9fbd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
benchmarks/analysis.ipynb
+ 1054
− 196
View file @ 35c12ed7
%% Cell type:code id: tags:
``` python
import os
import re
import csv
import pandas as pd
import math
import plotly.io as pio
import plotly.graph_objects as go
# pio.kaleido.scope.mathjax = None
# models to analyse
models = ["tgc", "coffee", "fischer"]
# csv with results
csv_filename = "results.csv"
# folder with tools results
log_folder = "logs"
# folder with the mdoels
models_folder = "models"
# filenames
imitator_file = "{model}-EFwitness.imiprop.{location}.res"
maude_files = [
{"name": "no_folding", "file": "{model}.no-folding.maude.{location}.res"},
{"name": "no_folding_FME", "file": "{model}.no-folding.maude.{location}.FEM.res"},
{"name": "folding", "file": "{model}.folding.maude.{location}.res"},
{"name": "folding_FME", "file": "{model}.folding.maude.{location}.FEM.res"},
]
# maude labels for the tables
maude_labels = []
for f in maude_files:
prefix = f'maude_{f["name"]}'
maude_labels.append(f"{prefix}_rewrites")
maude_labels.append(f"{prefix}_cpu(ms)")
maude_labels.append(f"{prefix}_real(ms)")
```
%% Cell type:markdown id: tags:
# Generate CSV file with data
%% Cell type:code id: tags:
``` python
def format_unit(value, unit):
if unit == "ms":
return float(value)
elif unit == "second" or unit == "seconds":
return float(value) * 1000
else:
raise Exception(f"Unit {unit} is not supported")
def parse_imi_file(model, loc):
# regex
regex_imitator = re.compile(r"Total computation time\s*:\s*(\d+(?:\.\d+)?) (\w+)")
regex_clocks = re.compile(r"Number of clocks\s*:\s*(\d+)")
regex_parameters = re.compile(r"Number of parameters\s*:\s*(\d+)")
regex_actions = re.compile(r"Number of actions\s*:\s*(\d+)")
regex_locations = re.compile(r"Total number of locations\s*:\s*(\d+)")
regex_transitions = re.compile(r"Total number of transitions\s*:\s*(\d+)")
output = {}
# search in imitator file
imi_filename = imitator_file.format(model=model, location=loc)
with open(os.path.join(log_folder, model, imi_filename), "r") as imi_file:
imi_content = imi_file.read()
# get imitator times
imi_search = regex_imitator.search(imi_content)
imi_time, imi_unit = imi_search.groups()
output["time"] = f"{format_unit(imi_time, imi_unit)}"
# get model's information
output["nb_clocks"] = regex_clocks.search(imi_content).group(1)
output["nb_parameters"] = regex_parameters.search(imi_content).group(1)
output["nb_actions"] = regex_actions.search(imi_content).group(1)
output["nb_locations"] = regex_locations.search(imi_content).group(1)
output["nb_transitions"] = regex_transitions.search(imi_content).group(1)
return output
def parse_maude_file(filename_file, model, loc):
regex_maude = re.compile(r"rewrites: (\d+) in (\d+)(\w+) cpu \((\d+)(\w+) real\)")
output = {}
# search in maude file
maude_filename = filename_file.format(model=model, location=loc)
with open(os.path.join(log_folder, model, maude_filename), "r") as rl_file:
maude_content = regex_maude.search(rl_file.read())
(rewrites, cpu, cpu_unit, real, real_unit) = maude_content.groups()
output["rewrites"] = rewrites
output["cpu"] = f"{format_unit(cpu, cpu_unit)}"
output["real"] = f"{format_unit(real, real_unit)}"
return output
def generate_csv():
with open(csv_filename, "w") as csv_file:
fieldnames = [
"model",
"clocks",
"parameters",
"actions",
"locations",
"transitions",
"location_reached",
"imitator_time(ms)",
]
for f in maude_files:
prefix = f'maude_{f["name"]}'
fieldnames.append(f"{prefix}_rewrites")
fieldnames.append(f"{prefix}_cpu(ms)")
fieldnames.append(f"{prefix}_real(ms)")
] + maude_labels
writer = csv.DictWriter(csv_file, fieldnames=fieldnames)
writer.writeheader()
for model in models:
with open(os.path.join(models_folder, f"{model}_loc.txt")) as loc_file:
locations = [l.replace("\n", "").split(" ")[1] for l in loc_file]
for loc in locations:
imitator_info = parse_imi_file(model, loc)
results = {
"model": model,
"location_reached": loc,
"clocks": imitator_info["nb_clocks"],
"parameters": imitator_info["nb_parameters"],
"actions": imitator_info["nb_actions"],
"locations": imitator_info["nb_locations"],
"transitions": imitator_info["nb_transitions"],
"imitator_time(ms)": imitator_info["time"],
}
for f in maude_files:
maude_info = parse_maude_file(f["file"], model, loc)
prefix = f'maude_{f["name"]}'
results[f"{prefix}_rewrites"] = maude_info["rewrites"]
results[f"{prefix}_cpu(ms)"] = maude_info["cpu"]
results[f"{prefix}_real(ms)"] = maude_info["real"]
# save info
writer.writerow(results)
```
%% Cell type:code id: tags:
``` python
generate_csv()
```
%% Cell type:markdown id: tags:
# Analyse Data
%% Cell type:code id: tags:
``` python
def export_to_latex(df):
styler = df.style
styler.hide(axis="index")
return styler.to_latex(hrules=True)
```
%% Cell type:code id: tags:
``` python
df = pd.read_csv(csv_filename)
df = df.set_index("model")
df
```
%% Output
clocks parameters actions locations transitions location_reached
model
tgc 3 6 8 12 12 train0 \
tgc 3 6 8 12 12 train1
tgc 3 6 8 12 12 train2
tgc 3 6 8 12 12 train3
tgc 3 6 8 12 12 gate0
tgc 3 6 8 12 12 gate1
tgc 3 6 8 12 12 gate2
tgc 3 6 8 12 12 gate3
tgc 3 6 8 12 12 controller0
tgc 3 6 8 12 12 controller1
tgc 3 6 8 12 12 controller2
tgc 3 6 8 12 12 controller3
coffee 2 3 4 4 6 idle
coffee 2 3 4 4 6 addsugar
coffee 2 3 4 4 6 preparingcoffee
coffee 2 3 4 4 6 cdone
fischer 2 2 12 14 20 idle1
fischer 2 2 12 14 20 active1
fischer 2 2 12 14 20 check1
fischer 2 2 12 14 20 locaccess1
fischer 2 2 12 14 20 cs1
fischer 2 2 12 14 20 idle2
fischer 2 2 12 14 20 active2
fischer 2 2 12 14 20 check2
fischer 2 2 12 14 20 locaccess2
fischer 2 2 12 14 20 cs2
fischer 2 2 12 14 20 obswaiting
fischer 2 2 12 14 20 obs1
fischer 2 2 12 14 20 obs2
fischer 2 2 12 14 20 obsviolation
imitator_time(ms) maude_no_folding_rewrites
model
tgc 6.0 150 \
tgc 11.0 354
tgc 13.0 667
tgc 16.0 1222
tgc 7.0 150
tgc 14.0 767
tgc 21.0 1463
tgc 45.0 10740
tgc 6.0 150
tgc 11.0 354
tgc 18.0 767
tgc 30.0 4279
coffee 5.0 111
coffee 10.0 261
coffee 14.0 562
coffee 18.0 1174
fischer 6.0 112
fischer 11.0 297
fischer 15.0 627
fischer 22.0 1402
fischer 32.0 2933
fischer 6.0 112
fischer 11.0 349
fischer 17.0 819
fischer 24.0 1782
fischer 31.0 3718
fischer 5.0 112
fischer 28.0 2933
fischer 30.0 3718
fischer 70.0 49279
maude_no_folding_cpu(ms) maude_no_folding_real(ms)
model
tgc 526.0 526.0 \
tgc 525.0 524.0
tgc 575.0 575.0
tgc 582.0 582.0
tgc 498.0 497.0
tgc 551.0 551.0
tgc 573.0 572.0
tgc 864.0 863.0
tgc 508.0 507.0
tgc 569.0 568.0
tgc 535.0 535.0
tgc 647.0 647.0
coffee 483.0 483.0
coffee 491.0 491.0
coffee 500.0 499.0
coffee 559.0 558.0
fischer 517.0 517.0
fischer 538.0 537.0
fischer 520.0 519.0
fischer 587.0 587.0
fischer 604.0 604.0
fischer 548.0 548.0
fischer 542.0 542.0
fischer 579.0 579.0
fischer 619.0 619.0
fischer 620.0 620.0
fischer 509.0 508.0
fischer 603.0 602.0
fischer 635.0 634.0
fischer 1885.0 1884.0
maude_no_folding_FME_rewrites maude_no_folding_FME_cpu(ms)
model
tgc 150 528.0 \
tgc 398 523.0
tgc 947 573.0
tgc 1989 607.0
tgc 150 514.0
tgc 1071 544.0
tgc 2300 585.0
tgc 18403 898.0
tgc 150 548.0
tgc 398 568.0
tgc 1071 531.0
tgc 7530 685.0
coffee 111 510.0
coffee 273 489.0
coffee 602 512.0
coffee 1280 543.0
fischer 112 503.0
fischer 331 505.0
fischer 826 520.0
fischer 2065 552.0
fischer 4466 670.0
fischer 112 563.0
fischer 383 518.0
fischer 1028 544.0
fischer 2435 560.0
fischer 5031 635.0
fischer 112 508.0
fischer 4466 644.0
fischer 5031 679.0
fischer 45904 1486.0
maude_no_folding_FME_real(ms) maude_folding_rewrites
model
tgc 529.0 424 \
tgc 523.0 999
tgc 573.0 2420
tgc 607.0 5898
tgc 513.0 424
tgc 544.0 2420
tgc 586.0 5898
tgc 897.0 35973
tgc 547.0 424
tgc 568.0 999
tgc 530.0 2420
tgc 686.0 20078
coffee 521.0 290
coffee 488.0 720
coffee 511.0 1977
coffee 543.0 4357
fischer 502.0 389
fischer 505.0 1218
fischer 520.0 3274
fischer 552.0 6752
fischer 669.0 11695
fischer 563.0 389
fischer 518.0 1218
fischer 544.0 3274
fischer 560.0 6752
fischer 635.0 11695
fischer 508.0 389
fischer 641.0 11695
fischer 678.0 11695
fischer 1485.0 79004
maude_folding_cpu(ms) maude_folding_real(ms)
model
tgc 507.0 507.0 \
tgc 574.0 573.0
tgc 641.0 640.0
tgc 855.0 855.0
tgc 536.0 534.0
tgc 672.0 672.0
tgc 815.0 813.0
tgc 2258.0 2260.0
tgc 536.0 535.0
tgc 642.0 641.0
tgc 690.0 689.0
tgc 1408.0 1407.0
coffee 537.0 537.0
coffee 526.0 526.0
coffee 607.0 606.0
coffee 670.0 668.0
fischer 524.0 524.0
fischer 595.0 594.0
fischer 707.0 706.0
fischer 860.0 860.0
fischer 1101.0 1101.0
fischer 540.0 540.0
fischer 616.0 616.0
fischer 732.0 731.0
fischer 959.0 959.0
fischer 1189.0 1189.0
fischer 539.0 538.0
fischer 1118.0 1117.0
fischer 1212.0 1213.0
fischer 3968.0 3967.0
maude_folding_FME_rewrites maude_folding_FME_cpu(ms)
model
tgc 468 532.0 \
tgc 1316 595.0
tgc 3297 709.0
tgc 7753 878.0
tgc 468 524.0
tgc 3297 689.0
tgc 7753 864.0
tgc 45102 2382.0
tgc 468 549.0
tgc 1316 641.0
tgc 3297 674.0
tgc 23670 1495.0
coffee 334 504.0
coffee 763 545.0
coffee 2019 602.0
coffee 4419 698.0
fischer 423 565.0
fischer 1427 638.0
fischer 3869 709.0
fischer 7535 861.0
fischer 12672 1078.0
fischer 423 522.0
fischer 1427 620.0
fischer 3869 733.0
fischer 7535 902.0
fischer 12672 1070.0
fischer 423 566.0
fischer 12672 1165.0
fischer 12672 1116.0
fischer 75437 3586.0
maude_folding_FME_real(ms)
model
tgc 532.0
tgc 593.0
tgc 707.0
tgc 877.0
tgc 523.0
tgc 689.0
tgc 862.0
tgc 2383.0
tgc 548.0
tgc 640.0
tgc 673.0
tgc 1494.0
coffee 504.0
coffee 545.0
coffee 601.0
coffee 696.0
fischer 564.0
fischer 637.0
fischer 709.0
fischer 861.0
fischer 1077.0
fischer 522.0
fischer 620.0
fischer 733.0
fischer 901.0
fischer 1070.0
fischer 565.0
fischer 1164.0
fischer 1114.0
fischer 3585.0
%% Cell type:code id: tags:
``` python
df_model_info = df.drop_duplicates(
subset=["clocks", "parameters", "actions", "locations", "transitions"], keep="last"
).reset_index()
df_model_info = df_model_info.drop(
labels=["location_reached", "imitator_time(ms)"] + maude_labels,
axis=1,
)
df_model_info = df_model_info.sort_values(
by="model", key=lambda col: col.str.lower(), ignore_index=True
)
df_model_info
```
%% Output
model clocks parameters actions locations transitions
0 coffee 2 3 4 4 6
1 fischer 2 2 12 14 20
2 tgc 3 6 8 12 12
%% Cell type:code id: tags:
``` python
with open("images/table.tex", "w") as latex_file:
latex_file.write(export_to_latex(df_model_info))
```
%% Cell type:markdown id: tags:
# Plot
%% Cell type:code id: tags:
``` python
def plot(df, model_name):
model = df.loc[[model_name]]
max_value_model = (
model.drop(axis=1, labels=["maude_rewrites", "maude_collapsing_rewrites"])
.max(numeric_only=True, axis=0)
.max()
)
axis_bound = math.ceil(math.log10(max_value_model))
fig = go.Figure()
# no collapsing
fig.add_trace(
go.Scatter(
x=model["maude_real(ms)"],
y=model["imitator_time(ms)"],
text=model["location_reached"],
mode="markers",
marker_symbol="circle-open",
marker_color="red",
marker_size=12,
name="no-collapsing",
)
)
# collapsing
fig.add_trace(
go.Scatter(
x=model["maude_collapsing_real(ms)"],
y=model["imitator_time(ms)"],
text=model["location_reached"],
mode="markers",
marker_symbol="circle-open",
marker_color="blue",
marker_size=12,
name="collapsing",
)
)
# identity line
fig.add_trace(
go.Scatter(
x=[0, 10**axis_bound],
y=[0, 10**axis_bound],
mode="lines",
line=dict(color="black", width=1),
showlegend=False,
)
)
fig.update_xaxes(
type="log",
showgrid=False,
mirror=True,
linewidth=1,
linecolor="black",
constrain="domain",
range=[-1, axis_bound],
title="Maude (ms)",
)
fig.update_yaxes(
type="log",
showgrid=False,
mirror=True,
linewidth=1,
linecolor="black",
scaleanchor="x",
scaleratio=1,
range=[-1, axis_bound],
title="Imitator (ms)",
)
legend_options = dict(
yanchor="top",
y=0.99,
xanchor="left",
x=0.05,
bordercolor="Black",
borderwidth=1,
)
margin = margin = dict(l=20, r=20, t=20, b=20)
fig.update_layout(
width=800,
height=800,
paper_bgcolor="white",
plot_bgcolor="white",
legend_title_text="Method",
legend=legend_options,
autosize=False,
margin=margin,
font=dict(size=28),
)
fig.update_traces(
hovertemplate="<b>%{text}</b><br><br>Maude: %{x} ms <br>Imitator: %{y} ms<extra></extra>"
)
return fig
```
%% Cell type:code id: tags:
``` python
def export_to_latex(df):
styler = df.style
styler.hide(axis="index")
return styler.to_latex(hrules=True)
```
%% Cell type:code id: tags:
``` python
df = pd.read_csv(csv_filename)
df = df.set_index("model")
df
```
%% Output
clocks parameters actions locations transitions location_reached \
model
coffee 2 3 4 4 6 addsugar
coffee 2 3 4 4 6 cdone
coffee 2 3 4 4 6 idle
coffee 2 3 4 4 6 preparingcoffee
imitator_time(ms) maude_rewrites maude_cpu(ms) maude_real(ms) \
model
coffee 0.0 2 0.0 0.0
coffee 0.0 12 0.0 0.0
coffee 0.0 0 0.0 0.0
coffee 0.0 6 0.0 0.0
maude_collapsing_rewrites maude_collapsing_cpu(ms) \
model
coffee 85 4.0
coffee 373 8.0
coffee 801 12.0
coffee 182 8.0
maude_collapsing_real(ms)
model
coffee 5.0
coffee 7.0
coffee 15.0
coffee 6.0
%% Cell type:code id: tags:
``` python
df_model_info = df.drop_duplicates(
subset=["clocks", "parameters", "actions", "locations", "transitions"], keep="last"
).reset_index()
df_model_info = df_model_info.drop(
labels=[
"location_reached",
"imitator_time(ms)",
"maude_rewrites",
"maude_cpu(ms)",
"maude_real(ms)",
"maude_collapsing_rewrites",
"maude_collapsing_cpu(ms)",
"maude_collapsing_real(ms)",
],
axis=1,
)
df_model_info = df_model_info.sort_values(
by="model", key=lambda col: col.str.lower(), ignore_index=True
)
df_model_info
```
%% Output
model clocks parameters actions locations transitions
0 coffee 2 3 4 4 6
%% Cell type:markdown id: tags:
# Plot
%% Cell type:code id: tags:
``` python
with open("images/table.tex", "w") as latex_file:
latex_file.write(export_to_latex(df_model_info))
```
%% Cell type:code id: tags:
``` python
for m in models:
fig = plot(df, m)
filename = m.replace("_", "-")
fig.write_html(f"images/{filename}.html")
fig.write_image(f"images/{filename}.pdf", format="pdf")
```
%% Output
../../sandbox/linux/seccomp-bpf-helpers/sigsys_handlers.cc:**CRASHING**:seccomp-bpf failure in syscall 0230
../../sandbox/linux/seccomp-bpf-helpers/sigsys_handlers.cc:**CRASHING**:seccomp-bpf failure in syscall 0230
../../sandbox/linux/seccomp-bpf-helpers/sigsys_handlers.cc:**CRASHING**:seccomp-bpf failure in syscall 0230
%% Cell type:code id: tags:
``` python
# show a figure
plot(df, models[0])
```
%% Output
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment