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

/**CFile***********************************************************************

  FileName    [rtMain.c]

  PackageName [rt]

  Synopsis    [Regression Test]

  Description  [ This  file contains  the  functions for  regression test.  The
command 'regression_test' will read a  description of the regression test to be
performed from the  argument file, and will then carry  out the test.  Finally,
it will produce a LaTeX file with a set of tables summarizing the results.

  The regression_test command can be  used to compare two different versions of
vis, or two different scripts on the same version of vis, or even two different
scripts  on  two  different   versions  of  vis.   regression_test  spawns  the
version(s) of vis  to be used for the experiments as  child processes.  It does
no  other computation  except setting  up the  experiments, starting  the child
processes, waiting for their termination, and collecting the results.

 ]

  Author [HoonSang Jin]

  Copyright   [Copyright (c) 2001-2002 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "rtInt.h"
#include "rt.h"
#include "ntm.h"
#include "part.h"
#include <errno.h>
#include <math.h>

static char rcsid[] UNUSED = "$Id: rtMain.c,v 1.36 2010/04/10 00:38:42 fabio Exp $";


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int CommandRt( Hrc_Manager_t **hmgr, int argc, char **argv);
static RtConfigs_t * Rt_ReadConfigFile(char *filename);
static char * Rt_SplitLine( char * command, int * argc, char *** argv);
static int Rt_CompareResult(RtConfigs_t *config, RtDesignLists_t *designList, int refOnly);
static int Rt_WriteBatchCommand(RtConfigs_t *config, RtDesignLists_t *designList);
static int Rt_ExecuteVis(RtConfigs_t *config, RtDesignLists_t *designList, int refAndNew, FILE *scriptOut);
static int Rt_WriteResult(RtConfigs_t *config, int size);
static void Rt_FreeRtConfig(RtConfigs_t * config);
static void Rt_FreeCommandResult(RtCommandResults_t *result);
static void Rt_FreeCompareItem(RtCompareItems_t *item);
static void Rt_FreeResultProperty(RtResultPropertys_t *prop);
static void Rt_FreeDesignList(RtDesignLists_t *list);
static void Rt_FreeArgv(int  argc,  char ** argv);
static int Rt_ReadDesignListFile(RtConfigs_t * config);
static int Rt_ReadCommandTemplate(RtConfigs_t * config);
static int RtCheckInputFileAvailability( RtConfigs_t *config, RtDesignLists_t *designList, int withWarning);
static void Rt_RemoveUnderscore(char *name, char *newName);
static int Rt_IsNum(char *tmp);
static int Rt_SetBooleanValue(char *str, char *option);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis [Initialize mc package]

  SideEffects []

******************************************************************************/


/**Function********************************************************************

  Synopsis [Initialize rt package]

  SideEffects []

******************************************************************************/
void
Rt_Init(void)
{
  Cmd_CommandAdd("regression_test", CommandRt, /* doesn't changes_network */ 0);
}

/**Function********************************************************************

  Synopsis [End rt package]

  SideEffects []

******************************************************************************/
void
Rt_End(void)
{
}

