Commit 7cb023fa authored by Jaime Arias's avatar Jaime Arias
Browse files

update plot script

parent 46a392ba
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -399,7 +399,7 @@ myPlot.on('plotly_click', function(data){
"""
# In[7]:
# In[8]:
def create_figure_explored_states(table_explored_states, model):
......@@ -426,11 +426,13 @@ def create_figure_explored_states(table_explored_states, model):
table_stats = table_model.groupby(['property']).agg(['mean'])
fig = go.Figure()
max_x = 0
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)
max_x = max(max_x, x_axis[-1]+1)
mean = stats['explored_states','mean']
figure = px.scatter(data,
......@@ -457,7 +459,7 @@ def create_figure_explored_states(table_explored_states, model):
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_xaxes(title="formula", range=[0, max_x])
fig.update_yaxes(title="# explored states")
fig.update_annotations(dict(
......@@ -469,7 +471,7 @@ def create_figure_explored_states(table_explored_states, model):
return fig
# In[8]:
# In[9]:
# Experiment filters
......@@ -588,7 +590,7 @@ plots = {
# # Load Data
# In[9]:
# In[10]:
# Root folder
......@@ -602,7 +604,7 @@ OUTPUT_FOLDER = os.path.join(PROJECT_FOLDER,"results", "figures")
create_folder(OUTPUT_FOLDER)
# In[10]:
# In[11]:
# read data
......@@ -615,7 +617,7 @@ df = df.drop(columns=['strategy', 'num_nodes', 'num_threads'])
df.head()
# In[11]:
# In[12]:
# ground truth for properties
......@@ -635,7 +637,7 @@ p_df.sort_index(inplace=True)
p_df.head()
# In[12]:
# In[13]:
# table with times, verification output and error for each experiment
......@@ -645,14 +647,14 @@ table.head()
# # Preprocessing of data
# In[13]:
# In[14]:
ZERO = 10e-5
TIMEOUT = 10 * 60 # 10 minutes = 600 seconds
# In[14]:
# In[15]:
# table with times for each experiment
......@@ -670,7 +672,7 @@ table_time = pd.concat([table_time, p_df], axis=1)
table_time.head()
# In[15]:
# In[16]:
# table with verification output for each experiment
......@@ -685,7 +687,7 @@ table_property = pd.concat([table_property, p_df], axis=1)
table_property.head()
# In[16]:
# In[17]:
# table with error for each experiment
......@@ -694,7 +696,7 @@ table_error = table['error'].copy()
table_error.head()
# In[17]:
# In[18]:
# table with explored states for each experiment using ltsmin
......@@ -712,7 +714,7 @@ table_explored_states = table_explored_states.reset_index()
table_explored_states.head()
# In[18]:
# In[19]:
# calculate the stats of the number of explored states
......@@ -724,22 +726,22 @@ table_explored_states_stats.head()
# # Examples
# In[19]:
# In[21]:
create_figure_explored_states(table_explored_states, 'robot20')
create_figure_explored_states(table_explored_states, 'spool1')
# In[20]:
# In[22]:
create_figure(df, "philo10")
create_figure(df, "spool1")
# In[21]:
# In[25]:
create_log_figure(table_time, table_error, "philo10", "pmc-sog_otf_couv99-default_2_8", "pnml2lts-mc_dfs_1_16", True, open_logs_callback)
create_log_figure(table_time, table_error, "spool1", "pmc-sog_otf_couv99-default_2_16", "pnml2lts-mc_dfs_1_16", True, open_logs_callback)
# # Generate 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