src/ctlsp/ctlspCmd.c

Go to the documentation of this file.

#include "ctlspInt.h"

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

static int CommandCtlspTest(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandLtlToSNF(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int FormulaArrayCountSubformulae(array_t *formulaArray);
static void FormulaVisitUnvisitedSubformulae(Ctlsp_Formula_t *formula, int *ptr);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
void
Ctlsp_Init(void)
{
  Cmd_CommandAdd("_ctlsp_test",   CommandCtlspTest,   0);
  Cmd_CommandAdd("ltl2snf", CommandLtlToSNF, 0);
}


void
Ctlsp_End(void)
{
}

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


void
CtlspFormulaSetStatesToNULL(
  Ctlsp_Formula_t *formula)
{
  if(formula!=NIL(Ctlsp_Formula_t)) {
    formula->states = NIL(mdd_t);
    if(formula->type != Ctlsp_ID_c) {
      CtlspFormulaSetStatesToNULL(formula->left);
      CtlspFormulaSetStatesToNULL(formula->right);
    }
  }
}


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

static int
CommandCtlspTest(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int     c;
  int      i;
  FILE    *fp;
  array_t *formulaArray;
  array_t *CtlformulaArray;
  array_t *LTLformulaArray;

  array_t *convertedArray;  /* in DAG format */

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      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 CTL* formulas in the file.
   */
  formulaArray = Ctlsp_FileParseFormulaArray(fp);
  (void) fclose(fp);

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


  convertedArray = Ctlsp_FormulaArrayConvertToDAG(formulaArray);
  /*  array_free(formulaArray); */

  /*
   * Print each original formula and its corresponding converted formula.
   */
  for (i = 0; i < array_n(convertedArray); i++) {
    Ctlsp_Formula_t *formula;

    formula = array_fetch(Ctlsp_Formula_t *, convertedArray, i);
    (void) fprintf(vis_stdout, "original formula: ");
    Ctlsp_FormulaPrint(vis_stdout, formula);
    
    (void) fprintf(vis_stdout, " [CTL* ");

    if (Ctlsp_isCtlFormula(formula)){
       (void) fprintf(vis_stdout, ",CTL ");
    }

    if (Ctlsp_isLtlFormula(formula)){
       (void) fprintf(vis_stdout, ",LTL ");
    }
   
    (void) fprintf(vis_stdout, "]\n");

  }
 
  (void)fprintf(vis_stdout, "No. of subformulae (including formulae) = %d\n",
                FormulaArrayCountSubformulae(convertedArray));

  /* Converts array of CTL* formula to CTL */
  CtlformulaArray = Ctlsp_FormulaArrayConvertToCTL(formulaArray);
  if (CtlformulaArray !=  NIL(array_t)){
    for (i = 0; i < array_n(CtlformulaArray); i++) { 
      Ctlp_Formula_t *newFormula;

      newFormula = array_fetch(Ctlp_Formula_t *, CtlformulaArray, i);
      (void) fprintf(vis_stdout, "CTL formula: ");
      Ctlp_FormulaPrint(vis_stdout, newFormula);
      (void) fprintf(vis_stdout, "\n");
      
    }
  array_free(CtlformulaArray);
  }

  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
  if (LTLformulaArray !=  NIL(array_t)){
    for (i = 0; i < array_n(LTLformulaArray); i++) { 
      Ctlsp_Formula_t *newFormula;

      newFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i);
      (void) fprintf(vis_stdout, "LTL formula: ");
      Ctlsp_FormulaPrint(vis_stdout, newFormula);
      (void) fprintf(vis_stdout, "\n");
      
    }
  array_free(LTLformulaArray);
  } else {
   (void) fprintf(vis_stdout, "No LTL \n");
  }

  array_free(formulaArray);
  Ctlsp_FormulaArrayFree(convertedArray);

  fflush(vis_stdout);
  fflush(vis_stderr);

  return 0;             /* normal exit */

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


static int
CommandLtlToSNF(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int     c, i;
  FILE    *fp;
  array_t *formulaArray;
  array_t *LTLformulaArray;
  char    *ltlFileName = (char *)0;
  int     negateFormula = 0;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hf:n")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
    case 'f':
      ltlFileName = util_strsav(util_optarg);
      break;
    case 'n':
      negateFormula = 1;
      break;
    default:
      goto usage;
    }
  }
  if (!ltlFileName){
    (void) fprintf(vis_stderr, "** ltl2snf error: ltl file not provided\n");
    goto usage;
  }
  fp = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  FREE(ltlFileName);
  if (fp == NIL(FILE)) {
    (void) fprintf(vis_stdout,  "** ltl2snf error: error in opening file %s\n", ltlFileName);
    return 1;
  }
  /*
   * Parse the CTL* formulas in the file.
   */
  formulaArray = Ctlsp_FileParseFormulaArray(fp);
  (void) fclose(fp);

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

  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
  if (LTLformulaArray !=  NIL(array_t)){
    for (i = 0; i < array_n(LTLformulaArray); i++) { 
      Ctlsp_Formula_t *newFormula;

      newFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i);
      (void) fprintf(vis_stdout, "LTL formula: ");
      Ctlsp_FormulaPrint(vis_stdout, newFormula);
      (void) fprintf(vis_stdout, "\n");

      if(negateFormula){
        newFormula = Ctlsp_LtllFormulaNegate(newFormula);
        
        (void) fprintf(vis_stdout, "Negated LTL formula: ");
        Ctlsp_FormulaPrint(vis_stdout, newFormula);
        (void) fprintf(vis_stdout, "\n");
      }
      
      printf("SNF \n");
      Ctlsp_LtlTranslateIntoSNF(newFormula);
    }
  array_free(LTLformulaArray);
  } else {
    (void) fprintf(vis_stdout, "No LTL \n");
  }

  array_free(formulaArray);

  fflush(vis_stdout);
  fflush(vis_stderr);

  return 0;             /* normal exit */

usage:
  (void) fprintf(vis_stderr, "usage: ltl2snf  <-f ltl_file> [-h]\n");
  (void) fprintf(vis_stderr, "   -f <ltl_file>\n");
  (void) fprintf(vis_stderr, "   -n  negate formula\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;             /* error exit */
}


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

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