/**Function********************************************************************

  Synopsis    [Compare two different execution of vis and make a set of
               tables summarizing results.]

  CommandName [regression_test]

  CommandSynopsis [perform regression test with the information given
                   in arguments file]

  CommandArguments [ \[-s &lt;script_file_name&gt;\] ]

  CommandDescription  [
  Invokes two set of execution of vis to compare the performance and to check
sanity of each execution. Then make a set of tables summarizing results,
such as CPU sec, memoty usage and fail/pass of model_check, etc.. This
command will read a description of the regression test to be performed
from the argument file, which is configuartion file. Besides the configuration
file, one needs to prepare two template files and a design list. We now
describe these in turn. As running example we shall use a regression test
that compares check_invariant with and without guided search.
<p>The configuration file for our example is shown below, delimited by
lines of dashes (which are not part of the file). The order in which the
lines appear in the file is immaterial. A line beginning with '#' is a
comment, and is ignored by regression_test.
<br>----------------------------------------------------------------------
<br>DesignDirectory : /projects/development/hsv/vis/Regression
<br>DesignList : ./DesignListInv
<br>ReferenceVis : /usr/local/vis/i686-o/vis-cu
<br>ReferenceVisNickName : BFS
<br>ReferenceOutputDir : ./result_inv_bfs
<br>RefCommandTemplate : ./TemplateRefInv
<br>bRefRun : FALSE
<br>NewVis : /usr/local/vis/i686-o/vis-cu
<br>NewVisNickName : GS
<br>NewOutputDir : ./result_inv_gs
<br>bNewRun : FALSE
<br>NewCommandTemplate : ./TemplateNewInv
<br>bCompareCounterExample : TRUE
<br>bDefaultInitCommand : FALSE
<br>ResultForPerformance : ./BFSvsGS.tex
<br>CompareItem : cpu : elapse:
<br>CompareItem : mem : Memory in use:
<br>CompareItem : bdd : Peak number of live nodes:
<br>----------------------------------------------------------------------
<br>&nbsp;
<p>Each line defines a parameter of the regression test.
<p>* DesignDirectory gives the path to the directory where the input files
are stored. In this case, we are using the central repository under ~hsv/vis/Regression.
It's typically a good idea to store the results of regression tests in
a separate place from the input files. In our examples, the results are
stored in the current directory.
<p>&nbsp;* DesignList gives the name of the file containing the list of
test cases to run. Each line consists of several white space-separated
fields describing the files making up the test case. The first field is
a path to the files relative to DesignDirectory. The second field is the
test case name. The remaining fields are file names. More on this later,
when we talk about the design list file in detail.
<p>&nbsp;* ReferenceVis and NewVis give paths to the two versions of vis
to be compared in the regression test. They can be the same, as in this
case in which both are the "nightly build."
<p>&nbsp;* ReferenceVisNickName and NewVisNickName are two identifiers
that are used in the LaTeX tables to refer to the two versions that are
compared. Short mnemonics are preferable. Avoid using underscores, because
they currently cause trouble with LaTeX.
<p>&nbsp;* ReferenceOutputDir and NewOutputDir give the names of the directories
in which the results of the runs will be stored. In each of these directories,
vis_reg will create a directory for each test case. The names of these
directories are the test case names taken from the design list. Therefore,
these names must be unique.
<p>&nbsp;* RefCommandTemplate and NewCommandTemplate are the templates
from which vis_reg produces the scripts used to run the test cases. The
mechanism used to derive the scripts from the templates and the design
list is described in detail when we talk about the template files. The
two templates can be the same file.
<p>&nbsp;* bRefRun and bNewRun are flags that tell vis_reg which of the
two sets of experiments should be run (if any). If one set of results has
been already computed, the corresponding flag should be set to FALSE. If
both flags are FALSE, vis_reg simply regenerates the
summary table.
<p>&nbsp;* bCompareCounterExample is a flag that instructs vis_reg to scan
the output files for counterexamples and record their lengths. For each
counterexample, stem and cycle length are found. If this flag is set to
FALSE, counterexamples are not analyzed and the corresponding table is
not produced.
<p>&nbsp;* bDefaultInitCommand is a flag that, if set to TRUE, instructs
vis_reg to generate a default set of commands to initialize each vis run.
This option allows one to save some time in preparing the templates, at
the expense of some flexibility.
<p>&nbsp;* ResultForPerformance is the name of the LaTeX file to which
vis_reg writes the summary of the experiments. Its format is described
in detail later.
<p>&nbsp;* CompareItem specifies one item to be monitored in the experiments.
Multiple CompareItem lines may appear in the configuration file. Each one
consists of two items: an identifier, and a pattern. The identifier is
used in the table to denote the item, whereas the pattern is used to extract
from the output files the information to be put in the tables.
<p>&nbsp;In our example, we declare
<p>&nbsp;CompareItem : mem : Memory in use:
<p>We instruct regression_test to search for a line beginning with "Memory
in use:" in each section of the output file. The token immediately following
the occurrence of the pattern is the data item to be put in the table under
"mem." so that the resulting LaTeX table contains data on the memmory usage.
<p>&nbsp;Since the output file is divided into sections delimited by strings
"CommandBegin" and "CommandEnd." (See below.), each section is searched
for the patterns specified by the CompareItem declarations. If the pattern
is matched, the item appears in the table for that section.
<p>&nbsp;To run the regression_test we need configuration file, template
file and design list. In case of template file, we need a two template
files, since we want to compare two different run of vis. The syntax of
the two templates is identical. We describe the template for "new," but
all we say applies to "ref" as well. The "new" template for our example
is shown below.
<br>----------------------------------------------------------------------
<p>echo CommandBegin init
<br>read_model
<br>flt
<br>order_vars
<br>part
<br>time
<br>print_bdd_stats
<br>echo CommandEnd init
<br>echo CommandBegin ci
<br>set hd_frontier_approx_threshold 3500
<br>ci -t 3600 -g $HintFile $InvFile
<br>time
<br>print_bdd_stats
<br>echo CommandEnd ci
<br>echo CommandBegin ci_cex
<br>ci -d 1 -i -t 3600 -g $HintFile $InvFile
<br>time
<br>print_bdd_stats
<br>echo CommandEnd ci_cex
<br>----------------------------------------------------------------------
<p>Before proceeding to its discussion, it is instructive to examine the
script that regression_test produces from it for one test case. regression_test
relies on vis's shell variables and aliases to customize the script. The
script consists of a preamble in which variables and aliases are defined,
followed by one or more sections, each corresponding to a major step in
the experiment. Statistics will be collected for each step separately.
Our example has three sections, whose names are "init," "ci," and "ci_cex."
The names of the sections are arbitrary, except that the automatically
generated initialization section is always called "init."
<br>----------------------------------------------------------------------
<p>set vis_stdout ./result_inv_gs/am2901/am2901.out
<br>set vis_stderr ./result_inv_gs/am2901/am2901.err
<br>set BlifFile /projects/development/hsv/vis/Regression/Am2901/am2901.mv
<br>set OrdFile /projects/development/hsv/vis/Regression/Am2901/am2901.ord
<br>set InvFile /projects/development/hsv/vis/Regression/Am2901/am2901.inv
<br>set HintFile /projects/development/hsv/vis/Regression/Am2901/am2901.hint
<br>alias read_model "rlmv $BlifFile"
<br>alias set_fairness " "
<br>alias order_vars "so -s input_and_latch $OrdFile"
<br>echo CommandBegin init
<br>read_model
<br>flt
<br>order_vars
<br>part
<br>time
<br>print_bdd_stats
<br>echo CommandEnd init
<br>echo CommandBegin ci
<br>set hd_frontier_approx_threshold 3500
<br>ci -t 3600 -g $HintFile $InvFile
<br>time
<br>print_bdd_stats
<br>echo CommandEnd ci
<br>echo CommandBegin ci_cex
<br>ci -d 1 -i -t 3600 -g $HintFile $InvFile
<br>time
<br>print_bdd_stats
<br>echo CommandEnd ci_cex
<br>quit
<br>----------------------------------------------------------------------
<p>The variables and the aliases are defined by vis_reg by examining the
fields of the test case description in the design file. regression_test
uses file extensions to identify file types. (E.g., .ord indicates an order
file in "input_and_latch" format.) A full list of extensions is given below.
<p>regression_test defines variables for all the file types actually available
for the experiment, and only for those. It also defines three aliases that
provide some flexibility in mixing different experiments in the same batch.
<p>For instance, "read_model" is defined as either
<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; read_blif_mv $BlifFile
<p>or
<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; read_blif $BlifFile
<p>depending on whether the design list specifies a .mv file or a .blif
file as model file.
<p>The definition of "order_vars" takes into account whether an order file
is available or not. Finally, the definition of "set_fairness" depends
on whether a .fair file is available. This allows one to mix model checking
experiments for which no fairness condition is specified to experiments
that do require fairness conditions.
<p>When bDefaultInitCommand is FALSE, the script is simply the preamble,
followed by the unchanged template, follows by the "quit" command, which
is always automatically added.
<p>When bDefaultInitCommand is TRUE, regression_test also adds an automatically
generated "init" section between the preamble and the template. This default
section is equivalent to
<p>echo CommandBegin init
<br>read_model
<br>flt
<br>order_vars
<br>part
<br>time
<br>print_bdd_stats
<br>echo CommandEnd init
<p>Notice that one has no control over dynamic reordering during the initialization
phase if bDefaultInitCommand is TRUE.
<p>The template should refer to the defined aliases and variables to tailor
itself to each test case. Notice, however, that one is not forced to use
"order_vars." If one wants to always use vis's static ordering algorithm,
(s)he can simply use "so" instead of "order_vars." Likewise, one can decide
to always ignore fairness constraints by not including "set_fairness."
<p>On the other hand, it is usually a bad idea to explicitly include commands
like
<p>read_blif_mv
<br>read_blif
<br>so -s input_and_latch
<br>read_fairness
<p>in the templates, because they limit the range of test cases to which
they can be applied.
<p>As we said, the templates, and hence the scripts, are divided in sections.
Each section begins and ends with an "echo" command. These commands write
delimiters to the output file, which are used by vis_reg to define the
scope of the pattern searches. It is important that the tag specified in
corresponding pairs of CommandBegin and CommandEnd be the same.
<p>The calls to "print_bdd_stats" are typically used to add to the output
files the information requested by the CompareItem declarations. It is
a good idea to specify timeouts for potentially expensive steps.
<p>The design list file has one line for each test case. A master design
list is in ~hsv/vis/Regression/DesignList. Specific design lists can be
obtained by commenting out or deleting lines from this master list. One
can also create an entirely new list according to the following rules.
<p>Lines starting with '#' are interpreted as comments and are skipped,
as in all files read by vis_reg.
<p>A test case is a named collection of related files that can be used
to run one or more experiments. As mentioned before, each line consists
of white space-separated fields. The first is a (relative) path, while
the second is the collection name. The remaining fields specify the files
in the collection.
<p>The smallest collection will specify one .mv or one .blif file. This
file is called the "model file," and should always appear in the third
field of the line. If the model file is the only file specified, one can
run reachability analysis, but not much more. Vis_reg understands the file
extensions shown in the following table. For each extension, the variable
bound to the file name and a short explanation are given.
<p>.mv $BlifFile model file to be read with rlmv
<br>.blif $BlifFile model file to be read with rl
<br>.ord $OrdFIle order file to be read with so -s input_and_latch
<br>.inv $InvFile invariant file to be read with ci
<br>.ctl $CtlFile property file to be read with mc
<br>.fair $FairFile fairness file to be read with rf
<br>.hint $HintFile hint file to be read with the -g option of mc, ci,
and rch
<p>Only one file of each type can appear in the collection defining one
test case. If multiple property files, or different order files are available
for one model file, one has to create two test cases for that model. Different
models, on the other hand, can share property files, order files, and so
on. The master design list provides examples for both these situations.
<p>It is not possible to specify both a .mv file and a .blif file for one
test case. There must be exactly one model file per test case.
<p>As was mentioned before, it is important that the name of a test case
be unique in the entire batch used for a regression test. On the other
hand, several test cases may share the same directory, and often do when
they have some files in common.
<p>The result summary created by regression_test is a LaTeX file consisting
of several tables. There is one table with performance stats for each section
of the output file. In addition, there is an optional counterexample comparison
table that summarizes PASS/FAIL information for the properties and the
length of counterexamples. For each failing property, the length of the
stem and the length of the cycle (if applicable) are reported.
<p>Each performance table consists of one column for the test case name,
followed by as many groups of three columns as there are CompareItem declarations
applicable to the section that the table summarizes.
<p>Each group of three columns gives the data for the reference run, the
data for the new run, and the improvement. Vis_reg regards smaller as better.
Hence, the improvement is positive if the CPU time, memory occupation,
and so on, have decreased from the reference run to the new run. The improvement
is computed as
<p>(value(ref) - value(new)) / value(ref) * 100.
<p>Notice that this formula tends to make "new" look bad. for instance,
if new is twice as fast as ref, the improvement is 50%. If ref is twice
as fast, however, the "improvement" is -100%.
<p>The results of each test case are stored in a separate directory, whose
name is obtained by concatenating ReferenceOutputDir (or NewOutputDir)
with the test case name. Each directory stores three files, whose names
are given by the test case name concatenated with .src, .out, and .err.
<p>* test_case_name.src stores the script used to run vis.
<br>* test_case_name.out stores what vis writes to vis_stdout.
<br>* test_case_name.err stores what vis writes to vis_stderr.
<p>One has to be careful, because vis_reg will overwrite these results
directories without warning if run twice with the same ReferenceOutputDir
or NewOutputDir and bRefRun or bNewRun set to TRUE.
<p>With '-s' option, you can create c-shell script file to be able to run
experiments in shell. We add this option to solve the problem that are
happened when your template file contains child-process by system call.
]

  Comment [
  * One cannot compare the number of iterations to convergence with BFS
  to those of HD or GS, because the first is reported as "FSM depth,"
  while the other two are reported as "computation depth."  <p>

  * Tables are split so that the number of rows is not too large.
  However, tables may be too wide.  All "CompareItem" items found in
  one section are put in the same table.  <p>

  * Currently, under Linux, the datasize limit is not enforced (not
  systematically enforced?) for the child processes spawned by
  vis_reg.  One has to monitor experiments that may produce very large
  processes, because there is a concrete risk of thrashing the machine
  on which the regression test is run.  <p>

  * One cannot create experiments that read two different property
  files, or two different invariant files, or that perform equivalence
  checking.  (That would require two model files.)  <p>

]

  SideEffects []

******************************************************************************/
static int
CommandRt(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  char *configurationFile;
  char *scriptFile;
  RtConfigs_t *config;
  RtDesignLists_t *designList;
  array_t *designArr;
  int i;
  FILE *scriptOut;
  int c;
  error_init();

  if(argc < 2) {
     fprintf(vis_stdout, "Error : ConfigurationFile is missed\n");
     return(1);
  }

  util_getopt_reset();
  scriptFile = 0;
  scriptOut = 0;
  while ((c = util_getopt(argc, argv, "s:h")) != EOF) {
    switch(c) {
    case 's':
      scriptFile = util_strsav(util_optarg);
      break;
    case 'h':
      (void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
      (void) fprintf(vis_stderr, "    -h \tprint help information\n");
      (void) fprintf(vis_stderr, "    -s <scriptfile>\n");
      (void) fprintf(vis_stderr, "       \tgenerate shell script file for regression_test\n");
      return 0;
    default:
      (void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
      (void) fprintf(vis_stderr, "    -h \tprint help information\n");
      (void) fprintf(vis_stderr, "    -s <scriptfile>\n");
      (void) fprintf(vis_stderr, "       \tgenerate shell script file for regression_test\n");
      return 0;
    }
  }
  if(scriptFile) {
    if(!(scriptOut = fopen(scriptFile, "w"))) {
      fprintf(vis_stdout, "Error : Can't open script file '%s'\n", scriptFile);
      return(1);
    }
  }

  configurationFile = argv[util_optind];
  config = Rt_ReadConfigFile(configurationFile);
  if(config == 0)                       return(1);

  config->scriptFile = scriptFile;
  if(Rt_ReadDesignListFile(config))     {
    Rt_FreeRtConfig(config);
    return(1);
  }
  if(Rt_ReadCommandTemplate(config))    {
    Rt_FreeRtConfig(config);
    return(1);
  }


  designArr = config->designListArr;
  for(i=0; i<array_n(designArr); i++) {
    designList = array_fetch(RtDesignLists_t *, designArr, i);

    /** 
     * One have to use reserved words in their template file, such as
     * $OrdFile, $BlifFile, etc.. 
     * Somehow your template file contains the reserved words that are
     * not provied in desigl list, then skip the design.
     **/
    if(RtCheckInputFileAvailability(config, designList, 1)) {
       fprintf(vis_stdout, "Skip the design '%s' ..(%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
       continue;
    }
    /** 
     * Create result directory structure and script file that are used
     * to run individual experiments. Each directory, whose
     * name is obtained by concatenating ReferenceOutputDir(or NewOutputDir)
     * with the test case name, contains test_case_name.src after
     * executing this function.
     **/
    if(Rt_WriteBatchCommand(config, designList)) {
       fprintf(vis_stdout, "ERROR : can't write script for design '%s'\n", designList->designNickName);
       continue;
    }
    /** 
     * Run vis using the executable that is obtained ReferenceVis of
     * configuration file
     **/
    if(Rt_ExecuteVis(config, designList, 1, scriptOut)) {
       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->referenceVisNickName, designList->designNickName);
    }
    /** 
     * Run vis using the executable that is obtained NewVis of
     * configuration file
     **/
    if(Rt_ExecuteVis(config, designList, 2, scriptOut)) {
       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->newVisNickName, designList->designNickName);
    }
    /** 
     * After running two set of experimental results, read the log file
     * of each run and compare the results.
     **/
    if(Rt_CompareResult(config, designList, config->bRefOnly)) {
       fprintf(vis_stdout, "ERROR : can't compare result for design '%s'\n", designList->designNickName);
    }
    fprintf(vis_stdout, "%s complete.. (%d/%d)\n", designList->designNickName, i+1, array_n(designArr));

    /** 
     * Write a LaTeX file summarizing the results, after running each
     * design, so that one can see the results before finishing the
     * whole experiments.
     **/
    if(config->scriptFile == 0) {
      if(config->bRefRun || config->bNewRun)
        Rt_WriteResult(config, i+1);
    }
  }

  /** 
   * Write a LateX file summarizing the results. 
   **/
  if(config->scriptFile == 0)
    if(Rt_WriteResult(config, array_n(designArr)))      return(1);
  alarm(0);

  Rt_FreeRtConfig(config);
  if(scriptOut) fclose(scriptOut);
  return 0;
}

/**Function********************************************************************

  Synopsis    [Check whether the used file in template file is available
               or not. ]

  Description [ 
      One have to use reserved words in their template file, such as
     $OrdFile, $BlifFile,  $InvFile, $CtlFile, $FairFile, $HintFile and
     $LeFile. Somehow your template file contains the reserved words that are
     not provied in design list, then skip the design.
     ]

  Comment []

  SideEffects []

******************************************************************************/
static int
RtCheckInputFileAvailability(
  RtConfigs_t *config, 
  RtDesignLists_t *designList,
  int withWarning)
{
  st_table *keyTable;
  st_generator *gen;
  int errorFlag;
  char *keyWord;

  keyTable = config->keyWordTable;
  if(keyTable == 0)     return(0);
  errorFlag = 0;
  st_foreach_item(keyTable, gen, &keyWord, NIL(char *)) {
    if(!strcasecmp(keyWord, "$CtlFile") && !designList->ctlFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$CtlFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$OrdFile") && !designList->ordFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$OrdFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$InvFile")&& !designList->invFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$InvFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$FairFile")&& !designList->fairFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$FairFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$LeFile")&& !designList->leFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$LeFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$LtlFile")&& !designList->ltlFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$LtlFile', but not in design list\n");
      errorFlag = 1;
    }
    else if(!strcasecmp(keyWord, "$HintFile")&& !designList->hintFile) {
      if(withWarning)
      fprintf(vis_stdout, "WARNING : Template contains the '$HintFile', but not in design list\n");
      errorFlag = 1;
    }
  }
  if(errorFlag == 1)    return(1);
  else                  return(0);
}

