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

fix analysis notebook

parent ad260349
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
benchmarks/analysis.ipynb
+ 205
− 90
View file @ 1d8b9fbd
%% 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
# pio.kaleido.scope.mathjax = None
# models to analyse
models = ["accel-1000", "tgc", "Pipeline_KP12_2_3", "gear-1000", "coffee", "blowup-200", "RCP"]
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"
no_collapsing_maude_file = "{model}.no-collapsing.maude.{location}.res"
collapsing_maude_file = "{model}.collapsing.maude.{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"},
]
```
%% 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
return float(value) * 1000
else:
raise Exception(f"Unit {unit} is not supported")
def generate_csv():
def parse_imi_file(model, loc):
# regex
regex_imitator = re.compile(r"Total computation time\s*:\s*(\d+(?:\.\d+)?) (\w+)")
regex_maude = re.compile(r"rewrites: (\d+) in (\d+)(\w+) cpu \((\d+)(\w+) real\)")
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)', 'maude_rewrites', 'maude_cpu(ms)', 'maude_real(ms)', 'maude_collapsing_rewrites', 'maude_collapsing_cpu(ms)', 'maude_collapsing_real(ms)']
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)")
writer = csv.DictWriter(csv_file, fieldnames=fieldnames)
writer.writeheader()
for model in models:
with open(os.path.join(log_folder, model,"locations.txt")) as loc_file:
for location in loc_file:
loc = location.replace("\n","")
imi_filename = imitator_file.format(model=model, location=loc)
maude_filename = no_collapsing_maude_file.format(model=model, location=loc)
collapsing_maude_filename = collapsing_maude_file.format(model=model, location=loc)
imitator_time=""
maude_rewrites=""
maude_cpu=""
maude_real=""
c_maude_rewrites=""
c_maude_cpu=""
c_maude_real=""
# search in imitator file
with open(os.path.join(log_folder, model, imi_filename), 'r') as imi_file:
imi_content = imi_file.read()
imi_search = regex_imitator.search(imi_content)
imi_time, imi_unit = imi_search.groups()
imitator_time=f"{format_unit(imi_time, imi_unit)}"
# get model's information
nb_clocks = regex_clocks.search(imi_content).group(1)
nb_parameters = regex_parameters.search(imi_content).group(1)
nb_actions = regex_actions.search(imi_content).group(1)
nb_locations = regex_locations.search(imi_content).group(1)
nb_transitions = regex_transitions.search(imi_content).group(1)
# search in maude file
with open(os.path.join(log_folder, model, maude_filename), 'r') as rl_file:
maude_rewrites, _maude_cpu, maude_cpu_unit, _maude_real, maude_real_unit = regex_maude.search(rl_file.read()).groups()
maude_cpu=f"{format_unit(_maude_cpu, maude_cpu_unit)}"
maude_real=f"{format_unit(_maude_real, maude_real_unit)}"
# search in collapsing maude file
with open(os.path.join(log_folder, model, collapsing_maude_filename), 'r') as collapsing_file:
c_maude_rewrites, _c_maude_cpu, c_maude_cpu_unit, _c_maude_real, c_maude_real_unit = regex_maude.search(collapsing_file.read()).groups()
c_maude_cpu=f"{format_unit(_c_maude_cpu, c_maude_cpu_unit)}"
c_maude_real=f"{format_unit(_c_maude_real, c_maude_real_unit)}"
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({"model":model,
"location_reached": loc,
"clocks": nb_clocks,
"parameters": nb_parameters,
"actions": nb_actions,
"locations": nb_locations,
"transitions": nb_transitions,
"imitator_time(ms)": imitator_time,
"maude_rewrites": maude_rewrites,
"maude_cpu(ms)": maude_cpu,
"maude_real(ms)": maude_real,
"maude_collapsing_rewrites": c_maude_rewrites,
"maude_collapsing_cpu(ms)": c_maude_cpu,
"maude_collapsing_real(ms)": c_maude_real})
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 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()
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"))
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"))
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>')
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')
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 = 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:
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("_","-")
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