analyse-experiments.php

PHP script to analyse output form LTSmin. - Jeroen Meijer, 25 Jun 2014 10:54

Download (54.3 KB)

 
1
<?php
2
/*
3
 *  -------------- NOTE ----------------
4
 * In order for the regular expression to work you have to make two changes to your PHP configuration.
5
 * In php.ini set/increase:
6
 *  - pcre.backtrack_limit=10000000
7
 *  - pcre.recursion_limit=10000000
8
 */
9

    
10
/*
11
 * At least the following information is collected from the std out
12
 * 
13
 * state-length: length of the state vector
14
 * groups: number of transition groups
15
 * guards: number of guards
16
 * checks: number of times transition relation is expanded
17
 * guard-eval: number of times guard have been evaluated
18
 * next-state: number of times the next-state has been applied
19
 * reach-time: reachability time (w/o setup time)
20
 * states: number of reachable states
21
 * struct-size: size of the datastructure (typically number of BDD nodes)
22
 * next: size of the combined transition relation (number of BDD nodes)
23
 * explored: number of BDD nodes of the projected reachable states for which the transition relation has to be learned
24
 * false: total amount of BDD nodes for states for guards which evaluate to false
25
 * true: total amount of BDD nodes for states for guards which evaluate to true
26
 * exit: exit status of the program
27
 * all-time: reachability time including set up time.
28
 * mem: memory usage reported by memtime
29
 */
30

    
31
// the value of infinity
32
$INFINITY_TIME = 1800;
33
$INFINITY_NODES = 10000000;
34

    
35
// array of models not to include in the results
36

    
37
$skip = array(
38
    // DVE
39
    // mCRL2    
40
    // Promela
41
);
42

    
43
// array of models to allow in the results although they produce incorrect results.
44
$allow = array(
45
);
46

    
47
// array of models to highlight
48
$highlight = array (
49
    "1394-fin.mcrl2.suminst.lps",
50
    "blocks.3.dve2C",
51
    "vasy.lps"
52
);
53

    
54
/*
55
 * Some stuff to write to std err in PHP
56
 */
57
global $errh;
58
$errh = fopen('php://stderr','a');
59

    
60
function echoerr($text) {
61
    fwrite($GLOBALS['errh'],$text);
62
}
63

    
64
function errHandle($errNo, $errStr, $errFile, $errLine) {
65
    $msg = "$errStr in $errFile on line $errLine";
66
    echoerr($msg);
67
    exit(1);
68
}
69

    
70
set_error_handler('errHandle');
71

    
72
$mcrl2_count = array();
73
$promela_count = array();
74
$dve_count = array();
75

    
76
// Path to successful experiments
77
$path0 = "/home/jeroen/gitprojects/rtproposal/report/ext/scripts/out/0";
78
// File to failed experiments (out of time/memory or error)
79
$path1 = "/home/jeroen/gitprojects/rtproposal/report/ext/scripts/out/1/failed";
80

    
81
$results = array();
82

    
83
// extract information for *2lts-sym w/ guard-splitting.
84
function get_symbolic_info_guard($file) {
85
    $regex =    "/2lts-sym: state vector length is (\d+), there are (\d+) groups and (\d+) guards.+" .
86
                "2lts-sym: Exploration took (\d+) group checks, (\d+) label checks and (\d+) next state calls.+" .
87
                "2lts-sym: reachability took \d+\.\d+ real (\d+\.\d+).+" .
88
                "2lts-sym: state space has \d+ \((.+)\) states, (\d+) BDD nodes.+" .
89
                "2lts-sym: group_next: (\d+) nodes total.+" .
90
                "2lts-sym: group_explored: (\d+) nodes total.+" .
91
                "2lts-sym: label_false: (\d+) nodes total.+" .
92
                "2lts-sym: label_true: (\d+) nodes total.+" .
93
                "Exit \[(\d+)\]\n" .
94
                "(\d+\.\d+) user.* Max VSize = (\d+)KB/s";
95
    
96
    $values = array();
97
    
98
    preg_match($regex, file_get_contents($file), $values);
99
            
100
    if (count($values) !== 17) {        
101
        echoerr("Not found 16 matches in symbolic in file '$file'");
102
        exit(1);
103
    }
104
    
105
    $result = array();
106
    
107
    $result["state-length"] = $values[1];
108
    $result["groups"] = $values[2];
109
    $result["guards"] = $values[3];
110
    $result["checks"] = $values[4];
111
    $result["guard-eval"] = $values[5];
112
    $result["next-state"] = $values[6];
113
    $result["reach-time"] = $values[7];
114
    $result["states"] = $values[8];
115
    $result["struct-size"] = $values[9];
116
    $result["next"] = $values[10];
117
    $result["explored"] = $values[11];
118
    $result["false"] = $values[12];
119
    $result["true"] = $values[13];
120
    $result["exit"] = $values[14];
121
    $result["all-time"] = $values[15];
122
    $result["mem"] = $values[16];
123
        
124
    return $result;    
125
    
126
}
127

    
128
// extract information for *lts-sym w/o guard splitting
129
function get_symbolic_info($file) {
130
    $regex =    "/2lts-sym: state vector length is (\d+); there are (\d+) groups.+" .
131
                "2lts-sym: Exploration took (\d+) group checks and (\d+) next state calls.+" .
132
                "2lts-sym: reachability took \d+\.\d+ real (\d+\.\d+).+" .
133
                "2lts-sym: state space has \d+ \((.+)\) states, (\d+) BDD nodes.+" .
134
                "2lts-sym: group_next: (\d+) nodes total.+" .
135
                "2lts-sym: group_explored: (\d+) nodes total.+" .
136
                "Exit \[(\d+)\]\n" .
137
                "(\d+\.\d+) user.* Max VSize = (\d+)KB/s";
138
    
139
    $values = array();
140
    
141
    preg_match($regex, file_get_contents($file), $values);
142
        
143
    if (count($values) !== 13) {        
144
        echoerr("Not found 12 matches in symbolic in file '$file'");
145
        exit(1);
146
    }
147
    
148
    $result = array();
149
    
150
    $result["state-length"] = $values[1];
151
    $result["groups"] = $values[2];
152
    $result["guards"] = "-1";
153
    $result["checks"] = $values[3];
154
    $result["guard-eval"] = "-1";
155
    $result["next-state"] = $values[4];
156
    $result["reach-time"] = $values[5];
157
    $result["states"] = $values[6];
158
    $result["struct-size"] = $values[7];
159
    $result["next"] = $values[8];
160
    $result["explored"] = $values[9];
161
    $result["exit"] = $values[10];
162
    $result["all-time"] = $values[11];
163
    $result["mem"] = $values[12];
164
    $result["false"] = "-1";
165
    $result["true"] = "-1";
166
    
167
    return $result;    
168
    
169
}
170

    
171
// extract information for *2lts-seq
172
function get_sequential_info($file) {    
173
    $regex =    "/2lts-seq: There are (\d+) state labels and.+" .
174
                "2lts-seq: State length is (\d+), there are (\d+) groups.+" .
175
                "2lts-seq: state space \d+ levels, (\d+)states \d+ transitions.+" .
176
                "Exit (\d+)\n" .
177
                "(\d+\.\d+) user.* Max VSize = (\d+)KB/s";
178
    
179
    $values = array();
180
    
181
    $count = preg_match_all($regex, file_get_contents($file), $values);
182
    
183
    if ($count !== 8) {
184
        echoerr("Not found 7 matches in sequential in file '$file'");
185
        exit(1);
186
    }
187
        
188
    $result = array();
189
    
190
    $result["state-length"] = $values[2];
191
    $result["groups"] = $values[3];
192
    $result["guards"] = $values[1];
193
    $result["checks"] = -1;
194
    $result["guard-eval"] = -1;
195
    $result["next-state"] = -1;
196
    $result["reach-time"] = -1;
197
    $result["states"] = $values[4];
198
    $result["struct-size"] = -1;
199
    $result["exit"] = $values[5];
200
    $result["all-time"] = $values[6];
201
    $result["mem"] = $values[7];
202
    $result["next"] = -1;
203
    $result["explored"] = -1;
204
    $result["false"] = -1;
205
    $result["true"] = -1;
206
    
207
    return $result;
208
}
209

    
210
// compute the average
211
function avg($array) {
212
    return round(array_sum($array) / count($array),3);
213
}
214

    
215
// compute the standard deviation (we don't sample)
216
function sd($aValues, $bSample = false)
217
{
218
    $fMean = array_sum($aValues) / count($aValues);
219
    $fVariance = 0.0;
220
    foreach ($aValues as $i)
221
    {
222
        $fVariance += pow($i - $fMean, 2);
223
    }
224
    $fVariance /= ( $bSample ? count($aValues) - 1 : count($aValues) );
225
    return round((float) sqrt($fVariance), 3);
226
}
227

    
228
/**
229
 * Combine all found results. Does the following:
230
 *  - checks if experiments are consistent.
231
 *  - computes avg/sd for reach-time
232
 *  - computes avg/sd for time reported by memtime
233
 *  - computes avg/sd for memory reported by memtime
234
 */
