/**CFile***********************************************************************

  FileName    [ioWriteSmv.c]

  PackageName [io]

  Synopsis    [Writes out an Smv file.]

  Description [Write the current model to a file compatible with NuSMV v2.1]

  Author      [Daniel Sheridan, Chao Wang]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado. All 
  rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.]

******************************************************************************/

#include "ioInt.h"

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


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


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


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


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


/**AutomaticStart*************************************************************/

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


/**AutomaticEnd***************************************************************/


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


/**Function********************************************************************

  Synopsis    [Prints out variable name, cleaned for NuSMV]

  Description []

  SideEffects []

  SeeAlso     []

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


/**Function********************************************************************

  Synopsis    [The top-level routine for writing out an NuSMV file.]

  Description [The top-level routine for writing out an NuSMV file.
  The user has to check if the hmgr has a hierarchy read in before
  calling this procedure.]

  SideEffects []

  SeeAlso     []

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

/**Function********************************************************************

  Synopsis    [Prints out VAR declaration for a given variable.]

  Description [Prints out VAR declaration for a given variable.]

  SideEffects []

  SeeAlso     []

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

/**Function********************************************************************

  Synopsis    [Prints out VAR declaration for a given variable, with the
               special string "_bufin" appended to the variable name.]

  Description [Prints out VAR declaration for a given variable.]

  SideEffects []

  SeeAlso     []

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