/**Function********************************************************************

  Synopsis    [ Write LaTeX file summarizing results.]

  Description [ The  result summary created by regression_test  is a LaTeX file
consisting of  several tables.  There is  one table with  performance stats for
each  section  of  the  output   file.   In  addition,  there  is  an  optional
counterexample comparison  table that summarizes PASS/FAIL  information for the
properties and the  length of counterexamples.  For each  failing property, the
length of the stem and the length of the cycle (if applicable) are reported.

Each performance table consists of one  column for the test case name, followed
by  as many  groups  of three  columns  as there  are CompareItem  declarations
applicable to the section that the table summarizes.  ]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_WriteResult(RtConfigs_t *config, int size)
{
  FILE *fout;
  array_t *cResultArr, *cResultArr2;
  array_t *cResultArrSample, *cItemArrSample, *cItemArrSampleMax;
  array_t *cItemArr, *cItemArr2, *designArr;
  array_t *pArr, *pArr2, *pArrSample;
  RtCommandResults_t *cResult, *cResult2, *cResultSample;
  RtCompareItems_t *cItem, *cItem2, *cItemSample;
  RtDesignLists_t *designList;
  RtResultPropertys_t *rProp, *rProp2;
  int i, j, k, first_flag;
  int property_flag;
  int lineNo, estLineNo, errorFlag;
  char newName[1024], endStr[10];
  char newNName[1024], refNName[1024];
  char newTimeout[1024], refTimeout[1024];
  double value1, value2;
  int lastFailedIndex;
  array_t *cResultArrMax;
  array_t *cItemArrMax;
  double *resultArr;
  double totalNum;
  double gap;

  pArrSample = 0;
  if(!(fout = fopen(config->resultForPerformance, "w"))) {
    fprintf(vis_stdout, "Error : Can't open result file '%s'\n", config->resultForPerformance);
    return(1);
  }
  designArr = config->designListArr;

  /** Check whether both runs contain the same set of item, since we
   * compare two experiments.
   **/
  cItemArrSample = 0;
  cResultArrSample = NIL(array_t);
  for(k=0; k<array_n(designArr) && k<size; k++) {
    designList = array_fetch(RtDesignLists_t *, designArr, k);
    cResultArrSample = designList->resultForCommandArr1;
    errorFlag = 0;
    if(cResultArrSample)        {
      for(i=0; i<array_n(cResultArrSample); i++) {
        cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
        cItemArrSample = cResult->compareItemArr;
        if(cItemArrSample == NIL(array_t)) {
          errorFlag = 1;
          break;
        }
      }
    }
    if(errorFlag == 0)  break;
  }
  if(cResultArrSample == NIL(array_t)) {
     fprintf(fout, "ERROR : Can't find any output for your design list\n");
     fclose(fout);
     return(1);
  }

  /** Write performance table header **/
  fprintf(fout, "\\documentclass[plain]{article}\n");
  fprintf(fout, "\\usepackage{lscape}\n");
  fprintf(fout, "\\begin{document}\n");
  fprintf(fout, "\\setlength{\\oddsidemargin}{-0.5in}\n");
  /**
  fprintf(fout, "\\landscape\n");
  **/

  for(i=0; i<array_n(cResultArrSample); i++) {

    fprintf(fout, "\\begin{table}\n");
    cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
    cItemArrSample = cResult->compareItemArr;
 
    cItemArrSampleMax = cItemArrSample;
    for(k=0; k<array_n(designArr) && k<size; k++) {
      designList = array_fetch(RtDesignLists_t *, designArr, k);
      cResultArr = designList->resultForCommandArr1;
      if(cResultArr)    {
          if(array_n(cResultArr) > i) 
              cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
          else
              cResult = 0;
          if(!cResult)  continue;
          cItemArrSample = cResult->compareItemArr;
          if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrSampleMax)) {
            cItemArrSampleMax = cItemArrSample;
          }
      }
    }
    cItemArrSample = cItemArrSampleMax;
    if(cItemArrSample == 0) {
       fprintf(fout, "ERROR : Can't find any output for your design list\n");
       fclose(fout);
       return(1);
    }
      
    cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
    Rt_RemoveUnderscore(cResult->command, newName);
    Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
    Rt_RemoveUnderscore(config->newVisNickName, newNName);
    fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
        newName, refNName, newNName);
    fprintf(fout, "\\begin{center}\n");
    fprintf(fout, "\\begin{tabular}{|c||");
    for(j=0; j<array_n(cItemArrSample); j++) {
      fprintf(fout, "c|c|c|");
    }
    fprintf(fout, "} \\hline \n");
    fprintf(fout, " &");
    Rt_RemoveUnderscore(cResult->command, newName);
    fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
    fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
  
    fprintf(fout, " &");
    for(j=0; j<array_n(cItemArrSample); j++) {
      cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
      if(j+1 == array_n(cItemArrSample)) 
        fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
      else 
        fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
    }
    fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
  
    fprintf(fout, "Design &");
    for(j=0; j<array_n(cItemArrSample); j++) {
      if(j+1 == array_n(cItemArrSample)) 
        fprintf(fout, "ref & new & (\\%%)");
      else 
        fprintf(fout, "ref & new & (\\%%) &");
    }
    fprintf(fout, "\\\\ \\hline \\hline\n");
  
    lineNo = 0;
    for(k=0; k<array_n(designArr) && k<size ; k++) {
      lineNo++;
  
      /** 
       * If the result table have more than 31 line then split the
       * table.
       **/
      if(lineNo == 31) {
        fprintf(fout, "\\end{tabular}\n");
        fprintf(fout, "\\end{center}\n");
        fprintf(fout, "\\end{table}\n");
        fprintf(fout, "\\clearpage\n");
  
        fprintf(fout, "\\begin{table}\n");
        cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
        cItemArrSample = cResult->compareItemArr;
        Rt_RemoveUnderscore(cResult->command, newName);
        Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
        Rt_RemoveUnderscore(config->newVisNickName, newNName);
        fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
            newName, refNName, newNName);
        fprintf(fout, "\\begin{center}\n");
        fprintf(fout, "\\begin{tabular}{|c||");
        for(j=0; j<array_n(cItemArrSample); j++) {
          fprintf(fout, "c|c|c|");
        }
        fprintf(fout, "} \\hline \n");
        fprintf(fout, " &");
        Rt_RemoveUnderscore(cResult->command, newName);
        fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
        fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
      
        fprintf(fout, " &");
        for(j=0; j<array_n(cItemArrSample); j++) {
          cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
          if(j+1 == array_n(cItemArrSample)) 
            fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
          else 
            fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
        }
        fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
      
        fprintf(fout, "Design &");
        for(j=0; j<array_n(cItemArrSample); j++) {
          if(j+1 == array_n(cItemArrSample)) 
            fprintf(fout, "ref & new & (\\%%)");
          else 
            fprintf(fout, "ref & new & (\\%%) &");
        }
        fprintf(fout, "\\\\ \\hline \\hline\n");
      
        lineNo = 1;
      }
      designList = array_fetch(RtDesignLists_t *, designArr, k);
      strcpy(newTimeout, "-");
      strcpy(refTimeout, "-");
      if(RtCheckInputFileAvailability(config, designList, 0)) {
        continue;
      }
      cResultArr = designList->resultForCommandArr1;
      cResultArr2 = designList->resultForCommandArr2;
      Rt_RemoveUnderscore(designList->designNickName, newName);
      fprintf(fout, "%s\t&", newName);
      if(cResultArr && array_n(cResultArr) > i)
        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
      else 
        cResult = 0;
  
      if(cResultArr2 && array_n(cResultArr2) > i)
        cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
      else 
        cResult2 = 0;
  
      if(cResult && cResult->bTimeOut)   {
        strcpy(refTimeout, "TimeOut");
      }
      if(cResult2 && cResult2->bTimeOut) {
        strcpy(newTimeout, "TimeOut");
      }
  
      if(cResult)
        cItemArr = cResult->compareItemArr;
      else
        cItemArr = 0;
      if(cResult2)
        cItemArr2 = cResult2->compareItemArr;
      else
        cItemArr2 = 0;
  
      if(cItemArr == 0 && cItemArr2 == 0)       {
        fprintf(vis_stdout, "Warning : no result for design '%s'\n", designList->designNickName);
        for(j=0; j<array_n(cItemArrSample); j++) {
          if(j+1 == array_n(cItemArrSample)) 
            fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
          else 
            fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
        }
        fprintf(fout, "\\\\ \\hline\n");
        continue;
      }
      else if(cItemArr && cItemArr2) {
        if(array_n(cItemArr) != array_n(cItemArr2)) {
          fprintf(vis_stdout, "Warning : Can't make table for the compare item,\n");
          fprintf(vis_stdout, "           since they are different for '%s'\n", designList->designNickName);
          fprintf(vis_stdout, "           Please check your template file again.\n");
          for(j=0; j<array_n(cItemArrSample); j++) {
            if(j+1 == array_n(cItemArrSample)) 
              fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
            else 
              fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
          }
          fprintf(fout, "\\\\ \\hline\n");
          continue;
        }
      }
      if(cItemArr)      cItemArrSample = cItemArr;
      else              cItemArrSample = cItemArr2;
      for(j=0; j<array_n(cItemArrSample); j++) {
        if(cItemArr) 
          cItem = array_fetch(RtCompareItems_t *, cItemArr, j);
        else
          cItem = 0;
        if(cItemArr2) 
          cItem2 = array_fetch(RtCompareItems_t *, cItemArr2, j);
        else
          cItem2 = 0;
    
        if(cItem)       sscanf(cItem->value, "%lf", &value1);
        if(cItem2)      sscanf(cItem2->value, "%lf", &value2);
  
        endStr[0] = '\0';
        if(j+1 != array_n(cItemArrSample))      {
          endStr[0] = '&';
          endStr[1] = '\0';
        }
        if(cItem2 && cItem) {
          fprintf(fout, "%s\t& %s\t& %.2f\t%s", cItem->value, cItem2->value, (value1-value2)/value1*100, endStr);
        }
        else if(cItem)  {
          fprintf(fout, "%s\t& %s\t& -\t%s", cItem->value, newTimeout, endStr);
        }
        else if(cItem2)  {
          fprintf(fout, "%s\t& %s\t& -\t%s", refTimeout, cItem2->value, endStr);
        }
      }
      fprintf(fout, "\\\\ \\hline\n");
    }
    fprintf(fout, "\\end{tabular}\n");
    fprintf(fout, "\\end{center}\n");
    fprintf(fout, "\\end{table}\n");
    fprintf(fout, "\\clearpage\n");
  }

  property_flag = 0;
  for(k=0; k<array_n(designArr) && k<size; k++) {
    designList = array_fetch(RtDesignLists_t *, designArr, k);
    cResultArr = designList->resultForCommandArr1;
    if(cResultArr)       {
      for(i=0; i<array_n(cResultArr); i++) {
        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
        pArr = cResult->resultForProperty;
        if(pArr && array_n(pArr) > 0)   {
          property_flag = 1;
          break;
        }
      }
    }
    cResultArr = designList->resultForCommandArr2;
    if(cResultArr)       {
      for(i=0; i<array_n(cResultArr); i++) {
        cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
        pArr = cResult->resultForProperty;
        if(pArr && array_n(pArr) > 0)   {
          property_flag = 1;
          break;
        }
      }
    }
    if(property_flag)   break;
  }

  /** 
   * Write the property comparison table in case of model checking
   * verification
   **/
  if(property_flag == 1) {
    fprintf(fout, "\\begin{table}\n");
    Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
    Rt_RemoveUnderscore(config->newVisNickName, newNName);
    fprintf(fout, "\\caption{Property Comparison Table for %s(ref) \
    and %s(new)}\n", refNName, newNName);
    fprintf(fout, "\\begin{center}\n");
    fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
    fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
    fprintf(fout, "Design & command & index & F or P & cex len & line len  & F or P & cex len  & line len& \\\\ \\hline\n");
  
    lineNo = 0;
    for(k=0; k<array_n(designArr) && k<size; k++) {
      designList = array_fetch(RtDesignLists_t *, designArr, k);
      if(RtCheckInputFileAvailability(config, designList, 0)) {
        continue;
      }
      cResultArr = designList->resultForCommandArr1;
      cResultArr2 = designList->resultForCommandArr2;
      if(cResultArr == 0 && cResultArr2 == 0) {
        fprintf(vis_stdout, "ERROR : '%s' didn't run properly\n", designList->designNickName);
        continue;
      }
      else if(cResultArr == 0 ) {
        cResultArrSample = cResultArr2;
      }
      else if(cResultArr2 == 0 ) {
        cResultArrSample = cResultArr;
      }
      else {
        cResultArrSample = cResultArr;
      }
  
      strcpy(refTimeout, "-");
      strcpy(newTimeout, "-");
  
      first_flag = 0;
      for(i=0; i<array_n(cResultArrSample); i++) {
        if(cResultArr && array_n(cResultArr) > i)
          cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
        else
          cResult = 0;
        if(cResultArr2 && array_n(cResultArr2) > i)
          cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
        else 
          cResult2 = 0;
  
        if(cResult == 0 && cResult2 == 0)       continue;
  
        if(cResult && cResult->bTimeOut)         {
          strcpy(refTimeout, "TimeOut");
        }
        if(cResult2 && cResult2->bTimeOut) {
          strcpy(newTimeout, "TimeOut");
        }
  
        else if((cResult && !cResult->resultForProperty) &&
                (cResult2 && !cResult2->resultForProperty))     continue;
  
        if(cResult)
          pArr = cResult->resultForProperty;
        else
          pArr = 0;
        if(cResult2)
          pArr2 = cResult2->resultForProperty;
        else
          pArr2 = 0;
  
        if((!pArr || array_n(pArr) < 1) && (!pArr2 || array_n(pArr2) < 1)) {
          continue;
        }
        else if(pArr && array_n(pArr) >= 1) {
          pArrSample = pArr;
        }
        else if(pArr2 && array_n(pArr2) >= 1) {
          pArrSample = pArr2;
        }
  
        estLineNo = 0;
        lastFailedIndex = -1;
        for(j=0; j<array_n(pArrSample); j++) {
          if(pArr && array_n(pArr) > j) 
            rProp = array_fetch(RtResultPropertys_t *, pArr, j);
          else
            rProp = 0;
          if(pArr2 && array_n(pArr2) > j) 
            rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
          else
            rProp2 = 0;
  
          if((rProp && !strncasecmp(rProp->failOrPass, "pass", 4)) && 
              (rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4))) {
          }
          else {
            estLineNo++;
            lastFailedIndex = j;
          }
  
        }
  
      /** 
       * If the result table have more than 40 line then split the
       * table.
       **/
        if(lineNo + estLineNo > 40) {
          fprintf(fout, "\\hline\n");
          fprintf(fout, "\\end{tabular}\n");
          fprintf(fout, "\\end{center}\n");
          fprintf(fout, "\\end{table}\n");
          fprintf(fout, "\\clearpage\n");
          fprintf(fout, "\\begin{table}\n");
          Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
          Rt_RemoveUnderscore(config->newVisNickName, newNName);
          fprintf(fout, "\\caption{Property Comparison Table for \
          %s(ref) and %s(new)}\n", refNName, newNName);
          fprintf(fout, "\\begin{center}\n");
          fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
          fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
          fprintf(fout, "Design & command & index & F or P & cex len & line len  & F or P & cex len  & line len& \\\\ \\hline\n");
          lineNo = 0;
        }
          
        Rt_RemoveUnderscore(designList->designNickName, newName);
        if(first_flag==0) {
          fprintf(fout, "%s &", newName);
          first_flag = 1;
        }
        else
          fprintf(fout, " &");
  
        for(j=0; j<array_n(pArrSample); j++) {
  
          lineNo++;
          if(pArr && array_n(pArr) > j) 
            rProp = array_fetch(RtResultPropertys_t *, pArr, j);
          else
            rProp = 0;
          if(pArr2 && array_n(pArr2) > j) 
            rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
          else
            rProp2 = 0;
            
          if(rProp && !strncasecmp(rProp->failOrPass, "pass", 4) && 
             rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4)) {
            if(j==0 && estLineNo == 0) {
              if(cResult)
                 Rt_RemoveUnderscore(cResult->command, newName);
              else 
                 Rt_RemoveUnderscore(cResult2->command, newName);
              fprintf(fout, " %s & [%d] & passed & passed & - & passed & passed & - & \\\\ ", newName, rProp->index+1);
              if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample)) 
                fprintf(fout, " \\hline\n");
              else if(j+1 == array_n(pArrSample))
                fprintf(fout, " \\cline{2-10}\n");
              else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))   
                fprintf(fout, " \\hline\n");
              else if(lastFailedIndex <= j)   
                fprintf(fout, " \\cline{2-10}\n");
              else 
                fprintf(fout, " \\cline{4-10}\n");
            }
            else {
              lineNo--;
            }
            continue;
          }
  
    
          if(first_flag==1) {
            if(cResult) {
              Rt_RemoveUnderscore(cResult->command, newName);
              fprintf(fout, " %s & ", newName);
            }
            else if(cResult2) {
              Rt_RemoveUnderscore(cResult2->command, newName);
              fprintf(fout, " %s & ", newName);
            }
            first_flag = 2;
          }
          else {
            fprintf(fout, " & & ");
          }
  
          if(rProp) {
            if(rProp->lengthOfInv != -1) 
              fprintf(fout, " [%d] & %s & (%d,-) & %d &", rProp->index+1, rProp->failOrPass, rProp->lengthOfInv, rProp->lengthOfCounterExample);
            else if(rProp->lengthOfStem == -1 && rProp->lengthOfCycle == -1)
              fprintf(fout, " [%d] & %s & - & - &", rProp->index+1, rProp->failOrPass);
            else 
              fprintf(fout, " [%d] & %s & (%d,%d) & %d & ", rProp->index+1, rProp->failOrPass, rProp->lengthOfStem, rProp->lengthOfCycle,rProp->lengthOfCounterExample );
          }
          else {
            if(rProp2)
              fprintf(fout, " [%d] & %s & %s & - & ", rProp2->index+1, refTimeout, refTimeout);
            else 
              fprintf(fout, " & %s & %s & - & ", refTimeout, refTimeout);
          }
  
          if(rProp2) {
            if(rProp2->lengthOfInv != -1) 
              fprintf(fout, " %s & (%d,-) & %d ", rProp2->failOrPass,
              rProp2->lengthOfInv,rProp2->lengthOfCounterExample );
            else if(rProp2->lengthOfStem == -1 && rProp2->lengthOfCycle == -1)
              fprintf(fout, " %s & - & - ", rProp2->failOrPass);
            else 
              fprintf(fout, " %s & (%d,%d) & %d ", rProp2->failOrPass,
              rProp2->lengthOfStem, rProp2->lengthOfCycle, rProp2->lengthOfCounterExample);
          }
          else {
            fprintf(fout, " %s & %s & - ", newTimeout, newTimeout);
          }
  
          endStr[0] = '\0';
          if(rProp2 && rProp) {
             if(rProp->failOrPass == 0 && rProp2->failOrPass)
               strcpy(endStr, "Check");
             else if(rProp->failOrPass && rProp2->failOrPass == 0)
               strcpy(endStr, "Check");
             if(rProp->failOrPass == 0 && rProp2->failOrPass == 0)
               strcpy(endStr, "Check");
             if(strcmp(rProp->failOrPass, rProp2->failOrPass))
               strcpy(endStr, "Check");
             else if(rProp->lengthOfStem != rProp2->lengthOfStem) 
               strcpy(endStr, "Check");
             else if(rProp->lengthOfCycle != rProp2->lengthOfCycle)
               strcpy(endStr, "Check");
             else if(rProp->lengthOfInv != rProp2->lengthOfInv)
               strcpy(endStr, "Check");
          }
          else {
            strcpy(endStr, "Check");
          }
          if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample)) 
            fprintf(fout, " & %s \\\\ \\hline\n",endStr);
          else if(j+1 == array_n(pArrSample))
            fprintf(fout, " & %s \\\\ \\cline{2-10}\n",endStr);
          else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))   
            fprintf(fout, " & %s \\\\ \\hline\n", endStr);
          else if(lastFailedIndex <= j)   
            fprintf(fout, " & %s \\\\ \\cline{2-10}\n", endStr);
          else 
            fprintf(fout, " & %s \\\\ \\cline{4-10}\n",endStr);
        }
      }
    }
  
    fprintf(fout, "\\end{tabular}\n");
    fprintf(fout, "\\end{center}\n");
    fprintf(fout, "\\end{table}\n");
    fprintf(fout, "\\clearpage\n");
  }


  /** 
   * Write the summary of comparison
   **/
  fprintf(fout, "\\begin{table}\n");
  Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
  Rt_RemoveUnderscore(config->newVisNickName, newNName);
  fprintf(fout, "\\caption{Summary for %s(ref) and %s(new)}\n", refNName, newNName);
  fprintf(fout, "\\begin{center}\n");
  fprintf(fout, "\\begin{tabular}{|c|c||c|c|c|c||r|r|} \\hline\n");
  fprintf(fout, " command & item & \\multicolumn{4}{c||}{ %s } & \\multicolumn{2}{c|}{ geo-mean } \\\\ \\cline{3-8}\n", newNName);
  fprintf(fout, " & & win & lose & tie & NA & ref & new \\\\ \\hline \\hline\n");

  cResultArrMax = 0;
  for(k=0; k<array_n(designArr) && k<size; k++) {
    designList = array_fetch(RtDesignLists_t *, designArr, k);
    cResultArr = designList->resultForCommandArr1;
    if(cResultArrMax == 0)      cResultArrMax = cResultArr;
    else if(cResultArr && array_n(cResultArr) > array_n(cResultArrMax)) {
       cResultArrMax = cResultArr;
    }
  }

  resultArr = ALLOC(double, 6); 
  for(i=0; i<array_n(cResultArrMax); i++) {
    cResultSample = array_fetch(RtCommandResults_t *, cResultArrMax, i);
    fprintf(fout, " %s & ", cResultSample->command);
    first_flag = 1;

    cItemArrMax = 0;
    for(k=0; k<array_n(designArr) && k<size; k++) {
      designList = array_fetch(RtDesignLists_t *, designArr, k);
      cResultArr = designList->resultForCommandArr1;
      if(cResultArr)    {
          if(array_n(cResultArr) > i) 
              cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
          else
              continue;
          cItemArrSample = cResult->compareItemArr;
          if(cItemArrMax == 0)  cItemArrMax = cItemArrSample;
          else if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrMax)) {
            cItemArrMax = cItemArrSample;
          }
      }
    }

    for(j=0; j<6; j++)  resultArr[j] = 0.0;
    resultArr[4] = 1.0;
    resultArr[5] = 1.0;

    for(j=0; j<array_n(cItemArrMax); j++) {
      for(k=0; k<6; k++)        resultArr[k] = 0.0;
      resultArr[4] = 1.0;
      resultArr[5] = 1.0;

      cItemSample = array_fetch(RtCompareItems_t *, cItemArrMax, j);
      if(first_flag) {
        fprintf(fout, "%s &\n", cItemSample->itemNickName);
        first_flag = 0;
      }
      else {
        fprintf(fout, " & %s &\n", cItemSample->itemNickName);
      }

      for(k=0; k<array_n(designArr) && k<size; k++) {
        designList = array_fetch(RtDesignLists_t *, designArr, k);
        if(designList->resultForCommandArr1 == 0 ||
           designList->resultForCommandArr2 == 0) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }
        if(array_n(designList->resultForCommandArr1) <= i ||
           array_n(designList->resultForCommandArr2) <= i) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }
        cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
        cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
        if(cResult == 0 || cResult2 == 0) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }
        if(cResult->compareItemArr == 0 ||
           cResult2->compareItemArr == 0) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }
        if(array_n(cResult->compareItemArr) <= j ||
           array_n(cResult2->compareItemArr) <= j) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }
        cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
        cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
        if(cItem == 0 || cItem2 == 0) {
           resultArr[3] = resultArr[3] + 1.0;
           continue;
        }

        value1 = atof(cItem->value);
        value2 = atof(cItem2->value);
        if(value1 > value2)     gap = value2;
        else                    gap = value1;
        gap = gap * 0.02;
        if(gap < 1.0)   gap = 1.0;

        if(value1 > value2 + gap)       resultArr[0] = resultArr[0] + 1.0; /** new win **/
        else if(value1+gap < value2)    resultArr[1] = resultArr[1] + 1.0; /** ref win **/
        else                            resultArr[2] += 1.0; /** tie **/
      }
      totalNum = resultArr[0] + resultArr[1] + resultArr[2];
      totalNum = 1.0/totalNum;
      for(k=0; k<array_n(designArr) && k<size; k++) {
        designList = array_fetch(RtDesignLists_t *, designArr, k);
        if(designList->resultForCommandArr1 == 0 ||
           designList->resultForCommandArr2 == 0) {
           continue;
        }
        if(array_n(designList->resultForCommandArr1) <= i ||
           array_n(designList->resultForCommandArr2) <= i) {
           continue;
        }
        cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
        cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
        if(cResult == 0 || cResult2 == 0) {
           continue;
        }
        if(cResult->compareItemArr == 0 ||
           cResult2->compareItemArr == 0) {
           continue;
        }
        if(array_n(cResult->compareItemArr) <= j ||
           array_n(cResult2->compareItemArr) <= j) {
           continue;
        }
        cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
        cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
        if(cItem == 0 || cItem2 == 0) {
           continue;
        }

        value1 = atof(cItem->value);
        value2 = atof(cItem2->value);
        if(value1 == 0.0)       value1 = 1.0;
        else                    value1 = pow(value1, totalNum);
        if(value2 == 0.0)       value2 = 1.0;
        else                    value2 = pow(value2, totalNum);

        resultArr[4] *= value1;
        resultArr[5] *= value2;
      }

      if(array_n(cItemArrMax) == j+1 ) {
        fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\hline\n", 
                    (int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
                    (int)resultArr[3], resultArr[4], resultArr[5]);
      }
      else {
        fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\cline{2-8}\n", 
                    (int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
                    (int)resultArr[3], resultArr[4], resultArr[5]);
      }
    }
  }
  free(resultArr);
  fprintf(fout, "\\end{tabular}\n");
  fprintf(fout, "\\end{center}\n");
  fprintf(fout, "\\end{table}\n");

  fprintf(fout, "\\begin{itemize}\n");
  Rt_RemoveUnderscore(config->configurationFile, newName);
  fprintf(fout, "\\item configuration file : %s\n", newName);
  Rt_RemoveUnderscore(config->designDirectory, newName);
  fprintf(fout, "\\item design directory : %s\n", newName);
  Rt_RemoveUnderscore(config->designList, newName);
  fprintf(fout, "\\item design list : %s\n", newName);
  Rt_RemoveUnderscore(config->referenceOutDirectory, newName);
  fprintf(fout, "\\item reference output dir : %s\n", newName);
  Rt_RemoveUnderscore(config->referenceVis, newName);
  fprintf(fout, "\\item reference executable : %s\n", newName);
  Rt_RemoveUnderscore(config->refCommandTemplate, newName);
  fprintf(fout, "\\item reference template : %s\n", newName);
  Rt_RemoveUnderscore(config->newOutDirectory, newName);
  fprintf(fout, "\\item new output dir : %s\n", newName);
  Rt_RemoveUnderscore(config->newVis, newName);
  fprintf(fout, "\\item new executable : %s\n", newName);
  Rt_RemoveUnderscore(config->newCommandTemplate, newName);
  fprintf(fout, "\\item new template : %s\n", newName);
  fprintf(fout, "\\end{itemize}\n");
  fprintf(fout, "\\clearpage\n");

  fprintf(fout, "\\end{document}\n");
  fclose(fout);
  fprintf(vis_stdout, "'%s' file was generated as result of regression_test\n", 
               config->resultForPerformance);
  return(0);
}

