src/amc/amcCmd.c

Go to the documentation of this file.

#include "amcInt.h"

static char rcsid[] UNUSED = "$Id: amcCmd.c,v 1.44 2005/05/19 02:36:36 awedh Exp $";


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

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

static jmp_buf timeOutEnv;

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

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

static int CommandAmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void ApproximateModelCheckUsage(void);
static void TimeOutHandle(void);

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

void
Amc_Init(void)
{
  Cmd_CommandAdd("approximate_model_check", CommandAmc, 0);
/*  Cmd_CommandAdd("approximate_compute_reach", CommandApproxReach, 0); */
}


void
Amc_End(void)
{
}


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


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

static int
CommandAmc(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  static int            timeOutPeriod;    /* CPU seconds allowed */
  char                  *ctlFileName;     /* Name of file containing formulas */
  FILE                  *ctlFile;         /* File to read the formulas from */
  Ntk_Network_t         *network;         /* Pointer to the current network */
  array_t               *ctlFormulaArray; /* Array of read ctl formulas */
  array_t               *ctlNormalForm;   /* Array of normal ctl formulas */
  Ctlp_Formula_t        *currentFormula;  /* Formula being verified */
  int                   c, i;
  Amc_VerbosityLevel    verbosity;        /* Verbosity level */

  long initialTime;
  long finalTime;


  /* Initialize Default Values */
  timeOutPeriod   = 0;
  ctlFileName     = NIL(char);
  verbosity       = Amc_VerbosityNone_c;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "ht:v:")) != EOF) {
    switch(c) {
      case 'h':
        ApproximateModelCheckUsage();
        return 1;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'v':
        verbosity = (Amc_VerbosityLevel) atoi(util_optarg);
        break;
      default:
        ApproximateModelCheckUsage();
        return 1;
    }
  }

  /* Make sure the CTL file has been provided */
  if (argc == util_optind) {
    ApproximateModelCheckUsage();
    return 1;
  }
  else {
    ctlFileName = argv[util_optind];
  }

  /* 
   * Obtain the network from the hierarchy manager 
   */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }
  /*
   * Check whether the fairness was read.
   */
  {
    Fsm_Fsm_t      *exactFsm = Fsm_NetworkReadOrCreateFsm(network);
    Fsm_Fairness_t *fairCons =  Fsm_FsmReadFairnessConstraint(exactFsm);
    int numOfDisjuncts = Fsm_FairnessReadNumDisjuncts(fairCons);
    if (numOfDisjuncts > 1) {
      /* non-Buchi */
      fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
    }
    else {
      int numOfConj     = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
      if (numOfConj > 1) {
        /* Buchi */
        fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
      }
    }
  } 

  /* 
   * Read in the array of CTL formulas provided in ctlFileName 
   */
  ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
  if (ctlFile == NIL(FILE)) {
    return 1;
  }
  ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
  fclose(ctlFile);

  if (ctlFormulaArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, "** amc error: Error while parsing ctl formulas in file.\n");
    return 1;
  } 

  ctlNormalForm = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlFormulaArray);

  /* 
   * Start the timer. 
   */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void (*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);

    /* The second time setjmp is called, it returns here !!*/
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "# AMC: timeout ocurred after %d seconds.\n",
                     timeOutPeriod);
      alarm(0);

      /* Note that there is a huge memory leak here. */
      Ctlp_FormulaArrayFree(ctlFormulaArray);
      Ctlp_FormulaArrayFree(ctlNormalForm);
      return 1;
    } 
  }


  /* 
   * Loop over every CTL formula in the array 
   */
  arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
    boolean validFormula;

    validFormula = FormulaTestIsForallQuantifier(currentFormula); 
    if (!validFormula) {
      fprintf(vis_stderr, "Formula ");
      Ctlp_FormulaPrint(vis_stderr, currentFormula);
      fprintf(vis_stderr, " is not a valid ACTL formula. Skipping it\n");
    }
    else if (!Mc_FormulaStaticSemanticCheckOnNetwork(currentFormula, network,
                                                     FALSE)) {
      (void) fprintf(vis_stdout, "\n** amc error: Error in parsing Atomic Formula:\n%s\n", error_string());
      error_init();
      Ctlp_FormulaFree( currentFormula );
      continue;
    }
    else {
      error_init();
      initialTime = util_cpu_time();
      Amc_AmcEvaluateFormula(network, currentFormula, verbosity);
      finalTime = util_cpu_time();
      if(verbosity == Amc_VerbosityVomit_c) {
        (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
                       (finalTime - initialTime) / 1000);
      }
      fprintf(vis_stdout, "\n");
    }

  } /* End of arrayForEachItem in ctlFormulaArray */



  /* Deactivate the alarm */
  alarm(0);


  /* Clean up */
  Ctlp_FormulaArrayFree(ctlFormulaArray);
  Ctlp_FormulaArrayFree(ctlNormalForm);
  error_cleanup();


  /* normal exit */
  return 0;
}

static void
ApproximateModelCheckUsage(void)
{
  (void) fprintf(vis_stderr, "usage: approximate_model_check [-h] ");
  (void) fprintf(vis_stderr, "[-t secs] [-v] ctlfile\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");
  (void) fprintf(vis_stderr, "   -v number verbosity level\n");
  (void) fprintf(vis_stderr, "   ctlfile   File containing the ctl formulas\n");

  return;
} /* End of ApproximateModelCheckUsage */



boolean
FormulaTestIsForallQuantifier(
  Ctlp_Formula_t *formula)
{
  Ctlp_Formula_t    *newFormula;
  boolean           converted; 
  Ctlp_FormulaClass result;

  if (!Ctlp_FormulaTestIsConverted(formula)) {
    newFormula = Ctlp_FormulaConvertToExistentialForm(formula);
    converted = TRUE;
  }
  else {
    newFormula = formula;
    converted = FALSE;
  }

  result = Ctlp_CheckClassOfExistentialFormula(newFormula);

  if (converted) {
    Ctlp_FormulaFree(newFormula);
  } /* End of if */

  return result == Ctlp_ACTL_c || result == Ctlp_QuantifierFree_c;

} /* End of FormulaTestIsForallQuantifier */


static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */