src/ctlp/ctlpCmd.c

Go to the documentation of this file.

#include "ctlpInt.h"

static char rcsid[] UNUSED = "$Id: ctlpCmd.c,v 1.14 2005/05/19 02:35:25 awedh Exp $";

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

static int CommandCtlpTest(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int FormulaArrayCountSubformulae(array_t *formulaArray);
static void FormulaVisitUnvisitedSubformulae(Ctlp_Formula_t *formula, int *ptr);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
void
Ctlp_Init(void)
{
  Cmd_CommandAdd("_ctlp_test",   CommandCtlpTest,   0);
}


void
Ctlp_End(void)
{
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

void
CtlpFormulaSetStatesToNULL(
  Ctlp_Formula_t *formula)
{
  if(formula!=NIL(Ctlp_Formula_t)) {
    formula->states = NIL(mdd_t);
    if(formula->type != Ctlp_ID_c) {
      CtlpFormulaSetStatesToNULL(formula->left);
      CtlpFormulaSetStatesToNULL(formula->right);
    }
  }
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static int
CommandCtlpTest(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int     c;
  int      i;
  FILE    *fp;
  array_t *formulaArray;
  array_t *convertedArray;
  array_t *existentialConvertedArray;
  array_t *forwardExistentialArray = NIL(array_t);
  int     forwardTraversal = 0;
  
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "Fh")) != EOF) {
    switch(c) {
      case 'F':
        forwardTraversal = 1;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  /*
   * Open the ctl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** ctl error: ctl file not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** ctl error: too many arguments\n");
    goto usage;
  }

  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (fp == NIL(FILE)) {
    (void)fprintf(vis_stderr, "** ctl error: Cannot open the file %s\n", argv[util_optind]);
    return 1;
  }

  /*
   * Parse the formulas in the file.
   */
  formulaArray = Ctlp_FileParseFormulaArray(fp);
  (void) fclose(fp);

  if (formulaArray == NIL(array_t)) {
    fflush(vis_stdout);
    fflush(vis_stderr);
    return 1;
  }

  if (forwardTraversal)
    forwardExistentialArray =
      Ctlp_FormulaArrayConvertToForward(formulaArray, 1, FALSE);

  convertedArray = Ctlp_FormulaArrayConvertToDAG(formulaArray);
  array_free(formulaArray);
  existentialConvertedArray =
      Ctlp_FormulaDAGConvertToExistentialFormDAG(convertedArray);
  
  /*
   * Print each original formula and its corresponding converted formula.
   */
  for (i = 0; i < array_n(convertedArray); i++) {
    Ctlp_Formula_t *formula;

    formula = array_fetch(Ctlp_Formula_t *, convertedArray, i);
    (void) fprintf(vis_stdout, "original formula: ");
    Ctlp_FormulaPrint(vis_stdout, formula);
    (void) fprintf(vis_stdout, "\n");

    formula = array_fetch(Ctlp_Formula_t *, existentialConvertedArray, i);
    (void) fprintf(vis_stdout, "=> equivalent existential formula: ");
    Ctlp_FormulaPrint(vis_stdout, formula);
    (void) fprintf(vis_stdout, "\n");

    if (forwardTraversal) {
      formula = array_fetch(Ctlp_Formula_t *, forwardExistentialArray, i);
      (void) fprintf(vis_stdout, "=> equivalent forward existential formula: ");
      Ctlp_FormulaPrint(vis_stdout, formula);
      (void) fprintf(vis_stdout, "\n");
    }
  }

  (void)fprintf(vis_stdout, "No. of subformulae (including formulae) = %d\n",
                FormulaArrayCountSubformulae(existentialConvertedArray));
  if (forwardTraversal) {
    (void)fprintf(vis_stdout,
                  "No. of forward subformulae (including formulae) = %d\n",
                  FormulaArrayCountSubformulae(forwardExistentialArray));
  }


  Ctlp_FormulaArrayFree(convertedArray);
  Ctlp_FormulaArrayFree(existentialConvertedArray);
  if (forwardTraversal)
    Ctlp_FormulaArrayFree(forwardExistentialArray);
  
  fflush(vis_stdout);
  fflush(vis_stderr);

  return 0;             /* normal exit */

usage:
  (void) fprintf(vis_stderr, "usage: _ctlp_test file [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;             /* error exit */
}


static int
FormulaArrayCountSubformulae(
  array_t *formulaArray)
{
  int num, i;
  Ctlp_Formula_t *formula;
  int count = 0;
  
  num = array_n(formulaArray);
  for(i=0; i<num; i++){
    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
    FormulaVisitUnvisitedSubformulae(formula, &count);
  }
  /* Set the field states to NULL */
  for(i=0; i<num; i++){
    formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
    CtlpFormulaSetStatesToNULL(formula);
  }
  return count;
}

static void
FormulaVisitUnvisitedSubformulae(
  Ctlp_Formula_t *formula,
  int *ptr)
{
  if(formula!=NIL(Ctlp_Formula_t)) {
    if(formula->states == NIL(mdd_t)) {
      (*ptr)++;
      formula->states = (mdd_t *) 1;
      if(formula->type != Ctlp_ID_c) {
        FormulaVisitUnvisitedSubformulae(formula->left, ptr);
        FormulaVisitUnvisitedSubformulae(formula->right, ptr);
      }
    }
  }
}