/**Function********************************************************************

  Synopsis    [Remove underscopre from the string. ]

  Description [Remove underscore from the given string, since LaTeX consider
               underscore as subscript keyword. ]

  Comment []

  SideEffects []

******************************************************************************/
static void
Rt_RemoveUnderscore(char *name, 
                    char *newName)
{
int i, index ;

  index = 0;
  for(i=0; name[i] != '\0'; i++) {
    if(name[i] == '_') {
      newName[index++] = '\\';
    }
    newName[index++] = name[i];
  }
  newName[index] = '\0';
}

/**Function********************************************************************

  Synopsis    [Read the log file of both runs, and then store the information
               in the internal data structure. ]

  Description [Read the log file of runs, Current version supports
    reachability analysis, CTL model checking and invariant checking.
    If that is not the case, it may read the log file without errors
    except the couterexample trace.]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_CompareResult(RtConfigs_t *config,
                 RtDesignLists_t *designList,
                 int refOnly)
{
  FILE *fin1, *fin2;
  char filename1[1024], filename2[1024];
  char line[1024], *next;
  RtCompareItems_t *item, *newItem;
  RtResultPropertys_t *rProperty;
  RtCommandResults_t *cResult;
  int argc;
  char **argv;
  int i, len;
  int propertyIndex;
  int formulaSummary, commandBeginFlag;
  int basicLength, stemLength, cycleLength;
  int propertyIndexSummary, pIndex;
  int invCheckFlag;
  int nLine, countLineFlag;
  array_t *itemArr;

  propertyIndex = -1;
  basicLength = 0;
  stemLength = 0;
  cycleLength = 0;
  invCheckFlag = 0;
  propertyIndexSummary = 0;

  sprintf(filename1, "%s/%s/%s.out", config->referenceOutDirectory, 
                                     designList->designNickName, 
                                     designList->designNickName); 
  if(!(fin1 = fopen(filename1, "r"))) {
    fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename1);
    return(1);
  }

  fin2 = 0;
  if(!refOnly) {
    sprintf(filename2, "%s/%s/%s.out", config->newOutDirectory, 
                                     designList->designNickName, 
                                     designList->designNickName); 
    if(!(fin2 = fopen(filename2, "r"))) {
      fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename2);
      return(1);
    }
  }

  /** 
   * Compile the log file based on keywords, such as CommandEnd,
   * CommandBegin, # MC: formula, etc,. If timeout case is detected the
   * fill the data structure with 'TimeOut'.
   **/
  itemArr = config->compareItemArr;
  cResult = 0;
  formulaSummary = 0;
  commandBeginFlag = 0;
  nLine = 0;
  countLineFlag = 0;
  rProperty = 0;
  while(fgets(line, 1024, fin1)) {
    if(countLineFlag)   nLine++;
    if(line[0] == '\n') continue;
    if(!strncasecmp(line, "CommandEnd", 10)) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      rProperty = 0;
      commandBeginFlag = 0;
    }
    else if(!strncasecmp(line, "CommandBegin", 12)) {
      propertyIndex = -1;
      rProperty = 0;
      formulaSummary = 0;
      commandBeginFlag = 1;
      Rt_SplitLine(line, &argc, &argv);
      if(designList->resultForCommandArr1 == 0)
        designList->resultForCommandArr1= array_alloc(RtCommandResults_t *, 0);
      cResult = ALLOC(RtCommandResults_t, 1);
      cResult->resultForProperty = 0;
      cResult->compareItemArr = 0;
      cResult->command = strdup(argv[1]);
      cResult->bTimeOut = 0;
      array_insert_last(RtCommandResults_t *, designList->resultForCommandArr1,
      cResult);
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "** cmd error", 12)) {
      if(cResult)
        cResult->error = 1;
      fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
      designList->designNickName);
      continue;
    }
    else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[13], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1;
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if((!strncasecmp(line, "# AMC: formula", 14) ||
             !strncasecmp(line, "# IMC: formula", 14) ||
             !strncasecmp(line, "# BMC: formula", 14) ||
             !strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[14], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1; 
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[17], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1;
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "--Fair path stem:", 17)) {
      basicLength = 0;
      stemLength = 1;
      cycleLength = 0;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
      basicLength = 0;
      stemLength = 0;
      cycleLength = 1;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
      basicLength = 0;
      stemLength = 0;
      cycleLength = 1;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "--State ", 8)) {
      if(rProperty == 0) {
        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
        continue;
      }
      Rt_SplitLine(&line[8], &argc, &argv);
      len = strlen(argv[0]);
      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);

      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
      Rt_FreeArgv(argc, argv);
      if(countLineFlag == 0)    countLineFlag = 1;
      continue;
    }
    else if(!strncasecmp(line, "--Goes to state ", 16)) {
      if(rProperty == 0) {
        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
        continue;
      }
      Rt_SplitLine(&line[16], &argc, &argv);
      len = strlen(argv[0]);
      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);

      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "# INV: formula", 14)  && formulaSummary) {
      invCheckFlag = 1;
      basicLength = 0;
      Rt_SplitLine(&line[14], &argc, &argv);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
          rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
          propertyIndexSummary-1); 
          if(!rProperty) {
            rProperty = ALLOC(RtResultPropertys_t, 1);
            array_insert(RtResultPropertys_t *,cResult->resultForProperty,
            propertyIndexSummary-1, rProperty); 
            rProperty->lengthOfStem = -1;
            rProperty->lengthOfCycle = -1;
            rProperty->lengthOfInv = -1;
            rProperty->lengthOfCounterExample = -1; 
            rProperty->index = propertyIndexSummary;
          }
          if(rProperty->index != propertyIndexSummary) {
              fprintf(vis_stdout, "Error when compiling log file \n");
          }
      }
      else {
          rProperty = ALLOC(RtResultPropertys_t, 1);
          array_insert(RtResultPropertys_t *,cResult->resultForProperty,
          propertyIndexSummary-1, rProperty); 
          rProperty->lengthOfStem = -1;
          rProperty->lengthOfCycle = -1;
          rProperty->lengthOfInv = -1;
          rProperty->lengthOfCounterExample = -1; 
          rProperty->index = propertyIndexSummary;
      }
      if(argv[0][0] == 'f' || argv[0][0] == 'p')
        rProperty->failOrPass = strdup(argv[0]);
      else
        rProperty->failOrPass = strdup(argv[1]);
      basicLength = 0;
      stemLength = 0;
      cycleLength = 0;
      Rt_FreeArgv(argc, argv);
      propertyIndexSummary++;
      continue;
    }
    else if(!strncasecmp(line, "# INV: formula", 14)  && !formulaSummary) {
      invCheckFlag = 1;
      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
      countLineFlag = 0;
      nLine = 0;
      Rt_SplitLine(&line[14], &argc, &argv);
      if(Rt_IsNum(argv[0])) {
          if(cResult->resultForProperty == 0)
            cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
          pIndex = atoi(argv[0]);
          if(array_n(cResult->resultForProperty) > pIndex) {
              rProperty = array_fetch(RtResultPropertys_t *,
              cResult->resultForProperty, pIndex-1); 
              if(!rProperty) {
                  rProperty = ALLOC(RtResultPropertys_t, 1);
                  array_insert(RtResultPropertys_t *,cResult->resultForProperty,
                  pIndex-1, rProperty); 
                  rProperty->lengthOfStem = -1;
                  rProperty->lengthOfCycle = -1;
                  rProperty->lengthOfInv = -1;
                  rProperty->lengthOfCounterExample = -1; 
                  rProperty->index = pIndex;
              }
              if(rProperty->index != pIndex) {
                  fprintf(vis_stdout, "Error when compiling log file \n");
              }
          }
          else {
              rProperty = ALLOC(RtResultPropertys_t, 1);
              array_insert(RtResultPropertys_t *,cResult->resultForProperty,
              pIndex-1, rProperty); 
              rProperty->lengthOfStem = -1;
              rProperty->lengthOfCycle = -1;
              rProperty->lengthOfInv = -1;
              rProperty->lengthOfCounterExample = -1; 
              rProperty->index = pIndex;
          }
          if(argv[1][0] == 'f' || argv[1][0] == 'p')
            rProperty->failOrPass = strdup(argv[1]);
          else
            rProperty->failOrPass = strdup(argv[2]);
          basicLength = 0;
          stemLength = 0;
          cycleLength = 0;
          Rt_FreeArgv(argc, argv);
      }
      continue;
    }
    else if(!strncasecmp(line, "# INV: Summary", 14)) {
      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
      countLineFlag = 0;
      nLine = 0;
      formulaSummary = 1;
      propertyIndexSummary = 1;
      continue;
    }
    next = strstr(line, "timeout");
    if(next == 0) 
        next = strstr(line, "Timeout");
    if(next) {
        if(!strncasecmp(next, "timeout occurred after", 22)) {
            cResult->bTimeOut = 1;
        }
        else if(!strncasecmp(next, "timeout after", 14)) {
            cResult->bTimeOut = 1;
        }
    }
    for(i=0; i<array_n(itemArr); i++) {
      item = array_fetch(RtCompareItems_t *, itemArr, i);
      len = strlen(item->itemName);
      if(!strncasecmp(item->itemName, line, len)) {
        newItem = ALLOC(RtCompareItems_t, 1);
        newItem->itemNickName = strdup(item->itemNickName);
        newItem->itemName = 0;
        newItem->value = 0;
        Rt_SplitLine(&line[len], &argc, &argv);
        newItem->value = strdup(argv[0]);
        if(cResult->compareItemArr == 0)
          cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
        array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
        Rt_FreeArgv(argc, argv);
        break;
      }
    }
  }
  if(commandBeginFlag == 1) {
    if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0) 
      cResult->resultForProperty = 0;
    cResult->compareItemArr = 0;
  }

  cResult = 0;
  commandBeginFlag = 0;
  nLine = 0;
  countLineFlag = 0;
  rProperty = 0;
  while(fgets(line, 1024, fin2)) {
    if(countLineFlag) nLine++;
    if(line[0] == '\n') continue;
    if(!strncasecmp(line, "CommandEnd", 10)) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      rProperty = 0;
      nLine = 0;
      commandBeginFlag = 0;
    }
    else if(!strncasecmp(line, "CommandBegin", 12)) {
      propertyIndex = -1;
      rProperty = 0;
      formulaSummary = 0;
      commandBeginFlag = 1;
      Rt_SplitLine(line, &argc, &argv);
      if(designList->resultForCommandArr2 == 0)
        designList->resultForCommandArr2= array_alloc(RtCommandResults_t *, 0);
      cResult = ALLOC(RtCommandResults_t, 1);
      cResult->resultForProperty = 0;
      cResult->compareItemArr = 0;
      cResult->bTimeOut = 0;
      cResult->command = strdup(argv[1]);
      array_insert_last(RtCommandResults_t *, designList->resultForCommandArr2,
      cResult);
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "** cmd error", 12)) {
      if(cResult)
        cResult->error = 1;
      fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
      designList->designNickName);
      continue;
    }
    else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[13], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1; 
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if((!strncasecmp(line, "# AMC: formula", 14) ||
             !strncasecmp(line, "# IMC: formula", 14) ||
             !strncasecmp(line, "# BMC: formula", 14) ||
             !strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[14], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1; 
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
      if(rProperty && countLineFlag)    {
        rProperty->lengthOfCounterExample = nLine;
        if(rProperty->lengthOfBasic > -1) {
          if(rProperty->lengthOfStem > -1)
            rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
          else
            rProperty->lengthOfStem = rProperty->lengthOfBasic;
        }
      }
      countLineFlag = 0;
      nLine = 0;
      propertyIndex++;
      Rt_SplitLine(&line[17], &argc, &argv);
      rProperty = ALLOC(RtResultPropertys_t, 1);
      rProperty->lengthOfBasic = -1;
      rProperty->lengthOfStem = -1;
      rProperty->lengthOfCycle = -1;
      rProperty->lengthOfInv = -1;
      rProperty->lengthOfCounterExample = -1; 
      rProperty->index = propertyIndex;
      rProperty->failOrPass = strdup(argv[0]);
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty); 
      basicLength = 1;
      stemLength = 0;
      cycleLength = 0;
      invCheckFlag = 0;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "--Fair path stem:", 17)) {
      basicLength = 0;
      stemLength = 1;
      cycleLength = 0;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
      basicLength = 0;
      stemLength = 0;
      cycleLength = 1;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
      basicLength = 0;
      stemLength = 0;
      cycleLength = 1;
      rProperty->lengthOfInv = -1;
      continue;
    }
    else if(!strncasecmp(line, "--State ", 8)) {
      if(rProperty == 0) {
        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
        continue;
      }
      Rt_SplitLine(&line[8], &argc, &argv);
      len = strlen(argv[0]);
      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
      else if(stemLength)               rProperty->lengthOfStem = atoi(argv[0]);
      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;
      if(countLineFlag == 0)    countLineFlag = 1;
      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "--Goes to state ", 16)) {
      if(rProperty == 0) {
        fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
        continue;
      }
      Rt_SplitLine(&line[16], &argc, &argv);
      len = strlen(argv[0]);
      if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
      if(basicLength)           rProperty->lengthOfBasic = atoi(argv[0]);
      else if(stemLength)       rProperty->lengthOfStem = atoi(argv[0]);
      else if(cycleLength)      rProperty->lengthOfCycle = atoi(argv[0]);
      else if(invCheckFlag)     rProperty->lengthOfInv = atoi(argv[0]);
      if(stemLength || cycleLength)     rProperty->lengthOfInv = -1;

      Rt_FreeArgv(argc, argv);
      continue;
    }
    else if(!strncasecmp(line, "# INV: formula", 14)  && formulaSummary) {
      Rt_SplitLine(&line[14], &argc, &argv);
      invCheckFlag = 1;
      if(cResult->resultForProperty == 0)
        cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
      if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
          rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
          propertyIndexSummary-1); 
          if(!rProperty) {
            rProperty = ALLOC(RtResultPropertys_t, 1);
            array_insert(RtResultPropertys_t *,cResult->resultForProperty,
            propertyIndexSummary-1, rProperty); 
            rProperty->lengthOfStem = -1;
            rProperty->lengthOfCycle = -1;
            rProperty->lengthOfInv = -1;
            rProperty->lengthOfCounterExample = -1;
            rProperty->index = propertyIndexSummary;
          }
          if(rProperty->index != propertyIndexSummary) {
              fprintf(vis_stdout, "Error when compiling log file \n");
          }
      }
      else {
          rProperty = ALLOC(RtResultPropertys_t, 1);
          array_insert(RtResultPropertys_t *,cResult->resultForProperty,
          propertyIndexSummary-1, rProperty); 
          rProperty->lengthOfStem = -1;
          rProperty->lengthOfCycle = -1;
          rProperty->lengthOfInv = -1;
          rProperty->lengthOfCounterExample = -1;
          rProperty->index = propertyIndexSummary;
      }
      if(argv[0][0] == 'f' || argv[0][0] == 'p')
        rProperty->failOrPass = strdup(argv[0]);
      else
        rProperty->failOrPass = strdup(argv[1]);
      stemLength = 0;
      cycleLength = 0;
      Rt_FreeArgv(argc, argv);
      propertyIndexSummary++;
      continue;
    }
    else if(!strncasecmp(line, "# INV: formula", 14)  && !formulaSummary) {
      invCheckFlag = 1;
      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
      countLineFlag = 0;
      nLine = 0;
      Rt_SplitLine(&line[14], &argc, &argv);
      if(Rt_IsNum(argv[0])) {
          if(cResult->resultForProperty == 0)
            cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
          pIndex = atoi(argv[0]);
          if(array_n(cResult->resultForProperty) > pIndex) {
              rProperty = array_fetch(RtResultPropertys_t *,
              cResult->resultForProperty, pIndex-1); 
              if(!rProperty) {
                  rProperty = ALLOC(RtResultPropertys_t, 1);
                  array_insert(RtResultPropertys_t *,cResult->resultForProperty,
                  pIndex-1, rProperty); 
                  rProperty->lengthOfStem = -1;
                  rProperty->lengthOfCycle = -1;
                  rProperty->lengthOfInv = -1;
                  rProperty->lengthOfCounterExample = -1;
                  rProperty->index = pIndex;
              }
              if(rProperty->index != pIndex) {
                  fprintf(vis_stdout, "Error when compiling log file \n");
              }
          }
          else {
              rProperty = ALLOC(RtResultPropertys_t, 1);
              array_insert(RtResultPropertys_t *,cResult->resultForProperty,
              pIndex-1, rProperty); 
              rProperty->lengthOfStem = -1;
              rProperty->lengthOfCycle = -1;
              rProperty->lengthOfInv = -1;
              rProperty->lengthOfCounterExample = -1;
              rProperty->index = pIndex;
          }
          if(argv[1][0] == 'f' || argv[1][0] == 'p')
            rProperty->failOrPass = strdup(argv[1]);
          else
            rProperty->failOrPass = strdup(argv[2]);
          stemLength = 0;
          cycleLength = 0;
          Rt_FreeArgv(argc, argv);
      }
      continue;
    }
    else if(!strncasecmp(line, "# INV: Summary", 14)) {
      if(rProperty && countLineFlag)    rProperty->lengthOfCounterExample = nLine;
      countLineFlag = 0;
      nLine = 0;
      formulaSummary = 1;
      propertyIndexSummary = 1;
      continue;
    }

    next = strstr(line, "timeout");
    if(next == 0) 
        next = strstr(line, "Timeout");
    if(next) {
        if(!strncasecmp(next, "timeout occurred after", 22)) {
            cResult->bTimeOut = 1;
        }
        else if(!strncasecmp(next, "timeout after", 14)) {
            cResult->bTimeOut = 1;
        }
    }
    for(i=0; i<array_n(itemArr); i++) {
      item = array_fetch(RtCompareItems_t *, itemArr, i);
      len = strlen(item->itemName);
      if(!strncasecmp(item->itemName, line, len)) {
        newItem = ALLOC(RtCompareItems_t, 1);
        newItem->itemNickName = strdup(item->itemNickName);
        newItem->itemName = 0;
        newItem->value = 0;
        Rt_SplitLine(&line[len], &argc, &argv);
        newItem->value = strdup(argv[0]);
        if(cResult->compareItemArr == 0)
          cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
        array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
        Rt_FreeArgv(argc, argv);
        break;
      }
    }
  }
  if(commandBeginFlag == 1) {
    if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0) 
      cResult->resultForProperty = 0;
    cResult->compareItemArr = 0;
  }

  fclose(fin1);
  fclose(fin2);
  return(0);
}

