fix: add unit to axis of figures

scripts/plot-results.py

@@ -5,7 +5,7 @@
 
 
 ZERO = 10e-5
-TIMEOUT = 10 * 60 # 20 minutes = 1200 seconds
+TIMEOUT = 10 * 60 # 10 minutes = 6000 seconds
 
 
 # In[2]:
@@ -154,19 +154,19 @@ def get_axis_title(experiment, show_strategy=True):
         'otf': 'Hybrid'
     }
     
-    if (len(information) == 5):
-        info.append(library_dic[information[1]])
+    #if (len(information) == 5):
+    #    info.append("mode " + library_dic[information[1]])
 
-    if (show_strategy):
-        info.append('strategy: {}'.format(information[-3]))
+    #if (show_strategy):
+    #    info.append('strategy: {}'.format(information[-3]))
 
     nb_nodes = int(information[-2])
-    if (nb_nodes > 1):
+    if (nb_nodes):
         info.append('# nodes: {}'.format(nb_nodes))
 
     info.append('# cores: {}'.format(information[-1]))
 
-    title = '{} ({})'.format(tool_name, ', '.join(info))
+    title = 'Verification time (seconds)<br>{} ({})'.format(tool_name, ', '.join(info))
     
     return title
 
@@ -482,9 +482,9 @@ def create_log_figure(table, table_errors, model, tool_x, tool_y, show_strategy=
         full_table_x, full_table_y = filter_errors(full_table_x, full_table_y)
 
         traces = [
-            {"property": 'T', "color":"green"},
-            {"property": 'F', "color":"red"},
-            {"property": 'U', "color":"black"}
+            {"property": 'T', "color":"green", "label": "True"},
+            {"property": 'F', "color":"red", "label": "False"},
+            {"property": 'U', "color":"black", "label": "Unknown"}
         ]
 
         figures = []
@@ -505,7 +505,7 @@ def create_log_figure(table, table_errors, model, tool_x, tool_y, show_strategy=
 
             figures.append(go.Scatter(x=table_x.time,
                                       y=table_y.time,
-                                      name=t['property'],
+                                      name=t['label'],
                                       mode='markers',
                                       marker_symbol='circle-open',
                                       marker_color=t['color'],
@@ -708,14 +708,10 @@ df
 
 
 # filtering runtime errors
-#df = df[(df.error != "SEGMENTATION FAULT") & \
-#        (df.error != "ABORTED") & \
-#        (df.error != "TERMINATE") & \
-#        (df.error != "MDD")]
+df = df[(df.error != "SEGMENTATION FAULT") &         (df.error != "ABORTED") &         (df.error != "TERMINATE") &         (df.error != "MDD")]
 
-#df = df.reset_index(drop=True)
-#df
-df.model.unique()
+df = df.reset_index(drop=True)
+df
 
 
 # In[14]:
@@ -794,7 +790,7 @@ table_error = table['error'].copy()
 table_error.head()
 
 
-# In[21]:
+# In[19]:
 
 
 # table with explored states for each experiment using ltsmin
@@ -812,7 +808,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
@@ -824,35 +820,35 @@ table_explored_states_stats.head()
 
 # # Examples
 
-# In[23]:
+# In[21]:
 
 
-create_figure_explored_states(table_explored_states, 'train24')
+create_figure_explored_states(table_explored_states, 'robot20')
 
 
 # In[22]:
 
 
-create_figure(df, "train24")
+create_figure(df, "robot20")
 
 
-# In[27]:
+# In[23]:
 
 
-log_figure = create_log_figure(table_time, table_error, "train24", "pmc-sog_otfPR_couv99-default_4_8", "pnml2lts-mc_dfs_1_16", True, open_logs_callback)
+log_figure = create_log_figure(table_time, table_error, "robot20", "pmc-sog_otf_couv99-shy_2_8", "pnml2lts-mc_dfs_1_16", True, open_logs_callback)
 log_figure
 
 
-# In[30]:
+# In[24]:
 
 
-table = get_table(table_time, table_error, "train24", "pmc-sog_otfPR_couv99-default_4_8", "pnml2lts-mc_dfs_1_16")
+table = get_table(table_time, table_error, "robot20", "pmc-sog_otf_couv99-default_2_8", "pnml2lts-mc_dfs_1_16")
 table
 
 
 # # Generate Figures
 
-# In[31]:
+# In[ ]:
 
 
 # models
@@ -862,26 +858,26 @@ models = df.model.unique()
 tools = df.tool.unique()
 
 
-# In[34]:
+# In[ ]:
 
 
 # create all the figures of explored states
 
-# folder = os.path.join(OUTPUT_FOLDER, 'explored-states')
-# create_folder(folder)
+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'), include_plotlyjs='cdn')
-#        fig.write_image(os.path.join(folder, model + '.pdf'))
-#    except KeyError:
-#        print("Error: {} was not plotted".format(model))
+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'), include_plotlyjs='cdn')
+        fig.write_image(os.path.join(folder, model + '.pdf'))
+    except KeyError:
+        print("Error: {} was not plotted".format(model))
 
 
-# In[35]:
+# In[ ]:
 
 
 # create all the figures formula vs time
@@ -900,7 +896,7 @@ for model in models:
         print("Error: {} was not plotted".format(model))
 
 
-# In[36]:
+# In[ ]:
 
 
 # create all the log figures