src/io/ioWriteSmv.c

Go to the documentation of this file.

#include "ioInt.h"

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


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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


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


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


void
Io_SmvPrintVar(
  FILE *fp,
  Var_Variable_t *var)
{
  char * varname = Var_VariableReadName(var);
  int i;

  for(i=0; varname[i]; i++) {
    if(varname[i] == '<' || 
       varname[i] == '>' || 
       varname[i] == '*' || 
       varname[i] == '$') {
      fputc('_', fp);
    } else {
      fputc(varname[i], fp);
    }
  }
}

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


void
IoSmvWrite(
  FILE *fp,
  Hrc_Manager_t *hmgr)
{ 
  char *rootModelName;
  Hrc_Model_t *model, *rootModel;
  Hrc_Node_t *currentNode;
  array_t *models;
  int i;
  boolean isRootModel;
  char *rootInstanceName, *instanceName;
  
  currentNode = Hrc_ManagerReadCurrentNode(hmgr);
  models = Hrc_ManagerObtainComponentModels(hmgr);

  rootModelName = Hrc_NodeReadModelName(currentNode);
  rootModel = Hrc_ManagerFindModelByName(hmgr,rootModelName);
  rootInstanceName = Hrc_NodeReadInstanceName(currentNode);
  assert(rootModel != NIL(Hrc_Model_t));
  
  for (i=0; i < array_n(models); i++){
    model = array_fetch(Hrc_Model_t *,models,i);
    isRootModel = (model == rootModel) ? TRUE : FALSE;
    instanceName = (isRootModel == TRUE) ? rootInstanceName : NIL(char);
    Hrc_ModelWriteSmv(fp,model,isRootModel,instanceName);
  }  

  array_free(models);
}

void
IoSmvPrint(
  FILE *fp,
  Var_Variable_t *var)
{
  int is_enum, range, i;

  is_enum = Var_VariableTestIsEnumerative(var);
  range = Var_VariableReadNumValues(var);
    
  if (is_enum == 1){
    if (range == 2){
      (void)fprintf(fp,"VAR %s : boolean;\n",Var_VariableReadName(var));
    }
    else {
      (void)fprintf(fp,"VAR %s : 0..%d;\n",Var_VariableReadName(var),range-1);
    }
  }
  else {
  /* variable var is symbolic */
    (void)fprintf(fp,"VAR %s : {",Var_VariableReadName(var));
    for (i=0; i < range; i++){
      if (i == (range-1))
        (void)fprintf(fp,"%s ",Var_VariableReadSymbolicValueFromIndex(var,i));
      else
        (void)fprintf(fp,"%s, ",Var_VariableReadSymbolicValueFromIndex(var,i));
    }
    (void)fprintf(fp,"};\n");
  }
}

void
IoSmvPrintSpecial(
  FILE *fp,
  Var_Variable_t *var)
{
  int is_enum, range, i;

  is_enum = Var_VariableTestIsEnumerative(var);
  range = Var_VariableReadNumValues(var);
    
  if (is_enum == 1){
    if (range == 2){
      (void)fprintf(fp,"VAR %s_bufin : boolean;\n",Var_VariableReadName(var));
    }
    else {
      (void)fprintf(fp,"VAR %s_bufin : 0..%d;\n",Var_VariableReadName(var),
                    range-1);
    }
  }
  else {
  /* variable var is symbolic */
    (void)fprintf(fp,"VAR %s_bufin : {",Var_VariableReadName(var));
    for (i=0; i < range; i++){
      if (i == (range-1)) 
        (void)fprintf(fp,"%s_bufin ",
                      Var_VariableReadSymbolicValueFromIndex(var,i));
      else
        (void)fprintf(fp,"%s_bufin, ",
                      Var_VariableReadSymbolicValueFromIndex(var,i));
    }
    (void)fprintf(fp,"};\n");
  }
}