/**Function********************************************************************

  Synopsis    [Check whether given string is digit or not.]

  Description [ ]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_IsNum(char *tmp)
{
  int i, len;

  len = strlen(tmp);
  for(i=0; i<len; i++) {
    if(!isdigit((int)tmp[i]))return(0);
  }
  return(1);
}


/**Function********************************************************************

  Synopsis    [Exceute experiments based on 'ReferenceVis' and 'NewVis'. ]

  Description [ ]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_ExecuteVis(RtConfigs_t *config,
              RtDesignLists_t *designList,
              int refAndNew, FILE *scriptOut)
{
  char temp[1024];
  char dir[1024];
  char exe[1024];
  char name[1024];
  char srcFile[1024];
  char outFile[1024];


  if(refAndNew == 1 && !config->bRefRun)return(0);
  if(refAndNew == 2 && !config->bNewRun)return(0);

  if(refAndNew == 1) {
    sprintf(dir, "%s/%s", config->referenceOutDirectory, designList->designNickName);  
    sprintf(exe, "%s", config->referenceVis);  
    sprintf(name, "%s", designList->designNickName);  
  }
  if(refAndNew == 2) {
    sprintf(dir, "%s/%s", config->newOutDirectory, designList->designNickName);  
    sprintf(exe, "%s", config->newVis);  
    sprintf(name, "%s", designList->designNickName);  
  }
  sprintf(srcFile, "%s/%s.src", dir, name);
  sprintf(outFile, "%s/%s.out", dir, name);

  if(scriptOut) {
  /**
    sprintf(temp, "%s -x -f %s/%s.src >& %s/%s.out", exe, dir, name, dir, name);
    **/
    sprintf(temp, "%s -x -f %s.src >& %s.out", exe, name, name);
    fprintf(scriptOut, "echo %s begin\n", designList->designNickName);
    fprintf(scriptOut, "cd %s\n", dir);
    fprintf(scriptOut, "%s\n", temp);
    fprintf(scriptOut, "cd ../../\n");
  }
  else {
    sprintf(temp, "%s -x -f %s/%s.src > %s/%s.out", exe, dir, name, dir, name);
    if (system(temp))
      return(1);
  }
  /**
    sprintf(temp, "%s -x -f %s/%s.src", exe, dir, name);
   **/

  return(0);
}