235
function parse_results($results, $repeated) {
236
    $result = array();
237
        
238
    $guard_tau_models = array(
239
        'iprotocol.4.prom.spins'
240
    );    
241
    
242
    foreach ($results as $version=>$frontends) {
243
        $result[$version] = array();
244
        foreach ($frontends as $frontend => $backends) {
245
            foreach ($backends as $backend => $models) {
246
                foreach ($models as $model => $options) {
247
                    $result[$version][$model] = array();
248
                    foreach ($options as $option => $experiments) {
249
                        $result[$version][$model][$option] = array();
250
                        
251
                        $result[$version][$model][$option]["reach-time"] = array();
252
                        $result[$version][$model][$option]["all-time"] = array();
253
                        $result[$version][$model][$option]["mem"] = array();
254
                        foreach ($experiments as $experiment => $values) {
255
                            
256
                            $guard_tau = false;
257

    
258
                            if ($values["exit"] !== "0") {
259
                                echoerr("Experiment $version -> $frontend -> $backend -> $model -> $option -> $experiment exited with non-zero.");
260
                                exit(1);
261
                            }
262

    
263
                            if (array_key_exists("state-length", $result[$version][$model][$option])) {
264
                                if ($result[$version][$model][$option]["state-length"] !== $values["state-length"]) {
265
                                    echoerr("state-length does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
266
                                    exit(1);
267
                                }
268
                            }
269

    
270
                            if (array_key_exists("groups", $result[$version][$model][$option])) {
271
                                if ($result[$version][$model][$option]["groups"] !== $values["groups"]) {
272
                                    echoerr("groups does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
273
                                    exit(1);
274
                                }
275
                            }
276

    
277
                            if (array_key_exists("guards", $result[$version][$model][$option])) {
278
                                if ($result[$version][$model][$option]["guards"] !== $values["guards"]) {
279
                                    echoerr("guards does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
280
                                    exit(1);
281
                                }
282
                            }
283

    
284
                            if (array_key_exists("checks", $result[$version][$model][$option])) {
285
                                if ($result[$version][$model][$option]["checks"] !== $values["checks"]) {
286
                                    echoerr("checks does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
287
                                    exit(1);
288
                                }
289
                            }
290

    
291
                            if (array_key_exists("guard-eval", $result[$version][$model][$option])) {
292
                                if ($result[$version][$model][$option]["guard-eval"] !== $values["guard-eval"]) {
293
                                    echoerr("guard-eval does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
294
                                    exit(1);
295
                                }
296
                            }
297

    
298
                            if (array_key_exists("next-state", $result[$version][$model][$option])) {
299
                                if ($result[$version][$model][$option]["next-state"] !== $values["next-state"]) {
300
                                    echoerr("next-state does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
301
                                    exit(1);
302
                                }
303
                            }
304

    
305
                            if (array_key_exists("states", $result[$version][$model][$option])) {
306
                                if ($result[$version][$model][$option]["states"] !== $values["states"]) {
307
                                    echoerr("states does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
308
                                    exit(1);
309
                                }
310
                            }
311

    
312
                            if (array_key_exists("struct-size", $result[$version][$model][$option])) {
313
                                if ($result[$version][$model][$option]["struct-size"] !== $values["struct-size"]) {
314
                                    echoerr("struct-size does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
315
                                    exit(1);
316
                                }
317
                            }
318

    
319
                            if (array_key_exists("next", $result[$version][$model][$option])) {
320
                                if ($result[$version][$model][$option]["next"] !== $values["next"]) {                                                                        
321
                                    echoerr("next does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
322
                                    exit(1);
323
                                }
324
                            }
325

    
326
                            if (array_key_exists("explored", $result[$version][$model][$option])) {
327
                                if ($result[$version][$model][$option]["explored"] !== $values["explored"]) {
328
                                    echoerr("explored does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
329
                                    exit(1);
330
                                }
331
                            }
332

    
333
                            if (array_key_exists("false", $result[$version][$model][$option])) {
334
                                if ($result[$version][$model][$option]["false"] !== $values["false"]) {                                    
335
                                    if (in_array($model, $guard_tau_models)) {
336
                                        $guard_tau = true;
337
                                        echoerr("false does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value, but this is okay.\n");                                        
338
                                    } else {                                    
339
                                        echoerr("false does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
340
                                        exit(1);
341
                                    }
342
                                }
343
                            }
344

    
345
                            if (array_key_exists("true", $result[$version][$model][$option])) {
346
                                if ($result[$version][$model][$option]["true"] !== $values["true"]) {                                    
347
                                    if (in_array($model, $guard_tau_models)) {
348
                                        $guard_tau = true;
349
                                        echoerr("false does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value, but this is okay.\n");  
350
                                    } else {  
351
                                        echoerr("true does not match for $version -> $frontend -> $backend -> $model -> $option -> $experiment with previous value");
352
                                        exit(1);
353
                                    }
354
                                }
355
                            }
356

    
357
                            $result[$version][$model][$option]["backend"] = $backend;
358
                            $result[$version][$model][$option]["frontend"] = $frontend;
359
                            $result[$version][$model][$option]["state-length"] = $values["state-length"];
360
                            $result[$version][$model][$option]["groups"] = $values["groups"];
361
                            $result[$version][$model][$option]["guards"] = $values["guards"];
362
                            $result[$version][$model][$option]["checks"] = $values["checks"];
363
                            $result[$version][$model][$option]["guard-eval"] = $values["guard-eval"];
364
                            $result[$version][$model][$option]["next-state"] = $values["next-state"];
365
                            $result[$version][$model][$option]["states"] = $values["states"];
366
                            $result[$version][$model][$option]["struct-size"] = $values["struct-size"];
367
                            $result[$version][$model][$option]["all-time"][] = $values["all-time"];
368
                            $result[$version][$model][$option]["mem"][] = $values["mem"];
369
                            $result[$version][$model][$option]["next"] = $values["next"];
370
                            $result[$version][$model][$option]["explored"] = $values["explored"];
371
                            $result[$version][$model][$option]["false"] = $values["false"] . ($guard_tau ? "!" : "");
372
                            $result[$version][$model][$option]["true"] = $values["true"] . ($guard_tau ? "!" : "");
373

    
374
                            if ($values["reach-time"] === -1) {
375
                                $result[$version][$model][$option]["reach-time"] = "n/a";
376
                            } else {
377
                                $result[$version][$model][$option]["reach-time"][] = $values["reach-time"];
378
                            }
379
                        }
380
                    }
381
                }
382
            }
383
        }
384
    }
385
        
386
    foreach ($result as $version=>$models) {
387
        foreach($models as $model => $options) {
388
            foreach ($options as $option => $values) {
389
                if (is_array($result[$version][$model][$option]["reach-time"])) {
390
                    if (count($result[$version][$model][$option]["reach-time"]) != $repeated) {
391
                        echoerr("reach-time for $version -> $model -> $option does not have ". $repeated ." elements");
392
                        exit(1);
393
                    }
394

    
395
                    $result[$version][$model][$option]["reach-time-avg"] = avg($result[$version][$model][$option]["reach-time"]);
396
                    $result[$version][$model][$option]["reach-time-sd"] = sd($result[$version][$model][$option]["reach-time"]);
397
                    
398
                    $result[$version][$model][$option]["n"] = count($result[$version][$model][$option]["reach-time"]);
399
                    
400
                } else {            
401
                    $result[$version][$model][$option]["reach-time-avg"] = "n/a";
402
                    $result[$version][$model][$option]["reach-time-sd"] = "n/a";
403
                }
404
                
405
                unset($result[$version][$model][$option]["reach-time"]);
406

    
407
                $result[$version][$model][$option]["all-time-avg"] = avg($result[$version][$model][$option]["all-time"]);
408
                $result[$version][$model][$option]["all-time-sd"] = sd($result[$version][$model][$option]["all-time"]);
409
                unset($result[$version][$model][$option]["all-time"]);
410

    
411
                $result[$version][$model][$option]["mem-avg"] = avg($result[$version][$model][$option]["mem"]);
412
                $result[$version][$model][$option]["mem-sd"] = sd($result[$version][$model][$option]["mem"]);
413
                unset($result[$version][$model][$option]["mem"]);
414
            }
415
        }
416
    }
417
        
418
    return $result;
419
    
420
}
421

    
422
// Parse all failed experiments, puts a '-' in all rows in the CSV.
423
function get_failed_info($file) {
424
    
425
    $result = array();
426
    
427
    $string = file_get_contents($file);
428
   
429
    foreach (explode("\n", $string) as $line) {
430
        
431
        if (strlen($line) > 0) {
432
            
433
            // extract the required information (which experiment is this)
434
            $regex = "#\/home\/jeroen\/\.local\/bin\/memtime\/bin\/memtime -m\d+ -c\d+ \/home\/jeroen\/\.local\/bin\/ltsmin\/ltsmin\-(.+)\/bin\/(.+) -v (.+) \/home\/jeroen\/experiments\/in\/.+\/(.+)#";
435

    
436
            $values = array();
437

    
438
            preg_match($regex, $line, $values);
439

    
440
            $count = count($values);
441

    
442
            if ($count !== 5) {
443
                echoerr("Not found 4 matches in failed in file '$file'");
444
                exit(1);
445
            }
446

    
447
            $frontend = "";
448
            $backend = "";
449
            $command = $values[2];
450
            if (strpos($command, "lps2lts-sym") !== false) {
451
                $frontend = "mCRL2";
452
                $backend = "sym";
453
            } else if (strpos($command, "lps2lts-seq") !== false) {
454
                $frontend = "mCRL2";
455
                $backend = "seq";
456
            } else if (strpos($command, "prom2lts-seq") !== false) {
457
                $frontend = "Promela";
458
                $backend = "seq";
459
            } else if (strpos($command, "prom2lts-sym") !== false) {
460
                $frontend = "Promela";
461
                $backend = "sym";
462
            } else if (strpos($command, "dve2lts-sym") !== false) {
463
                $frontend = "DVE";
464
                $backend = "sym";
465
            } else {
466
                echoerr("unsupported backend/frontend");
467
                exit(1);
468
            }             
469

    
470
            $version = $values[1];
471
            $model = $values[4];
472
            $options = $values[3];
473
            
474
            $test_options = $options;
475
            
476
            if (strpos($test_options, "--por") !== false) {
477
                $options = "POR";
478
            } else if (strpos($test_options, "--order=chain-prev") !== false) {
479
                $options = "chain-prev";
480
            } else if (strpos($test_options, "--order=bfs-prev") !== false) {
481
                $options = "bfs-prev";
482
            }
483
            
484
            if (strpos($test_options, "--saturation=none") !== false) {
485
                $options .= ",no-sat";
486
            } else if (strpos($test_options, "--saturation=sat-like") !== false) {
487
                $options .= ",sat-like";                
488
            } else if (strpos($test_options, "--saturation=sat-loop") !== false) {
489
                $options .= ",sat-loop";                
490
            } else {
491
                $options .= ",no-sat";
492
            }
493
               
494
            if (strpos($test_options, "-rcn,ru,cs,rs,cw,rs,w2W,W2+") !== false) {
495
                $options .= ",cn;ru;cs;rs;cw;rs";   
496
                $version = "next";
497
            } else if (strpos($test_options, "-rcn,ru,cs,rs,cw,rs") !== false) {
498
                $options .= ",cn;ru;cs;rs;cw;rs";       
499
            } else if (strpos($test_options, "-rcn,ru,w2W,W2+") !== false) {
500
                $version = "next";
501
                $options .= ",cn;ru";                 
502
            } else if (strpos($test_options, "-rcn,ru") !== false) {
503
                $options .= ",cn;ru";                 
504
            } else if (strpos($test_options, "-rcs,rs,cw,rs,w2W,W2+") !== false) {
505
                $version = "next";
506
                $options .= ",cs;rs;cw;rs";                 
507
            } else if (strpos($test_options, "-rcs,rs,cw,rs") !== false) {
508
                $options .= ",cs;rs;cw;rs";                 
509
            } else if (strpos($test_options, "-rw2W,W2+") !== false) {
510
                $version = "next";
511
                $options .= ",";                 
512
            } else {
513
                $options .= ",";
514
            }
515
            
516
            if (!array_key_exists($version, $result)) {
517
                $result[$version] = array();
518
            }
519

    
520
            if (!array_key_exists($model, $result[$version])) {
521
                $result[$version][$model] = array();
522
            }
523

    
524
            if (!array_key_exists($options, $result[$version][$model])) {
525
                $result[$version][$model][$options] = array();
526
            }
527

    
528
            $result[$version][$model][$options]["frontend"] = $frontend;
529
            $result[$version][$model][$options]["backend"] = $backend;
530
            $result[$version][$model][$options]['n'] = "0";
531
            $result[$version][$model][$options]['state-length'] = "-";
532
            $result[$version][$model][$options]['groups'] = "-";
533
            $result[$version][$model][$options]['guards'] = "-";
534
            $result[$version][$model][$options]['checks'] = "-";
535
            $result[$version][$model][$options]['guard-eval'] = "-";
536
            $result[$version][$model][$options]['next-state'] = "-";
537
            $result[$version][$model][$options]['reach-time-avg'] = "-";
538
            $result[$version][$model][$options]['reach-time-sd'] = "-";
539
            $result[$version][$model][$options]['states'] = "-";
540
            $result[$version][$model][$options]['struct-size'] = "-";
541
            $result[$version][$model][$options]['next'] = "-";
542
            $result[$version][$model][$options]['explored'] = "-";
543
            $result[$version][$model][$options]['false'] = "-";
544
            $result[$version][$model][$options]['true'] = "-";
545
            $result[$version][$model][$options]['all-time-avg'] = "-";
546
            $result[$version][$model][$options]['all-time-sd'] = "-";
547
            $result[$version][$model][$options]['mem-avg'] = "-";
548
            $result[$version][$model][$options]['mem-sd'] = "-";
549
        }
550
    }
551
    
552
    return $result;
553
}
554

    
555
// function to rename model names.
556
function get_model($model) {
557
    
558
    $result = $model;
559
    
560
    switch($model) {
561
        case "diningphil-10.prom.spins":
562
            $result = "phil-10.pr";
563
        break;
564
        case "diningphil-15.prom.spins":
565
            $result = "phil-15.pr";
566
        break;
567
        case "lamport_nonatomic.5.dve2C":
568
            $result = "lamport_na.5.dve2C";
569
        break;
570
    }
571
    
572
    return $result;
573
}
574

    
575
// create a CSV file for $frontend and $opt.
576
function to_csv($array, $frontend, $opt, $models = array()) {
577
    
578
    $string = 'model,backend,n,N,K,M,checks,gev,ns,rt,rtsd,R,nodesR,nodesRel,nodesPiR,nodesF,nodesT,at,atsd,mem,memsd'."\n";
579
        
580
    foreach ($array as $model => $options) {
581
        ksort($options);
582
        foreach ($options as $option => $values) {
583
                        
584
            if (($frontend != null && $values['frontend'] === $frontend && $opt != null && $option === $opt) || in_array($model, $models)) {
585
            
586
                $string .= str_replace("_", "\\xline ", get_model($model)) . ",";
587
                $string .= $values['backend'] . ",";
588
                $string .= $values['n'] . ",";
589
                $string .= $values['state-length'] . ",";
590
                $string .= $values['groups'] . ",";
591
                $string .= $values['guards'] === -1 ? "n/a," : $values['guards'] . ",";
592
                $string .= $values['checks'] === -1 ? "n/a," : $values['checks'] . ",";
593
                $string .= $values['guard-eval'] === -1 ? "n/a," : $values['guard-eval'] . ",";
594
                $string .= $values['next-state'] === -1 ? "n/a," : $values['next-state'] . ",";
595
                $string .= $values['reach-time-avg'] . ",";
596
                $string .= $values['reach-time-sd'] . ",";
597
                $string .= $values['states'] . ",";
598
                $string .= $values['struct-size'] === -1 ? "n/a," : $values['struct-size'] . ",";
599
                $string .= $values['next'] === -1 ? "n/a," : $values['next'] . ",";
600
                $string .= $values['explored'] === -1 ? "n/a," : $values['explored'] . ",";
601
                $string .= $values['false'] === -1 ? "n/a," : $values['false'] . ",";
602
                $string .= $values['true'] === -1 ? "n/a," : $values['true'] . ",";
603
                $string .= $values['all-time-avg'] . ",";
604
                $string .= $values['all-time-sd'] . ",";
605
                $string .= $values['mem-avg'] . ",";
606
                $string .= $values['mem-sd'];
607

    
608
                $string .= "\n";
609
            }
610
        }
611
    }
612
    
613
    return $string;
614
}
615

    
616
// create a CSV file for $models
617
function to_csv_all($array, $models = array()) {
618
    
619
    $string = 'model,backend,order,dm,n,N,K,M,checks,gev,ns,rt,rtsd,R,nodesR,nodesRel,nodesPiR,nodesF,nodesT,at,atsd,mem,memsd'."\n";
620
    
621
    foreach ($array as $version=>$result) {
622
        
623
        foreach ($result as $model => $options) {
624
            ksort($options);
625
            foreach ($options as $option => $values) {
626

    
627
                if (in_array($model, $models)) {
628

    
629
                    $string .= str_replace("_", "\\xline ", get_model($model)) . ",";
630
                    $string .= $values['backend'] . ",";
631

    
632
                    $opts = explode(",", $option);
633
                    $string .= $opts[0] . ",";
634
                    $string .= $opts[2] . ($version == "next" ? ";w2W;W2+" : "") . ",";
635

    
636
                    $string .= $values['n'] . ",";
637
                    $string .= $values['state-length'] . ",";
638
                    $string .= $values['groups'] . ",";
639
                    $string .= $values['guards'] === -1 ? "n/a," : $values['guards'] . ",";
640
                    $string .= $values['checks'] === -1 ? "n/a," : $values['checks'] . ",";
641
                    $string .= $values['guard-eval'] === -1 ? "n/a," : $values['guard-eval'] . ",";
642
                    $string .= $values['next-state'] === -1 ? "n/a," : $values['next-state'] . ",";
643
                    $string .= $values['reach-time-avg'] . ",";
644
                    $string .= $values['reach-time-sd'] . ",";
645
                    $string .= $values['states'] . ",";
646
                    $string .= $values['struct-size'] === -1 ? "n/a," : $values['struct-size'] . ",";
647
                    $string .= $values['next'] === -1 ? "n/a," : $values['next'] . ",";
648
                    $string .= $values['explored'] === -1 ? "n/a," : $values['explored'] . ",";
649
                    $string .= $values['false'] === -1 ? "n/a," : $values['false'] . ",";
650
                    $string .= $values['true'] === -1 ? "n/a," : $values['true'] . ",";
651
                    $string .= $values['all-time-avg'] . ",";
652
                    $string .= $values['all-time-sd'] . ",";
653
                    $string .= $values['mem-avg'] . ",";
654
                    $string .= $values['mem-sd'];
655

    
656
                    $string .= "\n";
657
                }
658
            }
659
        }
660
    }
661
    
662
    return $string;
663
}
664

    
665
// create a csv file we can use for R.
666
function to_r($array, &$promela_count, &$mcrl2_count, &$dve_count, $infinity_time, $infinity_nodes) {
667
    
668
    $string = 'model,options,version,frontend,rt,nodes'."\n";
669
    ksort($array);
670
    foreach ($array as $version=>$models) {
671
        ksort($models);
672
        foreach ($models as $model => $options) {
673
            ksort($options);
674
            foreach ($options as $option => $values) {
675
                
676
                $string .= get_model($model) . ",";
677
                $string .= '"'.$option.'"' . ",";
678
                $string .= $version . ",";
679
                $string .= $values['frontend'] . ",";
680
                $string .= (($values['reach-time-avg'] === "-") ? $infinity_time : (($values['reach-time-avg'] < 0.1000000) ? 0.1 : $values['reach-time-avg'])). ","; 
681
                $string .= ($values['reach-time-avg'] === "-") ? $infinity_nodes : $values['struct-size'] + $values['next']; 
682
                
683

    
684
                $string .= "\n";
685
                
686
                if ($values['frontend'] === "Promela") $promela_count[$model] = $model;
687
                if ($values['frontend'] === "mCRL2") $mcrl2_count[$model] = $model;
688
                if ($values['frontend'] === "DVE") $dve_count[$model] = $model;
689
            }
690
        }
691
    }
692
    
693
    return $string;
694
}
695

    
696
// commandline options
697
$opt = $argv;
698

    
699
// usage information
700
if(!isset($opt[1])) {
701
    echoerr("Usage: {$opt[0]} output [--auto-add-missing]");
702
    exit(1);
703
}
704

    
705
$output = realpath($opt[1]);
706

    
707
// make sure output directory exists.
708
if (!file_exists($output)) {
709
    echoerr("Directory '{$opt[1]}' does not exist.");
710
    exit(1);
711
}
712

    
713
$repeated = -1;
714

    
715
// iterate over all successful experiments.
716
foreach (new DirectoryIterator($path0) as $fileInfo) {
717
        
718
    if ($fileInfo->isDot()) continue;
719
        
720
    $file = explode("_", $fileInfo->getBasename());
721
                
722
    $i = $file[0];
723
    
724
    $repeated = $repeated > $i ? $repeated : $i;
725
    
726
    $version = $file[1];
727
    
728
    $command = $file[2];
729
    $options = $file[3];
730
        
731
    $model = "";
732
    for ($j = 4; $j < count($file); $j++) {
733
        $model .= $file[$j];
734
        if($j+1 < count($file)) $model .= "_";
735
    }
736
    
737
    $model = basename($model);     
738
    
739
    if (in_array($model, $skip)) continue;
740
    
741
    $frontend = "";
742
    $backend = "";
743
    
744
    // find a nice name for the frontend and backend
745
    if (strpos($command, "lps2lts-sym") !== false) {
746
        $frontend = "mCRL2";
747
        $backend = "sym";
748
    } else if (strpos($command, "lps2lts-seq") !== false) {
749
        $frontend = "mCRL2";
750
        $backend = "seq";
751
    } else if (strpos($command, "prom2lts-seq") !== false) {
752
        $frontend = "Promela";
753
        $backend = "seq";
754
    } else if (strpos($command, "prom2lts-sym") !== false) {
755
        $frontend = "Promela";
756
        $backend = "sym";
757
    } else if (strpos($command, "dve2lts-sym") !== false) {
758
        $frontend = "DVE";
759
        $backend = "sym";
760
    } else {
761
        echoerr("unsupported backend/frontend");
762
        exit(1);
763
    }     
764
    
765
    $test_options = $options;
766
    
767
    // find a nice name for the options used.
768
    if (strpos($test_options, "--por") !== false) {
769
        $options = "POR";
770
    } else if (strpos($test_options, "--order=chain-prev") !== false) {
771
        $options = "chain-prev";
772
    } else if (strpos($test_options, "--order=bfs-prev") !== false) {
773
        $options = "bfs-prev";
774
    }       
775
            
776
    if (strpos($test_options, "--saturation=none") !== false) {
777
        $options .= ",no-sat";
778
    } else if (strpos($test_options, "--saturation=sat-like") !== false) {
779
        $options .= ",sat-like";                
780
    } else if (strpos($test_options, "--saturation=sat-loop") !== false) {
781
        $options .= ",sat-loop";                
782
    } else {
783
        $options .= ",no-sat";
784
    }
785
               
786
    if (strpos($test_options, "-rcn,ru,cs,rs,cw,rs,w2W,W2+") !== false) {
787
        $options .= ",cn;ru;cs;rs;cw;rs";   
788
        $version = "next";
789
    } else if (strpos($test_options, "-rcn,ru,cs,rs,cw,rs") !== false) {
790
        $options .= ",cn;ru;cs;rs;cw;rs";       
791
    } else if (strpos($test_options, "-rcn,ru,w2W,W2+") !== false) {
792
        $version = "next";
793
        $options .= ",cn;ru";                 
794
    } else if (strpos($test_options, "-rcn,ru") !== false) {
795
        $options .= ",cn;ru";                 
796
    } else if (strpos($test_options, "-rcs,rs,cw,rs,w2W,W2+") !== false) {
797
        $version = "next";
798
        $options .= ",cs;rs;cw;rs";                 
799
    } else if (strpos($test_options, "-rcs,rs,cw,rs") !== false) {
800
        $options .= ",cs;rs;cw;rs";                 
801
    } else if (strpos($test_options, "-rw2W,W2+") !== false) {
802
        $version = "next";
803
        $options .= ",";                 
804
    } else {
805
        $options .= ",";
806
    }
807
    
808
    // for each file analyze the std out.
809
    $result = array();
810
    if ($backend === "sym") {
811
        if ($version === "guard") {
812
            $result = get_symbolic_info_guard($fileInfo->getRealPath());
813
        } else {            
814
            $result = get_symbolic_info($fileInfo->getRealPath());
815
        }
816
    } else if($backend === "seq") {
817
        $result = get_sequential_info($fileInfo->getRealPath());
818
    }    
819
    
820
    // put everything in one array.
821
    $results[$version][$frontend][$backend][$model][$options][$i] = $result;    
822
    
823
}
824
    
825
// parse okey experiments
826
$results = parse_results($results, $repeated);
827

    
828
$new_res = $results;
829

    
830
$failed = array();
831

    
832
if (isset($opt[2]) && $opt[2] === "--auto-add-missing") {
833
    
834
    $models_options = array();
835
    
836
    foreach($results as $version=>$models) {
837
        foreach ($models as $model => $options) {
838
            foreach ($options as $option=>$values) {
839
                
840
                if (!array_key_exists($model, $models_options)) {
841
                    $models_options[$model] = array();
842
                }
843
                
844
                if (!array_key_exists($option, $models_options[$model])) {
845
                    $models_options[$model][$option] = array();
846
                }
847
                
848
                if (!array_key_exists($values['backend'], $models_options[$model][$option])) {
849
                    $models_options[$model][$option][$values['backend']] = array();
850
                }
851
                
852
                if (!array_key_exists($values['frontend'], $models_options[$model][$option][$values['backend']])) {
853
                    $models_options[$model][$option][$values['backend']][$values['frontend']] = array();
854
                }
855
                
856
                $models_options[$model][$option][$values['backend']][$values['frontend']] = 1;
857
            }
858
        }
859
    }
860
        
861
    foreach ($models_options as $model=>$options) {
862
        foreach ($options as $option=>$backends) {
863
            foreach ($backends as $backend=>$frontends) {
864
                foreach ($frontends as $frontend=>$blaat) {
865
                    foreach (array("guard", "rw", "next") as $version) {
866
                                                                        
867
                        if (!array_key_exists($version, $results) || !array_key_exists($model, $results[$version]) || !array_key_exists($option, $results[$version][$model])) {
868

    
869
                            
870
                            if (!array_key_exists($version, $failed)) {
871
                                $failed[$version] = array();
872
                            }
873

    
874
                            if (!array_key_exists($model, $failed[$version])) {
875
                                $failed[$version][$model] = array();
876
                            }
877

    
878
                            if (!array_key_exists($option, $failed[$version][$model])) {
879
                                $failed[$version][$model][$option] = array();
880
                            }
881

    
882
                            $failed[$version][$model][$option]["frontend"] = $frontend;
883
                            $failed[$version][$model][$option]["backend"] = $backend;
884
                            $failed[$version][$model][$option]['n'] = "0";
885
                            $failed[$version][$model][$option]['state-length'] = "-";
886
                            $failed[$version][$model][$option]['groups'] = "-";
887
                            $failed[$version][$model][$option]['guards'] = "-";
888
                            $failed[$version][$model][$option]['checks'] = "-";
889
                            $failed[$version][$model][$option]['guard-eval'] = "-";
890
                            $failed[$version][$model][$option]['next-state'] = "-";
891
                            $failed[$version][$model][$option]['reach-time-avg'] = "-";
892
                            $failed[$version][$model][$option]['reach-time-sd'] = "-";
893
                            $failed[$version][$model][$option]['states'] = "-";
894
                            $failed[$version][$model][$option]['struct-size'] = "-";
895
                            $failed[$version][$model][$option]['next'] = "-";
896
                            $failed[$version][$model][$option]['explored'] = "-";
897
                            $failed[$version][$model][$option]['false'] = "-";
898
                            $failed[$version][$model][$option]['true'] = "-";
899
                            $failed[$version][$model][$option]['all-time-avg'] = "-";
900
                            $failed[$version][$model][$option]['all-time-sd'] = "-";
901
                            $failed[$version][$model][$option]['mem-avg'] = "-";
902
                            $failed[$version][$model][$option]['mem-sd'] = "-";
903
                        
904
                        }
905
                    }
906
                }
907
            }
908
        }
909
    }
910
    
911
} else {
912

    
913
    // parse failed experiments
914
    $failed = get_failed_info($path1);
915
}
916

    
917
// combile all successful experiments with the failed experiments.
918
foreach ($results as $version => $result) {
919

    
920
    if (isset($failed[$version])) {
921
        foreach ($failed[$version] as $model => $options) {
922
            foreach ($options as $option => $fail) {
923
                $new_res[$version][$model][$option] = $fail;
924
            }
925
        }
926
    }
927
}
928

    
929
// remove all experiments which ran out of time for all versions (next/rw/guard), these are not interesting.
930
$test_results = $new_res;
931
$new_res = array();
932
$useless_count = 0;
933
foreach($test_results as $version=>$models) {
934
    foreach ($models as $model=>$options) {
935
        foreach($options as $option=>$values) {
936
            if ($values['reach-time-avg'] !== "-" && $values['reach-time-avg'] >= 0.100000000000) {
937
                foreach ($test_results as $version_good => $models_good) {
938
                    
939
                    if (!array_key_exists($version_good, $new_res)) {
940
                        $new_res[$version_good] = array();
941
                    }
942
                    
943
                    if (!array_key_exists($model, $new_res[$version_good])) {
944
                        $new_res[$version_good][$model] = array();
945
                    }
946
//                    foreach ($options as $option_good=>$values_good) {
947
//                        $new_res[$version_good][$model][$option_good] = $test_results[$version_good][$model][$option_good];
948
//                    }
949
                    $new_res[$version_good][$model][$option] = $test_results[$version_good][$model][$option];
950
                }
951
            } else {                
952
                $useless_count++;
953
            }
954
        }
955
    }
956
}
957
echoerr("Removed '$useless_count' useless results (exist rt < infinity).\n");
958

    
959
echoerr("Comparing state spaces\n");
960

    
961
$test_results = $new_res;
962
$new_res = array();
963

    
964
$false_models = array();
965

    
966
foreach (array("next" => "rw") as $old=>$new) {
967
    foreach ($test_results[$old] as $model=>$options) {
968
        foreach ($options as $option=>$values) {
969
            
970
            if (array_key_exists($new, $test_results) && array_key_exists($model, $test_results[$new]) && array_key_exists($option, $test_results[$new][$model])) {
971
                $new_values = $test_results[$new][$model][$option];
972
                        
973
                if ($values['states'] !== "-" && $new_values['states'] !== "-" && $values['states'] != $new_values['states']) {
974
                    echoerr("$model - $option do not match ($old: ".$values['states'].", $new: ".$new_values['states'].")\n");
975
                    $false_models[$model] = $model;
976
                } 
977
            }
978
        }
979
        
980
    }
981
}
982

    
983
foreach (array("next" => "rw") as $old=>$new) {
984
    foreach ($test_results[$old] as $model=>$options) {        
985
        if (!in_array($model, $false_models) || in_array($model, $allow)) {
986
            foreach ($options as $option=>$values) {
987
                
988
                if (!array_key_exists($old, $new_res)) {
989
                    $new_res[$old] = array();
990
                }
991

    
992
                if (!array_key_exists($model, $new_res[$old])) {
993
                    $new_res[$old][$model] = array();
994
                }
995
                $new_res[$old][$model][$option] = $values;
996
                                
997
                if (array_key_exists($new, $test_results) && array_key_exists($model, $test_results[$new]) && array_key_exists($option, $test_results[$new][$model])) {
998
                
999
                    if (!array_key_exists($new, $new_res)) {
1000
                        $new_res[$new] = array();
1001
                    }
1002

    
1003
                    if (!array_key_exists($model, $new_res[$new])) {
1004
                        $new_res[$new][$model] = array();
1005
                    }
1006

    
1007
                    $new_res[$new][$model][$option] = $test_results[$new][$model][$option];
1008
                }
1009
                
1010
            }
1011
        }
1012
    }
1013
}
1014

    
1015
// write results to a csv file for every combination of frontend and options.
1016
foreach ($new_res as $version => $result) {     
1017
    ksort($result);
1018
    
1019
    file_put_contents($output."/".$version."-promela-bfs-prev-no-sat.csv", to_csv($result, "Promela", "bfs-prev;no-sat"));
1020
    file_put_contents($output."/".$version."-promela-bfs-prev-sat-like.csv", to_csv($result, "Promela", "bfs-prev;sat-like"));
1021
    file_put_contents($output."/".$version."-promela-bfs-prev-sat-loop.csv", to_csv($result, "Promela", "bfs-prev;sat-loop"));
1022
    file_put_contents($output."/".$version."-promela-chain-prev-no-sat.csv", to_csv($result, "Promela", "chain-prev;no-sat"));
1023
    file_put_contents($output."/".$version."-promela-chain-prev-sat-like.csv", to_csv($result, "Promela", "chain-prev;sat-like"));
1024
    file_put_contents($output."/".$version."-promela-chain-prev-sat-loop.csv", to_csv($result, "Promela", "chain-prev;sat-loop"));
1025
    
1026
    file_put_contents($output."/".$version."-divine-bfs-prev-no-sat.csv", to_csv($result, "DVE", "bfs-prev;no-sat"));
1027
    file_put_contents($output."/".$version."-divine-bfs-prev-sat-like.csv", to_csv($result, "DVE", "bfs-prev;sat-like"));
1028
    file_put_contents($output."/".$version."-divine-bfs-prev-sat-loop.csv", to_csv($result, "DVE", "bfs-prev;sat-loop"));
1029
    file_put_contents($output."/".$version."-divine-chain-prev-no-sat.csv", to_csv($result, "DVE", "chain-prev;no-sat"));
1030
    file_put_contents($output."/".$version."-divine-chain-prev-sat-like.csv", to_csv($result, "DVE", "chain-prev;sat-like"));
1031
    file_put_contents($output."/".$version."-divine-chain-prev-sat-loop.csv", to_csv($result, "DVE", "chain-prev;sat-loop"));
1032
    
1033
    file_put_contents($output."/".$version."-mcrl-bfs-prev-no-sat.csv", to_csv($result, "mCRL2", "bfs-prev;no-sat"));
1034
    file_put_contents($output."/".$version."-mcrl-bfs-prev-sat-like.csv", to_csv($result, "mCRL2", "bfs-prev;sat-like"));
1035
    file_put_contents($output."/".$version."-mcrl-bfs-prev-sat-loop.csv", to_csv($result, "mCRL2", "bfs-prev;sat-loop"));
1036
    file_put_contents($output."/".$version."-mcrl-chain-prev-no-sat.csv", to_csv($result, "mCRL2", "chain-prev;no-sat"));
1037
    file_put_contents($output."/".$version."-mcrl-chain-prev-sat-like.csv", to_csv($result, "mCRL2", "chain-prev;sat-like"));
1038
    file_put_contents($output."/".$version."-mcrl-chain-prev-sat-loop.csv", to_csv($result, "mCRL2", "chain-prev;sat-loop"));
1039
}
1040

    
1041
file_put_contents($output."/highlights.csv", to_csv_all($new_res, $highlight));
1042

    
1043
// write the data for R
1044
file_put_contents($output."/scatter.csv", to_r($new_res, $promela_count, $mcrl2_count, $dve_count, $INFINITY_TIME, $INFINITY_NODES));
1045

    
1046
// create latex text for all tables.
1047

    
1048
// for rw w/o our changes
1049
$rw_tex_wo = "\n".'\begin{sidewaystable}[H]
1050
\resultcaption{Results w/o read-write separation for \%s{} (%s)}
1051
\footnotesize
1052
\csvreader[tabular=|l|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|,
1053
    table head=\hline model & backend & n & $N$ & $K$ & checks & ns & $\overline{\text{rt}}$ & rt-$\sigma$ & $\vert
1054
\mathcal{R}\vert$ & $\llbracket\mathcal{R}\rrbracket$ & $\llbracket\transrelexpr\rrbracket$ & $\llbracket\pi(\mathcal{R})\rrbracket$ &
1055
$\overline{\text{at}}$ & at-$\sigma$ & $\overline{\text{mem}}$ & mem-$\sigma$\\\\\hline, late after line=\\\\\hline]
1056
{../ext/scripts/csv/%s-%s-%s.csv}{model=\model, backend=\backend, n=\n, N=\N, K=\K,
1057
checks=\checks, ns=\ns, rt=\rt, rtsd=\rtsd, R=\R, nodesR=\nodesR, nodesRel=\nodesRel, nodesPiR=\nodesPiR, at=\at, atsd=\atsd, mem=\mem, memsd=\memsd}
1058
{\model & \backend & \n & \N & \K & \checks & \ns & \rt & \rtsd & \R & \nodesR & \nodesRel & \nodesPiR & \at & \atsd
1059
& \mem & \memsd}
1060
\normalsize 
1061
\label{tbl:appendix:rw-wo-%s-%s}
1062
\end{sidewaystable}'."\n";
1063

    
1064
// for rw w/ our changes
1065
$rw_tex_w = "\n".'\begin{sidewaystable}[H]
1066
\resultcaption{Results w/ read-write separation for \%s{} (%s)}
1067
\footnotesize
1068
\csvreader[tabular=|l|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|,
1069
    table head=\hline model & backend & n & $N$ & $K$ & checks & ns & $\overline{\text{rt}}$ & rt-$\sigma$ & $\vert
1070
\mathcal{R}\vert$ & $\llbracket\mathcal{R}\rrbracket$ & $\llbracket\transrelexpr\rrbracket$ & $\llbracket\pi(\mathcal{R})\rrbracket$ &
1071
$\overline{\text{at}}$ & at-$\sigma$ & $\overline{\text{mem}}$ & mem-$\sigma$\\\\\hline, late after line=\\\\\hline]
1072
{../ext/scripts/csv/%s-%s-%s.csv}{model=\model, backend=\backend, n=\n, N=\N, K=\K,
1073
checks=\checks, ns=\ns, rt=\rt, rtsd=\rtsd, R=\R, nodesR=\nodesR, nodesRel=\nodesRel, nodesPiR=\nodesPiR, at=\at, atsd=\atsd, mem=\mem, memsd=\memsd}
1074
{\model & \backend & \n & \N & \K & \checks & \ns & \rt & \rtsd & \R & \nodesR & \nodesRel & \nodesPiR & \at & \atsd
1075
& \mem & \memsd}
1076
\normalsize 
1077
\label{tbl:appendix:rw-w-%s-%s}
1078
\end{sidewaystable}'."\n";
1079

    
1080
// for guard w/o our changes
1081
$guard_tex_wo = "\n".'\begin{sidewaystable}[H]
1082
\resultcaption{Results w/o guard-splitting for \%s{} (%s)}
1083
\footnotesize
1084
\csvreader[tabular=|l|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|,
1085
    table head=\hline model & backend & n & $N$ & $K$ & checks & ns & $\overline{\text{rt}}$ & rt-$\sigma$ & $\vert
1086
\mathcal{R}\vert$ & $\llbracket\mathcal{R}\rrbracket$ & $\llbracket\transrelexpr\rrbracket$ & $\llbracket\pi(\mathcal{R})\rrbracket$ &
1087
$\overline{\text{at}}$ & at-$\sigma$ & $\overline{\text{mem}}$ & mem-$\sigma$ & $M$ & $\llbracket\mathcal{F}\rrbracket$ & $\llbracket\mathcal{T}\rrbracket$\\\\\hline, late
1088
after line=\\\\\hline]
1089
{../ext/scripts/csv/%s-%s-%s.csv}{model=\model, backend=\backend, n=\n, N=\N, K=\K,
1090
checks=\checks, ns=\ns, rt=\rt, rtsd=\rtsd, R=\R, nodesR=\nodesR, nodesRel=\nodesRel, nodesPiR=\nodesPiR, at=\at, atsd=\atsd, mem=\mem,
1091
memsd=\memsd, M=\M, nodesF=\nodesF, nodesT=\nodesT}
1092
{\model & \backend & \n & \N & \K & \checks & \ns & \rt & \rtsd & \R & \nodesR & \nodesRel & \nodesPiR & \at & \atsd
1093
& \mem & \memsd & \M & \nodesF & \nodesT}
1094
\normalsize
1095
\label{tbl:appendix:guard-wo-%s-%s}
1096
\end{sidewaystable}'."\n";
1097

    
1098
// for guard w our changes
1099
$guard_tex_w = "\n".'\begin{sidewaystable}[H]
1100
\resultcaption{Results w/ guard-splitting for \%s{} (%s)}
1101
\footnotesize
1102
\csvreader[tabular=|l|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|,
1103
    table head=\hline model & backend & n & $N$ & $K$ & checks & ns & $\overline{\text{rt}}$ & rt-$\sigma$ & $\vert
1104
\mathcal{R}\vert$ & $\llbracket\mathcal{R}\rrbracket$ & $\llbracket\transrelexpr\rrbracket$ & $\llbracket\pi(\mathcal{R})\rrbracket$ &
1105
$\overline{\text{at}}$ & at-$\sigma$ & $\overline{\text{mem}}$ & mem-$\sigma$ & $M$ & $\llbracket\mathcal{F}\rrbracket$ & $\llbracket\mathcal{T}\rrbracket$\\\\\hline, late
1106
after line=\\\\\hline]
1107
{../ext/scripts/csv/%s-%s-%s.csv}{model=\model, backend=\backend, n=\n, N=\N, K=\K,
1108
checks=\checks, ns=\ns, rt=\rt, rtsd=\rtsd, R=\R, nodesR=\nodesR, nodesRel=\nodesRel, nodesPiR=\nodesPiR, at=\at, atsd=\atsd, mem=\mem,
1109
memsd=\memsd, M=\M, nodesF=\nodesF, nodesT=\nodesT}
1110
{\model & \backend & \n & \N & \K & \checks & \ns & \rt & \rtsd & \R & \nodesR & \nodesRel & \nodesPiR & \at & \atsd
1111
& \mem & \memsd & \M & \nodesF & \nodesT}
1112
\normalsize
1113
\label{tbl:appendix:guard-w-%s-%s}
1114
\end{sidewaystable}'."\n";
1115

    
1116
$latex_rw = "";
1117

    
1118
// for every combination of frontend/options write the table to a file.
1119
foreach (array("promela", "mcrl", "dve") as $frontend) {
1120
    foreach (array("bfs-prev-no-sat", "bfs-prev-sat-like", "bfs-prev-sat-loop", "chain-prev-no-sat", "chain-prev-sat-like", "chain-prev-sat-loop") as $option) {
1121
        $latex_rw .= sprintf($rw_tex_wo, $frontend, $option, "next", $frontend, $option, $frontend, $option);
1122
        $latex_rw .= "
1123
            \\newpage
1124
            ";
1125
        $latex_rw .= sprintf($rw_tex_w, $frontend, $option, "rw", $frontend, $option, $frontend, $option);
1126
        $latex_rw .= "
1127
            \\newpage
1128
            ";
1129
    }
1130
}
1131

    
1132
file_put_contents($output."/bench-rw-csv.tex", $latex_rw); // use input{bench-rw-csv.tex} in latex
1133

    
1134
$latex_guard = "";
1135

    
1136
// for every combination of frontend/options write the table to an other file.
1137
foreach (array("promela", "mcrl", "divine") as $frontend) {
1138
    foreach (array("bfs-prev-no-sat", "bfs-prev-sat-like", "bfs-prev-sat-loop", "chain-prev-no-sat", "chain-prev-sat-like", "chain-prev-sat-loop") as $option) {
1139
        $latex_guard .= sprintf($guard_tex_wo, $frontend, $option, "rw", $frontend, $option, $frontend, $option);
1140
        $latex_guard .= "
1141
            \\newpage
1142
            ";
1143
        $latex_guard .= sprintf($guard_tex_w, $frontend, $option, "guard", $frontend, $option, $frontend, $option);
1144
        $latex_guard .= "
1145
            \\newpage
1146
            ";
1147
    }
1148
}
1149

    
1150
file_put_contents($output."/bench-guard-csv.tex", $latex_guard); // use input{bench-guard-csv.tex} in latex
1151

    
1152
foreach (array("time", "memory") as $time_or_mem) {
1153
    
1154
    foreach (array("read-write seperation" => "rw", "guard-splitting" => "guard") as $caption=>$breakdown) {
1155

    
1156
        foreach (array ("Promela" => count($promela_count), "mCRL2" => count($mcrl2_count), "DVE" => count($dve_count)) as $name => $count) {
1157

    
1158
            $out = "        
1159
    \\begin{sidewaysfigure}[H]
1160
    \\centering
1161
    ";
1162
            $first = 1;
1163
            for ($i = 0; $i <= floor($count/6); $i++) {
1164
                $begin = $i*6+1;
1165
                $end = ($i+1)*6;
1166

    
1167
                if ($end > $count) $end = $count;
1168
                if ($begin >= $end) break;
1169

    
1170
                $out .= sprintf("    \\includegraphics[width=0.48\\textheight]{../ext/scripts/r/pdf/%s-%s-%s-%d-%d}\n", $time_or_mem, $breakdown, $name, $begin, $end);
1171
                
1172
                if (($i+1) % 4 == 0 && ($i+1)*6+1 < $count) {
1173
                    $out .= "
1174
    \\plotcaption{".ucfirst($time_or_mem)." scatter plots $first -- $end for $name with $caption}
1175
    \\label{fig:scatter:$time_or_mem-$first-$end-$name-$breakdown}
1176
    \\end{sidewaysfigure}";
1177
                    
1178
                    $out .= "
1179
    \\newpage
1180
    \\begin{sidewaysfigure}[H]
1181
    \\centering
1182
    ";                  
1183
                
1184
                    $first = $begin + 6;
1185
                      
1186
                }
1187

    
1188
            }   
1189
            
1190
            $out .= sprintf(" 
1191
    \\plotcaption{".ucfirst($time_or_mem)." scatter plots $first -- $end for $name with $caption}
1192
    \\label{fig:scatter:$time_or_mem-$first-$end-$name-$breakdown}
1193
    \\end{sidewaysfigure}
1194
    ", $caption, $name, $time_or_mem);
1195
                
1196
            
1197
            
1198
            file_put_contents($output."/".$time_or_mem."-bench-".$breakdown."-".$name."-scatter.tex", $out); // use input{...tex} in latex
1199
        }
1200
    }
1201
}
1202

    
1203
// highlights
1204
$highlights = "\n".'\begin{sidewaystable}[H]
1205
%\resultcaption{Results}
1206
\footnotesize
1207
\csvreader[tabular=|l|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|,
1208
    table head=\hline model & backend & order & dm & n & $N$ & $K$ & checks & ns & $\overline{\text{rt}}$ & rt-$\sigma$ & $\vert
1209
\mathcal{R}\vert$ & $\llbracket\mathcal{R}\rrbracket$ & $\llbracket\transrelexpr\rrbracket$ & $\llbracket\pi(\mathcal{R})\rrbracket$ &
1210
$\overline{\text{at}}$ & at-$\sigma$ & $\overline{\text{mem}}$ & mem-$\sigma$\\\\\hline, late after line=\\\\\hline]
1211
{/home/jeroen/gitprojects/rtproposal/report/ext/scripts/csv/highlights.csv}{model=\model, backend=\backend, order=\order, dm=\dm, n=\n, N=\N, K=\K,
1212
checks=\checks, ns=\ns, rt=\rt, rtsd=\rtsd, R=\R, nodesR=\nodesR, nodesRel=\nodesRel, nodesPiR=\nodesPiR, at=\at, atsd=\atsd, mem=\mem, memsd=\memsd}
1213
{\model & \backend & \order & \dm & \n & \N & \K & \checks & \ns & \rt & \rtsd & \R & \nodesR & \nodesRel & \nodesPiR & \at & \atsd
1214
& \mem & \memsd}
1215
\normalsize 
1216
\label{tbl:appendix:highlights}
1217
\end{sidewaystable}'."\n";
1218

    
1219
file_put_contents($output."/highlights.tex", $highlights); // use input{bench-rw-csv.tex} in latex
1220

    
1221
// close the std err.
1222
fclose($errh);