1#!/usr/bin/env python2.7 2# ---------------------------------- 3""" 4Usage: do_dp_plots.py [Options] 5 6Create a number of plots from test data on the theory of arrays. This 7is rather specialized code. To change the number or contents of the 8plots, edit the code below. 9 10Plots can be displayed on the screen or written as eps files. 11 12Options: 13 14-h 15 Print this information and exit. 16 17-f 18 Create result files (default is to display graphs via X) 19 20-d<directory> 21 Point to the directory where the result files can be found. This 22 overrides the hard-coded default. 23 24Copyright 2004, 2005 Stephan Schulz, schulz@eprover.org 25 26This code is part of the support structure for the equational 27heorem prover E. Visit 28 29 http://www.eprover.org 30 31for more information. 32 33This program is free software; you can redistribute it and/or modify 34it under the terms of the GNU General Public License as published by 35the Free Software Foundation; either version 2 of the License, or 36(at your option) any later version. 37 38This program is distributed in the hope that it will be useful, 39but WITHOUT ANY WARRANTY; without even the implied warranty of 40MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 41GNU General Public License for more details. 42 43You should have received a copy of the GNU General Public License 44along with this program ; if not, write to the Free Software 45Foundation, Inc., 59 Temple Place, Suite 330, Boston, 46MA 02111-1307 USA 47 48The original copyright holder can be contacted as 49 50Stephan Schulz (I4) 51Technische Universitaet Muenchen 52Institut fuer Informatik 53Boltzmannstrasse 3 54Garching bei Muenchen 55Germany 56 57or via email (address above). 58""" 59 60import re 61import sys 62import os.path 63from os import system 64 65import pylib_io 66import pylib_graphs 67 68cvc_sc_pat = re.compile("storecomm_[^i].*nf_ai") 69cvc_scf_pat = re.compile("storecomm_[^i].*sf_ai") 70e_sc_pat = re.compile("storecomm_[^i].*sf_ai") 71e_sc_ni_pat = re.compile("storecomm_[^i].*sf_ni") 72 73cvc_si_pat = re.compile("storeinv_[^i].*nf_ai") 74cvc_sif_pat = re.compile("storeinv_[^i].*sf_ai") 75e_si_pat = re.compile("storeinv_[^i].*sf_ai") 76 77cvc_sw_pat = re.compile("swap_[^i].*nf_ai") 78cvc_swf_pat = re.compile("swap_[^i].*sf_ai") 79e_sw_pat = re.compile("swap_[^i].*sf_ai") 80 81cvc_scinv_pat = re.compile("storecomm_invalid.*nf_ai") 82cvc_scfinv_pat = re.compile("storecomm_invalid.*sf_ai") 83e_scinv_pat = re.compile("storecomm_invalid.*sf_ai") 84e_scinv_ni_pat = re.compile("storecomm_invalid.*sf_ni") 85 86cvc_siinv_pat = re.compile("storeinv_invalid.*nf_ai") 87cvc_sifinv_pat = re.compile("storeinv_invalid.*sf_ai") 88e_siinv_pat = re.compile("storeinv_invalid.*sf_ai") 89 90cvc_swinv_pat = re.compile("swap_invalid.*nf_ai") 91cvc_swfinv_pat = re.compile("swap_invalid.*sf_ai") 92e_swinv_pat = re.compile("swap_invalid.*sf_ai") 93 94 95cvc_ios_pat = re.compile("ios_t1_ios_bia_np_sf_ai.*cvc") 96e_ios_pat = re.compile("ios_t1_ios_np_sf_ai.*tptp") 97 98#cvc_circqueue_pat = re.compile("circular_queue_t1_record_ios_mod_np_sf_ai.*cvc"); 99#cvc_queue_pat = re.compile("queue_t1_record_ios_np_sf_ai.*cvc"); 100#e_circqueue_pat = re.compile("circular_queue_t1_record_ios_mod_np_sf_ai.*tptp"); 101#e_queue_pat = re.compile("queue_t1_record_ios_np_sf_ai.*tptp"); 102 103cvc_circqueue_pat = re.compile("circular_queue_t1_native_record_ios_mod_np_sf_ai.*cvc"); 104cvc_queue_pat = re.compile("queue_t1_native_record_ios_np_sf_ai.*cvc"); 105e_circqueue_pat = re.compile("circular_queue_t1_native_record_ios_mod_np_sf_ai.*tptp"); 106e_queue_pat = re.compile("queue_t1_native_record_ios_np_sf_ai.*tptp"); 107 108 109 110 111dir = "/Users/schulz/SOURCES/Projects/VERONA/dp/array/TEST_RESULTS/" 112files = False 113 114options = pylib_io.get_options() 115 116for o in options: 117 if o == "-f": 118 files = True 119 if o[0:2] == "-d": 120 dir = o[2:] 121 if o=="-h": 122 print __doc__ 123 sys.exit() 124 125if dir[-1]!="/": 126 dir = dir + "/" 127 128dir = os.path.expanduser(dir) 129 130plot_list = [] 131 132 133sd = { 134 "CVC" : 1, 135 "CVC Lite" : 2, 136 "CVC (flattened)" : 3, 137 "CVC Lite (flattened)" : 4, 138 "E (sts11), built-in index type" : 5, 139 "E (sts11), axiomatized indices" : 6, 140 "E (sts11)" : 6, # Intentional reuse! 141 "E (good-lpo), built-in index type" : 5, 142 "E (good-lpo), axiomatized indices" : 6, 143 "E (good-lpo)" : 6, # Intentional reuse! 144 "E (sts28)" : 7, 145 "E (std-kbo)" : 7, 146 "E (auto)" : 8 147 } 148 149pylib_graphs.style_dict = sd 150 151# All systems with system-specific input - T1 152 153# Storecomm 154 155data = [ 156 ("CVC" , dir+"protokoll_CVC_Auto", cvc_sc_pat), 157 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_sc_pat), 158 ("E (good-lpo), built-in index type" , dir+"protokoll_E_sts11_t1", e_sc_ni_pat), 159 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_sc_pat) 160 ] 161 162plot = pylib_graphs.plot("Storecomm, T1, Native", data) 163plot_list.append(plot) 164 165# Storecomm_invalid 166 167data = [ 168 ("CVC" , dir+"protokoll_CVC_Auto", cvc_scinv_pat), 169 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_scinv_pat), 170 ("E (good-lpo), built-in index type", dir+"protokoll_E_sts11_t1", e_scinv_ni_pat), 171 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_scinv_pat) 172 ] 173 174plot = pylib_graphs.plot("Storecomm_invalid, T1, Native", data) 175plot_list.append(plot) 176 177#Storeinv 178 179data = [ 180 ("CVC" , dir+"protokoll_CVC_Auto", cvc_si_pat), 181 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_si_pat), 182 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_si_pat) 183 ] 184 185plot = pylib_graphs.plot("Storeinv, T1, Native", data) 186plot_list.append(plot) 187 188#Storeinv_invalid 189 190data = [ 191 ("CVC" , dir+"protokoll_CVC_Auto", cvc_siinv_pat), 192 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_siinv_pat), 193 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_siinv_pat) 194 ] 195 196plot = pylib_graphs.plot("Storeinv_invalid, T1, Native", data) 197plot_list.append(plot) 198 199#Swap 200 201data = [ 202 ("CVC" , dir+"protokoll_CVC_Auto", cvc_sw_pat), 203 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_sw_pat), 204 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_sw_pat) 205 ] 206 207 208plot = pylib_graphs.plot("Swap, T1, Native", data) 209plot_list.append(plot) 210 211#Swap_invalid 212 213data = [ 214 ("CVC" , dir+"protokoll_CVC_Auto", cvc_swinv_pat), 215 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_swinv_pat), 216 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_swinv_pat) 217 ] 218 219plot = pylib_graphs.plot("Swap_invalid, T1, Native", data) 220plot_list.append(plot) 221 222 223 224 225 226# All systems with flattend input - T1 227 228# Storecomm 229 230data = [ 231 ("CVC (flattened)" , dir+"protokoll_CVC_Auto", cvc_scf_pat), 232 ("CVC Lite (flattened)" , dir+"protokoll_CVCL_Auto", cvc_scf_pat), 233 ("E (good-lpo), built-in index type" , dir+"protokoll_E_sts11_t1", e_sc_ni_pat), 234 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_sc_pat), 235 ] 236 237plot = pylib_graphs.plot("Storecomm, T1, Flat", data) 238plot_list.append(plot) 239 240# Storecomm_invalid 241 242data = [ 243 ("CVC (flattened)" , dir+"protokoll_CVC_Auto", cvc_scfinv_pat), 244 ("CVC Lite (flattened)" , dir+"protokoll_CVCL_Auto", cvc_scfinv_pat), 245 ("E (good-lpo), built-in index type", dir+"protokoll_E_sts11_t1", e_scinv_ni_pat), 246 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_scinv_pat), 247 ] 248 249plot = pylib_graphs.plot("Storecomm_invalid, T1, Flat",data) 250plot_list.append(plot) 251 252#Storeinv 253 254data = [ 255 ("CVC" , dir+"protokoll_CVC_Auto", cvc_sif_pat), 256 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_sif_pat), 257 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_si_pat) 258 ] 259 260plot = pylib_graphs.plot("Storeinv, T1, Flat", data) 261plot_list.append(plot) 262 263#Storeinv_invalid 264 265data = [ 266 ("CVC" , dir+"protokoll_CVC_Auto", cvc_sifinv_pat), 267 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_sifinv_pat), 268 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_siinv_pat) 269 ] 270 271plot = pylib_graphs.plot("Storeinv_invalid, T1, Flat", data) 272plot_list.append(plot) 273 274#Swap 275 276data = [ 277 ("CVC" , dir+"protokoll_CVC_Auto", cvc_swf_pat), 278 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_swf_pat), 279 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_sw_pat) 280 ] 281 282plot = pylib_graphs.plot("Swap, T1, Flat", data) 283plot_list.append(plot) 284 285#Swap_invalid 286 287data = [ 288 ("CVC" , dir+"protokoll_CVC_Auto", cvc_swfinv_pat), 289 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_swfinv_pat), 290 ("E (good-lpo)" , dir+"protokoll_E_sts11_t1", e_swinv_pat) 291 ] 292 293plot = pylib_graphs.plot("Swap_invalid, T1, Flat", data) 294plot_list.append(plot) 295 296 297# All systems with system-specific input - T3 on swap 298 299 300#Swap 301 302data = [ 303 ("CVC" , dir+"protokoll_CVC_Auto", cvc_sw_pat), 304 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_sw_pat), 305 ("E (good-lpo)" , dir+"protokoll_E_sts11_t3", e_sw_pat) 306 ] 307 308 309plot = pylib_graphs.plot("Swap, T3, Native", data) 310plot_list.append(plot) 311 312 313data = [ 314 ("CVC" , dir+"protokoll_CVC_Auto", cvc_swf_pat), 315 ("CVC Lite" , dir+"protokoll_CVCL_Auto", cvc_swf_pat), 316 ("E (good-lpo)" , dir+"protokoll_E_sts11_t3", e_sw_pat) 317 ] 318 319 320plot = pylib_graphs.plot("Swap, T3, Flat", data) 321plot_list.append(plot) 322 323 324 325# IOS 326 327data = [ 328 ("CVC" , dir+"protokoll_CVC_Auto_ios", cvc_ios_pat), 329 ("CVC Lite" , dir+"protokoll_CVCL_Auto_ios", cvc_ios_pat), 330 ("E (good-lpo)" , dir+"protokoll_E_sts11_ios", e_ios_pat), 331 ("E (std-kbo)" , dir+"protokoll_E_sts28_ios", e_ios_pat), 332 ] 333 334 335plot = pylib_graphs.plot("IOS", data) 336plot_list.append(plot) 337 338data = [ 339 ("CVC" , dir+"protokoll_CVC_Auto_ios", cvc_ios_pat), 340 ("CVC Lite" , dir+"protokoll_CVCL_Auto_ios", cvc_ios_pat), 341 ("E (std-kbo)" , dir+"protokoll_E_sts28_ios", e_ios_pat) 342 ] 343 344 345plot = pylib_graphs.plot("IOS_opt", data) 346plot_list.append(plot) 347 348# Queues 349 350data = [ 351 ("CVC" , dir+"protokoll_CVC_Auto_ios", cvc_queue_pat), 352 ("CVC Lite" , dir+"protokoll_CVCL_Auto_ios", cvc_queue_pat), 353 ("E (good-lpo)" , dir+"protokoll_E_sts11_ios", e_queue_pat), 354 ] 355 356 357plot = pylib_graphs.plot("Queues", data) 358plot_list.append(plot) 359 360 361# Circular queues 362 363data = [ 364 ("CVC Lite" , dir+"protokoll_CVCL_Auto_ios", cvc_circqueue_pat), 365 ("E (good-lpo)" , dir+"protokoll_E_sts11_ios", e_circqueue_pat), 366 ] 367 368 369plot = pylib_graphs.plot("Circular queues", data) 370plot_list.append(plot) 371 372 373# E for IWIL 374 375 376data = [ 377 ("CVC (flattened)" , dir+"protokoll_CVC_Auto", cvc_scf_pat), 378 ("CVC Lite (flattened)" , dir+"protokoll_CVCL_Auto", cvc_scf_pat), 379 ("E (good-lpo), built-in index type" , dir+"protokoll_E_sts11_t1", e_sc_ni_pat), 380 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_sc_pat) 381 ] 382 383plot = pylib_graphs.plot("Storecomm, Flat, IWIL", data) 384plot_list.append(plot) 385 386 387data = [ 388 ("CVC (flattened)" , dir+"protokoll_CVC_Auto", cvc_scfinv_pat), 389 ("CVC Lite (flattened)" , dir+"protokoll_CVCL_Auto", cvc_scfinv_pat), 390 ("E (good-lpo), built-in index type", dir+"protokoll_E_sts11_t1", e_scinv_ni_pat), 391 ("E (good-lpo), axiomatized indices" , dir+"protokoll_E_sts11_t1", e_scinv_pat) 392 ] 393 394plot = pylib_graphs.plot("Storecomm_Invalid, Flat, IWIL", data) 395plot_list.append(plot) 396 397 398# Create files 399 400 401for i in plot_list: 402 print "Title: "+i.title+ " (linear)"; 403 i.gnuplot(files, None); 404 print "Title: "+i.title+ " (log)"; 405 i.gnuplot(files, True); 406 407