source: vis_dev/vis-2.3/src/rt/rtMain.c @ 23

Last change on this file since 23 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 114.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [rtMain.c]
4
5  PackageName [rt]
6
7  Synopsis    [Regression Test]
8
9  Description  [ This  file contains  the  functions for  regression test.  The
10command 'regression_test' will read a  description of the regression test to be
11performed from the  argument file, and will then carry  out the test.  Finally,
12it will produce a LaTeX file with a set of tables summarizing the results.
13
14  The regression_test command can be  used to compare two different versions of
15vis, or two different scripts on the same version of vis, or even two different
16scripts  on  two  different   versions  of  vis.   regression_test  spawns  the
17version(s) of vis  to be used for the experiments as  child processes.  It does
18no  other computation  except setting  up the  experiments, starting  the child
19processes, waiting for their termination, and collecting the results.
20
21 ]
22
23  Author [HoonSang Jin]
24
25  Copyright   [Copyright (c) 2001-2002 The Regents of the Univ. of Colorado.
26  All rights reserved.
27
28  Permission is hereby granted, without written agreement and without license
29  or royalty fees, to use, copy, modify, and distribute this software and its
30  documentation for any purpose, provided that the above copyright notice and
31  the following two paragraphs appear in all copies of this software.
32
33  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
34  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
35  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
36  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
37
38  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
39  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
40  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
41  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
42  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
43
44******************************************************************************/
45
46#include "rtInt.h"
47#include "rt.h"
48#include "ntm.h"
49#include "part.h"
50#include <errno.h>
51#include <math.h>
52
53static char rcsid[] UNUSED = "$Id: rtMain.c,v 1.36 2010/04/10 00:38:42 fabio Exp $";
54
55
56/*---------------------------------------------------------------------------*/
57/* Macro declarations                                                        */
58/*---------------------------------------------------------------------------*/
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63
64/**AutomaticStart*************************************************************/
65
66/*---------------------------------------------------------------------------*/
67/* Static function prototypes                                                */
68/*---------------------------------------------------------------------------*/
69
70static int CommandRt( Hrc_Manager_t **hmgr, int argc, char **argv);
71static RtConfigs_t * Rt_ReadConfigFile(char *filename);
72static char * Rt_SplitLine( char * command, int * argc, char *** argv);
73static int Rt_CompareResult(RtConfigs_t *config, RtDesignLists_t *designList, int refOnly);
74static int Rt_WriteBatchCommand(RtConfigs_t *config, RtDesignLists_t *designList);
75static int Rt_ExecuteVis(RtConfigs_t *config, RtDesignLists_t *designList, int refAndNew, FILE *scriptOut);
76static int Rt_WriteResult(RtConfigs_t *config, int size);
77static void Rt_FreeRtConfig(RtConfigs_t * config);
78static void Rt_FreeCommandResult(RtCommandResults_t *result);
79static void Rt_FreeCompareItem(RtCompareItems_t *item);
80static void Rt_FreeResultProperty(RtResultPropertys_t *prop);
81static void Rt_FreeDesignList(RtDesignLists_t *list);
82static void Rt_FreeArgv(int  argc,  char ** argv);
83static int Rt_ReadDesignListFile(RtConfigs_t * config);
84static int Rt_ReadCommandTemplate(RtConfigs_t * config);
85static int RtCheckInputFileAvailability( RtConfigs_t *config, RtDesignLists_t *designList, int withWarning);
86static void Rt_RemoveUnderscore(char *name, char *newName);
87static int Rt_IsNum(char *tmp);
88static int Rt_SetBooleanValue(char *str, char *option);
89
90/**AutomaticEnd***************************************************************/
91
92
93/*---------------------------------------------------------------------------*/
94/* Definition of exported functions                                          */
95/*---------------------------------------------------------------------------*/
96
97
98/**Function********************************************************************
99
100  Synopsis [Initialize mc package]
101
102  SideEffects []
103
104******************************************************************************/
105
106
107/**Function********************************************************************
108
109  Synopsis [Initialize rt package]
110
111  SideEffects []
112
113******************************************************************************/
114void
115Rt_Init(void)
116{
117  Cmd_CommandAdd("regression_test", CommandRt, /* doesn't changes_network */ 0);
118}
119
120/**Function********************************************************************
121
122  Synopsis [End rt package]
123
124  SideEffects []
125
126******************************************************************************/
127void
128Rt_End(void)
129{
130}
131
132/**Function********************************************************************
133
134  Synopsis    [Compare two different execution of vis and make a set of
135               tables summarizing results.]
136
137  CommandName [regression_test]
138
139  CommandSynopsis [perform regression test with the information given
140                   in arguments file]
141
142  CommandArguments [ \[-s &lt;script_file_name&gt;\] ]
143
144  CommandDescription  [
145  Invokes two set of execution of vis to compare the performance and to check
146sanity of each execution. Then make a set of tables summarizing results,
147such as CPU sec, memoty usage and fail/pass of model_check, etc.. This
148command will read a description of the regression test to be performed
149from the argument file, which is configuartion file. Besides the configuration
150file, one needs to prepare two template files and a design list. We now
151describe these in turn. As running example we shall use a regression test
152that compares check_invariant with and without guided search.
153<p>The configuration file for our example is shown below, delimited by
154lines of dashes (which are not part of the file). The order in which the
155lines appear in the file is immaterial. A line beginning with '#' is a
156comment, and is ignored by regression_test.
157<br>----------------------------------------------------------------------
158<br>DesignDirectory : /projects/development/hsv/vis/Regression
159<br>DesignList : ./DesignListInv
160<br>ReferenceVis : /usr/local/vis/i686-o/vis-cu
161<br>ReferenceVisNickName : BFS
162<br>ReferenceOutputDir : ./result_inv_bfs
163<br>RefCommandTemplate : ./TemplateRefInv
164<br>bRefRun : FALSE
165<br>NewVis : /usr/local/vis/i686-o/vis-cu
166<br>NewVisNickName : GS
167<br>NewOutputDir : ./result_inv_gs
168<br>bNewRun : FALSE
169<br>NewCommandTemplate : ./TemplateNewInv
170<br>bCompareCounterExample : TRUE
171<br>bDefaultInitCommand : FALSE
172<br>ResultForPerformance : ./BFSvsGS.tex
173<br>CompareItem : cpu : elapse:
174<br>CompareItem : mem : Memory in use:
175<br>CompareItem : bdd : Peak number of live nodes:
176<br>----------------------------------------------------------------------
177<br>&nbsp;
178<p>Each line defines a parameter of the regression test.
179<p>* DesignDirectory gives the path to the directory where the input files
180are stored. In this case, we are using the central repository under ~hsv/vis/Regression.
181It's typically a good idea to store the results of regression tests in
182a separate place from the input files. In our examples, the results are
183stored in the current directory.
184<p>&nbsp;* DesignList gives the name of the file containing the list of
185test cases to run. Each line consists of several white space-separated
186fields describing the files making up the test case. The first field is
187a path to the files relative to DesignDirectory. The second field is the
188test case name. The remaining fields are file names. More on this later,
189when we talk about the design list file in detail.
190<p>&nbsp;* ReferenceVis and NewVis give paths to the two versions of vis
191to be compared in the regression test. They can be the same, as in this
192case in which both are the "nightly build."
193<p>&nbsp;* ReferenceVisNickName and NewVisNickName are two identifiers
194that are used in the LaTeX tables to refer to the two versions that are
195compared. Short mnemonics are preferable. Avoid using underscores, because
196they currently cause trouble with LaTeX.
197<p>&nbsp;* ReferenceOutputDir and NewOutputDir give the names of the directories
198in which the results of the runs will be stored. In each of these directories,
199vis_reg will create a directory for each test case. The names of these
200directories are the test case names taken from the design list. Therefore,
201these names must be unique.
202<p>&nbsp;* RefCommandTemplate and NewCommandTemplate are the templates
203from which vis_reg produces the scripts used to run the test cases. The
204mechanism used to derive the scripts from the templates and the design
205list is described in detail when we talk about the template files. The
206two templates can be the same file.
207<p>&nbsp;* bRefRun and bNewRun are flags that tell vis_reg which of the
208two sets of experiments should be run (if any). If one set of results has
209been already computed, the corresponding flag should be set to FALSE. If
210both flags are FALSE, vis_reg simply regenerates the
211summary table.
212<p>&nbsp;* bCompareCounterExample is a flag that instructs vis_reg to scan
213the output files for counterexamples and record their lengths. For each
214counterexample, stem and cycle length are found. If this flag is set to
215FALSE, counterexamples are not analyzed and the corresponding table is
216not produced.
217<p>&nbsp;* bDefaultInitCommand is a flag that, if set to TRUE, instructs
218vis_reg to generate a default set of commands to initialize each vis run.
219This option allows one to save some time in preparing the templates, at
220the expense of some flexibility.
221<p>&nbsp;* ResultForPerformance is the name of the LaTeX file to which
222vis_reg writes the summary of the experiments. Its format is described
223in detail later.
224<p>&nbsp;* CompareItem specifies one item to be monitored in the experiments.
225Multiple CompareItem lines may appear in the configuration file. Each one
226consists of two items: an identifier, and a pattern. The identifier is
227used in the table to denote the item, whereas the pattern is used to extract
228from the output files the information to be put in the tables.
229<p>&nbsp;In our example, we declare
230<p>&nbsp;CompareItem : mem : Memory in use:
231<p>We instruct regression_test to search for a line beginning with "Memory
232in use:" in each section of the output file. The token immediately following
233the occurrence of the pattern is the data item to be put in the table under
234"mem." so that the resulting LaTeX table contains data on the memmory usage.
235<p>&nbsp;Since the output file is divided into sections delimited by strings
236"CommandBegin" and "CommandEnd." (See below.), each section is searched
237for the patterns specified by the CompareItem declarations. If the pattern
238is matched, the item appears in the table for that section.
239<p>&nbsp;To run the regression_test we need configuration file, template
240file and design list. In case of template file, we need a two template
241files, since we want to compare two different run of vis. The syntax of
242the two templates is identical. We describe the template for "new," but
243all we say applies to "ref" as well. The "new" template for our example
244is shown below.
245<br>----------------------------------------------------------------------
246<p>echo CommandBegin init
247<br>read_model
248<br>flt
249<br>order_vars
250<br>part
251<br>time
252<br>print_bdd_stats
253<br>echo CommandEnd init
254<br>echo CommandBegin ci
255<br>set hd_frontier_approx_threshold 3500
256<br>ci -t 3600 -g $HintFile $InvFile
257<br>time
258<br>print_bdd_stats
259<br>echo CommandEnd ci
260<br>echo CommandBegin ci_cex
261<br>ci -d 1 -i -t 3600 -g $HintFile $InvFile
262<br>time
263<br>print_bdd_stats
264<br>echo CommandEnd ci_cex
265<br>----------------------------------------------------------------------
266<p>Before proceeding to its discussion, it is instructive to examine the
267script that regression_test produces from it for one test case. regression_test
268relies on vis's shell variables and aliases to customize the script. The
269script consists of a preamble in which variables and aliases are defined,
270followed by one or more sections, each corresponding to a major step in
271the experiment. Statistics will be collected for each step separately.
272Our example has three sections, whose names are "init," "ci," and "ci_cex."
273The names of the sections are arbitrary, except that the automatically
274generated initialization section is always called "init."
275<br>----------------------------------------------------------------------
276<p>set vis_stdout ./result_inv_gs/am2901/am2901.out
277<br>set vis_stderr ./result_inv_gs/am2901/am2901.err
278<br>set BlifFile /projects/development/hsv/vis/Regression/Am2901/am2901.mv
279<br>set OrdFile /projects/development/hsv/vis/Regression/Am2901/am2901.ord
280<br>set InvFile /projects/development/hsv/vis/Regression/Am2901/am2901.inv
281<br>set HintFile /projects/development/hsv/vis/Regression/Am2901/am2901.hint
282<br>alias read_model "rlmv $BlifFile"
283<br>alias set_fairness " "
284<br>alias order_vars "so -s input_and_latch $OrdFile"
285<br>echo CommandBegin init
286<br>read_model
287<br>flt
288<br>order_vars
289<br>part
290<br>time
291<br>print_bdd_stats
292<br>echo CommandEnd init
293<br>echo CommandBegin ci
294<br>set hd_frontier_approx_threshold 3500
295<br>ci -t 3600 -g $HintFile $InvFile
296<br>time
297<br>print_bdd_stats
298<br>echo CommandEnd ci
299<br>echo CommandBegin ci_cex
300<br>ci -d 1 -i -t 3600 -g $HintFile $InvFile
301<br>time
302<br>print_bdd_stats
303<br>echo CommandEnd ci_cex
304<br>quit
305<br>----------------------------------------------------------------------
306<p>The variables and the aliases are defined by vis_reg by examining the
307fields of the test case description in the design file. regression_test
308uses file extensions to identify file types. (E.g., .ord indicates an order
309file in "input_and_latch" format.) A full list of extensions is given below.
310<p>regression_test defines variables for all the file types actually available
311for the experiment, and only for those. It also defines three aliases that
312provide some flexibility in mixing different experiments in the same batch.
313<p>For instance, "read_model" is defined as either
314<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; read_blif_mv $BlifFile
315<p>or
316<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; read_blif $BlifFile
317<p>depending on whether the design list specifies a .mv file or a .blif
318file as model file.
319<p>The definition of "order_vars" takes into account whether an order file
320is available or not. Finally, the definition of "set_fairness" depends
321on whether a .fair file is available. This allows one to mix model checking
322experiments for which no fairness condition is specified to experiments
323that do require fairness conditions.
324<p>When bDefaultInitCommand is FALSE, the script is simply the preamble,
325followed by the unchanged template, follows by the "quit" command, which
326is always automatically added.
327<p>When bDefaultInitCommand is TRUE, regression_test also adds an automatically
328generated "init" section between the preamble and the template. This default
329section is equivalent to
330<p>echo CommandBegin init
331<br>read_model
332<br>flt
333<br>order_vars
334<br>part
335<br>time
336<br>print_bdd_stats
337<br>echo CommandEnd init
338<p>Notice that one has no control over dynamic reordering during the initialization
339phase if bDefaultInitCommand is TRUE.
340<p>The template should refer to the defined aliases and variables to tailor
341itself to each test case. Notice, however, that one is not forced to use
342"order_vars." If one wants to always use vis's static ordering algorithm,
343(s)he can simply use "so" instead of "order_vars." Likewise, one can decide
344to always ignore fairness constraints by not including "set_fairness."
345<p>On the other hand, it is usually a bad idea to explicitly include commands
346like
347<p>read_blif_mv
348<br>read_blif
349<br>so -s input_and_latch
350<br>read_fairness
351<p>in the templates, because they limit the range of test cases to which
352they can be applied.
353<p>As we said, the templates, and hence the scripts, are divided in sections.
354Each section begins and ends with an "echo" command. These commands write
355delimiters to the output file, which are used by vis_reg to define the
356scope of the pattern searches. It is important that the tag specified in
357corresponding pairs of CommandBegin and CommandEnd be the same.
358<p>The calls to "print_bdd_stats" are typically used to add to the output
359files the information requested by the CompareItem declarations. It is
360a good idea to specify timeouts for potentially expensive steps.
361<p>The design list file has one line for each test case. A master design
362list is in ~hsv/vis/Regression/DesignList. Specific design lists can be
363obtained by commenting out or deleting lines from this master list. One
364can also create an entirely new list according to the following rules.
365<p>Lines starting with '#' are interpreted as comments and are skipped,
366as in all files read by vis_reg.
367<p>A test case is a named collection of related files that can be used
368to run one or more experiments. As mentioned before, each line consists
369of white space-separated fields. The first is a (relative) path, while
370the second is the collection name. The remaining fields specify the files
371in the collection.
372<p>The smallest collection will specify one .mv or one .blif file. This
373file is called the "model file," and should always appear in the third
374field of the line. If the model file is the only file specified, one can
375run reachability analysis, but not much more. Vis_reg understands the file
376extensions shown in the following table. For each extension, the variable
377bound to the file name and a short explanation are given.
378<p>.mv $BlifFile model file to be read with rlmv
379<br>.blif $BlifFile model file to be read with rl
380<br>.ord $OrdFIle order file to be read with so -s input_and_latch
381<br>.inv $InvFile invariant file to be read with ci
382<br>.ctl $CtlFile property file to be read with mc
383<br>.fair $FairFile fairness file to be read with rf
384<br>.hint $HintFile hint file to be read with the -g option of mc, ci,
385and rch
386<p>Only one file of each type can appear in the collection defining one
387test case. If multiple property files, or different order files are available
388for one model file, one has to create two test cases for that model. Different
389models, on the other hand, can share property files, order files, and so
390on. The master design list provides examples for both these situations.
391<p>It is not possible to specify both a .mv file and a .blif file for one
392test case. There must be exactly one model file per test case.
393<p>As was mentioned before, it is important that the name of a test case
394be unique in the entire batch used for a regression test. On the other
395hand, several test cases may share the same directory, and often do when
396they have some files in common.
397<p>The result summary created by regression_test is a LaTeX file consisting
398of several tables. There is one table with performance stats for each section
399of the output file. In addition, there is an optional counterexample comparison
400table that summarizes PASS/FAIL information for the properties and the
401length of counterexamples. For each failing property, the length of the
402stem and the length of the cycle (if applicable) are reported.
403<p>Each performance table consists of one column for the test case name,
404followed by as many groups of three columns as there are CompareItem declarations
405applicable to the section that the table summarizes.
406<p>Each group of three columns gives the data for the reference run, the
407data for the new run, and the improvement. Vis_reg regards smaller as better.
408Hence, the improvement is positive if the CPU time, memory occupation,
409and so on, have decreased from the reference run to the new run. The improvement
410is computed as
411<p>(value(ref) - value(new)) / value(ref) * 100.
412<p>Notice that this formula tends to make "new" look bad. for instance,
413if new is twice as fast as ref, the improvement is 50%. If ref is twice
414as fast, however, the "improvement" is -100%.
415<p>The results of each test case are stored in a separate directory, whose
416name is obtained by concatenating ReferenceOutputDir (or NewOutputDir)
417with the test case name. Each directory stores three files, whose names
418are given by the test case name concatenated with .src, .out, and .err.
419<p>* test_case_name.src stores the script used to run vis.
420<br>* test_case_name.out stores what vis writes to vis_stdout.
421<br>* test_case_name.err stores what vis writes to vis_stderr.
422<p>One has to be careful, because vis_reg will overwrite these results
423directories without warning if run twice with the same ReferenceOutputDir
424or NewOutputDir and bRefRun or bNewRun set to TRUE.
425<p>With '-s' option, you can create c-shell script file to be able to run
426experiments in shell. We add this option to solve the problem that are
427happened when your template file contains child-process by system call.
428]
429
430  Comment [
431  * One cannot compare the number of iterations to convergence with BFS
432  to those of HD or GS, because the first is reported as "FSM depth,"
433  while the other two are reported as "computation depth."  <p>
434
435  * Tables are split so that the number of rows is not too large.
436  However, tables may be too wide.  All "CompareItem" items found in
437  one section are put in the same table.  <p>
438
439  * Currently, under Linux, the datasize limit is not enforced (not
440  systematically enforced?) for the child processes spawned by
441  vis_reg.  One has to monitor experiments that may produce very large
442  processes, because there is a concrete risk of thrashing the machine
443  on which the regression test is run.  <p>
444
445  * One cannot create experiments that read two different property
446  files, or two different invariant files, or that perform equivalence
447  checking.  (That would require two model files.)  <p>
448
449]
450
451  SideEffects []
452
453******************************************************************************/
454static int
455CommandRt(
456  Hrc_Manager_t **hmgr,
457  int argc,
458  char **argv)
459{
460  char *configurationFile;
461  char *scriptFile;
462  RtConfigs_t *config;
463  RtDesignLists_t *designList;
464  array_t *designArr;
465  int i;
466  FILE *scriptOut;
467  int c;
468  error_init();
469
470  if(argc < 2) {
471     fprintf(vis_stdout, "Error : ConfigurationFile is missed\n");
472     return(1);
473  }
474
475  util_getopt_reset();
476  scriptFile = 0;
477  scriptOut = 0;
478  while ((c = util_getopt(argc, argv, "s:h")) != EOF) {
479    switch(c) {
480    case 's':
481      scriptFile = util_strsav(util_optarg);
482      break;
483    case 'h':
484      (void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
485      (void) fprintf(vis_stderr, "    -h \tprint help information\n");
486      (void) fprintf(vis_stderr, "    -s <scriptfile>\n");
487      (void) fprintf(vis_stderr, "       \tgenerate shell script file for regression_test\n");
488      return 0;
489    default:
490      (void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
491      (void) fprintf(vis_stderr, "    -h \tprint help information\n");
492      (void) fprintf(vis_stderr, "    -s <scriptfile>\n");
493      (void) fprintf(vis_stderr, "       \tgenerate shell script file for regression_test\n");
494      return 0;
495    }
496  }
497  if(scriptFile) {
498    if(!(scriptOut = fopen(scriptFile, "w"))) {
499      fprintf(vis_stdout, "Error : Can't open script file '%s'\n", scriptFile);
500      return(1);
501    }
502  }
503
504  configurationFile = argv[util_optind];
505  config = Rt_ReadConfigFile(configurationFile);
506  if(config == 0)                       return(1);
507
508  config->scriptFile = scriptFile;
509  if(Rt_ReadDesignListFile(config))     {
510    Rt_FreeRtConfig(config);
511    return(1);
512  }
513  if(Rt_ReadCommandTemplate(config))    {
514    Rt_FreeRtConfig(config);
515    return(1);
516  }
517
518
519  designArr = config->designListArr;
520  for(i=0; i<array_n(designArr); i++) {
521    designList = array_fetch(RtDesignLists_t *, designArr, i);
522
523    /**
524     * One have to use reserved words in their template file, such as
525     * $OrdFile, $BlifFile, etc..
526     * Somehow your template file contains the reserved words that are
527     * not provied in desigl list, then skip the design.
528     **/
529    if(RtCheckInputFileAvailability(config, designList, 1)) {
530       fprintf(vis_stdout, "Skip the design '%s' ..(%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
531       continue;
532    }
533    /**
534     * Create result directory structure and script file that are used
535     * to run individual experiments. Each directory, whose
536     * name is obtained by concatenating ReferenceOutputDir(or NewOutputDir)
537     * with the test case name, contains test_case_name.src after
538     * executing this function.
539     **/
540    if(Rt_WriteBatchCommand(config, designList)) {
541       fprintf(vis_stdout, "ERROR : can't write script for design '%s'\n", designList->designNickName);
542       continue;
543    }
544    /**
545     * Run vis using the executable that is obtained ReferenceVis of
546     * configuration file
547     **/
548    if(Rt_ExecuteVis(config, designList, 1, scriptOut)) {
549       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->referenceVisNickName, designList->designNickName);
550    }
551    /**
552     * Run vis using the executable that is obtained NewVis of
553     * configuration file
554     **/
555    if(Rt_ExecuteVis(config, designList, 2, scriptOut)) {
556       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->newVisNickName, designList->designNickName);
557    }
558    /**
559     * After running two set of experimental results, read the log file
560     * of each run and compare the results.
561     **/
562    if(Rt_CompareResult(config, designList, config->bRefOnly)) {
563       fprintf(vis_stdout, "ERROR : can't compare result for design '%s'\n", designList->designNickName);
564    }
565    fprintf(vis_stdout, "%s complete.. (%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
566
567    /**
568     * Write a LaTeX file summarizing the results, after running each
569     * design, so that one can see the results before finishing the
570     * whole experiments.
571     **/
572    if(config->scriptFile == 0) {
573      if(config->bRefRun || config->bNewRun)
574        Rt_WriteResult(config, i+1);
575    }
576  }
577
578  /**
579   * Write a LateX file summarizing the results.
580   **/
581  if(config->scriptFile == 0)
582    if(Rt_WriteResult(config, array_n(designArr)))      return(1);
583  alarm(0);
584
585  Rt_FreeRtConfig(config);
586  if(scriptOut) fclose(scriptOut);
587  return 0;
588}
589
590/**Function********************************************************************
591
592  Synopsis    [Check whether the used file in template file is available
593               or not. ]
594
595  Description [
596      One have to use reserved words in their template file, such as
597     $OrdFile, $BlifFile,  $InvFile, $CtlFile, $FairFile, $HintFile and
598     $LeFile. Somehow your template file contains the reserved words that are
599     not provied in design list, then skip the design.
600     ]
601
602  Comment []
603
604  SideEffects []
605
606******************************************************************************/
607static int
608RtCheckInputFileAvailability(
609  RtConfigs_t *config, 
610  RtDesignLists_t *designList,
611  int withWarning)
612{
613  st_table *keyTable;
614  st_generator *gen;
615  int errorFlag;
616  char *keyWord;
617
618  keyTable = config->keyWordTable;
619  if(keyTable == 0)     return(0);
620  errorFlag = 0;
621  st_foreach_item(keyTable, gen, &keyWord, NIL(char *)) {
622    if(!strcasecmp(keyWord, "$CtlFile") && !designList->ctlFile) {
623      if(withWarning)
624      fprintf(vis_stdout, "WARNING : Template contains the '$CtlFile', but not in design list\n");
625      errorFlag = 1;
626    }
627    else if(!strcasecmp(keyWord, "$OrdFile") && !designList->ordFile) {
628      if(withWarning)
629      fprintf(vis_stdout, "WARNING : Template contains the '$OrdFile', but not in design list\n");
630      errorFlag = 1;
631    }
632    else if(!strcasecmp(keyWord, "$InvFile")&& !designList->invFile) {
633      if(withWarning)
634      fprintf(vis_stdout, "WARNING : Template contains the '$InvFile', but not in design list\n");
635      errorFlag = 1;
636    }
637    else if(!strcasecmp(keyWord, "$FairFile")&& !designList->fairFile) {
638      if(withWarning)
639      fprintf(vis_stdout, "WARNING : Template contains the '$FairFile', but not in design list\n");
640      errorFlag = 1;
641    }
642    else if(!strcasecmp(keyWord, "$LeFile")&& !designList->leFile) {
643      if(withWarning)
644      fprintf(vis_stdout, "WARNING : Template contains the '$LeFile', but not in design list\n");
645      errorFlag = 1;
646    }
647    else if(!strcasecmp(keyWord, "$LtlFile")&& !designList->ltlFile) {
648      if(withWarning)
649      fprintf(vis_stdout, "WARNING : Template contains the '$LtlFile', but not in design list\n");
650      errorFlag = 1;
651    }
652    else if(!strcasecmp(keyWord, "$HintFile")&& !designList->hintFile) {
653      if(withWarning)
654      fprintf(vis_stdout, "WARNING : Template contains the '$HintFile', but not in design list\n");
655      errorFlag = 1;
656    }
657  }
658  if(errorFlag == 1)    return(1);
659  else                  return(0);
660}
661
662/**Function********************************************************************
663
664  Synopsis    [ Write LaTeX file summarizing results.]
665
666  Description [ The  result summary created by regression_test  is a LaTeX file
667consisting of  several tables.  There is  one table with  performance stats for
668each  section  of  the  output   file.   In  addition,  there  is  an  optional
669counterexample comparison  table that summarizes PASS/FAIL  information for the
670properties and the  length of counterexamples.  For each  failing property, the
671length of the stem and the length of the cycle (if applicable) are reported.
672
673Each performance table consists of one  column for the test case name, followed
674by  as many  groups  of three  columns  as there  are CompareItem  declarations
675applicable to the section that the table summarizes.  ]
676
677  Comment []
678
679  SideEffects []
680
681******************************************************************************/
682static int
683Rt_WriteResult(RtConfigs_t *config, int size)
684{
685  FILE *fout;
686  array_t *cResultArr, *cResultArr2;
687  array_t *cResultArrSample, *cItemArrSample, *cItemArrSampleMax;
688  array_t *cItemArr, *cItemArr2, *designArr;
689  array_t *pArr, *pArr2, *pArrSample;
690  RtCommandResults_t *cResult, *cResult2, *cResultSample;
691  RtCompareItems_t *cItem, *cItem2, *cItemSample;
692  RtDesignLists_t *designList;
693  RtResultPropertys_t *rProp, *rProp2;
694  int i, j, k, first_flag;
695  int property_flag;
696  int lineNo, estLineNo, errorFlag;
697  char newName[1024], endStr[10];
698  char newNName[1024], refNName[1024];
699  char newTimeout[1024], refTimeout[1024];
700  double value1, value2;
701  int lastFailedIndex;
702  array_t *cResultArrMax;
703  array_t *cItemArrMax;
704  double *resultArr;
705  double totalNum;
706  double gap;
707
708  pArrSample = 0;
709  if(!(fout = fopen(config->resultForPerformance, "w"))) {
710    fprintf(vis_stdout, "Error : Can't open result file '%s'\n", config->resultForPerformance);
711    return(1);
712  }
713  designArr = config->designListArr;
714
715  /** Check whether both runs contain the same set of item, since we
716   * compare two experiments.
717   **/
718  cItemArrSample = 0;
719  cResultArrSample = NIL(array_t);
720  for(k=0; k<array_n(designArr) && k<size; k++) {
721    designList = array_fetch(RtDesignLists_t *, designArr, k);
722    cResultArrSample = designList->resultForCommandArr1;
723    errorFlag = 0;
724    if(cResultArrSample)        {
725      for(i=0; i<array_n(cResultArrSample); i++) {
726        cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
727        cItemArrSample = cResult->compareItemArr;
728        if(cItemArrSample == NIL(array_t)) {
729          errorFlag = 1;
730          break;
731        }
732      }
733    }
734    if(errorFlag == 0)  break;
735  }
736  if(cResultArrSample == NIL(array_t)) {
737     fprintf(fout, "ERROR : Can't find any output for your design list\n");
738     fclose(fout);
739     return(1);
740  }
741
742  /** Write performance table header **/
743  fprintf(fout, "\\documentclass[plain]{article}\n");
744  fprintf(fout, "\\usepackage{lscape}\n");
745  fprintf(fout, "\\begin{document}\n");
746  fprintf(fout, "\\setlength{\\oddsidemargin}{-0.5in}\n");
747  /**
748  fprintf(fout, "\\landscape\n");
749  **/
750
751  for(i=0; i<array_n(cResultArrSample); i++) {
752
753    fprintf(fout, "\\begin{table}\n");
754    cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
755    cItemArrSample = cResult->compareItemArr;
756 
757    cItemArrSampleMax = cItemArrSample;
758    for(k=0; k<array_n(designArr) && k<size; k++) {
759      designList = array_fetch(RtDesignLists_t *, designArr, k);
760      cResultArr = designList->resultForCommandArr1;
761      if(cResultArr)    {
762          if(array_n(cResultArr) > i) 
763              cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
764          else
765              cResult = 0;
766          if(!cResult)  continue;
767          cItemArrSample = cResult->compareItemArr;
768          if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrSampleMax)) {
769            cItemArrSampleMax = cItemArrSample;
770          }
771      }
772    }
773    cItemArrSample = cItemArrSampleMax;
774    if(cItemArrSample == 0) {
775       fprintf(fout, "ERROR : Can't find any output for your design list\n");
776       fclose(fout);
777       return(1);
778    }
779     
780    cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
781    Rt_RemoveUnderscore(cResult->command, newName);
782    Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
783    Rt_RemoveUnderscore(config->newVisNickName, newNName);
784    fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
785        newName, refNName, newNName);
786    fprintf(fout, "\\begin{center}\n");
787    fprintf(fout, "\\begin{tabular}{|c||");
788    for(j=0; j<array_n(cItemArrSample); j++) {
789      fprintf(fout, "c|c|c|");
790    }
791    fprintf(fout, "} \\hline \n");
792    fprintf(fout, " &");
793    Rt_RemoveUnderscore(cResult->command, newName);
794    fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
795    fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
796 
797    fprintf(fout, " &");
798    for(j=0; j<array_n(cItemArrSample); j++) {
799      cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
800      if(j+1 == array_n(cItemArrSample)) 
801        fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
802      else 
803        fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
804    }
805    fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
806 
807    fprintf(fout, "Design &");
808    for(j=0; j<array_n(cItemArrSample); j++) {
809      if(j+1 == array_n(cItemArrSample)) 
810        fprintf(fout, "ref & new & (\\%%)");
811      else 
812        fprintf(fout, "ref & new & (\\%%) &");
813    }
814    fprintf(fout, "\\\\ \\hline \\hline\n");
815 
816    lineNo = 0;
817    for(k=0; k<array_n(designArr) && k<size ; k++) {
818      lineNo++;
819 
820      /**
821       * If the result table have more than 31 line then split the
822       * table.
823       **/
824      if(lineNo == 31) {
825        fprintf(fout, "\\end{tabular}\n");
826        fprintf(fout, "\\end{center}\n");
827        fprintf(fout, "\\end{table}\n");
828        fprintf(fout, "\\clearpage\n");
829 
830        fprintf(fout, "\\begin{table}\n");
831        cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
832        cItemArrSample = cResult->compareItemArr;
833        Rt_RemoveUnderscore(cResult->command, newName);
834        Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
835        Rt_RemoveUnderscore(config->newVisNickName, newNName);
836        fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
837            newName, refNName, newNName);
838        fprintf(fout, "\\begin{center}\n");
839        fprintf(fout, "\\begin{tabular}{|c||");
840        for(j=0; j<array_n(cItemArrSample); j++) {
841          fprintf(fout, "c|c|c|");
842        }
843        fprintf(fout, "} \\hline \n");
844        fprintf(fout, " &");
845        Rt_RemoveUnderscore(cResult->command, newName);
846        fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
847        fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
848     
849        fprintf(fout, " &");
850        for(j=0; j<array_n(cItemArrSample); j++) {
851          cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
852          if(j+1 == array_n(cItemArrSample)) 
853            fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
854          else 
855            fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
856        }
857        fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
858     
859        fprintf(fout, "Design &");
860        for(j=0; j<array_n(cItemArrSample); j++) {
861          if(j+1 == array_n(cItemArrSample)) 
862            fprintf(fout, "ref & new & (\\%%)");
863          else 
864            fprintf(fout, "ref & new & (\\%%) &");
865        }
866        fprintf(fout, "\\\\ \\hline \\hline\n");
867     
868        lineNo = 1;
869      }
870      designList = array_fetch(RtDesignLists_t *, designArr, k);
871      strcpy(newTimeout, "-");
872      strcpy(refTimeout, "-");
873      if(RtCheckInputFileAvailability(config, designList, 0)) {
874        continue;
875      }
876      cResultArr = designList->resultForCommandArr1;
877      cResultArr2 = designList->resultForCommandArr2;
878      Rt_RemoveUnderscore(designList->designNickName, newName);
879      fprintf(fout, "%s\t&", newName);
880      if(cResultArr && array_n(cResultArr) > i)
881        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
882      else 
883        cResult = 0;
884 
885      if(cResultArr2 && array_n(cResultArr2) > i)
886        cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
887      else 
888        cResult2 = 0;
889 
890      if(cResult && cResult->bTimeOut)   {
891        strcpy(refTimeout, "TimeOut");
892      }
893      if(cResult2 && cResult2->bTimeOut) {
894        strcpy(newTimeout, "TimeOut");
895      }
896 
897      if(cResult)
898        cItemArr = cResult->compareItemArr;
899      else
900        cItemArr = 0;
901      if(cResult2)
902        cItemArr2 = cResult2->compareItemArr;
903      else
904        cItemArr2 = 0;
905 
906      if(cItemArr == 0 && cItemArr2 == 0)       {
907        fprintf(vis_stdout, "Warning : no result for design '%s'\n", designList->designNickName);
908        for(j=0; j<array_n(cItemArrSample); j++) {
909          if(j+1 == array_n(cItemArrSample)) 
910            fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
911          else 
912            fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
913        }
914        fprintf(fout, "\\\\ \\hline\n");
915        continue;
916      }
917      else if(cItemArr && cItemArr2) {
918        if(array_n(cItemArr) != array_n(cItemArr2)) {
919          fprintf(vis_stdout, "Warning : Can't make table for the compare item,\n");
920          fprintf(vis_stdout, "           since they are different for '%s'\n", designList->designNickName);
921          fprintf(vis_stdout, "           Please check your template file again.\n");
922          for(j=0; j<array_n(cItemArrSample); j++) {
923            if(j+1 == array_n(cItemArrSample)) 
924              fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
925            else 
926              fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
927          }
928          fprintf(fout, "\\\\ \\hline\n");
929          continue;
930        }
931      }
932      if(cItemArr)      cItemArrSample = cItemArr;
933      else              cItemArrSample = cItemArr2;
934      for(j=0; j<array_n(cItemArrSample); j++) {
935        if(cItemArr) 
936          cItem = array_fetch(RtCompareItems_t *, cItemArr, j);
937        else
938          cItem = 0;
939        if(cItemArr2) 
940          cItem2 = array_fetch(RtCompareItems_t *, cItemArr2, j);
941        else
942          cItem2 = 0;
943   
944        if(cItem)       sscanf(cItem->value, "%lf", &value1);
945        if(cItem2)      sscanf(cItem2->value, "%lf", &value2);
946 
947        endStr[0] = '\0';
948        if(j+1 != array_n(cItemArrSample))      {
949          endStr[0] = '&';
950          endStr[1] = '\0';
951        }
952        if(cItem2 && cItem) {
953          fprintf(fout, "%s\t& %s\t& %.2f\t%s", cItem->value, cItem2->value, (value1-value2)/value1*100, endStr);
954        }
955        else if(cItem)  {
956          fprintf(fout, "%s\t& %s\t& -\t%s", cItem->value, newTimeout, endStr);
957        }
958        else if(cItem2)  {
959          fprintf(fout, "%s\t& %s\t& -\t%s", refTimeout, cItem2->value, endStr);
960        }
961      }
962      fprintf(fout, "\\\\ \\hline\n");
963    }
964    fprintf(fout, "\\end{tabular}\n");
965    fprintf(fout, "\\end{center}\n");
966    fprintf(fout, "\\end{table}\n");
967    fprintf(fout, "\\clearpage\n");
968  }
969
970  property_flag = 0;
971  for(k=0; k<array_n(designArr) && k<size; k++) {
972    designList = array_fetch(RtDesignLists_t *, designArr, k);
973    cResultArr = designList->resultForCommandArr1;
974    if(cResultArr)       {
975      for(i=0; i<array_n(cResultArr); i++) {
976        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
977        pArr = cResult->resultForProperty;
978        if(pArr && array_n(pArr) > 0)   {
979          property_flag = 1;
980          break;
981        }
982      }
983    }
984    cResultArr = designList->resultForCommandArr2;
985    if(cResultArr)       {
986      for(i=0; i<array_n(cResultArr); i++) {
987        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
988        pArr = cResult->resultForProperty;
989        if(pArr && array_n(pArr) > 0)   {
990          property_flag = 1;
991          break;
992        }
993      }
994    }
995    if(property_flag)   break;
996  }
997
998  /**
999   * Write the property comparison table in case of model checking
1000   * verification
1001   **/
1002  if(property_flag == 1) {
1003    fprintf(fout, "\\begin{table}\n");
1004    Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
1005    Rt_RemoveUnderscore(config->newVisNickName, newNName);
1006    fprintf(fout, "\\caption{Property Comparison Table for %s(ref) \
1007    and %s(new)}\n", refNName, newNName);
1008    fprintf(fout, "\\begin{center}\n");
1009    fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
1010    fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
1011    fprintf(fout, "Design & command & index & F or P & cex len & line len  & F or P & cex len  & line len& \\\\ \\hline\n");
1012 
1013    lineNo = 0;
1014    for(k=0; k<array_n(designArr) && k<size; k++) {
1015      designList = array_fetch(RtDesignLists_t *, designArr, k);
1016      if(RtCheckInputFileAvailability(config, designList, 0)) {
1017        continue;
1018      }
1019      cResultArr = designList->resultForCommandArr1;
1020      cResultArr2 = designList->resultForCommandArr2;
1021      if(cResultArr == 0 && cResultArr2 == 0) {
1022        fprintf(vis_stdout, "ERROR : '%s' didn't run properly\n", designList->designNickName);
1023        continue;
1024      }
1025      else if(cResultArr == 0 ) {
1026        cResultArrSample = cResultArr2;
1027      }
1028      else if(cResultArr2 == 0 ) {
1029        cResultArrSample = cResultArr;
1030      }
1031      else {
1032        cResultArrSample = cResultArr;
1033      }
1034 
1035      strcpy(refTimeout, "-");
1036      strcpy(newTimeout, "-");
1037 
1038      first_flag = 0;
1039      for(i=0; i<array_n(cResultArrSample); i++) {
1040        if(cResultArr && array_n(cResultArr) > i)
1041          cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
1042        else
1043          cResult = 0;
1044        if(cResultArr2 && array_n(cResultArr2) > i)
1045          cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
1046        else 
1047          cResult2 = 0;
1048 
1049        if(cResult == 0 && cResult2 == 0)       continue;
1050 
1051        if(cResult && cResult->bTimeOut)         {
1052          strcpy(refTimeout, "TimeOut");
1053        }
1054        if(cResult2 && cResult2->bTimeOut) {
1055          strcpy(newTimeout, "TimeOut");
1056        }
1057 
1058        else if((cResult && !cResult->resultForProperty) &&
1059                (cResult2 && !cResult2->resultForProperty))     continue;
1060 
1061        if(cResult)
1062          pArr = cResult->resultForProperty;
1063        else
1064          pArr = 0;
1065        if(cResult2)
1066          pArr2 = cResult2->resultForProperty;
1067        else
1068          pArr2 = 0;
1069 
1070        if((!pArr || array_n(pArr) < 1) && (!pArr2 || array_n(pArr2) < 1)) {
1071          continue;
1072        }
1073        else if(pArr && array_n(pArr) >= 1) {
1074          pArrSample = pArr;
1075        }
1076        else if(pArr2 && array_n(pArr2) >= 1) {
1077          pArrSample = pArr2;
1078        }
1079 
1080        estLineNo = 0;
1081        lastFailedIndex = -1;
1082        for(j=0; j<array_n(pArrSample); j++) {
1083          if(pArr && array_n(pArr) > j) 
1084            rProp = array_fetch(RtResultPropertys_t *, pArr, j);
1085          else
1086            rProp = 0;
1087          if(pArr2 && array_n(pArr2) > j) 
1088            rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
1089          else
1090            rProp2 = 0;
1091 
1092          if((rProp && !strncasecmp(rProp->failOrPass, "pass", 4)) && 
1093              (rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4))) {
1094          }
1095          else {
1096            estLineNo++;
1097            lastFailedIndex = j;
1098          }
1099 
1100        }
1101 
1102      /**
1103       * If the result table have more than 40 line then split the
1104       * table.
1105       **/
1106        if(lineNo + estLineNo > 40) {
1107          fprintf(fout, "\\hline\n");
1108          fprintf(fout, "\\end{tabular}\n");
1109          fprintf(fout, "\\end{center}\n");
1110          fprintf(fout, "\\end{table}\n");
1111          fprintf(fout, "\\clearpage\n");
1112          fprintf(fout, "\\begin{table}\n");
1113          Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
1114          Rt_RemoveUnderscore(config->newVisNickName, newNName);
1115          fprintf(fout, "\\caption{Property Comparison Table for \
1116          %s(ref) and %s(new)}\n", refNName, newNName);
1117          fprintf(fout, "\\begin{center}\n");
1118          fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
1119          fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
1120          fprintf(fout, "Design & command & index & F or P & cex len & line len  & F or P & cex len  & line len& \\\\ \\hline\n");
1121          lineNo = 0;
1122        }
1123         
1124        Rt_RemoveUnderscore(designList->designNickName, newName);
1125        if(first_flag==0) {
1126          fprintf(fout, "%s &", newName);
1127          first_flag = 1;
1128        }
1129        else
1130          fprintf(fout, " &");
1131 
1132        for(j=0; j<array_n(pArrSample); j++) {
1133 
1134          lineNo++;
1135          if(pArr && array_n(pArr) > j) 
1136            rProp = array_fetch(RtResultPropertys_t *, pArr, j);
1137          else
1138            rProp = 0;
1139          if(pArr2 && array_n(pArr2) > j) 
1140            rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
1141          else
1142            rProp2 = 0;
1143           
1144          if(rProp && !strncasecmp(rProp->failOrPass, "pass", 4) && 
1145             rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4)) {
1146            if(j==0 && estLineNo == 0) {
1147              if(cResult)
1148                 Rt_RemoveUnderscore(cResult->command, newName);
1149              else 
1150                 Rt_RemoveUnderscore(cResult2->command, newName);
1151              fprintf(fout, " %s & [%d] & passed & passed & - & passed & passed & - & \\\\ ", newName, rProp->index+1);
1152              if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample)) 
1153                fprintf(fout, " \\hline\n");
1154              else if(j+1 == array_n(pArrSample))
1155                fprintf(fout, " \\cline{2-10}\n");
1156              else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))   
1157                fprintf(fout, " \\hline\n");
1158              else if(lastFailedIndex <= j)   
1159                fprintf(fout, " \\cline{2-10}\n");
1160              else 
1161                fprintf(fout, " \\cline{4-10}\n");
1162            }
1163            else {
1164              lineNo--;
1165            }
1166            continue;
1167          }
1168 
1169   
1170          if(first_flag==1) {
1171            if(cResult) {
1172              Rt_RemoveUnderscore(cResult->command, newName);
1173              fprintf(fout, " %s & ", newName);
1174            }
1175            else if(cResult2) {
1176              Rt_RemoveUnderscore(cResult2->command, newName);
1177              fprintf(fout, " %s & ", newName);
1178            }
1179            first_flag = 2;
1180          }
1181          else {
1182            fprintf(fout, " & & ");
1183          }
1184 
1185          if(rProp) {
1186            if(rProp->lengthOfInv != -1) 
1187              fprintf(fout, " [%d] & %s & (%d,-) & %d &", rProp->index+1, rProp->failOrPass, rProp->lengthOfInv, rProp->lengthOfCounterExample);
1188            else if(rProp->lengthOfStem == -1 && rProp->lengthOfCycle == -1)
1189              fprintf(fout, " [%d] & %s & - & - &", rProp->index+1, rProp->failOrPass);
1190            else 
1191              fprintf(fout, " [%d] & %s & (%d,%d) & %d & ", rProp->index+1, rProp->failOrPass, rProp->lengthOfStem, rProp->lengthOfCycle,rProp->lengthOfCounterExample );
1192          }
1193          else {
1194            if(rProp2)
1195              fprintf(fout, " [%d] & %s & %s & - & ", rProp2->index+1, refTimeout, refTimeout);
1196            else 
1197              fprintf(fout, " & %s & %s & - & ", refTimeout, refTimeout);
1198          }
1199 
1200          if(rProp2) {
1201            if(rProp2->lengthOfInv != -1) 
1202              fprintf(fout, " %s & (%d,-) & %d ", rProp2->failOrPass,
1203              rProp2->lengthOfInv,rProp2->lengthOfCounterExample );
1204            else if(rProp2->lengthOfStem == -1 && rProp2->lengthOfCycle == -1)
1205              fprintf(fout, " %s & - & - ", rProp2->failOrPass);
1206            else 
1207              fprintf(fout, " %s & (%d,%d) & %d ", rProp2->failOrPass,
1208              rProp2->lengthOfStem, rProp2->lengthOfCycle, rProp2->lengthOfCounterExample);
1209          }
1210          else {
1211            fprintf(fout, " %s & %s & - ", newTimeout, newTimeout);
1212          }
1213 
1214          endStr[0] = '\0';
1215          if(rProp2 && rProp) {
1216             if(rProp->failOrPass == 0 && rProp2->failOrPass)
1217               strcpy(endStr, "Check");
1218             else if(rProp->failOrPass && rProp2->failOrPass == 0)
1219               strcpy(endStr, "Check");
1220             if(rProp->failOrPass == 0 && rProp2->failOrPass == 0)
1221               strcpy(endStr, "Check");
1222             if(strcmp(rProp->failOrPass, rProp2->failOrPass))
1223               strcpy(endStr, "Check");
1224             else if(rProp->lengthOfStem != rProp2->lengthOfStem) 
1225               strcpy(endStr, "Check");
1226             else if(rProp->lengthOfCycle != rProp2->lengthOfCycle)
1227               strcpy(endStr, "Check");
1228             else if(rProp->lengthOfInv != rProp2->lengthOfInv)
1229               strcpy(endStr, "Check");
1230          }
1231          else {
1232            strcpy(endStr, "Check");
1233          }
1234          if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample)) 
1235            fprintf(fout, " & %s \\\\ \\hline\n",endStr);
1236          else if(j+1 == array_n(pArrSample))
1237            fprintf(fout, " & %s \\\\ \\cline{2-10}\n",endStr);
1238          else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))   
1239            fprintf(fout, " & %s \\\\ \\hline\n", endStr);
1240          else if(lastFailedIndex <= j)   
1241            fprintf(fout, " & %s \\\\ \\cline{2-10}\n", endStr);
1242          else 
1243            fprintf(fout, " & %s \\\\ \\cline{4-10}\n",endStr);
1244        }
1245      }
1246    }
1247 
1248    fprintf(fout, "\\end{tabular}\n");
1249    fprintf(fout, "\\end{center}\n");
1250    fprintf(fout, "\\end{table}\n");
1251    fprintf(fout, "\\clearpage\n");
1252  }
1253
1254
1255  /**
1256   * Write the summary of comparison
1257   **/
1258  fprintf(fout, "\\begin{table}\n");
1259  Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
1260  Rt_RemoveUnderscore(config->newVisNickName, newNName);
1261  fprintf(fout, "\\caption{Summary for %s(ref) and %s(new)}\n", refNName, newNName);
1262  fprintf(fout, "\\begin{center}\n");
1263  fprintf(fout, "\\begin{tabular}{|c|c||c|c|c|c||r|r|} \\hline\n");
1264  fprintf(fout, " command & item & \\multicolumn{4}{c||}{ %s } & \\multicolumn{2}{c|}{ geo-mean } \\\\ \\cline{3-8}\n", newNName);
1265  fprintf(fout, " & & win & lose & tie & NA & ref & new \\\\ \\hline \\hline\n");
1266
1267  cResultArrMax = 0;
1268  for(k=0; k<array_n(designArr) && k<size; k++) {
1269    designList = array_fetch(RtDesignLists_t *, designArr, k);
1270    cResultArr = designList->resultForCommandArr1;
1271    if(cResultArrMax == 0)      cResultArrMax = cResultArr;
1272    else if(cResultArr && array_n(cResultArr) > array_n(cResultArrMax)) {
1273       cResultArrMax = cResultArr;
1274    }
1275  }
1276
1277  resultArr = ALLOC(double, 6); 
1278  for(i=0; i<array_n(cResultArrMax); i++) {
1279    cResultSample = array_fetch(RtCommandResults_t *, cResultArrMax, i);
1280    fprintf(fout, " %s & ", cResultSample->command);
1281    first_flag = 1;
1282
1283    cItemArrMax = 0;
1284    for(k=0; k<array_n(designArr) && k<size; k++) {
1285      designList = array_fetch(RtDesignLists_t *, designArr, k);
1286      cResultArr = designList->resultForCommandArr1;
1287      if(cResultArr)    {
1288          if(array_n(cResultArr) > i) 
1289              cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
1290          else
1291              continue;
1292          cItemArrSample = cResult->compareItemArr;
1293          if(cItemArrMax == 0)  cItemArrMax = cItemArrSample;
1294          else if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrMax)) {
1295            cItemArrMax = cItemArrSample;
1296          }
1297      }
1298    }
1299
1300    for(j=0; j<6; j++)  resultArr[j] = 0.0;
1301    resultArr[4] = 1.0;
1302    resultArr[5] = 1.0;
1303
1304    for(j=0; j<array_n(cItemArrMax); j++) {
1305      for(k=0; k<6; k++)        resultArr[k] = 0.0;
1306      resultArr[4] = 1.0;
1307      resultArr[5] = 1.0;
1308
1309      cItemSample = array_fetch(RtCompareItems_t *, cItemArrMax, j);
1310      if(first_flag) {
1311        fprintf(fout, "%s &\n", cItemSample->itemNickName);
1312        first_flag = 0;
1313      }
1314      else {
1315        fprintf(fout, " & %s &\n", cItemSample->itemNickName);
1316      }
1317
1318      for(k=0; k<array_n(designArr) && k<size; k++) {
1319        designList = array_fetch(RtDesignLists_t *, designArr, k);
1320        if(designList->resultForCommandArr1 == 0 ||
1321           designList->resultForCommandArr2 == 0) {
1322           resultArr[3] = resultArr[3] + 1.0;
1323           continue;
1324        }
1325        if(array_n(designList->resultForCommandArr1) <= i ||
1326           array_n(designList->resultForCommandArr2) <= i) {
1327           resultArr[3] = resultArr[3] + 1.0;
1328           continue;
1329        }
1330        cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
1331        cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
1332        if(cResult == 0 || cResult2 == 0) {
1333           resultArr[3] = resultArr[3] + 1.0;
1334           continue;
1335        }
1336        if(cResult->compareItemArr == 0 ||
1337           cResult2->compareItemArr == 0) {
1338           resultArr[3] = resultArr[3] + 1.0;
1339           continue;
1340        }
1341        if(array_n(cResult->compareItemArr) <= j ||
1342           array_n(cResult2->compareItemArr) <= j) {
1343           resultArr[3] = resultArr[3] + 1.0;
1344           continue;
1345        }
1346        cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
1347        cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
1348        if(cItem == 0 || cItem2 == 0) {
1349           resultArr[3] = resultArr[3] + 1.0;
1350           continue;
1351        }
1352
1353        value1 = atof(cItem->value);
1354        value2 = atof(cItem2->value);
1355        if(value1 > value2)     gap = value2;
1356        else                    gap = value1;
1357        gap = gap * 0.02;
1358        if(gap < 1.0)   gap = 1.0;
1359
1360        if(value1 > value2 + gap)       resultArr[0] = resultArr[0] + 1.0; /** new win **/
1361        else if(value1+gap < value2)    resultArr[1] = resultArr[1] + 1.0; /** ref win **/
1362        else                            resultArr[2] += 1.0; /** tie **/
1363      }
1364      totalNum = resultArr[0] + resultArr[1] + resultArr[2];
1365      totalNum = 1.0/totalNum;
1366      for(k=0; k<array_n(designArr) && k<size; k++) {
1367        designList = array_fetch(RtDesignLists_t *, designArr, k);
1368        if(designList->resultForCommandArr1 == 0 ||
1369           designList->resultForCommandArr2 == 0) {
1370           continue;
1371        }
1372        if(array_n(designList->resultForCommandArr1) <= i ||
1373           array_n(designList->resultForCommandArr2) <= i) {
1374           continue;
1375        }
1376        cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
1377        cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
1378        if(cResult == 0 || cResult2 == 0) {
1379           continue;
1380        }
1381        if(cResult->compareItemArr == 0 ||
1382           cResult2->compareItemArr == 0) {
1383           continue;
1384        }
1385        if(array_n(cResult->compareItemArr) <= j ||
1386           array_n(cResult2->compareItemArr) <= j) {
1387           continue;
1388        }
1389        cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
1390        cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
1391        if(cItem == 0 || cItem2 == 0) {
1392           continue;
1393        }
1394
1395        value1 = atof(cItem->value);
1396        value2 = atof(cItem2->value);
1397        if(value1 == 0.0)       value1 = 1.0;
1398        else                    value1 = pow(value1, totalNum);
1399        if(value2 == 0.0)       value2 = 1.0;
1400        else                    value2 = pow(value2, totalNum);
1401
1402        resultArr[4] *= value1;
1403        resultArr[5] *= value2;
1404      }
1405
1406      if(array_n(cItemArrMax) == j+1 ) {
1407        fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\hline\n", 
1408                    (int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
1409                    (int)resultArr[3], resultArr[4], resultArr[5]);
1410      }
1411      else {
1412        fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\cline{2-8}\n", 
1413                    (int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
1414                    (int)resultArr[3], resultArr[4], resultArr[5]);
1415      }
1416    }
1417  }
1418  free(resultArr);
1419  fprintf(fout, "\\end{tabular}\n");
1420  fprintf(fout, "\\end{center}\n");
1421  fprintf(fout, "\\end{table}\n");
1422
1423  fprintf(fout, "\\begin{itemize}\n");
1424  Rt_RemoveUnderscore(config->configurationFile, newName);
1425  fprintf(fout, "\\item configuration file : %s\n", newName);
1426  Rt_RemoveUnderscore(config->designDirectory, newName);
1427  fprintf(fout, "\\item design directory : %s\n", newName);
1428  Rt_RemoveUnderscore(config->designList, newName);
1429  fprintf(fout, "\\item design list : %s\n", newName);
1430  Rt_RemoveUnderscore(config->referenceOutDirectory, newName);
1431  fprintf(fout, "\\item reference output dir : %s\n", newName);
1432  Rt_RemoveUnderscore(config->referenceVis, newName);
1433  fprintf(fout, "\\item reference executable : %s\n", newName);
1434  Rt_RemoveUnderscore(config->refCommandTemplate, newName);
1435  fprintf(fout, "\\item reference template : %s\n", newName);
1436  Rt_RemoveUnderscore(config->newOutDirectory, newName);
1437  fprintf(fout, "\\item new output dir : %s\n", newName);
1438  Rt_RemoveUnderscore(config->newVis, newName);
1439  fprintf(fout, "\\item new executable : %s\n", newName);
1440  Rt_RemoveUnderscore(config->newCommandTemplate, newName);
1441  fprintf(fout, "\\item new template : %s\n", newName);
1442  fprintf(fout, "\\end{itemize}\n");
1443  fprintf(fout, "\\clearpage\n");
1444
1445  fprintf(fout, "\\end{document}\n");
1446  fclose(fout);
1447  fprintf(vis_stdout, "'%s' file was generated as result of regression_test\n", 
1448               config->resultForPerformance);
1449  return(0);
1450}
1451
1452/**Function********************************************************************
1453
1454  Synopsis    [Remove underscopre from the string. ]
1455
1456  Description [Remove underscore from the given string, since LaTeX consider
1457               underscore as subscript keyword. ]
1458
1459  Comment []
1460
1461  SideEffects []
1462
1463******************************************************************************/
1464static void
1465Rt_RemoveUnderscore(char *name, 
1466                    char *newName)
1467{
1468int i, index ;
1469
1470  index = 0;
1471  for(i=0; name[i] != '\0'; i++) {
1472    if(name[i] == '_') {
1473      newName[index++] = '\\';
1474    }
1475    newName[index++] = name[i];
1476  }
1477  newName[index] = '\0';
1478}
1479
1480/**Function********************************************************************
1481
1482  Synopsis    [Read the log file of both runs, and then store the information
1483               in the internal data structure. ]
1484
1485  Description [Read the log file of runs, Current version supports
1486    reachability analysis, CTL model checking and invariant checking.
1487    If that is not the case, it may read the log file without errors
1488    except the couterexample trace.]
1489
1490  Comment []
1491
1492  SideEffects []
1493
1494******************************************************************************/
1495static int
1496Rt_CompareResult(RtConfigs_t *config,
1497                 RtDesignLists_t *designList,
1498                 int refOnly)
1499{
1500  FILE *fin1, *fin2;
1501  char filename1[1024], filename2[1024];
1502  char line[1024], *next;
1503  RtCompareItems_t *item, *newItem;
1504  RtResultPropertys_t *rProperty;
1505  RtCommandResults_t *cResult;
1506  int argc;
1507  char **argv;
1508  int i, len;
1509  int propertyIndex;
1510  int formulaSummary, commandBeginFlag;
1511  int basicLength, stemLength, cycleLength;
1512  int propertyIndexSummary, pIndex;
1513  int invCheckFlag;
1514  int nLine, countLineFlag;
1515  array_t *itemArr;
1516
1517  propertyIndex = -1;
1518  basicLength = 0;
1519  stemLength = 0;
1520  cycleLength = 0;
1521  invCheckFlag = 0;
1522  propertyIndexSummary = 0;
1523
1524  sprintf(filename1, "%s/%s/%s.out", config->referenceOutDirectory, 
1525                                     designList->designNickName, 
1526                                     designList->designNickName); 
1527  if(!(fin1 = fopen(filename1, "r"))) {
1528    fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename1);
1529    return(1);
1530  }
1531
1532  fin2 = 0;
1533  if(!refOnly) {
1534    sprintf(filename2, "%s/%s/%s.out", config->newOutDirectory, 
1535                                     designList->designNickName, 
1536                                     designList->designNickName); 
1537    if(!(fin2 = fopen(filename2, "r"))) {
1538      fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename2);
1539      return(1);
1540    }
1541  }
1542
1543  /**
1544   * Compile the log file based on keywords, such as CommandEnd,
1545   * CommandBegin, # MC: formula, etc,. If timeout case is detected the
1546   * fill the data structure with 'TimeOut'.
1547   **/
1548  itemArr = config->compareItemArr;
1549  cResult = 0;
1550  formulaSummary = 0;
1551  commandBeginFlag = 0;
1552  nLine = 0;
1553  countLineFlag = 0;
1554  rProperty = 0;
1555  while(fgets(line, 1024, fin1)) {
1556    if(countLineFlag)   nLine++;
1557    if(line[0] == '\n') continue;
1558    if(!strncasecmp(line, "CommandEnd", 10)) {
1559      if(rProperty && countLineFlag)    {
1560        rProperty->lengthOfCounterExample = nLine;
1561        if(rProperty->lengthOfBasic > -1) {
1562          if(rProperty->lengthOfStem > -1)
1563            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1564          else
1565            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1566        }
1567      }
1568      countLineFlag = 0;
1569      nLine = 0;
1570      rProperty = 0;
1571      commandBeginFlag = 0;
1572    }
1573    else if(!strncasecmp(line, "CommandBegin", 12)) {
1574      propertyIndex = -1;
1575      rProperty = 0;
1576      formulaSummary = 0;
1577      commandBeginFlag = 1;
1578      Rt_SplitLine(line, &argc, &argv);
1579      if(designList->resultForCommandArr1 == 0)
1580        designList->resultForCommandArr1= array_alloc(RtCommandResults_t *, 0);
1581      cResult = ALLOC(RtCommandResults_t, 1);
1582      cResult->resultForProperty = 0;
1583      cResult->compareItemArr = 0;
1584      cResult->command = strdup(argv[1]);
1585      cResult->bTimeOut = 0;
1586      array_insert_last(RtCommandResults_t *, designList->resultForCommandArr1,
1587      cResult);
1588      Rt_FreeArgv(argc, argv);
1589      continue;
1590    }
1591    else if(!strncasecmp(line, "** cmd error", 12)) {
1592      if(cResult)
1593        cResult->error = 1;
1594      fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
1595      designList->designNickName);
1596      continue;
1597    }
1598    else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
1599      if(rProperty && countLineFlag)    {
1600        rProperty->lengthOfCounterExample = nLine;
1601        if(rProperty->lengthOfBasic > -1) {
1602          if(rProperty->lengthOfStem > -1)
1603            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1604          else
1605            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1606        }
1607      }
1608      countLineFlag = 0;
1609      nLine = 0;
1610      propertyIndex++;
1611      Rt_SplitLine(&line[13], &argc, &argv);
1612      rProperty = ALLOC(RtResultPropertys_t, 1);
1613      rProperty->lengthOfBasic = -1;
1614      rProperty->lengthOfStem = -1;
1615      rProperty->lengthOfCycle = -1;
1616      rProperty->lengthOfInv = -1;
1617      rProperty->lengthOfCounterExample = -1;
1618      rProperty->index = propertyIndex;
1619      rProperty->failOrPass = strdup(argv[0]);
1620      if(cResult->resultForProperty == 0)
1621        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1622      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
1623      basicLength = 1;
1624      stemLength = 0;
1625      cycleLength = 0;
1626      invCheckFlag = 0;
1627      Rt_FreeArgv(argc, argv);
1628      continue;
1629    }
1630    else if((!strncasecmp(line, "# AMC: formula", 14) ||
1631             !strncasecmp(line, "# IMC: formula", 14) ||
1632             !strncasecmp(line, "# BMC: formula", 14) ||
1633             !strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
1634      if(rProperty && countLineFlag)    {
1635        rProperty->lengthOfCounterExample = nLine;
1636        if(rProperty->lengthOfBasic > -1) {
1637          if(rProperty->lengthOfStem > -1)
1638            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1639          else
1640            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1641        }
1642      }
1643      countLineFlag = 0;
1644      nLine = 0;
1645      propertyIndex++;
1646      Rt_SplitLine(&line[14], &argc, &argv);
1647      rProperty = ALLOC(RtResultPropertys_t, 1);
1648      rProperty->lengthOfBasic = -1;
1649      rProperty->lengthOfStem = -1;
1650      rProperty->lengthOfCycle = -1;
1651      rProperty->lengthOfInv = -1;
1652      rProperty->lengthOfCounterExample = -1; 
1653      rProperty->index = propertyIndex;
1654      rProperty->failOrPass = strdup(argv[0]);
1655      if(cResult->resultForProperty == 0)
1656        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1657      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
1658      basicLength = 1;
1659      stemLength = 0;
1660      cycleLength = 0;
1661      invCheckFlag = 0;
1662      Rt_FreeArgv(argc, argv);
1663      continue;
1664    }
1665    else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
1666      if(rProperty && countLineFlag)    {
1667        rProperty->lengthOfCounterExample = nLine;
1668        if(rProperty->lengthOfBasic > -1) {
1669          if(rProperty->lengthOfStem > -1)
1670            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1671          else
1672            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1673        }
1674      }
1675      countLineFlag = 0;
1676      nLine = 0;
1677      propertyIndex++;
1678      Rt_SplitLine(&line[17], &argc, &argv);
1679      rProperty = ALLOC(RtResultPropertys_t, 1);
1680      rProperty->lengthOfBasic = -1;
1681      rProperty->lengthOfStem = -1;
1682      rProperty->lengthOfCycle = -1;
1683      rProperty->lengthOfInv = -1;
1684      rProperty->lengthOfCounterExample = -1;
1685      rProperty->index = propertyIndex;
1686      rProperty->failOrPass = strdup(argv[0]);
1687      if(cResult->resultForProperty == 0)
1688        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1689      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
1690      basicLength = 1;
1691      stemLength = 0;
1692      cycleLength = 0;
1693      invCheckFlag = 0;
1694      Rt_FreeArgv(argc, argv);
1695      continue;
1696    }
1697    else if(!strncasecmp(line, "--Fair path stem:", 17)) {
1698      basicLength = 0;
1699      stemLength = 1;
1700      cycleLength = 0;
1701      rProperty->lengthOfInv = -1;
1702      continue;
1703    }
1704    else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
1705      basicLength = 0;
1706      stemLength = 0;
1707      cycleLength = 1;
1708      rProperty->lengthOfInv = -1;
1709      continue;
1710    }
1711    else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
1712      basicLength = 0;
1713      stemLength = 0;
1714      cycleLength = 1;
1715      rProperty->lengthOfInv = -1;
1716      continue;
1717    }
1718    else if(!strncasecmp(line, "--State ", 8)) {
1719      if(rProperty == 0) {
1720        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
1721        continue;
1722      }
1723      Rt_SplitLine(&line[8], &argc, &argv);
1724      len = strlen(argv[0]);
1725      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
1726      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
1727      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
1728      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
1729      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
1730
1731      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
1732      Rt_FreeArgv(argc, argv);
1733      if(countLineFlag == 0)    countLineFlag = 1;
1734      continue;
1735    }
1736    else if(!strncasecmp(line, "--Goes to state ", 16)) {
1737      if(rProperty == 0) {
1738        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
1739        continue;
1740      }
1741      Rt_SplitLine(&line[16], &argc, &argv);
1742      len = strlen(argv[0]);
1743      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
1744      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
1745      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
1746      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
1747      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
1748
1749      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
1750      Rt_FreeArgv(argc, argv);
1751      continue;
1752    }
1753    else if(!strncasecmp(line, "# INV: formula", 14)  && formulaSummary) {
1754      invCheckFlag = 1;
1755      basicLength = 0;
1756      Rt_SplitLine(&line[14], &argc, &argv);
1757      if(cResult->resultForProperty == 0)
1758        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1759      if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
1760          rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
1761          propertyIndexSummary-1); 
1762          if(!rProperty) {
1763            rProperty = ALLOC(RtResultPropertys_t, 1);
1764            array_insert(RtResultPropertys_t *,cResult->resultForProperty,
1765            propertyIndexSummary-1, rProperty); 
1766            rProperty->lengthOfStem = -1;
1767            rProperty->lengthOfCycle = -1;
1768            rProperty->lengthOfInv = -1;
1769            rProperty->lengthOfCounterExample = -1; 
1770            rProperty->index = propertyIndexSummary;
1771          }
1772          if(rProperty->index != propertyIndexSummary) {
1773              fprintf(vis_stdout, "Error when compiling log file \n");
1774          }
1775      }
1776      else {
1777          rProperty = ALLOC(RtResultPropertys_t, 1);
1778          array_insert(RtResultPropertys_t *,cResult->resultForProperty,
1779          propertyIndexSummary-1, rProperty); 
1780          rProperty->lengthOfStem = -1;
1781          rProperty->lengthOfCycle = -1;
1782          rProperty->lengthOfInv = -1;
1783          rProperty->lengthOfCounterExample = -1; 
1784          rProperty->index = propertyIndexSummary;
1785      }
1786      if(argv[0][0] == 'f' || argv[0][0] == 'p')
1787        rProperty->failOrPass = strdup(argv[0]);
1788      else
1789        rProperty->failOrPass = strdup(argv[1]);
1790      basicLength = 0;
1791      stemLength = 0;
1792      cycleLength = 0;
1793      Rt_FreeArgv(argc, argv);
1794      propertyIndexSummary++;
1795      continue;
1796    }
1797    else if(!strncasecmp(line, "# INV: formula", 14)  && !formulaSummary) {
1798      invCheckFlag = 1;
1799      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
1800      countLineFlag = 0;
1801      nLine = 0;
1802      Rt_SplitLine(&line[14], &argc, &argv);
1803      if(Rt_IsNum(argv[0])) {
1804          if(cResult->resultForProperty == 0)
1805            cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1806          pIndex = atoi(argv[0]);
1807          if(array_n(cResult->resultForProperty) > pIndex) {
1808              rProperty = array_fetch(RtResultPropertys_t *,
1809              cResult->resultForProperty, pIndex-1); 
1810              if(!rProperty) {
1811                  rProperty = ALLOC(RtResultPropertys_t, 1);
1812                  array_insert(RtResultPropertys_t *,cResult->resultForProperty,
1813                  pIndex-1, rProperty); 
1814                  rProperty->lengthOfStem = -1;
1815                  rProperty->lengthOfCycle = -1;
1816                  rProperty->lengthOfInv = -1;
1817                  rProperty->lengthOfCounterExample = -1; 
1818                  rProperty->index = pIndex;
1819              }
1820              if(rProperty->index != pIndex) {
1821                  fprintf(vis_stdout, "Error when compiling log file \n");
1822              }
1823          }
1824          else {
1825              rProperty = ALLOC(RtResultPropertys_t, 1);
1826              array_insert(RtResultPropertys_t *,cResult->resultForProperty,
1827              pIndex-1, rProperty); 
1828              rProperty->lengthOfStem = -1;
1829              rProperty->lengthOfCycle = -1;
1830              rProperty->lengthOfInv = -1;
1831              rProperty->lengthOfCounterExample = -1; 
1832              rProperty->index = pIndex;
1833          }
1834          if(argv[1][0] == 'f' || argv[1][0] == 'p')
1835            rProperty->failOrPass = strdup(argv[1]);
1836          else
1837            rProperty->failOrPass = strdup(argv[2]);
1838          basicLength = 0;
1839          stemLength = 0;
1840          cycleLength = 0;
1841          Rt_FreeArgv(argc, argv);
1842      }
1843      continue;
1844    }
1845    else if(!strncasecmp(line, "# INV: Summary", 14)) {
1846      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
1847      countLineFlag = 0;
1848      nLine = 0;
1849      formulaSummary = 1;
1850      propertyIndexSummary = 1;
1851      continue;
1852    }
1853    next = strstr(line, "timeout");
1854    if(next == 0) 
1855        next = strstr(line, "Timeout");
1856    if(next) {
1857        if(!strncasecmp(next, "timeout occurred after", 22)) {
1858            cResult->bTimeOut = 1;
1859        }
1860        else if(!strncasecmp(next, "timeout after", 14)) {
1861            cResult->bTimeOut = 1;
1862        }
1863    }
1864    for(i=0; i<array_n(itemArr); i++) {
1865      item = array_fetch(RtCompareItems_t *, itemArr, i);
1866      len = strlen(item->itemName);
1867      if(!strncasecmp(item->itemName, line, len)) {
1868        newItem = ALLOC(RtCompareItems_t, 1);
1869        newItem->itemNickName = strdup(item->itemNickName);
1870        newItem->itemName = 0;
1871        newItem->value = 0;
1872        Rt_SplitLine(&line[len], &argc, &argv);
1873        newItem->value = strdup(argv[0]);
1874        if(cResult->compareItemArr == 0)
1875          cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
1876        array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
1877        Rt_FreeArgv(argc, argv);
1878        break;
1879      }
1880    }
1881  }
1882  if(commandBeginFlag == 1) {
1883    if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0) 
1884      cResult->resultForProperty = 0;
1885    cResult->compareItemArr = 0;
1886  }
1887
1888  cResult = 0;
1889  commandBeginFlag = 0;
1890  nLine = 0;
1891  countLineFlag = 0;
1892  rProperty = 0;
1893  while(fgets(line, 1024, fin2)) {
1894    if(countLineFlag) nLine++;
1895    if(line[0] == '\n') continue;
1896    if(!strncasecmp(line, "CommandEnd", 10)) {
1897      if(rProperty && countLineFlag)    {
1898        rProperty->lengthOfCounterExample = nLine;
1899        if(rProperty->lengthOfBasic > -1) {
1900          if(rProperty->lengthOfStem > -1)
1901            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1902          else
1903            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1904        }
1905      }
1906      countLineFlag = 0;
1907      rProperty = 0;
1908      nLine = 0;
1909      commandBeginFlag = 0;
1910    }
1911    else if(!strncasecmp(line, "CommandBegin", 12)) {
1912      propertyIndex = -1;
1913      rProperty = 0;
1914      formulaSummary = 0;
1915      commandBeginFlag = 1;
1916      Rt_SplitLine(line, &argc, &argv);
1917      if(designList->resultForCommandArr2 == 0)
1918        designList->resultForCommandArr2= array_alloc(RtCommandResults_t *, 0);
1919      cResult = ALLOC(RtCommandResults_t, 1);
1920      cResult->resultForProperty = 0;
1921      cResult->compareItemArr = 0;
1922      cResult->bTimeOut = 0;
1923      cResult->command = strdup(argv[1]);
1924      array_insert_last(RtCommandResults_t *, designList->resultForCommandArr2,
1925      cResult);
1926      Rt_FreeArgv(argc, argv);
1927      continue;
1928    }
1929    else if(!strncasecmp(line, "** cmd error", 12)) {
1930      if(cResult)
1931        cResult->error = 1;
1932      fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
1933      designList->designNickName);
1934      continue;
1935    }
1936    else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
1937      if(rProperty && countLineFlag)    {
1938        rProperty->lengthOfCounterExample = nLine;
1939        if(rProperty->lengthOfBasic > -1) {
1940          if(rProperty->lengthOfStem > -1)
1941            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1942          else
1943            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1944        }
1945      }
1946      countLineFlag = 0;
1947      nLine = 0;
1948      propertyIndex++;
1949      Rt_SplitLine(&line[13], &argc, &argv);
1950      rProperty = ALLOC(RtResultPropertys_t, 1);
1951      rProperty->lengthOfBasic = -1;
1952      rProperty->lengthOfStem = -1;
1953      rProperty->lengthOfCycle = -1;
1954      rProperty->lengthOfInv = -1;
1955      rProperty->lengthOfCounterExample = -1; 
1956      rProperty->index = propertyIndex;
1957      rProperty->failOrPass = strdup(argv[0]);
1958      if(cResult->resultForProperty == 0)
1959        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1960      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
1961      basicLength = 1;
1962      stemLength = 0;
1963      cycleLength = 0;
1964      invCheckFlag = 0;
1965      Rt_FreeArgv(argc, argv);
1966      continue;
1967    }
1968    else if((!strncasecmp(line, "# AMC: formula", 14) ||
1969             !strncasecmp(line, "# IMC: formula", 14) ||
1970             !strncasecmp(line, "# BMC: formula", 14) ||
1971             !strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
1972      if(rProperty && countLineFlag)    {
1973        rProperty->lengthOfCounterExample = nLine;
1974        if(rProperty->lengthOfBasic > -1) {
1975          if(rProperty->lengthOfStem > -1)
1976            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
1977          else
1978            rProperty->lengthOfStem = rProperty->lengthOfBasic;
1979        }
1980      }
1981      countLineFlag = 0;
1982      nLine = 0;
1983      propertyIndex++;
1984      Rt_SplitLine(&line[14], &argc, &argv);
1985      rProperty = ALLOC(RtResultPropertys_t, 1);
1986      rProperty->lengthOfBasic = -1;
1987      rProperty->lengthOfStem = -1;
1988      rProperty->lengthOfCycle = -1;
1989      rProperty->lengthOfInv = -1;
1990      rProperty->lengthOfCounterExample = -1; 
1991      rProperty->index = propertyIndex;
1992      rProperty->failOrPass = strdup(argv[0]);
1993      if(cResult->resultForProperty == 0)
1994        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
1995      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
1996      basicLength = 1;
1997      stemLength = 0;
1998      cycleLength = 0;
1999      invCheckFlag = 0;
2000      Rt_FreeArgv(argc, argv);
2001      continue;
2002    }
2003    else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
2004      if(rProperty && countLineFlag)    {
2005        rProperty->lengthOfCounterExample = nLine;
2006        if(rProperty->lengthOfBasic > -1) {
2007          if(rProperty->lengthOfStem > -1)
2008            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
2009          else
2010            rProperty->lengthOfStem = rProperty->lengthOfBasic;
2011        }
2012      }
2013      countLineFlag = 0;
2014      nLine = 0;
2015      propertyIndex++;
2016      Rt_SplitLine(&line[17], &argc, &argv);
2017      rProperty = ALLOC(RtResultPropertys_t, 1);
2018      rProperty->lengthOfBasic = -1;
2019      rProperty->lengthOfStem = -1;
2020      rProperty->lengthOfCycle = -1;
2021      rProperty->lengthOfInv = -1;
2022      rProperty->lengthOfCounterExample = -1; 
2023      rProperty->index = propertyIndex;
2024      rProperty->failOrPass = strdup(argv[0]);
2025      if(cResult->resultForProperty == 0)
2026        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
2027      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
2028      basicLength = 1;
2029      stemLength = 0;
2030      cycleLength = 0;
2031      invCheckFlag = 0;
2032      Rt_FreeArgv(argc, argv);
2033      continue;
2034    }
2035    else if(!strncasecmp(line, "--Fair path stem:", 17)) {
2036      basicLength = 0;
2037      stemLength = 1;
2038      cycleLength = 0;
2039      rProperty->lengthOfInv = -1;
2040      continue;
2041    }
2042    else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
2043      basicLength = 0;
2044      stemLength = 0;
2045      cycleLength = 1;
2046      rProperty->lengthOfInv = -1;
2047      continue;
2048    }
2049    else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
2050      basicLength = 0;
2051      stemLength = 0;
2052      cycleLength = 1;
2053      rProperty->lengthOfInv = -1;
2054      continue;
2055    }
2056    else if(!strncasecmp(line, "--State ", 8)) {
2057      if(rProperty == 0) {
2058        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
2059        continue;
2060      }
2061      Rt_SplitLine(&line[8], &argc, &argv);
2062      len = strlen(argv[0]);
2063      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
2064      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
2065      else if(stemLength)               rProperty->lengthOfStem = atoi(argv[0]);
2066      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
2067      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
2068      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
2069      if(countLineFlag == 0)    countLineFlag = 1;
2070      Rt_FreeArgv(argc, argv);
2071      continue;
2072    }
2073    else if(!strncasecmp(line, "--Goes to state ", 16)) {
2074      if(rProperty == 0) {
2075        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
2076        continue;
2077      }
2078      Rt_SplitLine(&line[16], &argc, &argv);
2079      len = strlen(argv[0]);
2080      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
2081      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
2082      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
2083      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
2084      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
2085      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
2086
2087      Rt_FreeArgv(argc, argv);
2088      continue;
2089    }
2090    else if(!strncasecmp(line, "# INV: formula", 14)  && formulaSummary) {
2091      Rt_SplitLine(&line[14], &argc, &argv);
2092      invCheckFlag = 1;
2093      if(cResult->resultForProperty == 0)
2094        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
2095      if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
2096          rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
2097          propertyIndexSummary-1); 
2098          if(!rProperty) {
2099            rProperty = ALLOC(RtResultPropertys_t, 1);
2100            array_insert(RtResultPropertys_t *,cResult->resultForProperty,
2101            propertyIndexSummary-1, rProperty); 
2102            rProperty->lengthOfStem = -1;
2103            rProperty->lengthOfCycle = -1;
2104            rProperty->lengthOfInv = -1;
2105            rProperty->lengthOfCounterExample = -1;
2106            rProperty->index = propertyIndexSummary;
2107          }
2108          if(rProperty->index != propertyIndexSummary) {
2109              fprintf(vis_stdout, "Error when compiling log file \n");
2110          }
2111      }
2112      else {
2113          rProperty = ALLOC(RtResultPropertys_t, 1);
2114          array_insert(RtResultPropertys_t *,cResult->resultForProperty,
2115          propertyIndexSummary-1, rProperty); 
2116          rProperty->lengthOfStem = -1;
2117          rProperty->lengthOfCycle = -1;
2118          rProperty->lengthOfInv = -1;
2119          rProperty->lengthOfCounterExample = -1;
2120          rProperty->index = propertyIndexSummary;
2121      }
2122      if(argv[0][0] == 'f' || argv[0][0] == 'p')
2123        rProperty->failOrPass = strdup(argv[0]);
2124      else
2125        rProperty->failOrPass = strdup(argv[1]);
2126      stemLength = 0;
2127      cycleLength = 0;
2128      Rt_FreeArgv(argc, argv);
2129      propertyIndexSummary++;
2130      continue;
2131    }
2132    else if(!strncasecmp(line, "# INV: formula", 14)  && !formulaSummary) {
2133      invCheckFlag = 1;
2134      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
2135      countLineFlag = 0;
2136      nLine = 0;
2137      Rt_SplitLine(&line[14], &argc, &argv);
2138      if(Rt_IsNum(argv[0])) {
2139          if(cResult->resultForProperty == 0)
2140            cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
2141          pIndex = atoi(argv[0]);
2142          if(array_n(cResult->resultForProperty) > pIndex) {
2143              rProperty = array_fetch(RtResultPropertys_t *,
2144              cResult->resultForProperty, pIndex-1); 
2145              if(!rProperty) {
2146                  rProperty = ALLOC(RtResultPropertys_t, 1);
2147                  array_insert(RtResultPropertys_t *,cResult->resultForProperty,
2148                  pIndex-1, rProperty); 
2149                  rProperty->lengthOfStem = -1;
2150                  rProperty->lengthOfCycle = -1;
2151                  rProperty->lengthOfInv = -1;
2152                  rProperty->lengthOfCounterExample = -1;
2153                  rProperty->index = pIndex;
2154              }
2155              if(rProperty->index != pIndex) {
2156                  fprintf(vis_stdout, "Error when compiling log file \n");
2157              }
2158          }
2159          else {
2160              rProperty = ALLOC(RtResultPropertys_t, 1);
2161              array_insert(RtResultPropertys_t *,cResult->resultForProperty,
2162              pIndex-1, rProperty); 
2163              rProperty->lengthOfStem = -1;
2164              rProperty->lengthOfCycle = -1;
2165              rProperty->lengthOfInv = -1;
2166              rProperty->lengthOfCounterExample = -1;
2167              rProperty->index = pIndex;
2168          }
2169          if(argv[1][0] == 'f' || argv[1][0] == 'p')
2170            rProperty->failOrPass = strdup(argv[1]);
2171          else
2172            rProperty->failOrPass = strdup(argv[2]);
2173          stemLength = 0;
2174          cycleLength = 0;
2175          Rt_FreeArgv(argc, argv);
2176      }
2177      continue;
2178    }
2179    else if(!strncasecmp(line, "# INV: Summary", 14)) {
2180      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
2181      countLineFlag = 0;
2182      nLine = 0;
2183      formulaSummary = 1;
2184      propertyIndexSummary = 1;
2185      continue;
2186    }
2187
2188    next = strstr(line, "timeout");
2189    if(next == 0) 
2190        next = strstr(line, "Timeout");
2191    if(next) {
2192        if(!strncasecmp(next, "timeout occurred after", 22)) {
2193            cResult->bTimeOut = 1;
2194        }
2195        else if(!strncasecmp(next, "timeout after", 14)) {
2196            cResult->bTimeOut = 1;
2197        }
2198    }
2199    for(i=0; i<array_n(itemArr); i++) {
2200      item = array_fetch(RtCompareItems_t *, itemArr, i);
2201      len = strlen(item->itemName);
2202      if(!strncasecmp(item->itemName, line, len)) {
2203        newItem = ALLOC(RtCompareItems_t, 1);
2204        newItem->itemNickName = strdup(item->itemNickName);
2205        newItem->itemName = 0;
2206        newItem->value = 0;
2207        Rt_SplitLine(&line[len], &argc, &argv);
2208        newItem->value = strdup(argv[0]);
2209        if(cResult->compareItemArr == 0)
2210          cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
2211        array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
2212        Rt_FreeArgv(argc, argv);
2213        break;
2214      }
2215    }
2216  }
2217  if(commandBeginFlag == 1) {
2218    if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0) 
2219      cResult->resultForProperty = 0;
2220    cResult->compareItemArr = 0;
2221  }
2222
2223  fclose(fin1);
2224  fclose(fin2);
2225  return(0);
2226}
2227
2228/**Function********************************************************************
2229
2230  Synopsis    [Check whether given string is digit or not.]
2231
2232  Description [ ]
2233
2234  Comment []
2235
2236  SideEffects []
2237
2238******************************************************************************/
2239static int
2240Rt_IsNum(char *tmp)
2241{
2242  int i, len;
2243
2244  len = strlen(tmp);
2245  for(i=0; i<len; i++) {
2246    if(!isdigit((int)tmp[i]))return(0);
2247  }
2248  return(1);
2249}
2250
2251
2252/**Function********************************************************************
2253
2254  Synopsis    [Exceute experiments based on 'ReferenceVis' and 'NewVis'. ]
2255
2256  Description [ ]
2257
2258  Comment []
2259
2260  SideEffects []
2261
2262******************************************************************************/
2263static int
2264Rt_ExecuteVis(RtConfigs_t *config,
2265              RtDesignLists_t *designList,
2266              int refAndNew, FILE *scriptOut)
2267{
2268  char temp[1024];
2269  char dir[1024];
2270  char exe[1024];
2271  char name[1024];
2272  char srcFile[1024];
2273  char outFile[1024];
2274
2275
2276  if(refAndNew == 1 && !config->bRefRun)return(0);
2277  if(refAndNew == 2 && !config->bNewRun)return(0);
2278
2279  if(refAndNew == 1) {
2280    sprintf(dir, "%s/%s", config->referenceOutDirectory, designList->designNickName); 
2281    sprintf(exe, "%s", config->referenceVis); 
2282    sprintf(name, "%s", designList->designNickName); 
2283  }
2284  if(refAndNew == 2) {
2285    sprintf(dir, "%s/%s", config->newOutDirectory, designList->designNickName); 
2286    sprintf(exe, "%s", config->newVis); 
2287    sprintf(name, "%s", designList->designNickName); 
2288  }
2289  sprintf(srcFile, "%s/%s.src", dir, name);
2290  sprintf(outFile, "%s/%s.out", dir, name);
2291
2292  if(scriptOut) {
2293  /**
2294    sprintf(temp, "%s -x -f %s/%s.src >& %s/%s.out", exe, dir, name, dir, name);
2295    **/
2296    sprintf(temp, "%s -x -f %s.src >& %s.out", exe, name, name);
2297    fprintf(scriptOut, "echo %s begin\n", designList->designNickName);
2298    fprintf(scriptOut, "cd %s\n", dir);
2299    fprintf(scriptOut, "%s\n", temp);
2300    fprintf(scriptOut, "cd ../../\n");
2301  }
2302  else {
2303    sprintf(temp, "%s -x -f %s/%s.src > %s/%s.out", exe, dir, name, dir, name);
2304    if (system(temp))
2305      return(1);
2306  }
2307  /**
2308    sprintf(temp, "%s -x -f %s/%s.src", exe, dir, name);
2309   **/
2310
2311  return(0);
2312}
2313
2314/**Function********************************************************************
2315
2316  Synopsis    [Write the script file for VIS execution. ]
2317
2318  Description [ Wirte  the batch script for experiments.  The variables and the
2319aliases are defined by examining the fields of the test case description in the
2320design file.   It uses TemplateFile  to make a  script. So The  template should
2321refer  to the  defined aliases  and  variables to  tailor itself  to each  test
2322case. ]
2323
2324  Comment []
2325
2326  SideEffects []
2327
2328******************************************************************************/
2329static int
2330Rt_WriteBatchCommand(RtConfigs_t *config, 
2331                     RtDesignLists_t *designList)
2332{
2333  FILE *fout1;
2334  FILE *fout2;
2335  char filename1[1024];
2336  char filename2[1024];
2337  char refDir[1024];
2338  char temp[1024];
2339  int i;
2340  RtCommandResults_t *cTemplate;
2341  array_t *cTemplateArrOld;
2342  array_t *cTemplateArrNew;
2343 
2344  fout1 = fout2 = 0;
2345  if(config->bRefRun) {
2346    sprintf(temp, "\\mkdir -p %s/%s", config->referenceOutDirectory, 
2347                                   designList->designNickName);
2348    if (system(temp))
2349      return(1);
2350  }
2351  if(config->bNewRun) {
2352    sprintf(temp, "\\mkdir -p %s/%s", config->newOutDirectory, 
2353                                   designList->designNickName);
2354    if (system(temp))
2355      return(1);
2356  }
2357
2358  if(config->bRefRun) {
2359    sprintf(filename1, "%s/%s/%s.src", config->referenceOutDirectory, 
2360                                     designList->designNickName,
2361                                     designList->designNickName);
2362    if(!(fout1 = fopen(filename1, "w"))) {
2363      fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename1);
2364      return(0);
2365    }
2366  }
2367  if(config->bNewRun) {
2368    sprintf(filename2, "%s/%s/%s.src", config->newOutDirectory, 
2369                                     designList->designNickName,
2370                                     designList->designNickName);
2371    if(!(fout2 = fopen(filename2, "w"))) {
2372      fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename2);
2373      fclose(fout1);
2374      return(0);
2375    }
2376  }
2377
2378  cTemplateArrOld = config->refCommandTemplateArr;
2379  cTemplateArrNew = config->newCommandTemplateArr;
2380  sprintf(refDir, "%s/%s", config->designDirectory, designList->designDirectory);
2381
2382  if(config->bRefRun) {
2383  /**
2384    fprintf(fout1, "set vis_stdout %s/%s/%s.out\n",
2385       config->referenceOutDirectory, designList->designNickName, designList->designNickName);
2386    fprintf(fout1, "set vis_stderr %s/%s/%s.out\n",
2387       config->referenceOutDirectory, designList->designNickName, designList->designNickName);
2388   **/
2389    fprintf(fout1, "set BaseName %s\n", designList->designNickName);
2390  }
2391  if(config->bNewRun) {
2392  /**
2393    fprintf(fout2, "set vis_stdout %s/%s/%s.out\n",
2394       config->newOutDirectory, designList->designNickName, designList->designNickName);
2395    fprintf(fout2, "set vis_stderr %s/%s/%s.out\n",
2396       config->newOutDirectory, designList->designNickName, designList->designNickName);
2397   **/
2398    fprintf(fout2, "set BaseName %s\n", designList->designNickName);
2399  }
2400
2401  if(designList->blifFile) {
2402    if(config->bRefRun)
2403    fprintf(fout1, "set BlifFile %s/%s\n", refDir, designList->blifFile);
2404    if(config->bNewRun)
2405    fprintf(fout2, "set BlifFile %s/%s\n", refDir, designList->blifFile);
2406  }
2407  if(designList->ordFile) {
2408    if(config->bRefRun)
2409    fprintf(fout1, "set OrdFile %s/%s\n", refDir, designList->ordFile);
2410    if(config->bNewRun)
2411    fprintf(fout2, "set OrdFile %s/%s\n", refDir, designList->ordFile);
2412  }
2413  if(designList->ctlFile) {
2414    if(config->bRefRun)
2415    fprintf(fout1, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
2416    if(config->bNewRun)
2417    fprintf(fout2, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
2418  }
2419  if(designList->invFile) {
2420    if(config->bRefRun)
2421    fprintf(fout1, "set InvFile %s/%s\n", refDir, designList->invFile);
2422    if(config->bNewRun)
2423    fprintf(fout2, "set InvFile %s/%s\n", refDir, designList->invFile);
2424  }
2425  if(designList->leFile) {
2426    if(config->bRefRun)
2427    fprintf(fout1, "set LeFile %s/%s\n", refDir, designList->leFile);
2428    if(config->bNewRun)
2429    fprintf(fout2, "set LeFile %s/%s\n", refDir, designList->leFile);
2430  }
2431  if(designList->ltlFile) {
2432    if(config->bRefRun)
2433    fprintf(fout1, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
2434    if(config->bNewRun)
2435    fprintf(fout2, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
2436  }
2437  if(designList->fairFile) {
2438    if(config->bRefRun)
2439    fprintf(fout1, "set FairFile %s/%s\n", refDir, designList->fairFile);
2440    if(config->bNewRun)
2441    fprintf(fout2, "set FairFile %s/%s\n", refDir, designList->fairFile);
2442  }
2443  if(designList->hintFile) {
2444    if(config->bRefRun)
2445    fprintf(fout1, "set HintFile %s/%s\n", refDir, designList->hintFile);
2446    if(config->bNewRun)
2447    fprintf(fout2, "set HintFile %s/%s\n", refDir, designList->hintFile);
2448  }
2449
2450  if(config->bRefRun) {
2451    if(designList->fairFile)
2452      fprintf(fout1, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
2453    else
2454      fprintf(fout1, "set fairOption \" \"\n");
2455  }
2456  if(config->bNewRun) {
2457    if(designList->fairFile)
2458      fprintf(fout2, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
2459    else
2460      fprintf(fout2, "set fairOption \" \"\n");
2461  }
2462
2463
2464  if(config->bDefaultInitCommand) {
2465    if(config->bRefRun) {
2466      fprintf(fout1, "echo CommandBegin init\n");
2467      if(designList->ordFile) {
2468        if(designList->bIsMv)
2469           fprintf(fout1, "rlmv $BlifFile\n");
2470        else
2471           fprintf(fout1, "read_blif $BlifFile\n");
2472        fprintf(fout1, "flatten_hierarchy\n");
2473        fprintf(fout1, "static_order -s partial $OrdFile\n");
2474        fprintf(fout1, "build_partition_mdds\n");
2475        if(designList->fairFile)
2476          fprintf(fout1, "rf $FairFile\n");
2477      }
2478      else {
2479        if(designList->bIsMv)
2480           fprintf(fout1, "rlmv $BlifFile\n");
2481        else
2482           fprintf(fout1, "read_blif $BlifFile\n");
2483        fprintf(fout1, "echo init\n");
2484        fprintf(fout1, "init\n");
2485        if(designList->fairFile)
2486          fprintf(fout1, "rf $FairFile\n");
2487      }
2488      fprintf(fout1, "time\n");
2489      fprintf(fout1, "print_bdd_stats\n");
2490      fprintf(fout1, "echo CommandEnd init\n");
2491    }
2492    if(config->bNewRun) {
2493      fprintf(fout2, "echo CommandBegin init\n");
2494      if(designList->ordFile) {
2495        if(designList->bIsMv)
2496           fprintf(fout2, "rlmv $BlifFile\n");
2497        else
2498           fprintf(fout2, "read_blif $BlifFile\n");
2499        fprintf(fout2, "flatten_hierarchy\n");
2500        fprintf(fout2, "static_order -s partial $OrdFile\n");
2501        fprintf(fout2, "build_partition_mdds\n");
2502        if(designList->fairFile)
2503          fprintf(fout2, "rf $FairFile\n");
2504      }
2505      else {
2506        if(designList->bIsMv)
2507           fprintf(fout2, "rlmv $BlifFile\n");
2508        else
2509           fprintf(fout2, "read_blif $BlifFile\n");
2510        fprintf(fout2, "echo init\n");
2511        fprintf(fout2, "init\n");
2512        if(designList->fairFile)
2513          fprintf(fout2, "rf $FairFile\n");
2514      }
2515      fprintf(fout2, "time\n");
2516      fprintf(fout2, "print_bdd_stats\n");
2517      fprintf(fout2, "echo CommandEnd init\n");
2518    } 
2519  }
2520  else {
2521    /**
2522     * Alias read_model, set_fairness and order_vars  based on
2523     * whether the design list specifies a .mv file or a .blif file
2524     * as model file.
2525     **/
2526    if(config->bRefRun) {
2527      if(designList->bIsMv)
2528        fprintf(fout1, "alias read_model \"rlmv $BlifFile\"\n");
2529      else
2530        fprintf(fout1, "alias read_model \"read_blif $BlifFile\"\n");
2531      if(designList->fairFile) 
2532        fprintf(fout1, "alias set_fairness \"read_fairness $FairFile\"\n");
2533      else
2534        fprintf(fout1, "alias set_fairness \" \"\n");
2535      if(designList->ordFile)   
2536        fprintf(fout1, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
2537      else
2538        fprintf(fout1, "alias order_vars \"so\"\n");
2539    }
2540    if(config->bNewRun) {
2541      if(designList->bIsMv)
2542        fprintf(fout2, "alias read_model \"rlmv $BlifFile\"\n");
2543      else
2544        fprintf(fout2, "alias read_model \"read_blif $BlifFile\"\n");
2545      if(designList->fairFile) 
2546        fprintf(fout2, "alias set_fairness \"read_fairness $FairFile\"\n");
2547      else
2548        fprintf(fout2, "alias set_fairness \" \"\n");
2549      if(designList->ordFile)   
2550        fprintf(fout2, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
2551      else
2552        fprintf(fout2, "alias order_vars \"so\"\n");
2553    } 
2554  }
2555
2556  if(config->bRefRun) {
2557    for(i=0; i<array_n(cTemplateArrOld); i++) {
2558      cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrOld, i);
2559      fprintf(fout1, "%s\n", cTemplate->command);
2560    }
2561    fprintf(fout1, "quit\n");
2562    fclose(fout1);
2563  }
2564  if(config->bNewRun) {
2565    for(i=0; i<array_n(cTemplateArrNew); i++) {
2566      cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrNew, i);
2567      fprintf(fout2, "%s\n", cTemplate->command);
2568    }
2569    fprintf(fout2, "quit\n");
2570    fclose(fout2);
2571  }
2572
2573  return(0);
2574}
2575
2576/**Function********************************************************************
2577
2578  Synopsis    [ Read command template and check whether it contains illegal command and alias. ]
2579
2580  Description [ When read the template,  if we meet the string followed by '$',
2581then check whether  that string is reserved  word or not. If the  string is not
2582reserved work then we consider that as a variable.]
2583
2584  Comment []
2585
2586  SideEffects []
2587
2588******************************************************************************/
2589
2590static int
2591Rt_ReadCommandTemplate(RtConfigs_t * config)
2592{
2593  FILE  *fin;
2594  char line[1024];
2595  char *filename;
2596  char temp[1024];
2597  int i;
2598  RtCommandResults_t *cResult;
2599  int argc;
2600  char **argv;
2601  char *next, *tmp;
2602
2603  if(config->bRefRun) {
2604  filename = config->refCommandTemplate;
2605  if(!(fin = fopen(filename, "r"))) {
2606    fprintf(vis_stdout, "Error : Can't open command template file '%s' for reference\n", filename);
2607    return(1);
2608  }
2609
2610  if(config->keyWordTable == 0)
2611    config->keyWordTable = st_init_table(strcmp, st_strhash);
2612  config->refCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
2613  while(fgets(line, 1024, fin)) {
2614    if(line[0] == '#')  continue;
2615    cResult = ALLOC(RtCommandResults_t, 1);
2616    cResult->resultForProperty = 0;
2617    cResult->compareItemArr = 0;
2618    cResult->command = 0;
2619    Rt_SplitLine(line, &argc, &argv);
2620    temp[0] = '\0';
2621    for(i=0; i<argc; i++) {
2622      strcat(temp, argv[i]); 
2623      if(i+1 != argc) strcat(temp, " ");
2624      if(argv[i][0] == '$') {
2625         if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
2626            next = strdup(argv[i]);
2627            st_insert(config->keyWordTable, next, next);
2628         }
2629      }
2630    }
2631    Rt_FreeArgv(argc, argv);
2632    cResult->command = strdup(temp);
2633    array_insert_last(RtCommandResults_t *, config->refCommandTemplateArr, cResult);
2634
2635  }
2636  fclose(fin);
2637  }
2638
2639  if(config->bNewRun) {
2640  filename = config->newCommandTemplate;
2641  if(!(fin = fopen(filename, "r"))) {
2642    fprintf(vis_stdout, "Error : Can't open command template file '%s' for new\n", filename);
2643    return(1);
2644  }
2645  if(config->keyWordTable == 0)
2646    config->keyWordTable = st_init_table(strcmp, st_strhash);
2647  config->newCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
2648  while(fgets(line, 1024, fin)) {
2649    if(line[0] == '#')  continue;
2650    cResult = ALLOC(RtCommandResults_t, 1);
2651    cResult->resultForProperty = 0;
2652    cResult->compareItemArr = 0;
2653    cResult->command = 0;
2654    Rt_SplitLine(line, &argc, &argv);
2655    temp[0] = '\0';
2656    for(i=0; i<argc; i++) {
2657      strcat(temp, argv[i]); 
2658      if(i+1 != argc) strcat(temp, " ");
2659      if(argv[i][0] == '$') {
2660         if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
2661            next = strdup(argv[i]);
2662            st_insert(config->keyWordTable, next, next);
2663         }
2664      }
2665    }
2666    Rt_FreeArgv(argc, argv);
2667    cResult->command = strdup(temp);
2668    array_insert_last(RtCommandResults_t *, config->newCommandTemplateArr, cResult);
2669  }
2670  fclose(fin);
2671  }
2672  return(0);
2673}
2674
2675
2676/**Function********************************************************************
2677
2678  Synopsis    [Read the design list. ]
2679
2680  Description [  To specify the  type of file,  we use extension of  file name,
2681such  as .mv,  .blif,  .ord, .inv,  .ctl,  .fair, .ltl  and  .hint.  Each  line
2682consists  of white  space-separated fields.   The first  is a  (relative) path,
2683while the second is the  collection name.  The smallest collection will specify
2684one .mv  or one .blif file with  path and collection name.  Lines starting with
2685'#' are interpreted as comments and are skipped, as in all files read]
2686
2687  Comment []
2688
2689  SideEffects []
2690
2691******************************************************************************/
2692static int
2693Rt_ReadDesignListFile(RtConfigs_t * config)
2694{
2695  FILE  *fin;
2696  char line[1024];
2697  char *filename, *str;
2698  char suffix[1024];
2699  int i, j, index, bDot, strLen;
2700  RtDesignLists_t *designList;
2701  int argc;
2702  char **argv;
2703
2704  filename = config->designList;
2705
2706  if(!(fin = fopen(filename, "r"))) {
2707    fprintf(vis_stdout, "Error : Can't open design list file '%s'\n", filename);
2708    return(1);
2709  }
2710
2711  config->designListArr = array_alloc(RtDesignLists_t *, 0);
2712  while(fgets(line, 1024, fin)) {
2713    if(line[0] == '#')  continue;
2714    if(line[0] == '\n') continue;
2715    Rt_SplitLine(line, &argc, &argv);
2716    designList = ALLOC(RtDesignLists_t, 1);
2717    designList->designDirectory = strdup(argv[0]);
2718    designList->designNickName = strdup(argv[1]);
2719    designList->blifFile = strdup(argv[2]);
2720    designList->leFile = 0;
2721    designList->ltlFile = 0;
2722    designList->ordFile = 0;
2723    designList->hintFile = 0;
2724    designList->ctlFile = 0;
2725    designList->invFile = 0;
2726    designList->fairFile = 0;
2727    designList->resultForCommandArr1 = 0;
2728    designList->resultForCommandArr2 = 0;
2729
2730    str = argv[2];
2731    index = bDot = 0;
2732    strLen = strlen(str);
2733    for(j=strLen; j>=0; j--) {
2734      if(str[j] == '.') {       
2735        bDot = 1; 
2736        break;
2737      }
2738    }
2739    if(bDot==0) {
2740      fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
2741      designList->designNickName);
2742      Rt_FreeArgv(argc, argv);
2743      free(designList);
2744      continue;
2745    }
2746    else {
2747      j++;
2748      for(;str[j] != '\0'; j++) {
2749        suffix[index++] = str[j];
2750      }
2751    }
2752    suffix[index] = '\0';
2753
2754    if(!strcasecmp(suffix, "blif")) 
2755      designList->bIsMv = 0;
2756    else if(!strcasecmp(suffix, "mv")) 
2757      designList->bIsMv = 1;
2758    else {
2759      fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
2760      designList->designNickName);
2761      Rt_FreeArgv(argc, argv);
2762      free(designList);
2763      continue;
2764    }
2765
2766    for(i=3; i<argc; i++) {
2767      str = argv[i];
2768      index = bDot = 0;
2769      strLen = strlen(str);
2770      for(j=strLen; j>=0; j--) {
2771        if(str[j] == '.') {     
2772          bDot = 1; 
2773          break;
2774        }
2775      }
2776      if(bDot==0) {
2777        fprintf(vis_stdout, "Error : Illegal suffix of file '%s' in design list '%s'\n", 
2778          argv[i], designList->designNickName);
2779        Rt_FreeArgv(argc, argv);
2780        free(designList);
2781        continue;
2782      }
2783      else {
2784        j++;
2785        for(;str[j] != '\0'; j++) {
2786          suffix[index++] = str[j];
2787        }
2788      }
2789      suffix[index] = '\0';
2790      if(!strcasecmp(suffix, "ctl")) 
2791        designList->ctlFile = strdup(argv[i]);
2792      else if(!strcasecmp(suffix, "fair")) 
2793        designList->fairFile = strdup(argv[i]);
2794      else if(!strcasecmp(suffix, "inv")) 
2795        designList->invFile = strdup(argv[i]);
2796      else if(!strcasecmp(suffix, "le")) 
2797        designList->leFile = strdup(argv[i]);
2798      else if(!strcasecmp(suffix, "ltl")) 
2799        designList->ltlFile = strdup(argv[i]);
2800      else if(!strcasecmp(suffix, "ord")) 
2801        designList->ordFile = strdup(argv[i]);
2802      else if(!strcasecmp(suffix, "hint")) 
2803        designList->hintFile = strdup(argv[i]);
2804      else {
2805        fprintf(vis_stdout, "Illegal suffix of file '%s'\n", argv[i]);
2806        Rt_FreeArgv(argc, argv);
2807        fclose(fin);
2808        return(1);
2809      }
2810    }
2811    array_insert_last(RtDesignLists_t *, config->designListArr, designList);
2812    Rt_FreeArgv(argc, argv);
2813  }
2814
2815  fclose(fin);
2816  return(0);
2817}
2818
2819/**Function********************************************************************
2820
2821  Synopsis    [Read Configuration file ]
2822
2823  Description [Read each line of Configuration file and fill the data
2824  structure.  A line beginning with '#' is a comment. ]
2825
2826  Comment []
2827
2828  SideEffects []
2829
2830******************************************************************************/
2831static RtConfigs_t *
2832Rt_ReadConfigFile(char *filename)
2833{
2834  FILE  *fin;
2835  char line[1024];
2836  char temp[1024];
2837  RtConfigs_t *config;
2838  int i, argc;
2839  int errorFlag;
2840  char **argv;
2841  RtCompareItems_t *cItem;
2842
2843  if(!(fin = fopen(filename, "r"))) {
2844    fprintf(vis_stdout, "Error : Can't open configuration file '%s'\n", filename);
2845    return(0);
2846  }
2847
2848  config = ALLOC(RtConfigs_t, 1);
2849  memset(config, 0, sizeof(RtConfigs_t));
2850  config->configurationFile = strdup(filename);
2851  config->compareItemArr = 0;
2852  config->bRefOnly = 0;
2853  config->keyWordTable = 0;
2854  config->bRefRun = -1;
2855  config->bNewRun = -1;
2856  while(fgets(line, 1024, fin)) {
2857    if(line[0] == '#')  continue;
2858    if(line[0] == '\n') continue;
2859    Rt_SplitLine(line, &argc, &argv);
2860    if(argv[0][0] == '\n')      continue;
2861    if(argc < 3)        continue;
2862    if(argv[2] == 0)    continue;
2863    if(!strcasecmp("DesignDirectory", argv[0])) {
2864      config->designDirectory = strdup(argv[2]);
2865    }
2866    else if(!strcasecmp("ReferenceVis", argv[0])) {
2867      config->referenceVis = strdup(argv[2]);
2868    }
2869    else if(!strcasecmp("ReferenceVisNickName", argv[0])) {
2870      config->referenceVisNickName = strdup(argv[2]);
2871    }
2872    else if(!strcasecmp("ReferenceVisOptionFile", argv[0])) {
2873      config->referenceVisOptionFile = strdup(argv[2]);
2874    }
2875    else if(!strcasecmp("ReferenceOutputDir", argv[0])) {
2876      config->referenceOutDirectory = strdup(argv[2]);
2877    }
2878    else if(!strcasecmp("bRefRun", argv[0])) {
2879      config->bRefRun = Rt_SetBooleanValue(argv[2], argv[0]);
2880    }
2881    else if(!strcasecmp("NewVis", argv[0])) {
2882      config->newVis = strdup(argv[2]);
2883    }
2884    else if(!strcasecmp("NewVisNickName", argv[0])) {
2885      config->newVisNickName = strdup(argv[2]);
2886    }
2887    else if(!strcasecmp("NewVisOptionFile", argv[0])) {
2888      config->newVisOptionFile = strdup(argv[2]);
2889    }
2890    else if(!strcasecmp("NewOutputDir", argv[0])) {
2891      config->newOutDirectory = strdup(argv[2]);
2892    }
2893    else if(!strcasecmp("bNewRun", argv[0])) {
2894      config->bNewRun = Rt_SetBooleanValue(argv[2], argv[0]);
2895    }
2896    else if(!strcasecmp("NewCommandTemplate", argv[0])) {
2897      config->newCommandTemplate = strdup(argv[2]);
2898    }
2899    else if(!strcasecmp("RefCommandTemplate", argv[0])) {
2900      config->refCommandTemplate = strdup(argv[2]);
2901    }
2902    else if(!strcasecmp("DesignList", argv[0])) {
2903      config->designList = strdup(argv[2]);
2904    }
2905    else if(!strcasecmp("bCompareCounterExample", argv[0])) {
2906      config->bCompareCounterExample = Rt_SetBooleanValue(argv[2], argv[0]);
2907    }
2908    else if(!strcasecmp("bFinalResultOnly", argv[0])) {
2909      config->bFinalResultOnly = Rt_SetBooleanValue(argv[2], argv[0]);
2910    }
2911    else if(!strcasecmp("bDontRemoveTempFile", argv[0])) {
2912      config->bDontRemoveTempFile = Rt_SetBooleanValue(argv[2], argv[0]);
2913    }
2914    else if(!strcasecmp("bDefaultInitCommand", argv[0])) {
2915      config->bDefaultInitCommand = Rt_SetBooleanValue(argv[2], argv[0]);
2916    }
2917    else if(!strcasecmp("ResultForPerformance", argv[0])) {
2918      config->resultForPerformance = strdup(argv[2]);
2919    }
2920    else if(!strcasecmp("ResultForCounterExample", argv[0])) {
2921      config->resultForCounterExample = strdup(argv[2]);
2922    }
2923    else if(!strcasecmp("CompareItem", argv[0])) {
2924      cItem = ALLOC(RtCompareItems_t, 1);
2925      cItem->itemNickName = strdup(argv[2]);
2926      temp[0] = '\0';
2927      for(i=4; i<argc; i++) {
2928        strcat(temp, argv[i]);
2929        if(i+1 != argc) strcat(temp, " ");
2930      }
2931      cItem->itemName = strdup(temp);
2932      cItem->value = 0;
2933      if(!config->compareItemArr)
2934        config->compareItemArr = array_alloc(RtCompareItems_t *, 0);
2935      array_insert_last(RtCompareItems_t *, config->compareItemArr, cItem);
2936    }
2937    else {
2938      fprintf(vis_stdout, "Unknown option '%s' in configuration file\n", argv[0]);
2939      free(config);
2940      Rt_FreeArgv(argc, argv);
2941      fclose(fin);
2942      return(0);
2943    }
2944    Rt_FreeArgv(argc, argv);
2945  }
2946  fclose(fin);
2947
2948  errorFlag = 0;
2949  if(config->designDirectory == 0) {
2950    fprintf(stdout, "DesignDirectory is not specified in configuration file '%s'\n",
2951                filename);
2952    errorFlag = 1;
2953  }
2954  if(config->referenceVis == 0) {
2955    fprintf(stdout, "ReferenceVis is not specified in configuration file '%s'\n",
2956                filename);
2957    errorFlag = 1;
2958  }
2959  if(config->referenceVisNickName == 0) {
2960    fprintf(stdout, "ReferenceVisNickName is not specified in configuration file '%s'\n",
2961                filename);
2962    errorFlag = 1;
2963  }
2964  if(config->referenceOutDirectory == 0) {
2965    fprintf(stdout, "ReferenceOutDirectory is not specified in configuration file '%s'\n",
2966                filename);
2967    errorFlag = 1;
2968  }
2969  if(config->newVis == 0) {
2970    fprintf(stdout, "NewVis is not specified in configuration file '%s'\n",
2971                filename);
2972    errorFlag = 1;
2973  }
2974  if(config->newVisNickName == 0) {
2975    fprintf(stdout, "NewVisNickName is not specified in configuration file '%s'\n",
2976                filename);
2977    errorFlag = 1;
2978  }
2979  if(config->newOutDirectory == 0) {
2980    fprintf(stdout, "NewOutDirectory is not specified in configuration file '%s'\n",
2981                filename);
2982    errorFlag = 1;
2983  }
2984  if(config->bRefRun == -1) {
2985    fprintf(stdout, "bRefRun is not specified in configuration file '%s'\n",
2986                filename);
2987    errorFlag = 1;
2988  }
2989  if(config->bNewRun == -1) {
2990    fprintf(stdout, "bNewRun is not specified in configuration file '%s'\n",
2991                filename);
2992    errorFlag = 1;
2993  }
2994  if(config->designList == 0) {
2995    fprintf(stdout, "DesignList is not specified in configuration file '%s'\n",
2996                filename);
2997    errorFlag = 1;
2998  }
2999  if(config->newCommandTemplate == 0) {
3000    fprintf(stdout, "NewCommandTemplate is not specified in configuration file '%s'\n",
3001                filename);
3002    errorFlag = 1;
3003  }
3004  if(config->refCommandTemplate == 0) {
3005    fprintf(stdout, "RefCommandTemplate is not specified in configuration file '%s'\n",
3006                filename);
3007    errorFlag = 1;
3008  }
3009
3010  if(config->compareItemArr == 0 || array_n(config->compareItemArr) == 0) {
3011    fprintf(stdout, "CompareItem is not specified in configuration file '%s'\n",
3012                filename);
3013    errorFlag = 1;
3014  }
3015
3016  if(errorFlag) {
3017    free(config);
3018    return(0);
3019  }
3020 
3021  return(config);
3022}
3023
3024/**Function********************************************************************
3025
3026  Synopsis    [Return 1 if the string contains 'TURE', otherwise return 0. ]
3027
3028  Description [ ]
3029
3030  Comment []
3031
3032  SideEffects []
3033
3034******************************************************************************/
3035static int
3036Rt_SetBooleanValue(char *str, char *option)
3037{
3038
3039  if(!strcmp("TRUE", str) || !strcmp("1", str))
3040    return(1);
3041  else if(!strcmp("FALSE", str) || !strcmp("0", str))
3042    return(0);
3043  else {
3044    fprintf(vis_stdout, "Warning : Illegal argement for '%s'\n", option);
3045    fprintf(vis_stdout, "          Set with default '%s : TURE'\n", option);
3046    return(1);
3047  }
3048}
3049
3050/**Function********************************************************************
3051
3052  Synopsis    [Split line with respect to whitespace, '#' and ';', and save
3053  individual strings in array named 'argv'. ]
3054
3055  Description [ ]
3056
3057  Comment []
3058
3059  SideEffects []
3060
3061******************************************************************************/
3062static char *
3063Rt_SplitLine(
3064  char * command,
3065  int * argc,
3066  char *** argv)
3067{
3068  register char *p, *start, c;
3069  register int i, j;
3070  register char *new_arg;
3071  array_t *argv_array;
3072  int single_quote, double_quote;
3073
3074  argv_array = array_alloc(char *, 5);
3075
3076  p = command;
3077  for(;;) {
3078    /* skip leading white space */
3079    while (isspace((int)(*p))) {
3080      p++;
3081    }
3082
3083    /* skip until end of this token */
3084    single_quote = double_quote = 0;
3085    for(start = p; (c = *p) != '\0'; p++) {
3086      if (c == ';' || c == '#' || isspace((int)c)) {
3087        if (! single_quote && ! double_quote) {
3088          break;
3089        }
3090      }
3091      if (c == '\'') {
3092        single_quote = ! single_quote;
3093      }
3094      if (c == '"') {
3095        double_quote = ! double_quote;
3096      }
3097    }
3098    if (single_quote || double_quote) {
3099      (void) fprintf(vis_stderr, "** cmd warning: ignoring unbalanced quote ...\n");
3100    }
3101    if (start == p) break;
3102
3103    new_arg = ALLOC(char, p - start + 1);
3104    j = 0;
3105    for(i = 0; i < p - start; i++) {
3106      c = start[i];
3107      if ((c != '\'') && (c != '\"')) {
3108        new_arg[j++] = isspace((int)c) ? ' ' : start[i];
3109      }
3110    }
3111    new_arg[j] = '\0';
3112    array_insert_last(char *, argv_array, new_arg);
3113  }
3114
3115  *argc = array_n(argv_array);
3116  *argv = array_data(char *, argv_array);
3117  array_free(argv_array);
3118  if (*p == ';') {
3119    p++;
3120  }
3121  else if (*p == '#') {
3122    for(; *p != 0; p++) ;               /* skip to end of line */
3123  }
3124  return p;
3125}   
3126
3127
3128static void
3129Rt_FreeRtConfig(RtConfigs_t * config)
3130{
3131  int i;
3132  RtDesignLists_t *list;
3133  array_t *itemArr, *designArr, *resultArr;
3134  st_table *table;
3135  RtCompareItems_t *item;
3136  RtCommandResults_t *result;
3137  st_generator *gen;
3138  char *keyWord;
3139
3140
3141  if(config == 0)       return;
3142 
3143  if(config->designDirectory)           free(config->designDirectory);
3144  if(config->designList)                free(config->designList);
3145  if(config->scriptFile)                free(config->scriptFile);
3146  if(config->resultForCounterExample)   free(config->resultForCounterExample);
3147  if(config->resultForPerformance)      free(config->resultForPerformance);
3148
3149  if(config->referenceVis)              free(config->referenceVis);
3150  if(config->referenceVisNickName)      free(config->referenceVisNickName);
3151  if(config->referenceVisOptionFile)    free(config->referenceVisOptionFile);
3152  if(config->referenceOutDirectory)     free(config->referenceOutDirectory);
3153  if(config->refCommandTemplate)        free(config->refCommandTemplate);
3154
3155  if(config->newVis)                    free(config->newVis);
3156  if(config->newVisNickName)            free(config->newVisNickName);
3157  if(config->newVisOptionFile)          free(config->newVisOptionFile);
3158  if(config->newOutDirectory)           free(config->newOutDirectory);
3159  if(config->newCommandTemplate)        free(config->newCommandTemplate);
3160
3161  itemArr = config->compareItemArr;
3162  if(itemArr) {
3163    for(i=0; i<array_n(itemArr); i++) {
3164      item = array_fetch(RtCompareItems_t *, itemArr, i);
3165      Rt_FreeCompareItem(item);
3166    }
3167    array_free(itemArr);
3168  }
3169
3170  designArr = config->designListArr;
3171  if(designArr) {
3172    for(i=0; i<array_n(designArr); i++) {
3173      list = array_fetch(RtDesignLists_t *, designArr, i);
3174      Rt_FreeDesignList(list);
3175    }
3176    array_free(designArr);
3177  }
3178
3179  resultArr = config->refCommandTemplateArr;
3180  if(resultArr) {
3181    for(i=0; i<array_n(resultArr); i++) {
3182      result = array_fetch(RtCommandResults_t *, resultArr, i);
3183      Rt_FreeCommandResult(result);
3184    }
3185    array_free(resultArr);
3186  }
3187
3188  resultArr = config->newCommandTemplateArr;
3189  if(resultArr) {
3190    for(i=0; i<array_n(resultArr); i++) {
3191      result = array_fetch(RtCommandResults_t *, resultArr, i);
3192      Rt_FreeCommandResult(result);
3193    }
3194    array_free(resultArr);
3195  }
3196
3197  if(config->keyWordTable) {
3198    table = config->keyWordTable;
3199    st_foreach_item(table, gen, &keyWord, NIL(char *)) {
3200      free(keyWord);
3201    }
3202    st_free_table(table);
3203  }
3204
3205}
3206
3207static void
3208Rt_FreeDesignList(RtDesignLists_t *list)
3209{
3210  array_t *resultArr;
3211  RtCommandResults_t *result;
3212  int i;
3213
3214  if(list == 0) return;
3215
3216  if(list->designDirectory)     free(list->designDirectory);
3217  if(list->designNickName)      free(list->designNickName);
3218  if(list->blifFile)    free(list->blifFile);
3219  if(list->ctlFile)     free(list->ctlFile);
3220  if(list->invFile)     free(list->invFile);
3221  if(list->leFile)      free(list->leFile);
3222  if(list->fairFile)    free(list->fairFile);
3223  if(list->hintFile)    free(list->hintFile);
3224  if(list->ordFile)     free(list->ordFile);
3225  if(list->ltlFile)     free(list->ltlFile);
3226
3227  resultArr = list->resultForCommandArr1;
3228  if(resultArr) {
3229    for(i=0; i<array_n(resultArr); i++) {
3230      result = array_fetch(RtCommandResults_t *, resultArr, i);
3231      Rt_FreeCommandResult(result);
3232    }
3233    array_free(resultArr);
3234  }
3235  resultArr = list->resultForCommandArr2;
3236  if(resultArr) {
3237    for(i=0; i<array_n(resultArr); i++) {
3238      result = array_fetch(RtCommandResults_t *, resultArr, i);
3239      Rt_FreeCommandResult(result);
3240    }
3241    array_free(resultArr);
3242  }
3243
3244  free(list);
3245}
3246
3247static void
3248Rt_FreeCommandResult(RtCommandResults_t *result)
3249{
3250  array_t *itemArr;
3251  array_t *propArr;
3252  RtCompareItems_t *item;
3253  RtResultPropertys_t *prop;
3254  int i;
3255
3256  if(result == 0)       return;
3257 
3258  if(result->command)   free(result->command);
3259
3260  itemArr = result->compareItemArr;
3261  if(itemArr) {
3262    for(i=0; i<array_n(itemArr); i++) {
3263      item = array_fetch(RtCompareItems_t *, itemArr, i);
3264      Rt_FreeCompareItem(item);
3265    }
3266    array_free(itemArr);
3267  }
3268                         
3269  propArr = result->resultForProperty;
3270  if(propArr) {
3271    for(i=0; i<array_n(propArr); i++) {
3272      prop = array_fetch(RtResultPropertys_t *, propArr, i);
3273      Rt_FreeResultProperty(prop);
3274    }
3275    array_free(propArr);
3276  }
3277}
3278
3279static void
3280Rt_FreeCompareItem(RtCompareItems_t *item)
3281{
3282  if(item == 0) return;
3283
3284  if(item->itemName)    free(item->itemName);
3285  if(item->itemNickName)free(item->itemNickName);
3286  if(item->value)       free(item->value);
3287  free(item);
3288}
3289
3290static void
3291Rt_FreeResultProperty(RtResultPropertys_t *prop)
3292{
3293
3294  if(prop == 0) return;
3295
3296  if(prop->failOrPass)  free(prop->failOrPass);
3297  free(prop);
3298}
3299
3300static void
3301Rt_FreeArgv(int  argc,  char ** argv)
3302{
3303  int i;
3304
3305  for(i = 0; i < argc; i++) {
3306    FREE(argv[i]);
3307  }
3308  FREE(argv);
3309}
Note: See TracBrowser for help on using the repository browser.