src/rt/rtMain.c

Go to the documentation of this file.

#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                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* 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);

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


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

void
Rt_End(void)
{
}

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);

    if(RtCheckInputFileAvailability(config, designList, 1)) {
       fprintf(vis_stdout, "Skip the design '%s' ..(%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
       continue;
    }
    if(Rt_WriteBatchCommand(config, designList)) {
       fprintf(vis_stdout, "ERROR : can't write script for design '%s'\n", designList->designNickName);
       continue;
    }
    if(Rt_ExecuteVis(config, designList, 1, scriptOut)) {
       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->referenceVisNickName, designList->designNickName);
    }
    if(Rt_ExecuteVis(config, designList, 2, scriptOut)) {
       fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->newVisNickName, designList->designNickName);
    }
    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));

    if(config->scriptFile == 0) {
      if(config->bRefRun || config->bNewRun)
        Rt_WriteResult(config, i+1);
    }
  }

  if(config->scriptFile == 0)
    if(Rt_WriteResult(config, array_n(designArr)))      return(1);
  alarm(0);

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

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);
}

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;

  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);
  }

  fprintf(fout, "\\documentclass[plain]{article}\n");
  fprintf(fout, "\\usepackage{lscape}\n");
  fprintf(fout, "\\begin{document}\n");
  fprintf(fout, "\\setlength{\\oddsidemargin}{-0.5in}\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(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;
  }

  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(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");
  }


  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; 
        else if(value1+gap < value2)    resultArr[1] = resultArr[1] + 1.0; 
        else                            resultArr[2] += 1.0; 
      }
      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);
}

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';
}

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);
    }
  }

  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);
}

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);
}


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.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);
  }
  return(0);
}

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 BaseName %s\n", designList->designNickName);
  }
  if(config->bNewRun) {
    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 {
    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);
}

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);
}


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);
}

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);
}

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);
  }
}

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);
}