fix notebook

benchmarks/analysis.py

+#!/usr/bin/env python
+# coding: utf-8
+
+# In[1]:
+
+
+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 = ["accel-1000", "tgc", "Pipeline_KP12_2_3", "gear-1000", "coffee", "blowup-200", "RCP"]
+
+# csv with results
+csv_filename = "results.csv"
+
+# folder with tools results
+log_folder = "logs"
+
+# 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"
+
+
+# # Generate CSV file with data
+
+# In[2]:
+
+
+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 generate_csv():
+    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+)")
+
+
+    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)']
+        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)}"
+                    
+                    # 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})
+
+
+# In[3]:
+
+
+generate_csv()
+
+
+# # Analyse Data
+
+# In[4]:
+
+
+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
+
+
+# In[5]:
+
+
+def export_to_latex(df):
+    styler =df.style
+    styler.hide(axis='index')
+    return styler.to_latex(hrules=True)
+
+
+# In[6]:
+
+
+df = pd.read_csv(csv_filename)
+df = df.set_index("model")
+df
+
+
+# In[7]:
+
+
+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
+
+
+# # Plot
+
+# In[8]:
+
+
+with open("images/table.tex", 'w') as latex_file:
+    latex_file.write(export_to_latex(df_model_info))
+
+
+# In[9]:
+
+
+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")
+
+
+# In[10]:
+
+
+# show a figure
+plot(df, models[0])
+

benchmarks/requirements.txt

+jupyter
+pandas
+plotly
+requests
\ No newline at end of file