Commit faf99706 authored by Jaime Arias's avatar Jaime Arias
Browse files

update plot scripts

parent a6b41247
This diff is collapsed.
......@@ -698,7 +698,7 @@ df = pd.read_csv(csv_file)
df['tool'] = df[['tool', 'strategy', 'num_nodes', 'num_threads']].astype(str).apply('_'.join, axis=1)
df = df.drop(columns=['strategy', 'num_nodes', 'num_threads'])
# filtering philo20 experiments
# FIX: filtering philo20 experiments because there is a problem with the generated formulas
df = df[df.model != "philo20"]
df
......@@ -706,30 +706,14 @@ df
# In[13]:
# Found errors
errors_found = df.error.unique()
errors_found
# In[14]:
# filtering errors
df = df[(df.error != "SEGMENTATION FAULT") & (df.error != "ABORTED") & (df.error != "TERMINATE") & (df.error != "MDD")]
# filtering runtime errors
df = df[(df.error != "SEGMENTATION FAULT") & (df.error != "ABORTED") & (df.error != "TERMINATE") & (df.error != "MDD")]
df = df.reset_index(drop=True)
df
# In[15]:
# Found errors
errors_found = df.error.unique()
errors_found
# In[16]:
# In[14]:
# ground truth for properties
......@@ -753,7 +737,7 @@ p_df.sort_index(inplace=True)
p_df
# In[17]:
# In[15]:
# table with times, verification output and error for each experiment
......@@ -763,7 +747,7 @@ table
# # Preprocessing of data
# In[18]:
# In[16]:
# table with times for each experiment
......@@ -781,7 +765,7 @@ table_time = pd.concat([table_time, p_df], axis=1)
table_time
# In[19]:
# In[17]:
# table with verification output for each experiment
......@@ -796,7 +780,7 @@ table_property = pd.concat([table_property, p_df], axis=1)
table_property.head()
# In[20]:
# In[18]:
# table with error for each experiment
......@@ -805,7 +789,7 @@ table_error = table['error'].copy()
table_error.head()
# In[21]:
# In[19]:
# table with explored states for each experiment using ltsmin
......@@ -823,7 +807,7 @@ table_explored_states = table_explored_states.reset_index()
table_explored_states.head()
# In[22]:
# In[20]:
# calculate the stats of the number of explored states
......@@ -835,10 +819,10 @@ table_explored_states_stats.head()
# # Examples
# In[23]:
# In[25]:
create_figure_explored_states(table_explored_states, 'spool5')
create_figure_explored_states(table_explored_states, 'robot50')
# In[24]:
......@@ -847,7 +831,7 @@ create_figure_explored_states(table_explored_states, 'spool5')
create_figure(df, "robot50")
# In[25]:
# In[23]:
log_figure = create_log_figure(table_time, table_error, "robot50", "pmc-sog_otf_couv99-default_2_16", "pnml2lts-mc_dfs_1_16", True, open_logs_callback)
......@@ -873,7 +857,7 @@ models = df.model.unique()
tools = df.tool.unique()
# In[29]:
# In[ ]:
# create all the figures of explored states
......@@ -892,7 +876,7 @@ for model in models:
print("Error: {} was not plotted".format(model))
# In[30]:
# In[ ]:
# create all the figures formula vs time
......@@ -911,7 +895,7 @@ for model in models:
print("Error: {} was not plotted".format(model))
# In[31]:
# In[ ]:
# create all the log figures
......
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