Commit 1d49e609 authored by Jaime Arias's avatar Jaime Arias
Browse files

update notebook

parent 6b592c87
This diff is collapsed.
#!/usr/bin/env python
# coding: utf-8
# In[2]:
# In[19]:
import os
import pandas as pd
import numpy as np
import plotly.io as pio
import plotly.express as px
import plotly.graph_objs as go
......@@ -49,7 +50,7 @@ LAYOUT_FIGURES = dict(
# # Auxiliary Functions
# In[3]:
# In[2]:
def create_folder(path):
......@@ -69,7 +70,7 @@ def create_folder(path):
os.makedirs(path)
# In[4]:
# In[3]:
def create_figure(df, model):
......@@ -108,7 +109,7 @@ def create_figure(df, model):
return figure
# In[21]:
# In[4]:
def get_axis_title(experiment, show_strategy=True):
......@@ -160,7 +161,7 @@ def get_axis_title(experiment, show_strategy=True):
return title
# In[22]:
# In[5]:
def create_log_figure(table, table_errors, model, tool_x, tool_y, show_strategy=True):
......@@ -233,7 +234,77 @@ def create_log_figure(table, table_errors, model, tool_x, tool_y, show_strategy=
print(e)
# In[31]:
# In[6]:
def create_figure_explored_states(table_explored_states, model):
"""Creates figure showing the number of explorated states during the verification
Parameters
----------
table_explored_states : pandas.Dataframe
Dataframe with the explorated states of each experiment
model : string
Model to be analyzed
Returns
-------
plotly.graph_objects.Figure
Scatter figure
"""
colors={'T': 'green', 'F': 'red'}
float_formatter = "{:.2E}".format
table_model = table_explored_states[table_explored_states.property != 'U']
table_model = table_model[table_model.model == model]
table_stats = table_model.groupby(['property']).agg(['mean'])
fig = go.Figure()
for p in table_stats.index:
data = table_model[table_model.property==p]
stats = table_stats.loc[p]
x_axis = np.arange(1, data['formula'].count()+1, 1)
mean = stats['explored_states','mean']
figure = px.scatter(data,
x=x_axis,
y="explored_states",
title=model,
color='property',
color_discrete_map=colors,
symbol_sequence=["circle"])
line = go.Scatter(x=[x_axis[0], x_axis[-1]],
y=[mean, mean],
mode='lines', showlegend=False,
line=dict(color=colors[p], width=1.5))
fig.add_trace(figure['data'][0])
fig.add_trace(line)
fig.add_annotation(x=1,
y=mean,
font=dict(color=colors[p]),
text=f"mean = {float_formatter(mean)}")
fig.update_layout(title_text=model, title=LAYOUT_FIGURES['title'],
width = 500, height = 500, margin=dict(r=110))
fig.update_xaxes(title="formula", range=[x_axis[0]-1, x_axis[-1]+1])
fig.update_yaxes(title="# explored states")
fig.update_annotations(dict(
showarrow=False,
xanchor="left",
yanchor="middle",
xref='paper'))
return fig
# In[7]:
# Experiment filters
......@@ -391,7 +462,7 @@ p_df =p_df[
(p_df.num_threads == 16)]
# only property column is needed
p_df = p_df.drop(columns=['tool', 'strategy', 'num_nodes', 'num_threads', 'time', 'error'])
p_df = p_df.drop(columns=['tool', 'strategy', 'num_nodes', 'num_threads', 'time', 'explored_states', 'error'])
p_df.fillna('U', inplace=True)
p_df.set_index(['model', 'formula'], inplace=True)
p_df.sort_index(inplace=True)
......@@ -413,7 +484,7 @@ table.head()
ZERO = 10e-5
TIMEOUT = 10 * 60 # 5 minutes = 300 seconds
TIMEOUT = 10 * 60 # 10 minutes = 600 seconds
# In[13]:
......@@ -458,25 +529,57 @@ table_error = table['error'].copy()
table_error.head()
# In[16]:
# table with explored states for each experiment using ltsmin
table_explored_states = table.copy()
table_explored_states = table_explored_states['explored_states']
table_explored_states = table_explored_states[['pnml2lts-mc_dfs_1_16']]
table_explored_states = table_explored_states.rename(columns={"pnml2lts-mc_dfs_1_16": "explored_states"})
# add verification output to the table
table_explored_states = pd.concat([table_explored_states, p_df], axis=1)
# reshape
table_explored_states = table_explored_states.reset_index()
table_explored_states.head()
# In[17]:
# calculate the stats of the number of explored states
table_explored_states_stats = table_explored_states.groupby(['model', 'property']).agg(['mean', 'min', 'max'])
table_explored_states_stats = table_explored_states_stats['explored_states']
table_explored_states_stats.head()
# # Examples
# In[19]:
# In[20]:
fig = create_figure(df, "philo10")
fig.show()
create_figure_explored_states(table_explored_states, 'robot20')
# In[23]:
# In[21]:
create_figure(df, "philo10")
# In[22]:
fig = create_log_figure(table_time, table_error, "philo10", "pmc-sog_otf_couv99-default_2_8", "pnml2lts-mc_dfs_1_16")
fig.show()
create_log_figure(table_time, table_error, "philo10", "pmc-sog_otf_couv99-default_2_8", "pnml2lts-mc_dfs_1_16")
# # Generate Figures
# In[24]:
# In[23]:
# models
......@@ -486,7 +589,26 @@ models = df.model.unique()
tools = df.tool.unique()
# In[52]:
# In[ ]:
# create all the figures of explored states
folder = os.path.join(OUTPUT_FOLDER, 'explored-states')
create_folder(folder)
for model in models:
try:
fig = create_figure_explored_states(table_explored_states, model)
# save figures in html and pdf
fig.write_html(os.path.join(folder, model + '.html'))
fig.write_image(os.path.join(folder, model + '.pdf'))
except KeyError:
print("Error: {} was not plotted".format(model))
# In[ ]:
# create all the figures formula vs time
......
Markdown is supported
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