/**Function********************************************************************

  Synopsis    [Write the script file for VIS execution. ]

  Description [ Wirte  the batch script for experiments.  The variables and the
aliases are defined by examining the fields of the test case description in the
design file.   It uses TemplateFile  to make a  script. So The  template should
refer  to the  defined aliases  and  variables to  tailor itself  to each  test
case. ]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_WriteBatchCommand(RtConfigs_t *config, 
                     RtDesignLists_t *designList)
{
  FILE *fout1;
  FILE *fout2;
  char filename1[1024];
  char filename2[1024];
  char refDir[1024];
  char temp[1024];
  int i;
  RtCommandResults_t *cTemplate;
  array_t *cTemplateArrOld;
  array_t *cTemplateArrNew;
  
  fout1 = fout2 = 0;
  if(config->bRefRun) {
    sprintf(temp, "\\mkdir -p %s/%s", config->referenceOutDirectory, 
                                   designList->designNickName);
    if (system(temp))
      return(1);
  }
  if(config->bNewRun) {
    sprintf(temp, "\\mkdir -p %s/%s", config->newOutDirectory, 
                                   designList->designNickName);
    if (system(temp))
      return(1);
  }

  if(config->bRefRun) {
    sprintf(filename1, "%s/%s/%s.src", config->referenceOutDirectory, 
                                     designList->designNickName,
                                     designList->designNickName);
    if(!(fout1 = fopen(filename1, "w"))) {
      fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename1);
      return(0);
    }
  }
  if(config->bNewRun) {
    sprintf(filename2, "%s/%s/%s.src", config->newOutDirectory, 
                                     designList->designNickName,
                                     designList->designNickName);
    if(!(fout2 = fopen(filename2, "w"))) {
      fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename2);
      fclose(fout1);
      return(0);
    }
  }

  cTemplateArrOld = config->refCommandTemplateArr;
  cTemplateArrNew = config->newCommandTemplateArr;
  sprintf(refDir, "%s/%s", config->designDirectory, designList->designDirectory);

  if(config->bRefRun) {
  /**
    fprintf(fout1, "set vis_stdout %s/%s/%s.out\n", 
       config->referenceOutDirectory, designList->designNickName, designList->designNickName);
    fprintf(fout1, "set vis_stderr %s/%s/%s.out\n", 
       config->referenceOutDirectory, designList->designNickName, designList->designNickName);
   **/
    fprintf(fout1, "set BaseName %s\n", designList->designNickName);
  }
  if(config->bNewRun) {
  /**
    fprintf(fout2, "set vis_stdout %s/%s/%s.out\n", 
       config->newOutDirectory, designList->designNickName, designList->designNickName);
    fprintf(fout2, "set vis_stderr %s/%s/%s.out\n", 
       config->newOutDirectory, designList->designNickName, designList->designNickName);
   **/
    fprintf(fout2, "set BaseName %s\n", designList->designNickName);
  }

  if(designList->blifFile) {
    if(config->bRefRun)
    fprintf(fout1, "set BlifFile %s/%s\n", refDir, designList->blifFile);
    if(config->bNewRun)
    fprintf(fout2, "set BlifFile %s/%s\n", refDir, designList->blifFile);
  }
  if(designList->ordFile) {
    if(config->bRefRun)
    fprintf(fout1, "set OrdFile %s/%s\n", refDir, designList->ordFile);
    if(config->bNewRun)
    fprintf(fout2, "set OrdFile %s/%s\n", refDir, designList->ordFile);
  }
  if(designList->ctlFile) {
    if(config->bRefRun)
    fprintf(fout1, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
    if(config->bNewRun)
    fprintf(fout2, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
  }
  if(designList->invFile) {
    if(config->bRefRun)
    fprintf(fout1, "set InvFile %s/%s\n", refDir, designList->invFile);
    if(config->bNewRun)
    fprintf(fout2, "set InvFile %s/%s\n", refDir, designList->invFile);
  }
  if(designList->leFile) {
    if(config->bRefRun)
    fprintf(fout1, "set LeFile %s/%s\n", refDir, designList->leFile);
    if(config->bNewRun)
    fprintf(fout2, "set LeFile %s/%s\n", refDir, designList->leFile);
  }
  if(designList->ltlFile) {
    if(config->bRefRun)
    fprintf(fout1, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
    if(config->bNewRun)
    fprintf(fout2, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
  }
  if(designList->fairFile) {
    if(config->bRefRun)
    fprintf(fout1, "set FairFile %s/%s\n", refDir, designList->fairFile);
    if(config->bNewRun)
    fprintf(fout2, "set FairFile %s/%s\n", refDir, designList->fairFile);
  }
  if(designList->hintFile) {
    if(config->bRefRun)
    fprintf(fout1, "set HintFile %s/%s\n", refDir, designList->hintFile);
    if(config->bNewRun)
    fprintf(fout2, "set HintFile %s/%s\n", refDir, designList->hintFile);
  }

  if(config->bRefRun) {
    if(designList->fairFile)
      fprintf(fout1, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
    else
      fprintf(fout1, "set fairOption \" \"\n");
  }
  if(config->bNewRun) {
    if(designList->fairFile)
      fprintf(fout2, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
    else
      fprintf(fout2, "set fairOption \" \"\n");
  }


  if(config->bDefaultInitCommand) {
    if(config->bRefRun) {
      fprintf(fout1, "echo CommandBegin init\n");
      if(designList->ordFile) {
        if(designList->bIsMv)
           fprintf(fout1, "rlmv $BlifFile\n");
        else
           fprintf(fout1, "read_blif $BlifFile\n");
        fprintf(fout1, "flatten_hierarchy\n");
        fprintf(fout1, "static_order -s partial $OrdFile\n");
        fprintf(fout1, "build_partition_mdds\n");
        if(designList->fairFile)
          fprintf(fout1, "rf $FairFile\n");
      }
      else {
        if(designList->bIsMv)
           fprintf(fout1, "rlmv $BlifFile\n");
        else
           fprintf(fout1, "read_blif $BlifFile\n");
        fprintf(fout1, "echo init\n");
        fprintf(fout1, "init\n");
        if(designList->fairFile)
          fprintf(fout1, "rf $FairFile\n");
      }
      fprintf(fout1, "time\n");
      fprintf(fout1, "print_bdd_stats\n");
      fprintf(fout1, "echo CommandEnd init\n");
    }
    if(config->bNewRun) {
      fprintf(fout2, "echo CommandBegin init\n");
      if(designList->ordFile) {
        if(designList->bIsMv)
           fprintf(fout2, "rlmv $BlifFile\n");
        else
           fprintf(fout2, "read_blif $BlifFile\n");
        fprintf(fout2, "flatten_hierarchy\n");
        fprintf(fout2, "static_order -s partial $OrdFile\n");
        fprintf(fout2, "build_partition_mdds\n");
        if(designList->fairFile)
          fprintf(fout2, "rf $FairFile\n");
      }
      else {
        if(designList->bIsMv)
           fprintf(fout2, "rlmv $BlifFile\n");
        else
           fprintf(fout2, "read_blif $BlifFile\n");
        fprintf(fout2, "echo init\n");
        fprintf(fout2, "init\n");
        if(designList->fairFile)
          fprintf(fout2, "rf $FairFile\n");
      }
      fprintf(fout2, "time\n");
      fprintf(fout2, "print_bdd_stats\n");
      fprintf(fout2, "echo CommandEnd init\n");
    } 
  }
  else {
    /** 
     * Alias read_model, set_fairness and order_vars  based on 
     * whether the design list specifies a .mv file or a .blif file 
     * as model file.
     **/
    if(config->bRefRun) {
      if(designList->bIsMv)
        fprintf(fout1, "alias read_model \"rlmv $BlifFile\"\n");
      else
        fprintf(fout1, "alias read_model \"read_blif $BlifFile\"\n");
      if(designList->fairFile)  
        fprintf(fout1, "alias set_fairness \"read_fairness $FairFile\"\n");
      else
        fprintf(fout1, "alias set_fairness \" \"\n");
      if(designList->ordFile)   
        fprintf(fout1, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
      else
        fprintf(fout1, "alias order_vars \"so\"\n");
    }
    if(config->bNewRun) {
      if(designList->bIsMv)
        fprintf(fout2, "alias read_model \"rlmv $BlifFile\"\n");
      else
        fprintf(fout2, "alias read_model \"read_blif $BlifFile\"\n");
      if(designList->fairFile)  
        fprintf(fout2, "alias set_fairness \"read_fairness $FairFile\"\n");
      else
        fprintf(fout2, "alias set_fairness \" \"\n");
      if(designList->ordFile)   
        fprintf(fout2, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
      else
        fprintf(fout2, "alias order_vars \"so\"\n");
    } 
  }

  if(config->bRefRun) {
    for(i=0; i<array_n(cTemplateArrOld); i++) {
      cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrOld, i);
      fprintf(fout1, "%s\n", cTemplate->command);
    }
    fprintf(fout1, "quit\n");
    fclose(fout1);
  }
  if(config->bNewRun) {
    for(i=0; i<array_n(cTemplateArrNew); i++) {
      cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrNew, i);
      fprintf(fout2, "%s\n", cTemplate->command);
    }
    fprintf(fout2, "quit\n");
    fclose(fout2);
  }

  return(0);
}

/**Function********************************************************************

  Synopsis    [ Read command template and check whether it contains illegal command and alias. ]

  Description [ When read the template,  if we meet the string followed by '$',
then check whether  that string is reserved  word or not. If the  string is not
reserved work then we consider that as a variable.]

  Comment []

  SideEffects []

******************************************************************************/

static int
Rt_ReadCommandTemplate(RtConfigs_t * config)
{
  FILE  *fin;
  char line[1024];
  char *filename;
  char temp[1024];
  int i;
  RtCommandResults_t *cResult;
  int argc;
  char **argv;
  char *next, *tmp;

  if(config->bRefRun) {
  filename = config->refCommandTemplate;
  if(!(fin = fopen(filename, "r"))) {
    fprintf(vis_stdout, "Error : Can't open command template file '%s' for reference\n", filename);
    return(1);
  }

  if(config->keyWordTable == 0)
    config->keyWordTable = st_init_table(strcmp, st_strhash);
  config->refCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
  while(fgets(line, 1024, fin)) {
    if(line[0] == '#')  continue;
    cResult = ALLOC(RtCommandResults_t, 1);
    cResult->resultForProperty = 0;
    cResult->compareItemArr = 0;
    cResult->command = 0;
    Rt_SplitLine(line, &argc, &argv);
    temp[0] = '\0';
    for(i=0; i<argc; i++) {
      strcat(temp, argv[i]); 
      if(i+1 != argc) strcat(temp, " ");
      if(argv[i][0] == '$') {
         if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
            next = strdup(argv[i]);
            st_insert(config->keyWordTable, next, next);
         }
      }
    }
    Rt_FreeArgv(argc, argv);
    cResult->command = strdup(temp);
    array_insert_last(RtCommandResults_t *, config->refCommandTemplateArr, cResult);

  }
  fclose(fin);
  }

  if(config->bNewRun) {
  filename = config->newCommandTemplate;
  if(!(fin = fopen(filename, "r"))) {
    fprintf(vis_stdout, "Error : Can't open command template file '%s' for new\n", filename);
    return(1);
  }
  if(config->keyWordTable == 0)
    config->keyWordTable = st_init_table(strcmp, st_strhash);
  config->newCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
  while(fgets(line, 1024, fin)) {
    if(line[0] == '#')  continue;
    cResult = ALLOC(RtCommandResults_t, 1);
    cResult->resultForProperty = 0;
    cResult->compareItemArr = 0;
    cResult->command = 0;
    Rt_SplitLine(line, &argc, &argv);
    temp[0] = '\0';
    for(i=0; i<argc; i++) {
      strcat(temp, argv[i]); 
      if(i+1 != argc) strcat(temp, " ");
      if(argv[i][0] == '$') {
         if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
            next = strdup(argv[i]);
            st_insert(config->keyWordTable, next, next);
         }
      }
    }
    Rt_FreeArgv(argc, argv);
    cResult->command = strdup(temp);
    array_insert_last(RtCommandResults_t *, config->newCommandTemplateArr, cResult);
  }
  fclose(fin);
  }
  return(0);
}


/**Function********************************************************************

  Synopsis    [Read the design list. ]

  Description [  To specify the  type of file,  we use extension of  file name,
such  as .mv,  .blif,  .ord, .inv,  .ctl,  .fair, .ltl  and  .hint.  Each  line
consists  of white  space-separated fields.   The first  is a  (relative) path,
while the second is the  collection name.  The smallest collection will specify
one .mv  or one .blif file with  path and collection name.  Lines starting with
'#' are interpreted as comments and are skipped, as in all files read]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_ReadDesignListFile(RtConfigs_t * config)
{
  FILE  *fin;
  char line[1024];
  char *filename, *str;
  char suffix[1024];
  int i, j, index, bDot, strLen;
  RtDesignLists_t *designList;
  int argc;
  char **argv;

  filename = config->designList;

  if(!(fin = fopen(filename, "r"))) {
    fprintf(vis_stdout, "Error : Can't open design list file '%s'\n", filename);
    return(1);
  }

  config->designListArr = array_alloc(RtDesignLists_t *, 0);
  while(fgets(line, 1024, fin)) {
    if(line[0] == '#')  continue;
    if(line[0] == '\n') continue;
    Rt_SplitLine(line, &argc, &argv);
    designList = ALLOC(RtDesignLists_t, 1);
    designList->designDirectory = strdup(argv[0]);
    designList->designNickName = strdup(argv[1]);
    designList->blifFile = strdup(argv[2]);
    designList->leFile = 0;
    designList->ltlFile = 0;
    designList->ordFile = 0;
    designList->hintFile = 0;
    designList->ctlFile = 0;
    designList->invFile = 0;
    designList->fairFile = 0;
    designList->resultForCommandArr1 = 0;
    designList->resultForCommandArr2 = 0;

    str = argv[2];
    index = bDot = 0;
    strLen = strlen(str);
    for(j=strLen; j>=0; j--) {
      if(str[j] == '.') {       
        bDot = 1; 
        break;
      }
    }
    if(bDot==0) {
      fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
      designList->designNickName);
      Rt_FreeArgv(argc, argv);
      free(designList);
      continue;
    }
    else {
      j++;
      for(;str[j] != '\0'; j++) {
        suffix[index++] = str[j];
      }
    }
    suffix[index] = '\0';

    if(!strcasecmp(suffix, "blif")) 
      designList->bIsMv = 0;
    else if(!strcasecmp(suffix, "mv")) 
      designList->bIsMv = 1;
    else {
      fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
      designList->designNickName);
      Rt_FreeArgv(argc, argv);
      free(designList);
      continue;
    }

    for(i=3; i<argc; i++) {
      str = argv[i];
      index = bDot = 0;
      strLen = strlen(str);
      for(j=strLen; j>=0; j--) {
        if(str[j] == '.') {     
          bDot = 1; 
          break;
        }
      }
      if(bDot==0) {
        fprintf(vis_stdout, "Error : Illegal suffix of file '%s' in design list '%s'\n", 
          argv[i], designList->designNickName);
        Rt_FreeArgv(argc, argv);
        free(designList);
        continue;
      }
      else {
        j++;
        for(;str[j] != '\0'; j++) {
          suffix[index++] = str[j];
        }
      }
      suffix[index] = '\0';
      if(!strcasecmp(suffix, "ctl")) 
        designList->ctlFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "fair")) 
        designList->fairFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "inv")) 
        designList->invFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "le")) 
        designList->leFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "ltl")) 
        designList->ltlFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "ord")) 
        designList->ordFile = strdup(argv[i]);
      else if(!strcasecmp(suffix, "hint")) 
        designList->hintFile = strdup(argv[i]);
      else {
        fprintf(vis_stdout, "Illegal suffix of file '%s'\n", argv[i]);
        Rt_FreeArgv(argc, argv);
        fclose(fin);
        return(1);
      }
    }
    array_insert_last(RtDesignLists_t *, config->designListArr, designList);
    Rt_FreeArgv(argc, argv);
  }

  fclose(fin);
  return(0);
}

/**Function********************************************************************

  Synopsis    [Read Configuration file ]

  Description [Read each line of Configuration file and fill the data
  structure.  A line beginning with '#' is a comment. ]

  Comment []

  SideEffects []

******************************************************************************/
static RtConfigs_t *
Rt_ReadConfigFile(char *filename)
{
  FILE  *fin;
  char line[1024];
  char temp[1024];
  RtConfigs_t *config;
  int i, argc;
  int errorFlag;
  char **argv;
  RtCompareItems_t *cItem;

  if(!(fin = fopen(filename, "r"))) {
    fprintf(vis_stdout, "Error : Can't open configuration file '%s'\n", filename);
    return(0);
  }

  config = ALLOC(RtConfigs_t, 1);
  memset(config, 0, sizeof(RtConfigs_t));
  config->configurationFile = strdup(filename);
  config->compareItemArr = 0;
  config->bRefOnly = 0;
  config->keyWordTable = 0;
  config->bRefRun = -1;
  config->bNewRun = -1;
  while(fgets(line, 1024, fin)) {
    if(line[0] == '#')  continue;
    if(line[0] == '\n') continue;
    Rt_SplitLine(line, &argc, &argv);
    if(argv[0][0] == '\n')      continue;
    if(argc < 3)        continue;
    if(argv[2] == 0)    continue;
    if(!strcasecmp("DesignDirectory", argv[0])) {
      config->designDirectory = strdup(argv[2]);
    }
    else if(!strcasecmp("ReferenceVis", argv[0])) {
      config->referenceVis = strdup(argv[2]);
    }
    else if(!strcasecmp("ReferenceVisNickName", argv[0])) {
      config->referenceVisNickName = strdup(argv[2]);
    }
    else if(!strcasecmp("ReferenceVisOptionFile", argv[0])) {
      config->referenceVisOptionFile = strdup(argv[2]);
    }
    else if(!strcasecmp("ReferenceOutputDir", argv[0])) {
      config->referenceOutDirectory = strdup(argv[2]);
    }
    else if(!strcasecmp("bRefRun", argv[0])) {
      config->bRefRun = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("NewVis", argv[0])) {
      config->newVis = strdup(argv[2]);
    }
    else if(!strcasecmp("NewVisNickName", argv[0])) {
      config->newVisNickName = strdup(argv[2]);
    }
    else if(!strcasecmp("NewVisOptionFile", argv[0])) {
      config->newVisOptionFile = strdup(argv[2]);
    }
    else if(!strcasecmp("NewOutputDir", argv[0])) {
      config->newOutDirectory = strdup(argv[2]);
    }
    else if(!strcasecmp("bNewRun", argv[0])) {
      config->bNewRun = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("NewCommandTemplate", argv[0])) {
      config->newCommandTemplate = strdup(argv[2]);
    }
    else if(!strcasecmp("RefCommandTemplate", argv[0])) {
      config->refCommandTemplate = strdup(argv[2]);
    }
    else if(!strcasecmp("DesignList", argv[0])) {
      config->designList = strdup(argv[2]);
    }
    else if(!strcasecmp("bCompareCounterExample", argv[0])) {
      config->bCompareCounterExample = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("bFinalResultOnly", argv[0])) {
      config->bFinalResultOnly = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("bDontRemoveTempFile", argv[0])) {
      config->bDontRemoveTempFile = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("bDefaultInitCommand", argv[0])) {
      config->bDefaultInitCommand = Rt_SetBooleanValue(argv[2], argv[0]);
    }
    else if(!strcasecmp("ResultForPerformance", argv[0])) {
      config->resultForPerformance = strdup(argv[2]);
    }
    else if(!strcasecmp("ResultForCounterExample", argv[0])) {
      config->resultForCounterExample = strdup(argv[2]);
    }
    else if(!strcasecmp("CompareItem", argv[0])) {
      cItem = ALLOC(RtCompareItems_t, 1);
      cItem->itemNickName = strdup(argv[2]);
      temp[0] = '\0';
      for(i=4; i<argc; i++) {
        strcat(temp, argv[i]);
        if(i+1 != argc) strcat(temp, " ");
      }
      cItem->itemName = strdup(temp);
      cItem->value = 0;
      if(!config->compareItemArr)
        config->compareItemArr = array_alloc(RtCompareItems_t *, 0);
      array_insert_last(RtCompareItems_t *, config->compareItemArr, cItem);
    }
    else {
      fprintf(vis_stdout, "Unknown option '%s' in configuration file\n", argv[0]);
      free(config);
      Rt_FreeArgv(argc, argv);
      fclose(fin);
      return(0);
    }
    Rt_FreeArgv(argc, argv);
  }
  fclose(fin);

  errorFlag = 0;
  if(config->designDirectory == 0) {
    fprintf(stdout, "DesignDirectory is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->referenceVis == 0) {
    fprintf(stdout, "ReferenceVis is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->referenceVisNickName == 0) {
    fprintf(stdout, "ReferenceVisNickName is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->referenceOutDirectory == 0) {
    fprintf(stdout, "ReferenceOutDirectory is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->newVis == 0) {
    fprintf(stdout, "NewVis is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->newVisNickName == 0) {
    fprintf(stdout, "NewVisNickName is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->newOutDirectory == 0) {
    fprintf(stdout, "NewOutDirectory is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->bRefRun == -1) {
    fprintf(stdout, "bRefRun is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->bNewRun == -1) {
    fprintf(stdout, "bNewRun is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->designList == 0) {
    fprintf(stdout, "DesignList is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->newCommandTemplate == 0) {
    fprintf(stdout, "NewCommandTemplate is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }
  if(config->refCommandTemplate == 0) {
    fprintf(stdout, "RefCommandTemplate is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }

  if(config->compareItemArr == 0 || array_n(config->compareItemArr) == 0) {
    fprintf(stdout, "CompareItem is not specified in configuration file '%s'\n",
                filename);
    errorFlag = 1;
  }

  if(errorFlag) {
    free(config);
    return(0);
  }
  
  return(config);
}

/**Function********************************************************************

  Synopsis    [Return 1 if the string contains 'TURE', otherwise return 0. ]

  Description [ ]

  Comment []

  SideEffects []

******************************************************************************/
static int
Rt_SetBooleanValue(char *str, char *option)
{

  if(!strcmp("TRUE", str) || !strcmp("1", str))
    return(1);
  else if(!strcmp("FALSE", str) || !strcmp("0", str))
    return(0);
  else {
    fprintf(vis_stdout, "Warning : Illegal argement for '%s'\n", option);
    fprintf(vis_stdout, "          Set with default '%s : TURE'\n", option);
    return(1);
  }
}

/**Function********************************************************************

  Synopsis    [Split line with respect to whitespace, '#' and ';', and save
  individual strings in array named 'argv'. ]

  Description [ ]

  Comment []

  SideEffects []

******************************************************************************/
static char *
Rt_SplitLine(
  char * command,
  int * argc,
  char *** argv)
{
  register char *p, *start, c;
  register int i, j;
  register char *new_arg;
  array_t *argv_array;
  int single_quote, double_quote;

  argv_array = array_alloc(char *, 5);

  p = command;
  for(;;) {
    /* skip leading white space */
    while (isspace((int)(*p))) {
      p++;
    }

    /* skip until end of this token */
    single_quote = double_quote = 0;
    for(start = p; (c = *p) != '\0'; p++) {
      if (c == ';' || c == '#' || isspace((int)c)) {
        if (! single_quote && ! double_quote) {
          break;
        }
      }
      if (c == '\'') {
        single_quote = ! single_quote;
      }
      if (c == '"') {
        double_quote = ! double_quote;
      }
    }
    if (single_quote || double_quote) {
      (void) fprintf(vis_stderr, "** cmd warning: ignoring unbalanced quote ...\n");
    }
    if (start == p) break;

    new_arg = ALLOC(char, p - start + 1);
    j = 0;
    for(i = 0; i < p - start; i++) {
      c = start[i];
      if ((c != '\'') && (c != '\"')) {
        new_arg[j++] = isspace((int)c) ? ' ' : start[i];
      }
    }
    new_arg[j] = '\0';
    array_insert_last(char *, argv_array, new_arg);
  }

  *argc = array_n(argv_array);
  *argv = array_data(char *, argv_array);
  array_free(argv_array);
  if (*p == ';') {
    p++;
  }
  else if (*p == '#') {
    for(; *p != 0; p++) ;               /* skip to end of line */
  }
  return p;
}    


static void
Rt_FreeRtConfig(RtConfigs_t * config)
{
  int i;
  RtDesignLists_t *list;
  array_t *itemArr, *designArr, *resultArr;
  st_table *table;
  RtCompareItems_t *item;
  RtCommandResults_t *result;
  st_generator *gen;
  char *keyWord;


  if(config == 0)       return;
  
  if(config->designDirectory)           free(config->designDirectory);
  if(config->designList)                free(config->designList);
  if(config->scriptFile)                free(config->scriptFile);
  if(config->resultForCounterExample)   free(config->resultForCounterExample);
  if(config->resultForPerformance)      free(config->resultForPerformance);

  if(config->referenceVis)              free(config->referenceVis);
  if(config->referenceVisNickName)      free(config->referenceVisNickName);
  if(config->referenceVisOptionFile)    free(config->referenceVisOptionFile);
  if(config->referenceOutDirectory)     free(config->referenceOutDirectory);
  if(config->refCommandTemplate)        free(config->refCommandTemplate);

  if(config->newVis)                    free(config->newVis);
  if(config->newVisNickName)            free(config->newVisNickName);
  if(config->newVisOptionFile)          free(config->newVisOptionFile);
  if(config->newOutDirectory)           free(config->newOutDirectory);
  if(config->newCommandTemplate)        free(config->newCommandTemplate);

  itemArr = config->compareItemArr;
  if(itemArr) {
    for(i=0; i<array_n(itemArr); i++) {
      item = array_fetch(RtCompareItems_t *, itemArr, i);
      Rt_FreeCompareItem(item);
    }
    array_free(itemArr);
  }

  designArr = config->designListArr;
  if(designArr) {
    for(i=0; i<array_n(designArr); i++) {
      list = array_fetch(RtDesignLists_t *, designArr, i);
      Rt_FreeDesignList(list);
    }
    array_free(designArr);
  }

  resultArr = config->refCommandTemplateArr;
  if(resultArr) {
    for(i=0; i<array_n(resultArr); i++) {
      result = array_fetch(RtCommandResults_t *, resultArr, i);
      Rt_FreeCommandResult(result);
    }
    array_free(resultArr);
  }

  resultArr = config->newCommandTemplateArr;
  if(resultArr) {
    for(i=0; i<array_n(resultArr); i++) {
      result = array_fetch(RtCommandResults_t *, resultArr, i);
      Rt_FreeCommandResult(result);
    }
    array_free(resultArr);
  }

  if(config->keyWordTable) {
    table = config->keyWordTable;
    st_foreach_item(table, gen, &keyWord, NIL(char *)) {
      free(keyWord);
    }
    st_free_table(table);
  }

}

static void
Rt_FreeDesignList(RtDesignLists_t *list)
{
  array_t *resultArr;
  RtCommandResults_t *result;
  int i;

  if(list == 0) return;

  if(list->designDirectory)     free(list->designDirectory);
  if(list->designNickName)      free(list->designNickName);
  if(list->blifFile)    free(list->blifFile);
  if(list->ctlFile)     free(list->ctlFile);
  if(list->invFile)     free(list->invFile);
  if(list->leFile)      free(list->leFile);
  if(list->fairFile)    free(list->fairFile);
  if(list->hintFile)    free(list->hintFile);
  if(list->ordFile)     free(list->ordFile);
  if(list->ltlFile)     free(list->ltlFile);

  resultArr = list->resultForCommandArr1;
  if(resultArr) {
    for(i=0; i<array_n(resultArr); i++) {
      result = array_fetch(RtCommandResults_t *, resultArr, i);
      Rt_FreeCommandResult(result);
    }
    array_free(resultArr);
  }
  resultArr = list->resultForCommandArr2;
  if(resultArr) {
    for(i=0; i<array_n(resultArr); i++) {
      result = array_fetch(RtCommandResults_t *, resultArr, i);
      Rt_FreeCommandResult(result);
    }
    array_free(resultArr);
  }

  free(list);
}

static void
Rt_FreeCommandResult(RtCommandResults_t *result)
{
  array_t *itemArr;
  array_t *propArr;
  RtCompareItems_t *item;
  RtResultPropertys_t *prop;
  int i;

  if(result == 0)       return;
  
  if(result->command)   free(result->command);

  itemArr = result->compareItemArr;
  if(itemArr) {
    for(i=0; i<array_n(itemArr); i++) {
      item = array_fetch(RtCompareItems_t *, itemArr, i);
      Rt_FreeCompareItem(item);
    }
    array_free(itemArr);
  }
                          
  propArr = result->resultForProperty;
  if(propArr) {
    for(i=0; i<array_n(propArr); i++) {
      prop = array_fetch(RtResultPropertys_t *, propArr, i);
      Rt_FreeResultProperty(prop);
    }
    array_free(propArr);
  }
}

static void
Rt_FreeCompareItem(RtCompareItems_t *item)
{
  if(item == 0) return;

  if(item->itemName)    free(item->itemName);
  if(item->itemNickName)free(item->itemNickName);
  if(item->value)       free(item->value);
  free(item);
}

static void
Rt_FreeResultProperty(RtResultPropertys_t *prop)
{

  if(prop == 0) return;

  if(prop->failOrPass)  free(prop->failOrPass);
  free(prop);
}

static void
Rt_FreeArgv(int  argc,  char ** argv)
{
  int i;

  for(i = 0; i < argc; i++) {
    FREE(argv[i]);
  }
  FREE(argv);
}